proposition: Lemma preserve_update_loc_rel_lookup_None : ∀ ll (R : locRel ll) (l : seq heap_val) m, List.forallb (λ '(ℓ, s), ~~ isSome (lookup_hpv ℓ s l)) ll → preserve_update_mem l m (loc_rel ll R).
proof: Proof. intros ll R l m h. intros s₀ s₁ hh. unfold loc_rel in *. eapply remember_pre_pre in hh. induction ll as [| [ℓ si] ll ih] in R, l, h, s₀, s₁, hh |- *. - simpl. simpl in hh. destruct update_heaps. assumption. - simpl in *. move: h => /andP [hl h]. destruct lookup_hpv eqn:e1. 1: discriminate. destruct update_heaps eqn:e. erewrite lookup_hpv_None_spec. 2,3: eauto. specialize ih with (1 := h). specialize ih with (1 := hh). rewrite e in ih. apply ih. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup pkg_advantage) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)