proposition: Lemma CompileLoop {N} : forall {A} `{FacadeWrapper (Value QsADTs.ADTValue) A} lst init vhead vtest vlst vret fpop fempty fdealloc facadeBody facadeConclude env (ext: StringMap.t (Value QsADTs.ADTValue)) tenv tenv' (f: Comp A -> FiatWTuple N -> Comp A), GLabelMap.MapsTo fpop (Axiomatic (Pop)) env -> GLabelMap.MapsTo fempty (Axiomatic (Empty)) env -> GLabelMap.MapsTo fdealloc (Axiomatic (Delete)) 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 (FiatWTuple N)), {{ [[`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. hoare. hoare. rewrite TelEq_swap. set (tenvF := fun tenv init => [[ `vret ~~> init as _ ]] :: tenv). change ([[ `vlst ->> lst as _ ]] :: [[ `vret ~~> init as _ ]] :: tenv) with ([[ `vlst ->> lst as _ ]] :: tenvF tenv init). change ([[ `vret ~~> fold_left f lst init as _ ]] :: tenv) with (tenvF tenv (fold_left f lst init)). eapply CompileLoopBase__many; unfold tenvF in *; loop_t. setoid_rewrite Propagate_anonymous_ret; apply H5. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists CertifiedExtraction.Extraction.QueryStructures.CallRules.Tuple GLabelMapFacts