proposition: Lemma SemiInvariant_couple_lhs : ∀ L₀ L₁ ℓ ℓ' (R : _ → _ → Prop), ℓ \in L₀ :|: L₁ → ℓ' \in L₀ :|: L₁ → R (get_heap empty_heap ℓ) (get_heap empty_heap ℓ') → SemiInvariant L₀ L₁ (couple_lhs ℓ ℓ' R).
proof: Proof. intros L₀ L₁ ℓ ℓ' h hℓ hℓ' he. split. - intros s₀ s₁ l v hl₀ hl₁ ?. assert (hl : l \notin L₀ :|: L₁). { rewrite in_fsetU. rewrite (negbTE hl₀) (negbTE hl₁). reflexivity. } unfold couple_lhs. rewrite !get_set_heap_neq. + auto. + apply /negP => /eqP e. subst. rewrite hℓ' in hl. discriminate. + apply /negP => /eqP e. subst. rewrite hℓ in hl. discriminate. - simpl. auto. 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)