Commit db08223a by Robbert Krebbers

### Define shorthand EqDecision A := (∀ x y : A, Decision (x = y)).

parent 52cdec56
 ... @@ -100,6 +100,7 @@ on a type [A] we write [`{∀ x y : A, Decision (x = y)}] and use it by writing ... @@ -100,6 +100,7 @@ on a type [A] we write [`{∀ x y : A, Decision (x = y)}] and use it by writing [decide (x = y)]. *) [decide (x = y)]. *) Class Decision (P : Prop) := decide : {P} + {¬P}. Class Decision (P : Prop) := decide : {P} + {¬P}. Arguments decide _ {_}. Arguments decide _ {_}. Notation EqDecision A := (∀ x y : A, Decision (x = y)). (** ** Inhabited types *) (** ** Inhabited types *) (** This type class collects types that are inhabited. *) (** This type class collects types that are inhabited. *) ... @@ -918,9 +919,8 @@ Inductive NoDup {A} : list A → Prop := ... @@ -918,9 +919,8 @@ Inductive NoDup {A} : list A → Prop := (** Decidability of equality of the carrier set is admissible, but we add it (** Decidability of equality of the carrier set is admissible, but we add it anyway so as to avoid cycles in type class search. *) anyway so as to avoid cycles in type class search. *) Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C, Union C, Intersection C, Difference C, Intersection C, Difference C, Elements A C, EqDecision A} : Prop := { Elements A C, ∀ x y : A, Decision (x = y)} : Prop := { fin_collection :>> Collection A C; fin_collection :>> Collection A C; elem_of_elements X x : x ∈ elements X ↔ x ∈ X; elem_of_elements X x : x ∈ elements X ↔ x ∈ X; NoDup_elements X : NoDup (elements X) NoDup_elements X : NoDup (elements X) ... ...
 ... @@ -8,8 +8,8 @@ Arguments mkBSet {_} _. ... @@ -8,8 +8,8 @@ Arguments mkBSet {_} _. Arguments bset_car {_} _ _. Arguments bset_car {_} _ _. Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true). Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true). Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false). Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false). Instance bset_singleton {A} `{∀ x y : A, Decision (x = y)} : Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x, Singleton A (bset A) := λ x, mkBSet (λ y, bool_decide (y = x)). mkBSet (λ y, bool_decide (y = x)). Instance bset_elem_of {A} : ElemOf A (bset A) := λ x X, bset_car X x. Instance bset_elem_of {A} : ElemOf A (bset A) := λ x X, bset_car X x. Instance bset_union {A} : Union (bset A) := λ X1 X2, Instance bset_union {A} : Union (bset A) := λ X1 X2, mkBSet (λ x, bset_car X1 x || bset_car X2 x). mkBSet (λ x, bset_car X1 x || bset_car X2 x). ... @@ -17,8 +17,7 @@ Instance bset_intersection {A} : Intersection (bset A) := λ X1 X2, ... @@ -17,8 +17,7 @@ Instance bset_intersection {A} : Intersection (bset A) := λ X1 X2, mkBSet (λ x, bset_car X1 x && bset_car X2 x). mkBSet (λ x, bset_car X1 x && bset_car X2 x). Instance bset_difference {A} : Difference (bset A) := λ X1 X2, Instance bset_difference {A} : Difference (bset A) := λ X1 X2, mkBSet (λ x, bset_car X1 x && negb (bset_car X2 x)). mkBSet (λ x, bset_car X1 x && negb (bset_car X2 x)). Instance bset_collection {A} `{∀ x y : A, Decision (x = y)} : Instance bset_collection `{EqDecision A} : Collection A (bset A). Collection A (bset A). Proof. Proof. split; [split| |]. split; [split| |]. - by intros x ?. - by intros x ?. ... ...
 ... @@ -19,7 +19,7 @@ Local Open Scope positive_scope. ... @@ -19,7 +19,7 @@ Local Open Scope positive_scope. Inductive coPset_raw := Inductive coPset_raw := | coPLeaf : bool → coPset_raw | coPLeaf : bool → coPset_raw | coPNode : bool → coPset_raw → coPset_raw → coPset_raw. | coPNode : bool → coPset_raw → coPset_raw → coPset_raw. Instance coPset_raw_eq_dec (t1 t2 : coPset_raw) : Decision (t1 = t2). Instance coPset_raw_eq_dec : EqDecision coPset_raw. Proof. solve_decision. Defined. Proof. solve_decision. Defined. Fixpoint coPset_wf (t : coPset_raw) : bool := Fixpoint coPset_wf (t : coPset_raw) : bool := ... ...
 ... @@ -3,7 +3,7 @@ ... @@ -3,7 +3,7 @@ From stdpp Require Export list. From stdpp Require Export list. Local Open Scope positive. Local Open Scope positive. Class Countable A `{∀ x y : A, Decision (x = y)} := { Class Countable A `{EqDecision A} := { encode : A → positive; encode : A → positive; decode : positive → option A; decode : positive → option A; decode_encode x : decode (encode x) = Some x decode_encode x : decode (encode x) = Some x ... @@ -70,7 +70,7 @@ Section choice. ... @@ -70,7 +70,7 @@ Section choice. Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA. Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA. End choice. End choice. Lemma surj_cancel `{Countable A} `{∀ x y : B, Decision (x = y)} Lemma surj_cancel `{Countable A} `{EqDecision B} (f : A → B) `{!Surj (=) f} : { g : B → A & Cancel (=) f g }. (f : A → B) `{!Surj (=) f} : { g : B → A & Cancel (=) f g }. Proof. Proof. exists (λ y, choose (λ x, f x = y) (surj f y)). exists (λ y, choose (λ x, f x = y) (surj f y)). ... @@ -80,7 +80,7 @@ Qed. ... @@ -80,7 +80,7 @@ Qed. (** * Instances *) (** * Instances *) (** ** Injection *) (** ** Injection *) Section injective_countable. Section injective_countable. Context `{Countable A, ∀ x y : B, Decision (x = y)}. Context `{Countable A, EqDecision B}. Context (f : B → A) (g : A → option B) (fg : ∀ x, g (f x) = Some x). Context (f : B → A) (g : A → option B) (fg : ∀ x, g (f x) = Some x). Program Instance injective_countable : Countable B := Program Instance injective_countable : Countable B := ... ...
 ... @@ -164,15 +164,13 @@ Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : ... @@ -164,15 +164,13 @@ Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) : Decision (P ↔ Q) := and_dec _ _. Decision (P ↔ Q) := and_dec _ _. (** Instances of [Decision] for common data types. *) (** Instances of [Decision] for common data types. *) Instance bool_eq_dec (x y : bool) : Decision (x = y). Instance bool_eq_dec : EqDecision bool. Proof. solve_decision. Defined. Proof. solve_decision. Defined. Instance unit_eq_dec (x y : unit) : Decision (x = y). Instance unit_eq_dec : EqDecision unit. Proof. solve_decision. Defined. Proof. solve_decision. Defined. Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y)) Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B). `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y). Proof. solve_decision. Defined. Proof. solve_decision. Defined. Instance sum_eq_dec `(A_dec : ∀ x y : A, Decision (x = y)) Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B). `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y). Proof. solve_decision. Defined. Proof. solve_decision. Defined. Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p : Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p : ... @@ -181,9 +179,11 @@ Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p : ... @@ -181,9 +179,11 @@ Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p : | (x,y) => P_dec x y | (x,y) => P_dec x y end. end. Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)} Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} : `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y). EqDecision (sig P). Proof. refine (cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial. Defined. Proof. refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial. Defined. (** Some laws for decidable propositions *) (** Some laws for decidable propositions *) Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q. Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q. ... ...
 ... @@ -7,7 +7,7 @@ From stdpp Require Export collections fin_maps. ... @@ -7,7 +7,7 @@ From stdpp Require Export collections fin_maps. Class FinMapDom K M D `{FMap M, Class FinMapDom K M D `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A), ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A), ∀ i j : K, Decision (i = j), OMap M, Merge M, ∀ A, FinMapToList K A (M A), EqDecision K, ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D, ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D, Union D, Intersection D, Difference D} := { Union D, Intersection D, Difference D} := { finmap_dom_map :>> FinMap K M; finmap_dom_map :>> FinMap K M; ... ...
 ... @@ -27,7 +27,7 @@ Class FinMapToList K A M := map_to_list: M → list (K * A). ... @@ -27,7 +27,7 @@ Class FinMapToList K A M := map_to_list: M → list (K * A). Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A), PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A), ∀ i j : K, Decision (i = j)} := { EqDecision K} := { map_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2; map_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2; lookup_empty {A} i : (∅ : M A) !! i = None; lookup_empty {A} i : (∅ : M A) !! i = None; lookup_partial_alter {A} f (m : M A) i : lookup_partial_alter {A} f (m : M A) i : ... ...
 ... @@ -2,7 +2,7 @@ ... @@ -2,7 +2,7 @@ (* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *) From stdpp Require Export countable vector. From stdpp Require Export countable vector. Class Finite A `{∀ x y : A, Decision (x = y)} := { Class Finite A `{EqDecision A} := { enum : list A; enum : list A; NoDup_enum : NoDup enum; NoDup_enum : NoDup enum; elem_of_enum x : x ∈ enum elem_of_enum x : x ∈ enum ... @@ -189,7 +189,7 @@ End forall_exists. ... @@ -189,7 +189,7 @@ End forall_exists. (** Instances *) (** Instances *) Section enc_finite. Section enc_finite. Context `{∀ x y : A, Decision (x = y)}. Context `{EqDecision A}. Context (to_nat : A → nat) (of_nat : nat → A) (c : nat). Context (to_nat : A → nat) (of_nat : nat → A) (c : nat). Context (of_to_nat : ∀ x, of_nat (to_nat x) = x). Context (of_to_nat : ∀ x, of_nat (to_nat x) = x). Context (to_nat_c : ∀ x, to_nat x < c). Context (to_nat_c : ∀ x, to_nat x < c). ... @@ -212,7 +212,7 @@ Section enc_finite. ... @@ -212,7 +212,7 @@ Section enc_finite. End enc_finite. End enc_finite. Section bijective_finite. Section bijective_finite. Context `{Finite A, ∀ x y : B, Decision (x = y)} (f : A → B) (g : B → A). Context `{Finite A, EqDecision B} (f : A → B) (g : B → A). Context `{!Inj (=) (=) f, !Cancel (=) f g}. Context `{!Inj (=) (=) f, !Cancel (=) f g}. Program Instance bijective_finite: Finite B := {| enum := f <\$> enum A |}. Program Instance bijective_finite: Finite B := {| enum := f <\$> enum A |}. ... ...
 From stdpp Require Export base tactics. From stdpp Require Export base tactics. Section definitions. Section definitions. Context {A T : Type} `{∀ a b : A, Decision (a = b)}. Context {A T : Type} `{EqDecision A}. Global Instance fn_insert : Insert A T (A → T) := Global Instance fn_insert : Insert A T (A → T) := λ a t f b, if decide (a = b) then t else f b. λ a t f b, if decide (a = b) then t else f b. Global Instance fn_alter : Alter A T (A → T) := Global Instance fn_alter : Alter A T (A → T) := ... @@ -12,7 +12,7 @@ End definitions. ... @@ -12,7 +12,7 @@ End definitions. of equality of functions. *) of equality of functions. *) Section functions. Section functions. Context {A T : Type} `{∀ a b : A, Decision (a = b)}. Context {A T : Type} `{!EqDecision A}. Lemma fn_lookup_insert (f : A → T) a t : <[a:=t]>f a = t. Lemma fn_lookup_insert (f : A → T) a t : <[a:=t]>f a = t. Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed. Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed. ... ...
 ... @@ -22,10 +22,9 @@ Proof. ... @@ -22,10 +22,9 @@ Proof. split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=. split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=. f_equal; apply proof_irrel. f_equal; apply proof_irrel. Qed. Qed. Instance gmap_eq_eq `{Countable K} `{∀ x y : A, Decision (x = y)} Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A). (m1 m2 : gmap K A) : Decision (m1 = m2). Proof. Proof. refine (cast_if (decide (gmap_car m1 = gmap_car m2))); refine (λ m1 m2, cast_if (decide (gmap_car m1 = gmap_car m2))); abstract (by rewrite gmap_eq). abstract (by rewrite gmap_eq). Defined. Defined. ... ...
 ... @@ -15,7 +15,7 @@ Arguments Hashset {_ _} _ _. ... @@ -15,7 +15,7 @@ Arguments Hashset {_ _} _ _. Arguments hashset_car {_ _} _. Arguments hashset_car {_ _} _. Section hashset. Section hashset. Context `{∀ x y : A, Decision (x = y)} (hash : A → Z). Context `{EqDecision A} (hash : A → Z). Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l, Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l, hashset_car m !! hash x = Some l ∧ x ∈ l. hashset_car m !! hash x = Some l ∧ x ∈ l. ... @@ -137,7 +137,7 @@ Hint Extern 1 (Elements _ (hashset _)) => ... @@ -137,7 +137,7 @@ Hint Extern 1 (Elements _ (hashset _)) => eapply @hashset_elems : typeclass_instances. eapply @hashset_elems : typeclass_instances. Section remove_duplicates. Section remove_duplicates. Context `{∀ x y : A, Decision (x = y)} (hash : A → Z). Context `{EqDecision A} (hash : A → Z). Definition remove_dups_fast (l : list A) : list A := Definition remove_dups_fast (l : list A) : list A := match l with match l with ... ...
 ... @@ -245,7 +245,8 @@ Hint Extern 0 (_ `prefix_of` _) => reflexivity. ... @@ -245,7 +245,8 @@ Hint Extern 0 (_ `prefix_of` _) => reflexivity. Hint Extern 0 (_ `suffix_of` _) => reflexivity. Hint Extern 0 (_ `suffix_of` _) => reflexivity. Section prefix_suffix_ops. Section prefix_suffix_ops. Context `{∀ x y : A, Decision (x = y)}. Context `{EqDecision A}. Definition max_prefix_of : list A → list A → list A * list A * list A := Definition max_prefix_of : list A → list A → list A * list A * list A := fix go l1 l2 := fix go l1 l2 := match l1, l2 with match l1, l2 with ... @@ -284,7 +285,7 @@ Infix "`contains`" := contains (at level 70) : C_scope. ... @@ -284,7 +285,7 @@ Infix "`contains`" := contains (at level 70) : C_scope. Hint Extern 0 (_ `contains` _) => reflexivity. Hint Extern 0 (_ `contains` _) => reflexivity. Section contains_dec_help. Section contains_dec_help. Context {A} {dec : ∀ x y : A, Decision (x = y)}. Context `{EqDecision A}. Fixpoint list_remove (x : A) (l : list A) : option (list A) := Fixpoint list_remove (x : A) (l : list A) : option (list A) := match l with match l with | [] => None | [] => None ... @@ -302,14 +303,13 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) : ... @@ -302,14 +303,13 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) : | Forall3_cons x y z l k k' : | Forall3_cons x y z l k k' : P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k'). P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k'). (** Set operations on lists *) (** Set operations Decisionon lists *) Definition included {A} (l1 l2 : list A) := ∀ x, x ∈ l1 → x ∈ l2. Definition included {A} (l1 l2 : list A) := ∀ x, x ∈ l1 → x ∈ l2. Infix "`included`" := included (at level 70) : C_scope. Infix "`included`" := included (at level 70) : C_scope. Section list_set. Section list_set. Context {A} {dec : ∀ x y : A, Decision (x = y)}. Context `{dec : EqDecision A}. Global Instance elem_of_list_dec {dec : ∀ x y : A, Decision (x = y)} Global Instance elem_of_list_dec (x : A) : ∀ l, Decision (x ∈ l). (x : A) : ∀ l, Decision (x ∈ l). Proof. Proof. refine ( refine ( fix go l := fix go l := ... @@ -415,8 +415,8 @@ Proof. ... @@ -415,8 +415,8 @@ Proof. - discriminate (H 0). - discriminate (H 0). - f_equal; [by injection (H 0)|]. apply (IH _ \$ λ i, H (S i)). - f_equal; [by injection (H 0)|]. apply (IH _ \$ λ i, H (S i)). Qed. Qed. Global Instance list_eq_dec {dec : ∀ x y, Decision (x = y)} : ∀ l k, Global Instance list_eq_dec {dec : EqDecision A} : EqDecision (list A) := Decision (l = k) := list_eq_dec dec. list_eq_dec dec. Global Instance list_eq_nil_dec l : Decision (l = []). Global Instance list_eq_nil_dec l : Decision (l = []). Proof. by refine match l with [] => left _ | _ => right _ end. Defined. Proof. by refine match l with [] => left _ | _ => right _ end. Defined. Lemma list_singleton_reflect l : Lemma list_singleton_reflect l : ... @@ -695,7 +695,7 @@ Proof. ... @@ -695,7 +695,7 @@ Proof. Qed. Qed. Section no_dup_dec. Section no_dup_dec. Context `{!∀ x y, Decision (x = y)}. Context `{!EqDecision A}. Global Instance NoDup_dec: ∀ l, Decision (NoDup l) := Global Instance NoDup_dec: ∀ l, Decision (NoDup l) := fix NoDup_dec l := fix NoDup_dec l := match l return Decision (NoDup l) with match l return Decision (NoDup l) with ... @@ -724,7 +724,7 @@ End no_dup_dec. ... @@ -724,7 +724,7 @@ End no_dup_dec. (** ** Set operations on lists *) (** ** Set operations on lists *) Section list_set. Section list_set. Context {dec : ∀ x y, Decision (x = y)}. Context `{!EqDecision A}. Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k. Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k. Proof. Proof. split; induction l; simpl; try case_decide; split; induction l; simpl; try case_decide; ... @@ -1443,7 +1443,7 @@ Proof. ... @@ -1443,7 +1443,7 @@ Proof. - intros ?. by eexists []. - intros ?. by eexists []. - intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)). - intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)). Qed. Qed. Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2, Global Instance prefix_of_dec `{!EqDecision A} : ∀ l1 l2, Decision (l1 `prefix_of` l2) := fix go l1 l2 := Decision (l1 `prefix_of` l2) := fix go l1 l2 := match l1, l2 return { l1 `prefix_of` l2 } + { ¬l1 `prefix_of` l2 } with match l1, l2 return { l1 `prefix_of` l2 } + { ¬l1 `prefix_of` l2 } with | [], _ => left (prefix_of_nil _) | [], _ => left (prefix_of_nil _) ... @@ -1460,7 +1460,7 @@ Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2, ... @@ -1460,7 +1460,7 @@ Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2, end. end. Section prefix_ops. Section prefix_ops. Context `{∀ x y, Decision (x = y)}. Context `{!EqDecision A}. Lemma max_prefix_of_fst l1 l2 : Lemma max_prefix_of_fst l1 l2 : l1 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.1. l1 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.1. Proof. Proof. ... @@ -1577,7 +1577,7 @@ Lemma suffix_of_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2. ... @@ -1577,7 +1577,7 @@ Lemma suffix_of_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2. Proof. intros [? ->]. rewrite app_length. lia. Qed. Proof. intros [? ->]. rewrite app_length. lia. Qed. Lemma suffix_of_cons_not x l : ¬x :: l `suffix_of` l. Lemma suffix_of_cons_not x l : ¬x :: l `suffix_of` l. Proof. intros [??]. discriminate_list. Qed. Proof. intros [??]. discriminate_list. Qed. Global Instance suffix_of_dec `{∀ x y, Decision (x = y)} l1 l2 : Global Instance suffix_of_dec `{!EqDecision A} l1 l2 : Decision (l1 `suffix_of` l2). Decision (l1 `suffix_of` l2). Proof. Proof. refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2))); refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2))); ... @@ -1585,7 +1585,7 @@ Proof. ... @@ -1585,7 +1585,7 @@ Proof. Defined. Defined. Section max_suffix_of. Section max_suffix_of. Context `{∀ x y, Decision (x = y)}. Context `{!EqDecision A}. Lemma max_suffix_of_fst l1 l2 : Lemma max_suffix_of_fst l1 l2 : l1 = (max_suffix_of l1 l2).1.1 ++ (max_suffix_of l1 l2).2. l1 = (max_suffix_of l1 l2).1.1 ++ (max_suffix_of l1 l2).2. ... @@ -1987,7 +1987,7 @@ Proof. ... @@ -1987,7 +1987,7 @@ Proof. Qed. Qed. Section contains_dec. Section contains_dec. Context `{∀ x y, Decision (x = y)}. Context `{!EqDecision A}. Lemma list_remove_Permutation l1 l2 k1 x : Lemma list_remove_Permutation l1 l2 k1 x : l1 ≡ₚ l2 → list_remove x l1 = Some k1 → l1 ≡ₚ l2 → list_remove x l1 = Some k1 → ... @@ -2215,16 +2215,16 @@ Section Forall_Exists. ... @@ -2215,16 +2215,16 @@ Section Forall_Exists. Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l. Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l. Proof. induction 1; inversion_clear 1; contradiction. Qed. Proof. induction 1; inversion_clear 1; contradiction. Qed. Lemma Forall_list_difference `{∀ x y : A, Decision (x = y)} l k : Lemma Forall_list_difference `{!EqDecision A} l k : Forall P l → Forall P (list_difference l k). Forall P l → Forall P (list_difference l k). Proof. Proof. rewrite !Forall_forall. rewrite !Forall_forall. intros ? x; rewrite elem_of_list_difference; naive_solver. intros ? x; rewrite elem_of_list_difference; naive_solver. Qed. Qed. Lemma Forall_list_union `{∀ x y : A, Decision (x = y)} l k : Lemma Forall_list_union `{!EqDecision A} l k : Forall P l → Forall P k → Forall P (list_union l k). Forall P l → Forall P k → Forall P (list_union l k). Proof. intros. apply Forall_app; auto using Forall_list_difference. Qed. Proof. intros. apply Forall_app; auto using Forall_list_difference. Qed. Lemma Forall_list_intersection `{∀ x y : A, Decision (x = y)} l k : Lemma Forall_list_intersection `{!EqDecision A} l k : Forall P l → Forall P (list_intersection l k). Forall P l → Forall P (list_intersection l k). Proof. Proof. rewrite !Forall_forall. rewrite !Forall_forall. ... ...
 ... @@ -37,7 +37,7 @@ Proof. ... @@ -37,7 +37,7 @@ Proof. abstract (by rewrite listset_empty_alt). abstract (by rewrite listset_empty_alt). Defined. Defined. Context `{∀ x y : A, Decision (x = y)}. Context `{!EqDecision A}. Instance listset_intersection: Intersection (listset A) := λ l k, Instance listset_intersection: Intersection (listset A) := λ l k, let (l') := l in let (k') := k in Listset (list_intersection l' k'). let (l') := l in let (k') := k in Listset (list_intersection l' k'). ... ...
 ... @@ -13,7 +13,7 @@ Arguments listset_nodup_car {_} _. ... @@ -13,7 +13,7 @@ Arguments listset_nodup_car {_} _. Arguments listset_nodup_prf {_} _. Arguments listset_nodup_prf {_} _. Section list_collection. Section list_collection. Context {A : Type} `{∀ x y : A, Decision (x = y)}. Context `{EqDecision A}. Notation C := (listset_nodup A). Notation C := (listset_nodup A). Instance listset_nodup_elem_of: ElemOf A C := λ x l, x ∈ listset_nodup_car l. Instance listset_nodup_elem_of: ElemOf A C := λ x l, x ∈ listset_nodup_car l. ... ...
 ... @@ -68,11 +68,11 @@ Proof. ... @@ -68,11 +68,11 @@ Proof. Qed. Qed. Section deciders. Section deciders. Context `{∀ m1 m2 : M unit, Decision (m1 = m2)}. Context `{EqDecision (M unit)}. Global Instance mapset_eq_dec (X1 X2 : mapset M) : Decision (X1 = X2) | 1. Global Instance mapset_eq_dec : EqDecision (mapset M) | 1. Proof. Proof. refine refine (λ X1 X2, match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end; match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end); abstract congruence. abstract congruence. Defined. Defined. Global Instance mapset_equiv_dec (X1 X2 : mapset M) : Decision (X1 ≡ X2) | 1. Global Instance mapset_equiv_dec (X1 X2 : mapset M) : Decision (X1 ≡ X2) | 1. ... ...
 ... @@ -36,8 +36,7 @@ Proof. ... @@ -36,8 +36,7 @@ Proof. split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?]. split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?]. simplify_eq/=; f_equal; apply proof_irrel. simplify_eq/=; f_equal; apply proof_irrel. Qed. Qed. Global Instance natmap_eq_dec `{∀ x y : A, Decision (x = y)} Global Instance natmap_eq_dec `{EqDecision A} : EqDecision (natmap A) := λ m1 m2, (m1 m2 : natmap A) : Decision (m1 = m2) := match decide (natmap_car m1 = natmap_car m2) with match decide (natmap_car m1 = natmap_car m2) with | left H => left (proj2 (natmap_eq m1 m2) H) | left H => left (proj2 (natmap_eq m1 m2) H) | right H => right (H ∘ proj1 (natmap_eq m1 m2)) | right H => right (H ∘ proj1 (natmap_eq m1 m2)) ... ...
 ... @@ -12,13 +12,12 @@ Arguments Nmap_0 {_} _. ... @@ -12,13 +12,12 @@ Arguments Nmap_0 {_} _. Arguments Nmap_pos {_} _. Arguments Nmap_pos {_} _. Arguments NMap {_} _ _. Arguments NMap {_} _ _. Instance Nmap_eq_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Nmap A) :