Commit f50cfd4e by Ralf Jung

### Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 6beb51d3 714cc8ca
Pipeline #170 passed with stage
 ... ... @@ -47,7 +47,7 @@ Section heap. (** Conversion to heaps and back *) Global Instance of_heap_proper : Proper ((≡) ==> (=)) of_heap. Proof. by intros ??; fold_leibniz=>->. Qed. Proof. solve_proper. Qed. Lemma from_to_heap σ : of_heap (to_heap σ) = σ. Proof. apply map_eq=>l. rewrite lookup_omap lookup_fmap. by case (σ !! l). ... ... @@ -96,7 +96,7 @@ Section heap. (** Propers *) Global Instance heap_inv_proper : Proper ((≡) ==> (≡)) heap_inv. Proof. intros h1 h2. by fold_leibniz=> ->. Qed. Proof. solve_proper. Qed. (** General properties of mapsto *) Lemma heap_mapsto_disjoint l v1 v2 : (l ↦ v1 ★ l ↦ v2)%I ⊑ False. ... ...
 ... ... @@ -188,6 +188,7 @@ Tactic Notation "simplify_eq" := repeat | H : ?x = _ |- _ => subst x | H : _ = ?x |- _ => subst x | H : _ = _ |- _ => discriminate H | H : _ ≡ _ |- _ => apply leibniz_equiv in H | H : ?f _ = ?f _ |- _ => apply (inj f) in H | H : ?f _ _ = ?f _ _ |- _ => apply (inj2 f) in H; destruct H (* before [injection] to circumvent bug #2939 in some situations *) ... ... @@ -237,7 +238,7 @@ Ltac f_equiv := | |- pointwise_relation _ _ _ _ => intros ? end; (* Normalize away equalities. *) subst; simplify_eq; (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *) try match goal with | _ => first [ reflexivity | assumption | symmetry; assumption] ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!