proposition: Lemma CompileLoop__many {idx}: forall {A} vhead vtest vlst (tenvF: A -> Telescope ADTValue) tenv' (lst: list (RealElemType idx)) init (f: A -> (RealElemType idx) -> A) tenv0 tenv env (ext: StringMap.t (Value QsADTs.ADTValue)) fpop fempty fdealloc facadeBody facadeConclude, GLabelMap.MapsTo fpop (Axiomatic Pop) env -> GLabelMap.MapsTo fempty (Axiomatic Empty) env -> GLabelMap.MapsTo fdealloc (Axiomatic Delete) env -> PreconditionSet tenv ext [[[vhead; vtest; vlst]]] -> TelEq ext tenv0 ([[`vlst ->> lst as _]] :: TelAppend (tenvF init) tenv) -> (forall v, NotInTelescope vtest (TelAppend (tenvF v) tenv)) -> (forall v, NotInTelescope vhead (TelAppend (tenvF v) tenv)) -> (forall v, NotInTelescope vlst (TelAppend (tenvF v) tenv)) -> {{ TelAppend (tenvF (fold_left f lst init)) tenv }} facadeConclude {{ TelAppend (tenvF (fold_left f lst init)) tenv' }} ∪ {{ ext }} // env -> (forall head (acc: A) (s: list (RealElemType idx)), {{ TelAppend (tenvF acc) ([[`vhead ->> head as _]] :: tenv) }} facadeBody {{ TelAppend ([[ ret (f acc head) as facc ]] :: tenvF facc) tenv }} ∪ {{ [vtest |> wrap (bool2w false)] :: [vlst |> wrap s] :: ext }} // env) -> {{ tenv0 }} (Seq (Seq (Fold vhead vtest vlst fpop fempty facadeBody) (Call (DummyArgument vtest) fdealloc (vlst :: nil))) facadeConclude) {{ TelAppend ([[ ret (fold_left f lst init) as folded ]] :: tenvF folded) tenv' }} ∪ {{ ext }} // env.
proof: Proof. intros. rewrite H3. setoid_rewrite Propagate_anonymous_ret. hoare. pose (fun tenv init => TelAppend (tenvF init) tenv) as tenvF'. change (TelAppend (tenvF init) tenv) with (tenvF' tenv init). change (TelAppend (tenvF (fold_left f lst init)) tenv) with (tenvF' tenv (fold_left f lst init)). eapply @CompileLoopBase__many; eauto using TelEq_TelAppend_Cons_Second. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists