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/Natural/Abstract | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
-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 |
4 files changed, 13 insertions, 13 deletions
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. |