proposition: Lemma CompileCallFacadeImplementationOfMutation_SCA_Replace_strong: forall {av Tadt} `{FacadeWrapper av Tadt} {env} fADT, forall fpointer varg vtmp (arg: W) (target: Tadt) tenv tenv', GLabelMap.MapsTo fpointer (Axiomatic (FacadeImplementationOfMutation_SCA Tadt fADT)) env -> forall vret ext pArg pCoda, PreconditionSet tenv ext [[[varg; vtmp; vret]]] -> {{ [[ `vret ->> target as _]] :: tenv }} pArg {{ [[ `vret ->> target as _]] :: [[ `varg ->> arg as _]] :: tenv }} ∪ {{ ext }} // env -> {{ [[ `vret ->> (fADT arg target) as _]] :: tenv }} pCoda {{ [[ `vret ->> (fADT arg target) as _]] :: tenv' }} ∪ {{ ext }} // env -> {{ [[ `vret ->> target as _]] :: tenv }} Seq (Seq pArg (Call vtmp fpointer (vret :: varg :: nil))) pCoda {{ [[ `vret ->> (fADT arg target) as _]] :: tenv' }} ∪ {{ ext }} // env.
proof: Proof. intros; hoare. apply CompileCallFacadeImplementationOfMutation_SCA_Replace; PreconditionSet_t; eauto. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.External.Core