diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /theories/Numbers | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'theories/Numbers')
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 8 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDomain.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/BigZ.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 3 | ||||
-rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 6 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 4 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NAdd.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 10 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NStrongRec.v | 8 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 3 | ||||
-rw-r--r-- | theories/Numbers/NumPrelude.v | 6 |
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. |