diff options
Diffstat (limited to 'theories/Arith')
| -rw-r--r-- | theories/Arith/Arith.v | 4 | ||||
| -rw-r--r-- | theories/Arith/Arith_base.v | 4 | ||||
| -rw-r--r-- | theories/Arith/Between.v | 4 | ||||
| -rw-r--r-- | theories/Arith/Bool_nat.v | 6 | ||||
| -rw-r--r-- | theories/Arith/Compare.v | 6 | ||||
| -rw-r--r-- | theories/Arith/Compare_dec.v | 18 | ||||
| -rw-r--r-- | theories/Arith/Div2.v | 4 | ||||
| -rw-r--r-- | theories/Arith/EqNat.v | 4 | ||||
| -rw-r--r-- | theories/Arith/Euclid.v | 13 | ||||
| -rw-r--r-- | theories/Arith/Even.v | 4 | ||||
| -rw-r--r-- | theories/Arith/Factorial.v | 8 | ||||
| -rw-r--r-- | theories/Arith/Gt.v | 4 | ||||
| -rw-r--r-- | theories/Arith/Le.v | 11 | ||||
| -rw-r--r-- | theories/Arith/Lt.v | 11 | ||||
| -rw-r--r-- | theories/Arith/Max.v | 58 | ||||
| -rw-r--r-- | theories/Arith/Min.v | 52 | ||||
| -rw-r--r-- | theories/Arith/MinMax.v | 113 | ||||
| -rw-r--r-- | theories/Arith/Minus.v | 4 | ||||
| -rw-r--r-- | theories/Arith/Mult.v | 19 | ||||
| -rw-r--r-- | theories/Arith/NatOrderedType.v | 64 | ||||
| -rw-r--r-- | theories/Arith/Peano_dec.v | 26 | ||||
| -rw-r--r-- | theories/Arith/Plus.v | 31 | ||||
| -rw-r--r-- | theories/Arith/Wf_nat.v | 23 | ||||
| -rw-r--r-- | theories/Arith/vo.itarget | 2 |
24 files changed, 136 insertions, 357 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 2e9dc2de..6f3827a3 100644 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Arith.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Arith_base. Require Export ArithRing. diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v index e9953e54..4f21dadf 100644 --- a/theories/Arith/Arith_base.v +++ b/theories/Arith/Arith_base.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Arith_base.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Le. Require Export Lt. Require Export Plus. diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 65753e31..dd514653 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Between.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Le. Require Import Lt. diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v index b3dcd8ec..f384e148 100644 --- a/theories/Arith/Bool_nat.v +++ b/theories/Arith/Bool_nat.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Bool_nat.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Export Compare_dec. Require Export Peano_dec. Require Import Sumbool. @@ -36,4 +34,4 @@ Definition nat_noteq_bool x y := bool_of_sumbool (sumbool_not _ _ (eq_nat_dec x y)). Definition zerop_bool x := bool_of_sumbool (zerop x). -Definition notzerop_bool x := bool_of_sumbool (notzerop x).
\ No newline at end of file +Definition notzerop_bool x := bool_of_sumbool (notzerop x). diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index 2fe5c0d9..c9e6d3cf 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Compare.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Equality is decidable on [nat] *) Open Local Scope nat_scope. @@ -52,4 +50,4 @@ Qed. Require Export Wf_nat. -Require Export Min Max.
\ No newline at end of file +Require Export Min Max. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 99c7415e..360d760a 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Compare_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Le. Require Import Lt. Require Import Gt. @@ -22,21 +20,21 @@ Proof. destruct n; auto with arith. Defined. -Definition lt_eq_lt_dec : forall n m, {n < m} + {n = m} + {m < n}. +Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. Proof. - induction n; destruct m; auto with arith. + induction n in m |- *; destruct m; auto with arith. destruct (IHn m) as [H|H]; auto with arith. destruct H; auto with arith. Defined. -Definition gt_eq_gt_dec : forall n m, {m > n} + {n = m} + {n > m}. +Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}. Proof. intros; apply lt_eq_lt_dec; assumption. Defined. -Definition le_lt_dec : forall n m, {n <= m} + {m < n}. +Definition le_lt_dec n m : {n <= m} + {m < n}. Proof. - induction n. + induction n in m |- *. auto with arith. destruct m. auto with arith. @@ -200,7 +198,8 @@ Proof. apply -> nat_compare_lt; auto. Qed. -Lemma nat_compare_spec : forall x y, CompSpec eq lt x y (nat_compare x y). +Lemma nat_compare_spec : + forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y). Proof. intros. destruct (nat_compare x y) as [ ]_eqn; constructor. @@ -209,7 +208,6 @@ Proof. apply <- nat_compare_gt; auto. Qed. - (** Some projections of the above equivalences. *) Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 89620f5f..24cbc3f9 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Div2.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Lt. Require Import Plus. Require Import Compare_dec. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 60575beb..94986278 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqNat.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Equality on natural numbers *) Open Local Scope nat_scope. diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index f32e1ad4..513fd110 100644 --- a/theories/Arith/Euclid.v +++ b/theories/Arith/Euclid.v @@ -1,25 +1,22 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Euclid.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Mult. Require Import Compare_dec. Require Import Wf_nat. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types a b n q r : nat. Inductive diveucl a b : Set := divex : forall q r, b > r -> a = q * b + r -> diveucl a b. - Lemma eucl_dev : forall n, n > 0 -> forall m:nat, diveucl m n. Proof. intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. @@ -32,7 +29,7 @@ Proof. elim e; auto with arith. intros gtbn. apply divex with 0 n; simpl in |- *; auto with arith. -Qed. +Defined. Lemma quotient : forall n, @@ -50,7 +47,7 @@ Proof. elim H1; auto with arith. intros gtbn. exists 0; exists n; simpl in |- *; auto with arith. -Qed. +Defined. Lemma modulo : forall n, @@ -68,4 +65,4 @@ Proof. elim H1; auto with arith. intros gtbn. exists n; exists 0; simpl in |- *; auto with arith. -Qed. +Defined. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 5bab97c2..cd4dae98 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Even.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Here we define the predicates [even] and [odd] by mutual induction and we prove the decidability and the exclusion of those predicates. The main results about parity are proved in the module Div2. *) diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 3b434b96..146546dc 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Factorial.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Plus. Require Import Mult. Require Import Lt. @@ -15,13 +13,13 @@ Open Local Scope nat_scope. (** Factorial *) -Boxed Fixpoint fact (n:nat) : nat := +Fixpoint fact (n:nat) : nat := match n with | O => 1 | S n => S n * fact n end. -Arguments Scope fact [nat_scope]. +Arguments fact n%nat. Lemma lt_O_fact : forall n:nat, 0 < fact n. Proof. diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index 43df01c0..32f453e5 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Gt.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as: << Definition gt (n m:nat) := m < n. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index b73959e7..f0ebf162 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Le.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Order on natural numbers. [le] is defined in [Init/Peano.v] as: << Inductive le (n:nat) : nat -> Prop := @@ -84,8 +82,7 @@ Hint Immediate le_Sn_le: arith v62. Theorem le_S_n : forall n m, S n <= S m -> n <= m. Proof. - intros n m H; change (pred (S n) <= pred (S m)) in |- *. - destruct H; simpl; auto with arith. + exact Peano.le_S_n. Qed. Hint Immediate le_S_n: arith v62. @@ -105,11 +102,9 @@ Hint Resolve le_pred_n: arith v62. Theorem le_pred : forall n m, n <= m -> pred n <= pred m. Proof. - destruct n; simpl; auto with arith. - destruct m; simpl; auto with arith. + exact Peano.le_pred. Qed. - (** * [le] is a order on [nat] *) (** Antisymmetry *) diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 004274fe..e07bba8d 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Lt.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as: << Definition lt (n m:nat) := S n <= m. @@ -96,9 +94,9 @@ Proof. Qed. Hint Resolve lt_0_Sn: arith v62. -Theorem lt_n_O : forall n, ~ n < 0. -Proof le_Sn_O. -Hint Resolve lt_n_O: arith v62. +Theorem lt_n_0 : forall n, ~ n < 0. +Proof le_Sn_0. +Hint Resolve lt_n_0: arith v62. (** * Predecessor *) @@ -192,4 +190,5 @@ Hint Immediate lt_0_neq: arith v62. Notation lt_O_Sn := lt_0_Sn (only parsing). Notation neq_O_lt := neq_0_lt (only parsing). Notation lt_O_neq := lt_0_neq (only parsing). +Notation lt_n_O := lt_n_0 (only parsing). (* end hide *) diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index d1b1b269..77dfa508 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -1,44 +1,48 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Max.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) -(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *) - -Require Export MinMax. +Require Import NPeano. Local Open Scope nat_scope. Implicit Types m n p : nat. -Notation max := MinMax.max (only parsing). - -Definition max_0_l := max_0_l. -Definition max_0_r := max_0_r. -Definition succ_max_distr := succ_max_distr. -Definition plus_max_distr_l := plus_max_distr_l. -Definition plus_max_distr_r := plus_max_distr_r. -Definition max_case_strong := max_case_strong. -Definition max_spec := max_spec. -Definition max_dec := max_dec. -Definition max_case := max_case. -Definition max_idempotent := max_id. -Definition max_assoc := max_assoc. -Definition max_comm := max_comm. -Definition max_l := max_l. -Definition max_r := max_r. -Definition le_max_l := le_max_l. -Definition le_max_r := le_max_r. -Definition max_lub_l := max_lub_l. -Definition max_lub_r := max_lub_r. -Definition max_lub := max_lub. +Notation max := Peano.max (only parsing). + +Definition max_0_l := Nat.max_0_l. +Definition max_0_r := Nat.max_0_r. +Definition succ_max_distr := Nat.succ_max_distr. +Definition plus_max_distr_l := Nat.add_max_distr_l. +Definition plus_max_distr_r := Nat.add_max_distr_r. +Definition max_case_strong := Nat.max_case_strong. +Definition max_spec := Nat.max_spec. +Definition max_dec := Nat.max_dec. +Definition max_case := Nat.max_case. +Definition max_idempotent := Nat.max_id. +Definition max_assoc := Nat.max_assoc. +Definition max_comm := Nat.max_comm. +Definition max_l := Nat.max_l. +Definition max_r := Nat.max_r. +Definition le_max_l := Nat.le_max_l. +Definition le_max_r := Nat.le_max_r. +Definition max_lub_l := Nat.max_lub_l. +Definition max_lub_r := Nat.max_lub_r. +Definition max_lub := Nat.max_lub. (* begin hide *) (* Compatibility *) Notation max_case2 := max_case (only parsing). -Notation max_SS := succ_max_distr (only parsing). +Notation max_SS := Nat.succ_max_distr (only parsing). (* end hide *) + +Hint Resolve + Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith v62. + +Hint Resolve + Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith v62. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 0c8b5669..bcfbe0ef 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -1,44 +1,42 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Min.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) -(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *) - -Require Export MinMax. +Require Import NPeano. Open Local Scope nat_scope. Implicit Types m n p : nat. -Notation min := MinMax.min (only parsing). +Notation min := Peano.min (only parsing). -Definition min_0_l := min_0_l. -Definition min_0_r := min_0_r. -Definition succ_min_distr := succ_min_distr. -Definition plus_min_distr_l := plus_min_distr_l. -Definition plus_min_distr_r := plus_min_distr_r. -Definition min_case_strong := min_case_strong. -Definition min_spec := min_spec. -Definition min_dec := min_dec. -Definition min_case := min_case. -Definition min_idempotent := min_id. -Definition min_assoc := min_assoc. -Definition min_comm := min_comm. -Definition min_l := min_l. -Definition min_r := min_r. -Definition le_min_l := le_min_l. -Definition le_min_r := le_min_r. -Definition min_glb_l := min_glb_l. -Definition min_glb_r := min_glb_r. -Definition min_glb := min_glb. +Definition min_0_l := Nat.min_0_l. +Definition min_0_r := Nat.min_0_r. +Definition succ_min_distr := Nat.succ_min_distr. +Definition plus_min_distr_l := Nat.add_min_distr_l. +Definition plus_min_distr_r := Nat.add_min_distr_r. +Definition min_case_strong := Nat.min_case_strong. +Definition min_spec := Nat.min_spec. +Definition min_dec := Nat.min_dec. +Definition min_case := Nat.min_case. +Definition min_idempotent := Nat.min_id. +Definition min_assoc := Nat.min_assoc. +Definition min_comm := Nat.min_comm. +Definition min_l := Nat.min_l. +Definition min_r := Nat.min_r. +Definition le_min_l := Nat.le_min_l. +Definition le_min_r := Nat.le_min_r. +Definition min_glb_l := Nat.min_glb_l. +Definition min_glb_r := Nat.min_glb_r. +Definition min_glb := Nat.min_glb. (* begin hide *) (* Compatibility *) Notation min_case2 := min_case (only parsing). -Notation min_SS := succ_min_distr (only parsing). -(* end hide *)
\ No newline at end of file +Notation min_SS := Nat.succ_min_distr (only parsing). +(* end hide *) diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v deleted file mode 100644 index 8a23c8f6..00000000 --- a/theories/Arith/MinMax.v +++ /dev/null @@ -1,113 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import Orders NatOrderedType GenericMinMax. - -(** * Maximum and Minimum of two natural numbers *) - -Fixpoint max n m : nat := - match n, m with - | O, _ => m - | S n', O => n - | S n', S m' => S (max n' m') - end. - -Fixpoint min n m : nat := - match n, m with - | O, _ => 0 - | S n', O => 0 - | S n', S m' => S (min n' m') - end. - -(** These functions implement indeed a maximum and a minimum *) - -Lemma max_l : forall x y, y<=x -> max x y = x. -Proof. - induction x; destruct y; simpl; auto with arith. -Qed. - -Lemma max_r : forall x y, x<=y -> max x y = y. -Proof. - induction x; destruct y; simpl; auto with arith. -Qed. - -Lemma min_l : forall x y, x<=y -> min x y = x. -Proof. - induction x; destruct y; simpl; auto with arith. -Qed. - -Lemma min_r : forall x y, y<=x -> min x y = y. -Proof. - induction x; destruct y; simpl; auto with arith. -Qed. - - -Module NatHasMinMax <: HasMinMax Nat_as_OT. - Definition max := max. - Definition min := min. - Definition max_l := max_l. - Definition max_r := max_r. - Definition min_l := min_l. - Definition min_r := min_r. -End NatHasMinMax. - -(** We obtain hence all the generic properties of [max] and [min], - see file [GenericMinMax] or use SearchAbout. *) - -Module Export MMP := UsualMinMaxProperties Nat_as_OT NatHasMinMax. - - -(** * Properties specific to the [nat] domain *) - -(** Simplifications *) - -Lemma max_0_l : forall n, max 0 n = n. -Proof. reflexivity. Qed. - -Lemma max_0_r : forall n, max n 0 = n. -Proof. destruct n; auto. Qed. - -Lemma min_0_l : forall n, min 0 n = 0. -Proof. reflexivity. Qed. - -Lemma min_0_r : forall n, min n 0 = 0. -Proof. destruct n; auto. Qed. - -(** Compatibilities (consequences of monotonicity) *) - -Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m). -Proof. auto. Qed. - -Lemma succ_min_distr : forall n m, S (min n m) = min (S n) (S m). -Proof. auto. Qed. - -Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m. -Proof. -intros. apply max_monotone. repeat red; auto with arith. -Qed. - -Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p. -Proof. -intros. apply max_monotone with (f:=fun x => x + p). -repeat red; auto with arith. -Qed. - -Lemma plus_min_distr_l : forall n m p, min (p + n) (p + m) = p + min n m. -Proof. -intros. apply min_monotone. repeat red; auto with arith. -Qed. - -Lemma plus_min_distr_r : forall n m p, min (n + p) (m + p) = min n m + p. -Proof. -intros. apply min_monotone with (f:=fun x => x + p). -repeat red; auto with arith. -Qed. - -Hint Resolve - max_l max_r le_max_l le_max_r - min_l min_r le_min_l le_min_r : arith v62. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 1b36f236..ed215f54 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Minus.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as: << Fixpoint minus (n m:nat) : nat := diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 5dd61d67..479138a9 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mult.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Plus. Require Export Minus. Require Export Lt. @@ -177,19 +175,22 @@ Qed. Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. Proof. induction n; intros; simpl in *. - rewrite <- 2! plus_n_O; assumption. + rewrite <- 2 plus_n_O; assumption. auto using plus_lt_compat. Qed. Hint Resolve mult_S_lt_compat_l: arith. +Lemma mult_lt_compat_l : forall n m p, n < m -> 0 < p -> p * n < p * m. +Proof. + intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp). + now apply mult_S_lt_compat_l. +Qed. + Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p. Proof. - intros m n p H H0. - induction p. - elim (lt_irrefl _ H0). - rewrite mult_comm. - replace (n * S p) with (S p * n); auto with arith. + intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp). + rewrite (mult_comm m), (mult_comm n). now apply mult_S_lt_compat_l. Qed. Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p. diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v deleted file mode 100644 index fb4bf233..00000000 --- a/theories/Arith/NatOrderedType.v +++ /dev/null @@ -1,64 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import Lt Peano_dec Compare_dec EqNat - Equalities Orders OrdersTac. - - -(** * DecidableType structure for Peano numbers *) - -Module Nat_as_UBE <: UsualBoolEq. - Definition t := nat. - Definition eq := @eq nat. - Definition eqb := beq_nat. - Definition eqb_eq := beq_nat_true_iff. -End Nat_as_UBE. - -Module Nat_as_DT <: UsualDecidableTypeFull := Make_UDTF Nat_as_UBE. - -(** Note that the last module fulfills by subtyping many other - interfaces, such as [DecidableType] or [EqualityType]. *) - - - -(** * OrderedType structure for Peano numbers *) - -Module Nat_as_OT <: OrderedTypeFull. - Include Nat_as_DT. - Definition lt := lt. - Definition le := le. - Definition compare := nat_compare. - - Instance lt_strorder : StrictOrder lt. - Proof. split; [ exact lt_irrefl | exact lt_trans ]. Qed. - - Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) lt. - Proof. repeat red; intros; subst; auto. Qed. - - Definition le_lteq := le_lt_or_eq_iff. - Definition compare_spec := nat_compare_spec. - -End Nat_as_OT. - -(** Note that [Nat_as_OT] can also be seen as a [UsualOrderedType] - and a [OrderedType] (and also as a [DecidableType]). *) - - - -(** * An [order] tactic for Peano numbers *) - -Module NatOrder := OTF_to_OrderTac Nat_as_OT. -Ltac nat_order := NatOrder.order. - -(** Note that [nat_order] is domain-agnostic: it will not prove - [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) - -Section Test. -Let test : forall x y : nat, x<=y -> y<=x -> x=y. -Proof. nat_order. Qed. -End Test. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 5cceab8b..6eb667c1 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -1,15 +1,14 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Peano_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Decidable. - +Require Eqdep_dec. +Require Import Le Lt. Open Local Scope nat_scope. Implicit Types m n x y : nat. @@ -32,3 +31,22 @@ Hint Resolve O_or_S eq_nat_dec: arith. Theorem dec_eq_nat : forall n m, decidable (n = m). intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith. Defined. + +Definition UIP_nat:= Eqdep_dec.UIP_dec eq_nat_dec. + +Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2. +Proof. +fix 3. +refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh + with le_n => _ |le_S i H => _ end). +refine (fun hh => match hh as h' in _ <= k return forall eq: m = k, + le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with + |le_n => fun eq => _ |le_S j H' => fun eq => _ end eq_refl). +rewrite (UIP_nat _ _ eq eq_refl). reflexivity. +subst m. destruct (Lt.lt_irrefl j H'). +refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop + with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h' + with |le_n => _ |le_S j H2 => fun H' => _ end H). +destruct m. exact I. intros; destruct (Lt.lt_irrefl m H'). +f_equal. apply le_unique. +Qed. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 12f12300..02975d8f 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -1,13 +1,11 @@ -(************************************************************************) + (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Plus.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Properties of addition. [add] is defined in [Init/Peano.v] as: << Fixpoint plus (n m:nat) : nat := @@ -26,17 +24,10 @@ Open Local Scope nat_scope. Implicit Types m n p q : nat. -(** * Zero is neutral *) - -Lemma plus_0_l : forall n, 0 + n = n. -Proof. - reflexivity. -Qed. - -Lemma plus_0_r : forall n, n + 0 = n. -Proof. - intro; symmetry in |- *; apply plus_n_O. -Qed. +(** * Zero is neutral +Deprecated : Already in Init/Peano.v *) +Notation plus_0_l := plus_O_n (only parsing). +Definition plus_0_r n := eq_sym (plus_n_O n). (** * Commutativity *) @@ -49,14 +40,8 @@ Hint Immediate plus_comm: arith v62. (** * Associativity *) -Lemma plus_Snm_nSm : forall n m, S n + m = n + S m. -Proof. - intros. - simpl in |- *. - rewrite (plus_comm n m). - rewrite (plus_comm n (S m)). - trivial with arith. -Qed. +Definition plus_Snm_nSm : forall n m, S n + m = n + S m:= + plus_n_Sm. Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. Proof. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 23419531..b4468dd1 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf_nat.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Well-founded relations and natural numbers *) Require Import Lt. @@ -260,19 +258,6 @@ Qed. Unset Implicit Arguments. -(** [n]th iteration of the function [f] *) - -Fixpoint iter_nat (n:nat) (A:Type) (f:A -> A) (x:A) : A := - match n with - | O => x - | S n' => f (iter_nat n' A f x) - end. - -Theorem iter_nat_plus : - forall (n m:nat) (A:Type) (f:A -> A) (x:A), - iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x). -Proof. - simple induction n; - [ simpl in |- *; auto with arith - | intros; simpl in |- *; apply f_equal with (f := f); apply H ]. -Qed. +Notation iter_nat := @nat_iter (only parsing). +Notation iter_nat_plus := @nat_iter_plus (only parsing). +Notation iter_nat_invariant := @nat_iter_invariant (only parsing). diff --git a/theories/Arith/vo.itarget b/theories/Arith/vo.itarget index c3f29d21..0b6564e1 100644 --- a/theories/Arith/vo.itarget +++ b/theories/Arith/vo.itarget @@ -19,5 +19,3 @@ Mult.vo Peano_dec.vo Plus.vo Wf_nat.vo -NatOrderedType.vo -MinMax.vo |