proposition: Lemma BuildDFFun_is_syntax_ok av (env : StringMap.t DFFun -> Env av) {WrappedRepT RepT} cod dom WrappedCod WrappedDom meth RepInv (DecomposeRep : WrappedRepT -> RepT -> _) (numRepArgs : nat) wrappedRep (progOK : {prog : Stmt & (forall env_ext, LiftMethod (Cod := cod) (Dom := dom) (env env_ext) RepInv (DecomposeRep wrappedRep) WrappedCod WrappedDom prog meth) /\ NoUninitDec.is_no_uninited {| FuncCore.ArgVars := BuildArgNames (Datatypes.length dom) numRepArgs; FuncCore.RetVar := "ret"; FuncCore.Body := Compile.compile (CompileDFacade.compile prog) |} = true /\ (GoodModuleDec.is_arg_len_ok (Compile.compile (CompileDFacade.compile prog)) = true) /\ (GoodModuleDec.is_good_size (Datatypes.length (GetLocalVars.get_local_vars (Compile.compile (CompileDFacade.compile prog)) (BuildArgNames (Datatypes.length dom) numRepArgs) "ret") + Depth.depth (Compile.compile (CompileDFacade.compile prog))) = true) /\ is_disjoint (assigned prog) (StringSetFacts.of_list (BuildArgNames (Datatypes.length dom) numRepArgs)) = true /\ is_syntax_ok prog = true} ) : FModule.is_syntax_ok (CompileDFacade.compile_op {| ArgVars := BuildArgNames (Datatypes.length dom) numRepArgs; RetVar := "ret"; Body := projT1 progOK; args_no_dup := BuildArgNamesNoDup (Datatypes.length dom) numRepArgs; ret_not_in_args := ret_NIn_BuildArgNames (Datatypes.length dom) numRepArgs; no_assign_to_args := proj1 (proj2 (proj2 (proj2 (proj2 (projT2 progOK))))); args_name_ok := BuildArgNames_args_name_ok (Datatypes.length dom) numRepArgs; ret_name_ok := Ret_ret_name_ok; syntax_ok := proj2 (proj2 (proj2 (proj2 (proj2 (projT2 progOK))))) |}) = true.
proof: Proof. unfold FModule.is_syntax_ok; simpl. unfold GoodModuleDec.is_good_func; simpl. apply Bool.andb_true_iff; split; try eassumption. apply Bool.andb_true_iff; split; try eassumption. apply Bool.andb_true_iff; split; try eassumption. apply BuildArgNamesNoDup. destruct progOK; simpl in *; intuition. destruct progOK; simpl in *; intuition. destruct progOK; simpl in *; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction