proposition: Lemma OriginalCompileLoopBase__many : forall {A B} {Wrp: FacadeWrapper W B}, let Wrapper := WrapSCAList : FacadeWrapper (Value ADTValue) (list B) in forall (lst: list B) init vhead vtest vlst fpop fempty fdealloc facadeBody env (ext: StringMap.t (Value QsADTs.ADTValue)) tenv (f: A -> B -> A) tenvF, GLabelMap.MapsTo fpop (Axiomatic QsADTs.WordListADTSpec.Pop) env -> GLabelMap.MapsTo fempty (Axiomatic QsADTs.WordListADTSpec.Empty) env -> GLabelMap.MapsTo fdealloc (Axiomatic QsADTs.WordListADTSpec.Delete) env -> PreconditionSet tenv ext [[[vhead; vtest; vlst]]] -> (forall v, NotInTelescope vtest (tenvF tenv v)) -> (forall v, NotInTelescope vhead (tenvF tenv v)) -> (forall v, NotInTelescope vlst (tenvF tenv v)) -> (forall v (h: B), TelEq ext ([[ ` vhead ->> h as _]]::tenvF tenv v) (tenvF ([[ ` vhead ->> h as _]]::tenv) v)) -> (forall head (acc: A) (s: list B), {{ tenvF ([[`vhead ->> head as _]] :: tenv) acc }} facadeBody {{ [[ ret (f acc head) as facc ]] :: tenvF tenv facc }} ∪ {{ [vtest |> wrap (bool2w false)] :: [vlst |> wrap s] :: ext }} // env) -> {{ [[`vlst ->> lst as _]] :: tenvF tenv init }} (Seq (Fold vhead vtest vlst fpop fempty facadeBody) (Call (DummyArgument vtest) fdealloc (vlst :: nil))) {{ tenvF tenv (fold_left f lst init) }} ∪ {{ ext }} // env.
proof: Proof. intros. Transparent DummyArgument. unfold DummyArgument; loop_t. eapply (CompileWordListEmpty_alt); loop_t. apply Lifted_not_In_Telescope_not_in_Ext_not_mapsto_adt; loop_t. 2:eapply (CompileWordListDelete_spec); loop_t. loop_t. generalize dependent init; induction lst; loop_t. move_to_front vtest; apply CompileWhileFalse_Loop; loop_t. simpl. eapply CompileWhileTrue; [ loop_t.. | ]. apply generalized @CompileWordListPop; loop_t. rewrite <- GLabelMapFacts.find_mapsto_iff; try assumption. apply Lifted_not_In_Telescope_not_in_Ext_not_mapsto_adt; loop_t. move_to_front vtest. move_to_front vlst. match goal with | [ H: forall _ _, TelEq _ _ _ |- _ ] => setoid_rewrite H end. apply ProgOk_Chomp_Some; loop_t. apply ProgOk_Chomp_Some; loop_t. computes_to_inv; subst; defunctionalize_evar; solve [eauto]. move_to_front vtest. apply ProgOk_Remove_Skip_L; hoare. apply CompileDeallocSCA_discretely; try compile_do_side_conditions. apply ProgOk_Chomp_Some; try compile_do_side_conditions; intros. apply CompileSkip. apply CompileWordListEmpty_alt; loop_t. apply Lifted_not_In_Telescope_not_in_Ext_not_mapsto_adt; loop_t. loop_t. setoid_replace (DropName vtest ([[ ret (f init a) as facc ]] :: tenvF tenv facc)) with (tenvF tenv (f init a)) using relation (TelEq ext); simpl; loop_t. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.CertifiedExtraction.Extraction.Extraction Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Wrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Coq.Program.Program Coq.Lists.List Bedrock.Platform.Facade.examples.QsADTs