proposition: Lemma BuildCompileUnit2T_exports_in_domain 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)) (AbsR : Rep adtSpec -> Rep adtImpl -> Prop) {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) 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')) 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} ) : is_sub_domain (GenExports codWrap domWrap AbsR RepInv DecomposeRepPre DecomposeRepPost DecomposeRepPrePoseAgree ValidImpl) (BuildFun _ adtImpl DecomposeRep numRepArgs codWrap domWrap RepWrapper progsOK).
proof: Proof. simpl. unfold GenExports, BuildFun. generalize (NoDup_BuildFinUpTo n') UniqueMeth. clear; induction (BuildFinUpTo n'); simpl; intros. - reflexivity. - erewrite is_sub_domain_equal_maps. rewrite is_sub_domain_add. apply IHl; eauto. inversion H; eauto. 3: simpl; rewrite fold_left_add2_Eq; [ reflexivity | ]. 4: simpl; rewrite fold_left_add2_Eq; [ reflexivity | ]. + eapply NIn_StringMap_fold_left with (f := fun idx => methID (Vector.nth methSigs idx)). inversion H; subst; eauto. eapply methID_injective; eauto. rewrite empty_in_iff; tauto. + eapply NIn_StringMap_fold_left with (f := fun idx => methID (Vector.nth methSigs idx)). inversion H; subst; eauto. eapply methID_injective; eauto. rewrite empty_in_iff; tauto. + eapply NIn_StringMap_fold_left with (f := fun idx => methID (Vector.nth methSigs idx)). inversion H; subst; eauto. eapply methID_injective; eauto. rewrite empty_in_iff; tauto. + eapply NIn_StringMap_fold_left with (f := fun idx => methID (Vector.nth methSigs idx)). inversion H; subst; eauto. eapply methID_injective; eauto. rewrite empty_in_iff; tauto. 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