diff --git a/prelude/base.v b/prelude/base.v index 5bcf079aca48d42a6efae278c2c2d407cb4a8b5a..72d51f9be294ab9b8918463d178a220e2b98b648 100644 --- a/prelude/base.v +++ b/prelude/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/prelude/fin_maps.v b/prelude/fin_maps.v index ac03c01b3c0112a7e5f1535c165323af2dfd813b..e39403a832e7834f8e8b30faad449702bb34e995 100644 --- a/prelude/fin_maps.v +++ b/prelude/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/prelude/list.v b/prelude/list.v index 7712b36c9b9aa684ede4af56359adc445151b929..29b6aa699d294b06ff550b16661cf695a0e84038 100644 --- a/prelude/list.v +++ b/prelude/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/prelude/option.v b/prelude/option.v index 3ba95930d316ee470540c5052b562ec561d64403..9cf9be533ad53c90a3a90ee9937e396d2e982ba0 100644 --- a/prelude/option.v +++ b/prelude/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) :=