Commit 618afceb by Robbert Krebbers

### Remove PropHolds type class.

parent 409e0c1b
 ... @@ -90,21 +90,6 @@ Hint Extern 0 (_ ≡ _) => symmetry; assumption. ... @@ -90,21 +90,6 @@ Hint Extern 0 (_ ≡ _) => symmetry; assumption. (** * Type classes *) (** * 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 *) (** ** Decidable propositions *) (** This type class by (Spitters/van der Weegen, 2011) collects decidable (** This type class by (Spitters/van der Weegen, 2011) collects decidable propositions. For example to declare a parameter expressing decidable equality propositions. For example to declare a parameter expressing decidable equality ... @@ -176,22 +161,6 @@ Arguments total {_} _ {_} _ _. ... @@ -176,22 +161,6 @@ Arguments total {_} _ {_} _ _. Arguments trichotomy {_} _ {_} _ _. Arguments trichotomy {_} _ {_} _ _. Arguments trichotomyT {_} _ {_} _ _. 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. Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y → ¬R y x. Proof. intuition. Qed. Proof. intuition. Qed. Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y ↔ R y x. Lemma symmetry_iff `(R : relation A) `{!Symmetric R} x y : R x y ↔ R y x. ... ...
 ... @@ -39,8 +39,7 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, ... @@ -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 : elem_of_map_to_list {A} (m : M A) i x : (i,x) ∈ map_to_list m ↔ m !! i = Some 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_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) lookup_merge {A B C} (f: option A → option B → option C) `{!DiagNone f} m1 m2 i : `{!PropHolds (f None None = None)} m1 m2 i : merge f m1 m2 !! i = f (m1 !! i) (m2 !! i) merge f m1 m2 !! i = f (m1 !! i) (m2 !! i) }. }. ... @@ -150,8 +149,7 @@ Section setoid. ... @@ -150,8 +149,7 @@ Section setoid. intros ?? Hf; apply partial_alter_proper. intros ?? Hf; apply partial_alter_proper. by destruct 1; constructor; apply Hf. by destruct 1; constructor; apply Hf. Qed. Qed. Lemma merge_ext f g Lemma merge_ext f g `{!DiagNone f, !DiagNone g} : `{!PropHolds (f None None = None), !PropHolds (g None None = None)} : ((≡) ==> (≡) ==> (≡))%signature f g → ((≡) ==> (≡) ==> (≡))%signature f g → ((≡) ==> (≡) ==> (≡))%signature (merge (M:=M) f) (merge g). ((≡) ==> (≡) ==> (≡))%signature (merge (M:=M) f) (merge g). Proof. Proof. ... @@ -825,8 +823,7 @@ End map_Forall. ... @@ -825,8 +823,7 @@ End map_Forall. (** ** Properties of the [merge] operation *) (** ** Properties of the [merge] operation *) Section merge. Section merge. Context {A} (f : option A → option A → option A). Context {A} (f : option A → option A → option A) `{!DiagNone f}. Context `{!PropHolds (f None None = None)}. Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f). Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f). Proof. Proof. intros ??. apply map_eq. intros. intros ??. apply map_eq. intros. ... @@ -841,29 +838,25 @@ Lemma merge_comm m1 m2 : ... @@ -841,29 +838,25 @@ Lemma merge_comm m1 m2 : (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) → (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) → merge f m1 m2 = merge f m2 m1. merge f m1 m2 = merge f m2 m1. Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. Global Instance: Comm (=) f → Comm (=) (merge f). Global Instance merge_comm' : Comm (=) f → Comm (=) (merge f). Proof. Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed. intros ???. apply merge_comm. intros. by apply (comm f). Qed. Lemma merge_assoc m1 m2 m3 : Lemma merge_assoc m1 m2 m3 : (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) = (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) = f (f (m1 !! i) (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. 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. Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed. Global Instance: Assoc (=) f → Assoc (=) (merge f). Global Instance merge_assoc' : Assoc (=) f → Assoc (=) (merge f). Proof. Proof. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed. Lemma merge_idemp m1 : Lemma merge_idemp m1 : (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = 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. 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. Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed. End merge. End merge. Section more_merge. Section more_merge. Context {A B C} (f : option A → option B → option C). Context {A B C} (f : option A → option B → option C) `{!DiagNone f}. Context `{!PropHolds (f None None = None)}. Lemma merge_Some m1 m2 m : Lemma merge_Some m1 m2 m : (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m. (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m. Proof. Proof. ... @@ -983,7 +976,7 @@ Proof. ... @@ -983,7 +976,7 @@ Proof. split; [|naive_solver]. split; [|naive_solver]. intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver. intros [i[(x&y&?&?&?)|[(x&?&?&[])|(y&?&?&[])]]]; naive_solver. Qed. 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. Proof. intros A m1 m2. rewrite !map_disjoint_spec. naive_solver. Qed. Lemma map_disjoint_empty_l {A} (m : M A) : ∅ ⊥ₘ m. Lemma map_disjoint_empty_l {A} (m : M A) : ∅ ⊥ₘ m. Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed. Proof. rewrite !map_disjoint_spec. intros i x y. by rewrite lookup_empty. Qed. ... ...
 ... @@ -3668,5 +3668,3 @@ Ltac solve_suffix_of := by intuition (repeat ... @@ -3668,5 +3668,3 @@ Ltac solve_suffix_of := by intuition (repeat | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r | H : suffix_of _ _ → False |- _ => destruct H | H : suffix_of _ _ → False |- _ => destruct H end). end). Hint Extern 0 (PropHolds (suffix_of _ _)) => unfold PropHolds; solve_suffix_of : typeclass_instances.
 ... @@ -257,23 +257,33 @@ Lemma option_union_Some {A} (mx my : option A) z : ... @@ -257,23 +257,33 @@ Lemma option_union_Some {A} (mx my : option A) z : mx ∪ my = Some z → mx = Some z ∨ my = Some z. mx ∪ my = Some z → mx = Some z ∨ my = Some z. Proof. destruct mx, my; naive_solver. Qed. 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). 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. 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. 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. 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. 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. 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. 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. Proof. by intros [?|]. Qed. End option_union_intersection_difference. End union_intersection_difference. (** * Tactics *) (** * Tactics *) Tactic Notation "case_option_guard" "as" ident(Hx) := Tactic Notation "case_option_guard" "as" ident(Hx) := ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment