Commit 0afa9b92 authored by Robbert Krebbers's avatar Robbert Krebbers

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

parent 2d1cd803
Pipeline #2717 passed with stage
in 9 minutes and 21 seconds
......@@ -14,7 +14,7 @@ Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
match x with DecAgree a => Some a | _ => None end.
Section dec_agree.
Context {A : Type} `{ x y : A, Decision (x = y)}.
Context `{EqDecision A}.
Instance dec_agree_valid : Valid (dec_agree A) := λ x,
if x is DecAgree _ then True else False.
......
......@@ -39,7 +39,7 @@ Section iprod_cofe.
Canonical Structure iprodC : cofeT := CofeT (iprod B) iprod_cofe_mixin.
(** Properties of iprod_insert. *)
Context `{ x x' : A, Decision (x = x')}.
Context `{EqDecision A}.
Global Instance iprod_insert_ne n x :
Proper (dist n ==> dist n ==> dist n) (iprod_insert x).
......
......@@ -22,7 +22,7 @@ Bind Scope binder_scope with binder.
Definition cons_binder (mx : binder) (X : list string) : list string :=
match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
Instance binder_eq_dec_eq : EqDecision binder.
Proof. solve_decision. Defined.
Instance set_unfold_cons_binder x mx X P :
......@@ -125,17 +125,17 @@ Qed.
Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.
Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Instance un_op_eq_dec : EqDecision un_op.
Proof. solve_decision. Defined.
Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
Instance bin_op_eq_dec : EqDecision bin_op.
Proof. solve_decision. Defined.
Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
Instance expr_eq_dec : EqDecision expr.
Proof. solve_decision. Defined.
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
Instance val_eq_dec : EqDecision val.
Proof.
refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
Defined.
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
......
......@@ -100,6 +100,7 @@ on a type [A] we write [`{∀ x y : A, Decision (x = y)}] and use it by writing
[decide (x = y)]. *)
Class Decision (P : Prop) := decide : {P} + {¬P}.
Arguments decide _ {_}.
Notation EqDecision A := ( x y : A, Decision (x = y)).
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
......@@ -918,9 +919,8 @@ Inductive NoDup {A} : list A → Prop :=
(** Decidability of equality of the carrier set is admissible, but we add it
anyway so as to avoid cycles in type class search. *)
Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C,
Union C, Intersection C, Difference C,
Elements A C, x y : A, Decision (x = y)} : Prop := {
Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
fin_collection :>> Collection A C;
elem_of_elements X x : x elements X x X;
NoDup_elements X : NoDup (elements X)
......
......@@ -8,8 +8,8 @@ Arguments mkBSet {_} _.
Arguments bset_car {_} _ _.
Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
Instance bset_singleton {A} `{ x y : A, Decision (x = y)} :
Singleton A (bset A) := λ x, mkBSet (λ y, bool_decide (y = x)).
Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x,
mkBSet (λ y, bool_decide (y = 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,
mkBSet (λ x, bset_car X1 x || bset_car X2 x).
......@@ -17,8 +17,7 @@ Instance bset_intersection {A} : Intersection (bset A) := λ X1 X2,
mkBSet (λ x, bset_car X1 x && bset_car X2 x).
Instance bset_difference {A} : Difference (bset A) := λ X1 X2,
mkBSet (λ x, bset_car X1 x && negb (bset_car X2 x)).
Instance bset_collection {A} `{ x y : A, Decision (x = y)} :
Collection A (bset A).
Instance bset_collection `{EqDecision A} : Collection A (bset A).
Proof.
split; [split| |].
- by intros x ?.
......
......@@ -19,7 +19,7 @@ Local Open Scope positive_scope.
Inductive coPset_raw :=
| coPLeaf : bool 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.
Fixpoint coPset_wf (t : coPset_raw) : bool :=
......
......@@ -3,7 +3,7 @@
From iris.prelude Require Export list.
Local Open Scope positive.
Class Countable A `{ x y : A, Decision (x = y)} := {
Class Countable A `{EqDecision A} := {
encode : A positive;
decode : positive option A;
decode_encode x : decode (encode x) = Some x
......@@ -70,7 +70,7 @@ Section choice.
Definition choice (HA : x, P x) : { x | P x } := _choose_correct HA.
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 }.
Proof.
exists (λ y, choose (λ x, f x = y) (surj f y)).
......@@ -80,7 +80,7 @@ Qed.
(** * Instances *)
(** ** Injection *)
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).
Program Instance injective_countable : Countable B :=
......
......@@ -164,15 +164,13 @@ Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
Decision (P Q) := and_dec _ _.
(** 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.
Instance unit_eq_dec (x y : unit) : Decision (x = y).
Instance unit_eq_dec : EqDecision unit.
Proof. solve_decision. Defined.
Instance prod_eq_dec `(A_dec : x y : A, Decision (x = y))
`(B_dec : x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y).
Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Proof. solve_decision. Defined.
Instance sum_eq_dec `(A_dec : x y : A, Decision (x = y))
`(B_dec : x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y).
Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
Proof. solve_decision. Defined.
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
end.
Instance sig_eq_dec `(P : A Prop) `{ x, ProofIrrel (P x)}
`{ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
Proof. refine (cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial. Defined.
Instance sig_eq_dec `(P : A Prop) `{ x, ProofIrrel (P x), EqDecision A} :
EqDecision (sig P).
Proof.
refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
Defined.
(** Some laws for decidable propositions *)
Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P Q) ¬P ¬Q.
......
......@@ -7,7 +7,7 @@ From iris.prelude Require Export collections fin_maps.
Class FinMapDom K M D `{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), 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,
Union D, Intersection D, Difference D} := {
finmap_dom_map :>> FinMap K M;
......
......@@ -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,
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;
lookup_empty {A} i : ( : M A) !! i = None;
lookup_partial_alter {A} f (m : M A) i :
......
......@@ -2,7 +2,7 @@
(* This file is distributed under the terms of the BSD license. *)
From iris.prelude Require Export countable vector.
Class Finite A `{ x y : A, Decision (x = y)} := {
Class Finite A `{EqDecision A} := {
enum : list A;
NoDup_enum : NoDup enum;
elem_of_enum x : x enum
......@@ -189,7 +189,7 @@ End forall_exists.
(** Instances *)
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 (of_to_nat : x, of_nat (to_nat x) = x).
Context (to_nat_c : x, to_nat x < c).
......@@ -212,7 +212,7 @@ Section enc_finite.
End enc_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}.
Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
......
From iris.prelude Require Export base tactics.
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) :=
λ a t f b, if decide (a = b) then t else f b.
Global Instance fn_alter : Alter A T (A T) :=
......@@ -12,7 +12,7 @@ End definitions.
of equality of 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.
Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed.
......
......@@ -22,10 +22,9 @@ Proof.
split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
f_equal; apply proof_irrel.
Qed.
Instance gmap_eq_eq `{Countable K} `{ x y : A, Decision (x = y)}
(m1 m2 : gmap K A) : Decision (m1 = m2).
Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
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).
Defined.
......
......@@ -15,7 +15,7 @@ Arguments Hashset {_ _} _ _.
Arguments hashset_car {_ _} _.
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,
hashset_car m !! hash x = Some l x l.
......@@ -137,7 +137,7 @@ Hint Extern 1 (Elements _ (hashset _)) =>
eapply @hashset_elems : typeclass_instances.
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 :=
match l with
......
......@@ -245,7 +245,8 @@ Hint Extern 0 (_ `prefix_of` _) => reflexivity.
Hint Extern 0 (_ `suffix_of` _) => reflexivity.
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 :=
fix go l1 l2 :=
match l1, l2 with
......@@ -284,7 +285,7 @@ Infix "`contains`" := contains (at level 70) : C_scope.
Hint Extern 0 (_ `contains` _) => reflexivity.
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) :=
match l with
| [] => None
......@@ -302,14 +303,13 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) :
| 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').
(** Set operations on lists *)
(** Set operations Decisionon lists *)
Definition included {A} (l1 l2 : list A) := x, x l1 x l2.
Infix "`included`" := included (at level 70) : C_scope.
Section list_set.
Context {A} {dec : x y : A, Decision (x = y)}.
Global Instance elem_of_list_dec {dec : x y : A, Decision (x = y)}
(x : A) : l, Decision (x l).
Context `{dec : EqDecision A}.
Global Instance elem_of_list_dec (x : A) : l, Decision (x l).
Proof.
refine (
fix go l :=
......@@ -415,8 +415,8 @@ Proof.
- discriminate (H 0).
- f_equal; [by injection (H 0)|]. apply (IH _ $ λ i, H (S i)).
Qed.
Global Instance list_eq_dec {dec : x y, Decision (x = y)} : l k,
Decision (l = k) := list_eq_dec dec.
Global Instance list_eq_dec {dec : EqDecision A} : EqDecision (list A) :=
list_eq_dec dec.
Global Instance list_eq_nil_dec l : Decision (l = []).
Proof. by refine match l with [] => left _ | _ => right _ end. Defined.
Lemma list_singleton_reflect l :
......@@ -695,7 +695,7 @@ Proof.
Qed.
Section no_dup_dec.
Context `{! x y, Decision (x = y)}.
Context `{!EqDecision A}.
Global Instance NoDup_dec: l, Decision (NoDup l) :=
fix NoDup_dec l :=
match l return Decision (NoDup l) with
......@@ -724,7 +724,7 @@ End no_dup_dec.
(** ** Set operations on lists *)
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.
Proof.
split; induction l; simpl; try case_decide;
......@@ -1443,7 +1443,7 @@ Proof.
- intros ?. by eexists [].
- intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
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 :=
match l1, l2 return { l1 `prefix_of` l2 } + { ¬l1 `prefix_of` l2 } with
| [], _ => left (prefix_of_nil _)
......@@ -1460,7 +1460,7 @@ Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
end.
Section prefix_ops.
Context `{ x y, Decision (x = y)}.
Context `{!EqDecision A}.
Lemma max_prefix_of_fst l1 l2 :
l1 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.1.
Proof.
......@@ -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.
Lemma suffix_of_cons_not x l : ¬x :: l `suffix_of` l.
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).
Proof.
refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
......@@ -1585,7 +1585,7 @@ Proof.
Defined.
Section max_suffix_of.
Context `{ x y, Decision (x = y)}.
Context `{!EqDecision A}.
Lemma max_suffix_of_fst l1 l2 :
l1 = (max_suffix_of l1 l2).1.1 ++ (max_suffix_of l1 l2).2.
......@@ -1987,7 +1987,7 @@ Proof.
Qed.
Section contains_dec.
Context `{ x y, Decision (x = y)}.
Context `{!EqDecision A}.
Lemma list_remove_Permutation l1 l2 k1 x :
l1 ≡ₚ l2 list_remove x l1 = Some k1
......@@ -2215,16 +2215,16 @@ Section Forall_Exists.
Lemma Forall_not_Exists l : Forall (not P) l ¬Exists P l.
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).
Proof.
rewrite !Forall_forall.
intros ? x; rewrite elem_of_list_difference; naive_solver.
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).
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).
Proof.
rewrite !Forall_forall.
......
......@@ -37,7 +37,7 @@ Proof.
abstract (by rewrite listset_empty_alt).
Defined.
Context `{ x y : A, Decision (x = y)}.
Context `{!EqDecision A}.
Instance listset_intersection: Intersection (listset A) := λ l k,
let (l') := l in let (k') := k in Listset (list_intersection l' k').
......
......@@ -13,7 +13,7 @@ Arguments listset_nodup_car {_} _.
Arguments listset_nodup_prf {_} _.
Section list_collection.
Context {A : Type} `{ x y : A, Decision (x = y)}.
Context `{EqDecision A}.
Notation C := (listset_nodup A).
Instance listset_nodup_elem_of: ElemOf A C := λ x l, x listset_nodup_car l.
......
......@@ -68,11 +68,11 @@ Proof.
Qed.
Section deciders.
Context `{ m1 m2 : M unit, Decision (m1 = m2)}.
Global Instance mapset_eq_dec (X1 X2 : mapset M) : Decision (X1 = X2) | 1.
Context `{EqDecision (M unit)}.
Global Instance mapset_eq_dec : EqDecision (mapset M) | 1.
Proof.
refine
match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end;
refine (λ X1 X2,
match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
abstract congruence.
Defined.
Global Instance mapset_equiv_dec (X1 X2 : mapset M) : Decision (X1 X2) | 1.
......
......@@ -36,8 +36,7 @@ Proof.
split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
simplify_eq/=; f_equal; apply proof_irrel.
Qed.
Global Instance natmap_eq_dec `{ x y : A, Decision (x = y)}
(m1 m2 : natmap A) : Decision (m1 = m2) :=
Global Instance natmap_eq_dec `{EqDecision A} : EqDecision (natmap A) := λ m1 m2,
match decide (natmap_car m1 = natmap_car m2) with
| left H => left (proj2 (natmap_eq m1 m2) H)
| right H => right (H proj1 (natmap_eq m1 m2))
......
......@@ -12,13 +12,12 @@ Arguments Nmap_0 {_} _.
Arguments Nmap_pos {_} _.
Arguments NMap {_} _ _.
Instance Nmap_eq_dec `{ x y : A, Decision (x = y)} (t1 t2 : Nmap A) :
Decision (t1 = t2).
Instance Nmap_eq_dec `{EqDecision A} : EqDecision (Nmap A).
Proof.
refine
refine (λ t1 t2,
match t1, t2 with
| NMap x t1, NMap y t2 => cast_if_and (decide (x = y)) (decide (t1 = t2))
end; abstract congruence.
end); abstract congruence.
Defined.
Instance Nempty {A} : Empty (Nmap A) := NMap None .
Global Opaque Nempty.
......
......@@ -9,7 +9,7 @@ From iris.prelude Require Export base decidable option.
Open Scope nat_scope.
Coercion Z.of_nat : nat >-> Z.
Instance comparison_eq_dec (c1 c2 : comparison) : Decision (c1 = c2).
Instance comparison_eq_dec : EqDecision comparison.
Proof. solve_decision. Defined.
(** * Notations and properties of [nat] *)
......@@ -35,13 +35,13 @@ Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
Infix "`max`" := Nat.max (at level 35) : nat_scope.
Infix "`min`" := Nat.min (at level 35) : nat_scope.
Instance nat_eq_dec: x y : nat, Decision (x = y) := eq_nat_dec.
Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
Instance nat_le_dec: x y : nat, Decision (x y) := le_dec.
Instance nat_lt_dec: x y : nat, Decision (x < y) := lt_dec.
Instance nat_inhabited: Inhabited nat := populate 0%nat.
Instance: Inj (=) (=) S.
Instance S_inj: Inj (=) (=) S.
Proof. by injection 1. Qed.
Instance: PartialOrder ().
Instance nat_le_po: PartialOrder ().
Proof. repeat split; repeat intro; auto with lia. Qed.
Instance nat_le_pi: x y : nat, ProofIrrel (x y).
......@@ -116,7 +116,7 @@ Notation "(~1)" := xI (only parsing) : positive_scope.
Arguments Pos.of_nat : simpl never.
Arguments Pmult : simpl never.
Instance positive_eq_dec: x y : positive, Decision (x = y) := Pos.eq_dec.
Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
Instance positive_inhabited: Inhabited positive := populate 1.
Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
......@@ -198,7 +198,7 @@ Arguments N.add _ _ : simpl never.
Instance: Inj (=) (=) Npos.
Proof. by injection 1. Qed.
Instance N_eq_dec: x y : N, Decision (x = y) := N.eq_dec.
Instance N_eq_dec: EqDecision N := N.eq_dec.
Program Instance N_le_dec (x y : N) : Decision (x y)%N :=
match Ncompare x y with Gt => right _ | _ => left _ end.
Solve Obligations with naive_solver.
......@@ -206,7 +206,7 @@ Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
match Ncompare x y with Lt => left _ | _ => right _ end.
Solve Obligations with naive_solver.
Instance N_inhabited: Inhabited N := populate 1%N.
Instance: PartialOrder ()%N.
Instance N_le_po: PartialOrder ()%N.
Proof.
repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
Qed.
......@@ -239,11 +239,11 @@ Proof. by injection 1. Qed.
Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.
Instance Z_eq_dec: x y : Z, Decision (x = y) := Z.eq_dec.
Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
Instance Z_le_dec: x y : Z, Decision (x y) := Z_le_dec.
Instance Z_lt_dec: x y : Z, Decision (x < y) := Z_lt_dec.
Instance Z_inhabited: Inhabited Z := populate 1.
Instance Z_le_order : PartialOrder ().
Instance Z_le_po : PartialOrder ().
Proof.
repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
Qed.
......@@ -345,7 +345,7 @@ Notation "(<)" := Qclt (only parsing) : Qc_scope.
Hint Extern 1 (_ _) => reflexivity || discriminate.
Arguments Qred _ : simpl never.
Instance Qc_eq_dec: x y : Qc, Decision (x = y) := Qc_eq_dec.
Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
Program Instance Qc_le_dec (x y : Qc) : Decision (x y) :=
if Qclt_le_dec y x then right _ else left _.
Next Obligation. intros x y; apply Qclt_not_le. Qed.
......
......@@ -148,14 +148,13 @@ Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None) :=
match mx with Some _ => right (Some_ne_None _) | None => left eq_refl end.
Instance option_None_eq_dec {A} (mx : option A) : Decision (None = mx) :=
match mx with Some _ => right (None_ne_Some _) | None => left eq_refl end.
Instance option_eq_dec {A} {dec : x y : A, Decision (x = y)}
(mx my : option A) : Decision (mx = my).
Instance option_eq_dec `{dec : EqDecision A} : EqDecision (option A).
Proof.
refine
refine (λ mx my,
match mx, my with
| Some x, Some y => cast_if (decide (x = y))
| None, None => left _ | _, _ => right _
end; clear dec; abstract congruence.
end); clear dec; abstract congruence.
Defined.
(** * Monadic operations *)
......
......@@ -48,10 +48,9 @@ Section orders.
- intros [? HYX]. split. done. by intros <-.
- intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R).
Qed.
Lemma po_eq_dec `{!PartialOrder R, X Y, Decision (X Y)} (X Y : A) :
Decision (X = Y).
Lemma po_eq_dec `{!PartialOrder R, X Y, Decision (X Y)} : EqDecision A.
Proof.
refine (cast_if_and (decide (X Y)) (decide (Y X)));
refine (λ X Y, cast_if_and (decide (X Y)) (decide (Y X)));
abstract (rewrite anti_symm_iff; tauto).
Defined.
Lemma total_not `{!Total R} X Y : X Y Y X.
......
......@@ -26,8 +26,7 @@ Inductive Pmap_raw (A : Type) : Type :=
Arguments PLeaf {_}.
Arguments PNode {_} _ _ _.
Instance Pmap_raw_eq_dec `{ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
Decision (x = y).
Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A).
Proof. solve_decision. Defined.
Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool :=
......@@ -266,8 +265,7 @@ Proof.
split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
simplify_eq/=; f_equal; apply proof_irrel.
Qed.
Instance Pmap_eq_dec `{ x y : A, Decision (x = y)}
(m1 m2 : Pmap A) : Decision (m1 = m2) :=
Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
match Pmap_raw_eq_dec (pmap_car m1) (pmap_car m2) with
| left H => left (proj2 (Pmap_eq m1 m2) H)
| right H => right (H proj1 (Pmap_eq m1 m2))
......
......@@ -16,10 +16,10 @@ Infix "+:+" := String.append (at level 60, right associativity) : C_scope.
Arguments String.append _ _ : simpl never.
(** * Decision of equality *)
Instance assci_eq_dec : a1 a2, Decision (a1 = a2) := ascii_dec.
Instance string_eq_dec (s1 s2 : string) : Decision (s1 = s2).
Instance assci_eq_dec : EqDecision ascii := ascii_dec.
Instance string_eq_dec : EqDecision string.
Proof. solve_decision. Defined.
Instance: Inj (=) (=) (String.append s1).
Instance string_app_inj : Inj (=) (=) (String.append s1).
Proof. intros s1 ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
(* Reverse *)
......
......@@ -35,7 +35,7 @@ Coercion fin_to_nat : fin >-> nat.
Notation fin_of_nat := Fin.of_nat_lt.
Notation fin_rect2 := Fin.rect2.
Instance fin_dec {n} : i j : fin n, Decision (i = j).
Instance fin_dec {n} : EqDecision (fin n).
Proof.
refine (fin_rect2
(λ n (i j : fin n), { i = j } + { i j })
......@@ -163,8 +163,7 @@ Proof.
- apply IH. intros i. apply (Hi (FS i)).