diff options
Diffstat (limited to 'lib/Ordered.v')
| -rw-r--r-- | lib/Ordered.v | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/lib/Ordered.v b/lib/Ordered.v index a2c36673..c333cc50 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -31,11 +31,11 @@ Definition eq (x y: t) := x = y. Definition lt := Plt. Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof Plt_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. @@ -58,16 +58,16 @@ Module OrderedZ <: OrderedType. Definition t := Z. Definition eq (x y: t) := x = y. -Definition lt := Zlt. +Definition lt := Z.lt. Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. -Proof Zlt_trans. +Proof Z.lt_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof. unfold lt, eq, t; intros. omega. Qed. Lemma compare : forall x y : t, Compare lt eq x y. @@ -91,11 +91,11 @@ Definition eq (x y: t) := x = y. Definition lt (x y: t) := Int.unsigned x < Int.unsigned y. Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. omega. @@ -129,11 +129,11 @@ Definition eq (x y: t) := x = y. Definition lt (x y: t) := Plt (A.index x) (A.index y). Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. |