proposition: Lemma BuildCompileUnit2T_projT2 av (env : GLabelMap.t (AxiomaticSpec av)) (env' := GLabelMap.map (@Axiomatic av) env) {n n'} {consSigs : Vector.t consSig n} {methSigs : Vector.t methSig n'} (UniqueMeth : NoDup (Vector.to_list (Vector.map methID methSigs))) (adtSpec adtImpl : DecoratedADT (BuildADTSig consSigs methSigs)) {numRepArgs} {A} {B} {C} {RepT' : Vector.t A numRepArgs} (RepT : ilist3 (B := B) RepT') (RepWrapper : @RepWrapperT av numRepArgs A B C RepT' RepT) (RepMap : Rep adtImpl -> i3list C RepT) (AbsR : Rep adtSpec -> Rep adtImpl -> Prop) ValidImpl RepInv (DecomposeRep := fun repWrapper rep => Decomposei3list RepT' RepT repWrapper (RepMap rep)) (DecomposeRepPre := fun rep => DecomposePrei3list RepT' RepT RepWrapper (RepMap rep)) (DecomposeRepPost := fun rep rep' => DecomposePosti3list _ RepT RepWrapper (RepMap rep) (RepMap rep')) ax_mod_name' op_mod_name' codWrap domWrap (DecomposeRepPrePoseAgree := fun r r' => DecomposePrei3list_Agree av RepT RepWrapper (RepMap r) (RepMap r')) (env'' := fun env''' : StringMap.t DFFun => (GLabelMapFacts.UWFacts.WFacts.P.update (GLabelMapFacts.UWFacts.WFacts.P.update (GLabelMap.map (fun f : DFFun => Operational av f) (map_aug_mod_name op_mod_name' env''')) (GLabelMap.map (Axiomatic (ADTValue:=av)) (map_aug_mod_name op_mod_name' (GenExports codWrap domWrap AbsR RepInv DecomposeRepPre DecomposeRepPost DecomposeRepPrePoseAgree ValidImpl)))) env')) (progsOK : forall midx, {prog : Stmt & (forall env_ext, LiftMethod (env'' env_ext) RepInv (DecomposeRep RepWrapper) (codWrap midx) (domWrap midx) prog (Methods adtImpl midx)) /\ NoUninitDec.is_no_uninited {| FuncCore.ArgVars := BuildArgNames (Datatypes.length (fst (MethodDomCod (BuildADTSig consSigs methSigs) midx))) 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 (fst (MethodDomCod (BuildADTSig consSigs methSigs) midx))) numRepArgs) "ret") + Depth.depth (Compile.compile (CompileDFacade.compile prog))) = true) /\ is_disjoint (assigned prog) (StringSetFacts.of_list (BuildArgNames (Datatypes.length (fst (MethodDomCod (BuildADTSig consSigs methSigs) midx))) numRepArgs)) = true /\ is_syntax_ok prog = true} ) (distinct_mod_name : negb (ListFacts3.string_bool ax_mod_name' op_mod_name') = true) (unique_op_mod_name' : forallb (fun x : string => negb (ListFacts3.string_bool op_mod_name' x)) (map (fun x : string * string * AxiomaticSpec av => fst (fst x)) (GLabelMap.elements (elt:=AxiomaticSpec av) env)) = true) (no_cito_clash_op_mod : negb (prefix "__cmod_impl_" op_mod_name') = true) (no_cito_clash_env : forallb NameDecoration.is_good_module_name (map (fun x => fst (fst x)) (GLabelMap.elements env)) = true) proof env_ext : CompileUnit2Equiv (env'' env_ext) adtImpl RepInv DecomposeRep numRepArgs ax_mod_name' op_mod_name' codWrap domWrap RepWrapper {| module := {| Imports := env; Funs := BuildFun _ adtImpl DecomposeRep numRepArgs codWrap domWrap RepWrapper progsOK; import_module_names_good := no_cito_clash_env |}; ax_mod_name := ax_mod_name'; op_mod_name := op_mod_name'; exports_in_domain := BuildCompileUnit2T_exports_in_domain (UniqueMeth := UniqueMeth) env AbsR RepMap ValidImpl op_mod_name' codWrap domWrap progsOK; op_mod_name_ok := no_cito_clash_op_mod; op_mod_name_not_in_imports := unique_op_mod_name'; name_neq := distinct_mod_name; proof := proof |}.
proof: Proof. unfold CompileUnit2Equiv; repeat split; simpl; eauto. unfold DFModuleEquiv; intros. eexists (BuildDFFun _ DecomposeRep _ RepWrapper (progsOK midx)). simpl. repeat split. intros. eapply (proj1 (projT2 (progsOK midx)) _ r H). unfold BuildFun. eapply (@StringMapsTo_fold_left' _ _ (fun el => methID (Vector.nth methSigs el)) (fun el => BuildDFFun _ DecomposeRep numRepArgs RepWrapper (progsOK el))). apply methID_injective; eauto. 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