proposition: Lemma CompileLoop : forall `{FacadeWrapper (Value av) A} `{FacadeWrapper (Value av) A'} `{FacadeWrapper av (list A)} lst init vhead vtest vlst vret fpop fempty fdealloc facadeBody facadeConclude env (ext: StringMap.t (Value av)) tenv tenv' (f: Comp A' -> A -> Comp A'), GLabelMap.MapsTo fpop (Axiomatic (List_pop A)) env -> GLabelMap.MapsTo fempty (Axiomatic (List_empty A)) env -> GLabelMap.MapsTo fdealloc (Axiomatic (FacadeImplementationOfDestructor (list A))) env -> PreconditionSet tenv ext [[[vhead; vtest; vlst; vret]]] -> {{ [[`vret ~~> (fold_left f lst init) as _]] :: tenv }} facadeConclude {{ [[`vret ~~> (fold_left f lst init) as _]] :: tenv' }} ∪ {{ ext }} // env -> (forall head (acc: Comp A') (s: list A), {{ [[`vret ~~> acc as _]] :: [[`vhead ->> head as _]] :: tenv }} facadeBody {{ [[`vret ~~> (f acc head) as _]] :: tenv }} ∪ {{ [vtest |> wrap (bool2w false)] :: [vlst |> wrap s] :: ext }} // env) -> {{ [[`vret ~~> init as _]] :: [[`vlst ->> lst as _]] :: tenv }} (Seq (Seq (Fold vhead vtest vlst fpop fempty facadeBody) (Call (DummyArgument vtest) fdealloc (vlst :: nil))) facadeConclude) {{ [[`vret ~~> (fold_left f lst init) as _]] :: tenv' }} ∪ {{ ext }} // env.
proof: Proof. eauto using @CompileSeq, @CompileLoopBase. Qed.
imports: CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.External.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.GenericADTMethods CertifiedExtraction.Extraction.External.FacadeADTs