summaryrefslogtreecommitdiff
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Integer/Abstract/ZBase.v8
-rw-r--r--theories/Numbers/Integer/Abstract/ZDomain.v4
-rw-r--r--theories/Numbers/Integer/Abstract/ZMulOrder.v6
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v4
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v3
-rw-r--r--theories/Numbers/Integer/NatPairs/ZNatPairs.v6
-rw-r--r--theories/Numbers/NatInt/NZBase.v4
-rw-r--r--theories/Numbers/NatInt/NZOrder.v4
-rw-r--r--theories/Numbers/Natural/Abstract/NAdd.v4
-rw-r--r--theories/Numbers/Natural/Abstract/NBase.v10
-rw-r--r--theories/Numbers/Natural/Abstract/NDefOps.v4
-rw-r--r--theories/Numbers/Natural/Abstract/NStrongRec.v8
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v4
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml3
-rw-r--r--theories/Numbers/NumPrelude.v6
15 files changed, 36 insertions, 42 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 29e18548..0f71f2cc 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: ZBase.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: ZBase.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Export Decidable.
Require Export ZAxioms.
@@ -36,14 +36,14 @@ Proof NZpred_succ.
Theorem Zeq_refl : forall n : Z, n == n.
Proof (proj1 NZeq_equiv).
-Theorem Zeq_symm : forall n m : Z, n == m -> m == n.
+Theorem Zeq_sym : forall n m : Z, n == m -> m == n.
Proof (proj2 (proj2 NZeq_equiv)).
Theorem Zeq_trans : forall n m p : Z, n == m -> m == p -> n == p.
Proof (proj1 (proj2 NZeq_equiv)).
-Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n.
-Proof NZneq_symm.
+Theorem Zneq_sym : forall n m : Z, n ~= m -> m ~= n.
+Proof NZneq_sym.
Theorem Zsucc_inj : forall n1 n2 : Z, S n1 == S n2 -> n1 == n2.
Proof NZsucc_inj.
diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v
index 15beb2b9..9a17e151 100644
--- a/theories/Numbers/Integer/Abstract/ZDomain.v
+++ b/theories/Numbers/Integer/Abstract/ZDomain.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: ZDomain.v 10934 2008-05-15 21:58:20Z letouzey $ i*)
+(*i $Id: ZDomain.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Export NumPrelude.
@@ -49,7 +49,7 @@ assert (x == y); [rewrite Exx'; now rewrite Eyy' |
rewrite <- H2; assert (H3 : e x y); [now apply -> eq_equiv_e | now inversion H3]]].
Qed.
-Theorem neq_symm : forall n m, n # m -> m # n.
+Theorem neq_sym : forall n m, n # m -> m # n.
Proof.
intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
Qed.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index e3f1d9aa..c7996ffd 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: ZMulOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: ZMulOrder.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Export ZAddOrder.
@@ -173,7 +173,7 @@ Notation Zmul_neg := Zlt_mul_0 (only parsing).
Theorem Zle_0_mul :
forall n m : Z, 0 <= n * m -> 0 <= n /\ 0 <= m \/ n <= 0 /\ m <= 0.
Proof.
-assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm).
+assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_sym).
intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
rewrite Zlt_0_mul, Zeq_mul_0.
pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
@@ -184,7 +184,7 @@ Notation Zmul_nonneg := Zle_0_mul (only parsing).
Theorem Zle_mul_0 :
forall n m : Z, n * m <= 0 -> 0 <= n /\ m <= 0 \/ n <= 0 /\ 0 <= m.
Proof.
-assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_symm).
+assert (R : forall n : Z, 0 == n <-> n == 0) by (intros; split; apply Zeq_sym).
intros n m. repeat rewrite Zlt_eq_cases. repeat rewrite R.
rewrite Zlt_mul_0, Zeq_mul_0.
pose proof (Zlt_trichotomy n 0); pose proof (Zlt_trichotomy m 0). tauto.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index cb920124..e5e950ac 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: BigZ.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: BigZ.v 11576 2008-11-10 19:13:15Z msozeau $ i*)
Require Export BigN.
Require Import ZMulOrder.
@@ -104,8 +104,6 @@ exact sub_opp.
exact add_opp.
Qed.
-Typeclasses unfold NZadd NZmul NZsub NZeq.
-
Add Ring BigZr : BigZring.
(** Todo: tactic translating from [BigZ] to [Z] + omega *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 6305156b..98ad4c64 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: ZMake.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: ZMake.v 11576 2008-11-10 19:13:15Z msozeau $ i*)
Require Import ZArith.
Require Import BigNumPrelude.
@@ -30,7 +30,6 @@ Module Make (N:NType) <: ZType.
| Neg : N.t -> t_.
Definition t := t_.
- Typeclasses unfold t.
Definition zero := Pos N.zero.
Definition one := Pos N.one.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 8b3d815d..9427b37b 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: ZNatPairs.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: ZNatPairs.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Import NSub. (* The most complete file for natural numbers *)
Require Export ZMulOrder. (* The most complete file for integers *)
@@ -110,7 +110,7 @@ Proof.
unfold reflexive, Zeq. reflexivity.
Qed.
-Theorem ZE_symm : symmetric Z Zeq.
+Theorem ZE_sym : symmetric Z Zeq.
Proof.
unfold symmetric, Zeq; now symmetry.
Qed.
@@ -127,7 +127,7 @@ Qed.
Theorem NZeq_equiv : equiv Z Zeq.
Proof.
-unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm].
+unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_sym].
Qed.
Add Relation Z Zeq
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 8b01e353..bd4d6232 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -8,14 +8,14 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZBase.v 10934 2008-05-15 21:58:20Z letouzey $ i*)
+(*i $Id: NZBase.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Import NZAxioms.
Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig).
Open Local Scope NatIntScope.
-Theorem NZneq_symm : forall n m : NZ, n ~= m -> m ~= n.
+Theorem NZneq_sym : forall n m : NZ, n ~= m -> m ~= n.
Proof.
intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
Qed.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 15004824..d0e2faf8 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NZOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: NZOrder.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Import NZAxioms.
Require Import NZMul.
@@ -118,7 +118,7 @@ Qed.
Theorem NZneq_succ_diag_r : forall n : NZ, n ~= S n.
Proof.
-intro n; apply NZneq_symm; apply NZneq_succ_diag_l.
+intro n; apply NZneq_sym; apply NZneq_succ_diag_l.
Qed.
Theorem NZnlt_succ_diag_l : forall n : NZ, ~ S n < n.
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index f58b87d8..91ae5b70 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: NAdd.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Export NBase.
@@ -103,7 +103,7 @@ Qed.
Theorem succ_add_discr : forall n m : N, m ~= S (n + m).
Proof.
intro n; induct m.
-apply neq_symm. apply neq_succ_0.
+apply neq_sym. apply neq_succ_0.
intros m IH H. apply succ_inj in H. rewrite add_succ_r in H.
unfold not in IH; now apply IH.
Qed.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 3e4032b5..85e2c2ab 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NBase.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: NBase.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Export Decidable.
Require Export NAxioms.
@@ -48,14 +48,14 @@ Proof pred_0.
Theorem Neq_refl : forall n : N, n == n.
Proof (proj1 NZeq_equiv).
-Theorem Neq_symm : forall n m : N, n == m -> m == n.
+Theorem Neq_sym : forall n m : N, n == m -> m == n.
Proof (proj2 (proj2 NZeq_equiv)).
Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p.
Proof (proj1 (proj2 NZeq_equiv)).
-Theorem neq_symm : forall n m : N, n ~= m -> m ~= n.
-Proof NZneq_symm.
+Theorem neq_sym : forall n m : N, n ~= m -> m ~= n.
+Proof NZneq_sym.
Theorem succ_inj : forall n1 n2 : N, S n1 == S n2 -> n1 == n2.
Proof NZsucc_inj.
@@ -111,7 +111,7 @@ Qed.
Theorem neq_0_succ : forall n : N, 0 ~= S n.
Proof.
-intro n; apply neq_symm; apply neq_succ_0.
+intro n; apply neq_sym; apply neq_succ_0.
Qed.
(* Next, we show that all numbers are nonnegative and recover regular induction
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index e15e4672..0a8f5f1e 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NDefOps.v 11039 2008-06-02 23:26:13Z letouzey $ i*)
+(*i $Id: NDefOps.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Import Bool. (* To get the orb and negb function *)
Require Export NStrongRec.
@@ -243,7 +243,7 @@ Definition E2 := prod_rel Neq Neq.
Add Relation (prod N N) E2
reflexivity proved by (prod_rel_refl N N Neq Neq E_equiv E_equiv)
-symmetry proved by (prod_rel_symm N N Neq Neq E_equiv E_equiv)
+symmetry proved by (prod_rel_sym N N Neq Neq E_equiv E_equiv)
transitivity proved by (prod_rel_trans N N Neq Neq E_equiv E_equiv)
as E2_rel.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index 031dbdea..c6a6da48 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NStrongRec.v 11040 2008-06-03 00:04:16Z letouzey $ i*)
+(*i $Id: NStrongRec.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
(** This file defined the strong (course-of-value, well-founded) recursion
and proves its properties *)
@@ -81,9 +81,9 @@ Proof.
intros n1 n2 H. unfold g. now apply strong_rec_wd.
Qed.
-Theorem NtoA_eq_symm : symmetric (N -> A) (fun_eq Neq Aeq).
+Theorem NtoA_eq_sym : symmetric (N -> A) (fun_eq Neq Aeq).
Proof.
-apply fun_eq_symm.
+apply fun_eq_sym.
exact (proj2 (proj2 NZeq_equiv)).
exact (proj2 (proj2 Aeq_equiv)).
Qed.
@@ -97,7 +97,7 @@ exact (proj1 (proj2 Aeq_equiv)).
Qed.
Add Relation (N -> A) (fun_eq Neq Aeq)
- symmetry proved by NtoA_eq_symm
+ symmetry proved by NtoA_eq_sym
transitivity proved by NtoA_eq_trans
as NtoA_eq_rel.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 41c255b1..16007656 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: BigN.v 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: BigN.v 11576 2008-11-10 19:13:15Z msozeau $ i*)
(** * Natural numbers in base 2^31 *)
@@ -78,8 +78,6 @@ exact mul_assoc.
exact mul_add_distr_r.
Qed.
-Typeclasses unfold NZadd NZsub NZmul.
-
Add Ring BigNr : BigNring.
(** Todo: tactic translating from [BigN] to [Z] + omega *)
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 4d6b45c5..04c7b96d 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NMake_gen.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: NMake_gen.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*S NMake_gen.ml : this file generates NMake.v *)
@@ -139,7 +139,6 @@ let _ =
pr "";
pr " Definition %s := %s_." t t;
pr "";
- pr " Typeclasses unfold %s." t;
pr " Definition w_0 := w0_op.(znz_0).";
pr "";
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index fdccf214..95d8b366 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NumPrelude.v 10943 2008-05-19 08:45:13Z letouzey $ i*)
+(*i $Id: NumPrelude.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
Require Export Setoid.
@@ -212,7 +212,7 @@ unfold reflexive, prod_rel.
destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl.
Qed.
-Lemma prod_rel_symm : symmetric (A * B) prod_rel.
+Lemma prod_rel_sym : symmetric (A * B) prod_rel.
Proof.
unfold symmetric, prod_rel.
destruct x; destruct y;
@@ -229,7 +229,7 @@ Qed.
Theorem prod_rel_equiv : equiv (A * B) prod_rel.
Proof.
-unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_symm]].
+unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_sym]].
Qed.
End RelationOnProduct.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:04:54 +0000