proposition: Lemma CompileCallFacadeImplementationOfMutation_ADT_Alloc: forall {av Targ Tadt} `{FacadeWrapper av Tadt} `{FacadeWrapper av Targ} {env} fADT, forall fpointer varg vtmp (arg: Targ) (target: Tadt) tenv, GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationOfMutation_ADT Targ Tadt fADT)) env -> forall vret ext pArg pTarget, PreconditionSet tenv ext [[[varg; vtmp; vret]]] -> {{ tenv }} pArg {{ [[ `varg ->> arg as _]] :: tenv }} ∪ {{ ext }} // env -> {{ [[ `varg ->> arg as _]] :: tenv }} pTarget {{ [[ `varg ->> arg as _]] :: [[ `vret ->> target as _]] :: tenv }} ∪ {{ ext }} // env -> {{ tenv }} Seq pArg (Seq pTarget (Call vtmp fpointer (vret :: varg :: nil))) {{ [[ `vret ->> (fADT arg target) as _]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat hoare. rewrite TelEq_swap. apply CompileCallFacadeImplementationOfMutation_ADT; eauto. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core