proposition: Lemma CompileWordListDelete_spec: forall {A} {Wrp: FacadeWrapper W A}, let Wrapper := WrapSCAList : FacadeWrapper (Value ADTValue) (list A) in forall (vtmp vlst : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (tenv: Telescope QsADTs.ADTValue) ext (fpointer : GLabelMap.key), vlst <> vtmp -> vtmp ∉ ext -> vlst ∉ ext -> NotInTelescope vtmp tenv -> NotInTelescope vlst tenv -> GLabelMap.MapsTo fpointer (Axiomatic WordListADTSpec.Delete) env -> {{ [[ (NTSome vlst) ->> @nil A as _]] :: tenv }} (Call vtmp fpointer (vlst :: nil)) {{ tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. apply ProgOk_Remove_Skip_R; hoare. apply generalized @CompileWordListDelete; try (compile_do_side_conditions || Lifted_t). repeat match goal with | [ H: NotInTelescope _ _ |- _ ] => setoid_rewrite (DropName_NotInTelescope _ _ H) | _ => setoid_rewrite Propagate_anonymous_ret end. apply CompileDeallocW_discretely; try compile_do_side_conditions. apply CompileSkip. 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