diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-09 17:44:52 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-09 17:44:52 +0000 |
commit | bf90d39cec401f5daad2eb26c915ceba65e1a5cc (patch) | |
tree | ee1eb266a33d1f9d16af1268136f60ee72c5bc04 /theories/Arith | |
parent | 38dac30c6877122634e7b34ec7cd1b6ab2b67ebb (diff) |
NPeano improved, subsumes NatOrderedType
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12717 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Arith')
-rw-r--r-- | theories/Arith/Max.v | 33 | ||||
-rw-r--r-- | theories/Arith/Min.v | 33 | ||||
-rw-r--r-- | theories/Arith/MinMax.v | 69 | ||||
-rw-r--r-- | theories/Arith/NatOrderedType.v | 64 | ||||
-rw-r--r-- | theories/Arith/vo.itarget | 1 |
5 files changed, 43 insertions, 157 deletions
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 3d7fe9fc2..e49251a71 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -8,34 +8,35 @@ (*i $Id$ i*) -(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *) +(** THIS FILE IS DEPRECATED. Use [NPeano] and [MinMax] instead. *) +Require Import NPeano. Require Export MinMax. Local Open Scope nat_scope. Implicit Types m n p : nat. -Notation max := MinMax.max (only parsing). +Notation max := NPeano.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. +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 *) diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index c52fc0dd0..44060b56c 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -8,34 +8,35 @@ (*i $Id$ i*) -(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *) +(** THIS FILE IS DEPRECATED. Use [NPeano] and [MinMax] instead. *) +Require Import NPeano. Require Export MinMax. Open Local Scope nat_scope. Implicit Types m n p : nat. -Notation min := MinMax.min (only parsing). +Notation min := NPeano.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_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 *) diff --git a/theories/Arith/MinMax.v b/theories/Arith/MinMax.v index 6e86a88c5..9ce43ab8c 100644 --- a/theories/Arith/MinMax.v +++ b/theories/Arith/MinMax.v @@ -6,61 +6,10 @@ (* * 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. +Require Import Orders NPeano. +(** The Definition of maximum and minimum of two natural numbers + is now in NPeano, as well as generic properties. *) (** * Properties specific to the [nat] domain *) @@ -88,26 +37,26 @@ 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. +intros. apply Nat.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). +intros. apply Nat.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. +intros. apply Nat.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). +intros. apply Nat.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. + Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r + Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith v62. diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v deleted file mode 100644 index df5b37e01..000000000 --- a/theories/Arith/NatOrderedType.v +++ /dev/null @@ -1,64 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \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/vo.itarget b/theories/Arith/vo.itarget index c3f29d214..d8bff0ab9 100644 --- a/theories/Arith/vo.itarget +++ b/theories/Arith/vo.itarget @@ -19,5 +19,4 @@ Mult.vo Peano_dec.vo Plus.vo Wf_nat.vo -NatOrderedType.vo MinMax.vo |