proposition: Lemma SemiInvariant_loc_rel : ∀ L₀ L₁ l (R : locRel l), List.forallb (λ '(ℓ,_), ℓ \in L₀ :|: L₁) l → heapLocRel empty_heap empty_heap l R → SemiInvariant L₀ L₁ (loc_rel l R).
proof: Proof. intros L₀ L₁ l R h he. split. - intros s₀ s₁ ℓ v hℓ₀ hℓ₁ hh. assert (hℓ : ℓ \notin L₀ :|: L₁). { rewrite in_fsetU. rewrite (negbTE hℓ₀) (negbTE hℓ₁). reflexivity. } unfold loc_rel. induction l as [| [ℓ' si] l ih] in s₀, s₁, R, hh, h |- *. + assumption. + simpl. apply ih. * simpl in h. move: h => /andP [_ h]. assumption. * simpl in h. move: h => /andP [h _]. destruct si. all: simpl. all: rewrite !get_set_heap_neq. 1,3: assumption. -- apply /negP => /eqP e. subst. rewrite h in hℓ. discriminate. -- apply /negP => /eqP e. subst. rewrite h in hℓ. discriminate. - simpl. assumption. 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)