proposition: Lemma CompileDelete_spec {idx}: 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 Delete) env -> {{ [[ (NTSome vlst) ->> @nil (RealElemType idx) as _]] :: tenv }} (Call vtmp fpointer (vlst :: nil)) {{ tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. apply ProgOk_Remove_Skip_R; hoare. apply generalized @CompileDelete; 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: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists