From e36e7f9964837180d334da95010b01ef5ca97831 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 26 May 2016 14:02:26 +0200
Subject: [PATCH] Remove PropHolds type class.

theories/base.v  31 
theories/fin_maps.v  29 +++++++++++
theories/list.v  2 
theories/option.v  28 +++++++++++++++++++
4 files changed, 30 insertions(+), 60 deletions()
diff git a/theories/base.v b/theories/base.v
index 5bcf079..72d51f9 100644
 a/theories/base.v
+++ b/theories/base.v
@@ 90,21 +90,6 @@ Hint Extern 0 (_ ≡ _) => symmetry; assumption.
(** * Type classes *)
(** ** Provable propositions *)
(** This type class collects provable propositions. It is useful to constraint
type classes by arbitrary propositions. *)
Class PropHolds (P : Prop) := prop_holds: P.

Hint Extern 0 (PropHolds _) => assumption : typeclass_instances.
Instance: Proper (iff ==> iff) PropHolds.
Proof. repeat intro; trivial. Qed.

Ltac solve_propholds :=
 match goal with
   PropHolds (?P) => apply _
   ?P => change (PropHolds P); apply _
 end.

(** ** Decidable propositions *)
(** This type class by (Spitters/van der Weegen, 2011) collects decidable
propositions. For example to declare a parameter expressing decidable equality
@@ 176,22 +161,6 @@ Arguments total {_} _ {_} _ _.
Arguments trichotomy {_} _ {_} _ _.
Arguments trichotomyT {_} _ {_} _ _.
Instance left_id_propholds {A} (R : relation A) i f :
 LeftId R i f → ∀ x, PropHolds (R (f i x) x).
Proof. red. trivial. Qed.
Instance right_id_propholds {A} (R : relation A) i f :
 RightId R i f → ∀ x, PropHolds (R (f x i) x).
Proof. red. trivial. Qed.
Instance left_absorb_propholds {A} (R : relation A) i f :
 LeftAbsorb R i f → ∀ x, PropHolds (R (f i x) i).
Proof. red. trivial. Qed.
Instance right_absorb_propholds {A} (R : relation A) i f :
 RightAbsorb R i f → ∀ x, PropHolds (R (f x i) i).
Proof. red. trivial. Qed.
Instance idem_propholds {A} (R : relation A) f :
 IdemP R f → ∀ x, PropHolds (R (f x x) x).
Proof. red. trivial. Qed.

Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y → ¬R y x.
Proof. intuition. Qed.
Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y ↔ R y x.
diff git a/theories/fin_maps.v b/theories/fin_maps.v
index c044471..101ac68 100644
 a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ 39,8 +39,7 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
elem_of_map_to_list {A} (m : M A) i x :
(i,x) ∈ map_to_list m ↔ m !! i = Some x;
lookup_omap {A B} (f : A → option B) m i : omap f m !! i = m !! i ≫= f;
 lookup_merge {A B C} (f : option A → option B → option C)
 `{!PropHolds (f None None = None)} m1 m2 i :
+ lookup_merge {A B C} (f: option A → option B → option C) `{!DiagNone f} m1 m2 i :
merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
}.
@@ 150,8 +149,7 @@ Section setoid.
intros ?? Hf; apply partial_alter_proper.
by destruct 1; constructor; apply Hf.
Qed.
 Lemma merge_ext f g
 `{!PropHolds (f None None = None), !PropHolds (g None None = None)} :
+ Lemma merge_ext f g `{!DiagNone f, !DiagNone g} :
((≡) ==> (≡) ==> (≡))%signature f g →
((≡) ==> (≡) ==> (≡))%signature (merge (M:=M) f) (merge g).
Proof.
@@ 825,8 +823,7 @@ End map_Forall.
(** ** Properties of the [merge] operation *)
Section merge.
Context {A} (f : option A → option A → option A).
Context `{!PropHolds (f None None = None)}.
+Context {A} (f : option A → option A → option A) `{!DiagNone f}.
Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f).
Proof.
intros ??. apply map_eq. intros.
@@ 841,29 +838,25 @@ Lemma merge_comm m1 m2 :
(∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
merge f m1 m2 = merge f m2 m1.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: Comm (=) f → Comm (=) (merge f).
Proof.
 intros ???. apply merge_comm. intros. by apply (comm f).
Qed.
+Global Instance merge_comm' : Comm (=) f → Comm (=) (merge f).
+Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed.
Lemma merge_assoc m1 m2 m3 :
(∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: Assoc (=) f → Assoc (=) (merge f).
Proof.
 intros ????. apply merge_assoc. intros. by apply (assoc_L f).
Qed.
+Global Instance merge_assoc' : Assoc (=) f → Assoc (=) (merge f).
+Proof. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed.
Lemma merge_idemp m1 :
(∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = m1.
Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
Global Instance: IdemP (=) f → IdemP (=) (merge f).
+Global Instance merge_idemp' : IdemP (=) f → IdemP (=) (merge f).
Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed.
End merge.
Section more_merge.
Context {A B C} (f : option A → option B → option C).
Context `{!PropHolds (f None None = None)}.
+Context {A B C} (f : option A → option B → option C) `{!DiagNone f}.
+
Lemma merge_Some m1 m2 m :
(∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
Proof.
@@ 983,7 +976,7 @@ Proof.
split; [naive_solver].
intros [i[(x&y&?&?&?)[(x&?&?&[])(y&?&?&[])]]]; naive_solver.
Qed.
Global Instance: Symmetric (map_disjoint : relation (M A)).
+Global Instance map_disjoint_sym : Symmetric (map_disjoint : relation (M A)).
Proof. intros A m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed.
Lemma map_disjoint_empty_l {A} (m : M A) : ∅ ⊥ₘ m.
Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed.
diff git a/theories/list.v b/theories/list.v
index e0f6ede..6060b9e 100644
 a/theories/list.v
+++ b/theories/list.v
@@ 3668,5 +3668,3 @@ Ltac solve_suffix_of := by intuition (repeat
  suffix_of _ (_ ++ _) => apply suffix_of_app_r
 H : suffix_of _ _ → False  _ => destruct H
end).
Hint Extern 0 (PropHolds (suffix_of _ _)) =>
 unfold PropHolds; solve_suffix_of : typeclass_instances.
diff git a/theories/option.v b/theories/option.v
index 9d887e2..e79e2ef 100644
 a/theories/option.v
+++ b/theories/option.v
@@ 257,23 +257,33 @@ Lemma option_union_Some {A} (mx my : option A) z :
mx ∪ my = Some z → mx = Some z ∨ my = Some z.
Proof. destruct mx, my; naive_solver. Qed.
Section option_union_intersection_difference.
+Class DiagNone {A B C} (f : option A → option B → option C) :=
+ diag_none : f None None = None.
+
+Section union_intersection_difference.
Context {A} (f : A → A → option A).
 Global Instance: LeftId (=) None (union_with f).
+
+ Global Instance union_with_diag_none : DiagNone (union_with f).
+ Proof. reflexivity. Qed.
+ Global Instance intersection_with_diag_none : DiagNone (intersection_with f).
+ Proof. reflexivity. Qed.
+ Global Instance difference_with_diag_none : DiagNone (difference_with f).
+ Proof. reflexivity. Qed.
+ Global Instance union_with_left_id : LeftId (=) None (union_with f).
Proof. by intros [?]. Qed.
 Global Instance: RightId (=) None (union_with f).
+ Global Instance union_with_right_id : RightId (=) None (union_with f).
Proof. by intros [?]. Qed.
 Global Instance: Comm (=) f → Comm (=) (union_with f).
+ Global Instance union_with_comm : Comm (=) f → Comm (=) (union_with f).
Proof. by intros ? [?] [?]; compute; rewrite 1?(comm f). Qed.
 Global Instance: LeftAbsorb (=) None (intersection_with f).
+ Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f).
Proof. by intros [?]. Qed.
 Global Instance: RightAbsorb (=) None (intersection_with f).
+ Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
Proof. by intros [?]. Qed.
 Global Instance: Comm (=) f → Comm (=) (intersection_with f).
+ Global Instance difference_with_comm : Comm (=) f → Comm (=) (intersection_with f).
Proof. by intros ? [?] [?]; compute; rewrite 1?(comm f). Qed.
 Global Instance: RightId (=) None (difference_with f).
+ Global Instance difference_with_right_id : RightId (=) None (difference_with f).
Proof. by intros [?]. Qed.
End option_union_intersection_difference.
+End union_intersection_difference.
(** * Tactics *)
Tactic Notation "case_option_guard" "as" ident(Hx) :=

GitLab