diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 76 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 162 | ||||
| -rw-r--r-- | theories/NArith/NArith.v | 2 | ||||
| -rw-r--r-- | theories/NArith/NOrderedType.v | 60 | ||||
| -rw-r--r-- | theories/NArith/Ndec.v | 110 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 108 | ||||
| -rw-r--r-- | theories/NArith/Ndist.v | 20 | ||||
| -rw-r--r-- | theories/NArith/Nminmax.v | 126 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 74 | ||||
| -rw-r--r-- | theories/NArith/POrderedType.v | 60 | ||||
| -rw-r--r-- | theories/NArith/Pminmax.v | 126 | ||||
| -rw-r--r-- | theories/NArith/Pnat.v | 193 | ||||
| -rw-r--r-- | theories/NArith/vo.itarget | 12 |
13 files changed, 808 insertions, 321 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 3752abcc..f0ec2ad6 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinNat.v 11735 2009-01-02 17:22:31Z herbelin $ i*) +(*i $Id$ i*) Require Import BinPos. Unset Boxed Definitions. @@ -45,7 +45,7 @@ Definition Ndouble_plus_one x := (** Operation x -> 2*x *) -Definition Ndouble n := +Definition Ndouble n := match n with | N0 => N0 | Npos p => Npos (xO p) @@ -106,6 +106,15 @@ Definition Nmult n m := Infix "*" := Nmult : N_scope. +(** Boolean Equality *) + +Definition Neqb n m := + match n, m with + | N0, N0 => true + | Npos n, Npos m => Peqb n m + | _,_ => false + end. + (** Order *) Definition Ncompare n m := @@ -130,16 +139,24 @@ Infix ">" := Ngt : N_scope. (** Min and max *) -Definition Nmin (n n' : N) := match Ncompare n n' with +Definition Nmin (n n' : N) := match Ncompare n n' with | Lt | Eq => n | Gt => n' end. -Definition Nmax (n n' : N) := match Ncompare n n' with +Definition Nmax (n n' : N) := match Ncompare n n' with | Lt | Eq => n' | Gt => n end. +(** Decidability of equality. *) + +Definition N_eq_dec : forall n m : N, { n = m } + { n <> m }. +Proof. + decide equality. + apply positive_eq_dec. +Defined. + (** convenient induction principles *) Lemma N_ind_double : @@ -149,7 +166,7 @@ Lemma N_ind_double : (forall a, P a -> P (Ndouble_plus_one a)) -> P a. Proof. intros; elim a. trivial. - simple induction p. intros. + simple induction p. intros. apply (H1 (Npos p0)); trivial. intros; apply (H0 (Npos p0)); trivial. intros; apply (H1 N0); assumption. @@ -162,7 +179,7 @@ Lemma N_rec_double : (forall a, P a -> P (Ndouble_plus_one a)) -> P a. Proof. intros; elim a. trivial. - simple induction p. intros. + simple induction p. intros. apply (H1 (Npos p0)); trivial. intros; apply (H0 (Npos p0)); trivial. intros; apply (H1 N0); assumption. @@ -354,7 +371,16 @@ destruct p; intros Hp H. contradiction Hp; reflexivity. destruct n; destruct m; reflexivity || (try discriminate H). injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity. -Qed. +Qed. + +(** Properties of boolean order. *) + +Lemma Neqb_eq : forall n m, Neqb n m = true <-> n=m. +Proof. +destruct n as [|n], m as [|m]; simpl; split; auto; try discriminate. +intros; f_equal. apply (Peqb_eq n m); auto. +intros. apply (Peqb_eq n m). congruence. +Qed. (** Properties of comparison *) @@ -373,7 +399,7 @@ Qed. Theorem Ncompare_eq_correct : forall n m:N, (n ?= m) = Eq <-> n = m. Proof. -split; intros; +split; intros; [ apply Ncompare_Eq_eq; auto | subst; apply Ncompare_refl ]. Qed. @@ -383,11 +409,30 @@ destruct n; destruct m; simpl; auto. exact (Pcompare_antisym p p0 Eq). Qed. +Lemma Ngt_Nlt : forall n m, n > m -> m < n. +Proof. +unfold Ngt, Nlt; intros n m GT. +rewrite <- Ncompare_antisym, GT; reflexivity. +Qed. + Theorem Nlt_irrefl : forall n : N, ~ n < n. Proof. intro n; unfold Nlt; now rewrite Ncompare_refl. Qed. +Theorem Nlt_trans : forall n m q, n < m -> m < q -> n < q. +Proof. +destruct n; + destruct m; try discriminate; + destruct q; try discriminate; auto. +eapply Plt_trans; eauto. +Qed. + +Theorem Nlt_not_eq : forall n m, n < m -> ~ n = m. +Proof. + intros n m LT EQ. subst m. elim (Nlt_irrefl n); auto. +Qed. + Theorem Ncompare_n_Sm : forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m. Proof. @@ -400,6 +445,21 @@ pose proof (Pcompare_p_Sq p q) as (_,?); assert (p = q <-> Npos p = Npos q); [split; congruence | tauto]. Qed. +Lemma Nle_lteq : forall x y, x <= y <-> x < y \/ x=y. +Proof. +unfold Nle, Nlt; intros. +generalize (Ncompare_eq_correct x y). +destruct (x ?= y); intuition; discriminate. +Qed. + +Lemma Ncompare_spec : forall x y, CompSpec eq Nlt x y (Ncompare x y). +Proof. +intros. +destruct (Ncompare x y) as [ ]_eqn; constructor; auto. +apply Ncompare_Eq_eq; auto. +apply Ngt_Nlt; auto. +Qed. + (** 0 is the least natural number *) Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt. diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index e3293e70..a5f99cc6 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,10 +7,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinPos.v 11033 2008-06-01 22:56:50Z letouzey $ i*) +(*i $Id$ i*) Unset Boxed Definitions. +Declare ML Module "z_syntax_plugin". + (**********************************************************************) (** Binary positive numbers *) @@ -30,15 +33,15 @@ Bind Scope positive_scope with positive. Arguments Scope xO [positive_scope]. Arguments Scope xI [positive_scope]. -(** Postfix notation for positive numbers, allowing to mimic - the position of bits in a big-endian representation. - For instance, we can write 1~1~0 instead of (xO (xI xH)) +(** Postfix notation for positive numbers, allowing to mimic + the position of bits in a big-endian representation. + For instance, we can write 1~1~0 instead of (xO (xI xH)) for the number 6 (which is 110 in binary notation). *) -Notation "p ~ 1" := (xI p) +Notation "p ~ 1" := (xI p) (at level 7, left associativity, format "p '~' '1'") : positive_scope. -Notation "p ~ 0" := (xO p) +Notation "p ~ 0" := (xO p) (at level 7, left associativity, format "p '~' '0'") : positive_scope. Open Local Scope positive_scope. @@ -74,7 +77,7 @@ Fixpoint Pplus (x y:positive) : positive := | 1, q~0 => q~1 | 1, 1 => 1~0 end - + with Pplus_carry (x y:positive) : positive := match x, y with | p~1, q~1 => (Pplus_carry p q)~1 @@ -176,7 +179,7 @@ Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask := | 1, 1 => IsNul | 1, _ => IsNeg end - + with Pminus_mask_carry (x y:positive) {struct y} : positive_mask := match x, y with | p~1, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q) @@ -253,23 +256,41 @@ Notation "x < y < z" := (x < y /\ y < z) : positive_scope. Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope. -Definition Pmin (p p' : positive) := match Pcompare p p' Eq with - | Lt | Eq => p +Definition Pmin (p p' : positive) := match Pcompare p p' Eq with + | Lt | Eq => p | Gt => p' end. -Definition Pmax (p p' : positive) := match Pcompare p p' Eq with - | Lt | Eq => p' +Definition Pmax (p p' : positive) := match Pcompare p p' Eq with + | Lt | Eq => p' | Gt => p end. +(********************************************************************) +(** Boolean equality *) + +Fixpoint Peqb (x y : positive) {struct y} : bool := + match x, y with + | 1, 1 => true + | p~1, q~1 => Peqb p q + | p~0, q~0 => Peqb p q + | _, _ => false + end. + (**********************************************************************) -(** Miscellaneous properties of binary positive numbers *) +(** Decidability of equality on binary positive numbers *) + +Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}. +Proof. + decide equality. +Defined. -Lemma ZL11 : forall p:positive, p = 1 \/ p <> 1. +(* begin hide *) +Corollary ZL11 : forall p:positive, p = 1 \/ p <> 1. Proof. - intros x; case x; intros; (left; reflexivity) || (right; discriminate). + intro; edestruct positive_eq_dec; eauto. Qed. +(* end hide *) (**********************************************************************) (** Properties of successor on binary positive numbers *) @@ -371,14 +392,14 @@ Theorem Pplus_comm : forall p q:positive, p + q = q + p. Proof. induction p; destruct q; simpl; f_equal; auto. rewrite 2 Pplus_carry_spec; f_equal; auto. -Qed. +Qed. (** Permutation of [Pplus] and [Psucc] *) Theorem Pplus_succ_permute_r : forall p q:positive, p + Psucc q = Psucc (p + q). Proof. - induction p; destruct q; simpl; f_equal; + induction p; destruct q; simpl; f_equal; auto using Pplus_one_succ_r; rewrite Pplus_carry_spec; auto. Qed. @@ -423,10 +444,10 @@ Qed. Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q. Proof. intros p q r; revert p q; induction r. - intros [p|p| ] [q|q| ] H; simpl; destr_eq H; - f_equal; auto using Pplus_carry_plus; + intros [p|p| ] [q|q| ] H; simpl; destr_eq H; + f_equal; auto using Pplus_carry_plus; contradict H; auto using Pplus_carry_no_neutral. - intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto; + intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto; contradict H; auto using Pplus_no_neutral. intros p q H; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption. Qed. @@ -456,11 +477,11 @@ Qed. Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r. Proof. induction p. - intros [q|q| ] [r|r| ]; simpl; f_equal; auto; - rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, + intros [q|q| ] [r|r| ]; simpl; f_equal; auto; + rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto. intros [q|q| ] [r|r| ]; simpl; f_equal; auto; - rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, + rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto. intros p r; rewrite <- 2 Pplus_one_succ_l, Pplus_succ_permute_l; auto. Qed. @@ -484,7 +505,7 @@ Lemma Pplus_xO_double_minus_one : forall p q:positive, Pdouble_minus_one (p + q) = p~0 + Pdouble_minus_one q. Proof. induction p as [p IHp| p IHp| ]; destruct q; simpl; - rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI, + rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI, ?Pplus_xI_double_minus_one; try reflexivity. rewrite IHp; auto. rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity. @@ -494,7 +515,7 @@ Qed. Lemma Pplus_diag : forall p:positive, p + p = p~0. Proof. - induction p as [p IHp| p IHp| ]; simpl; + induction p as [p IHp| p IHp| ]; simpl; try rewrite ?Pplus_carry_spec, ?IHp; reflexivity. Qed. @@ -525,10 +546,10 @@ Fixpoint peanoView p : PeanoView p := | p~1 => peanoView_xI p (peanoView p) end. -Definition PeanoView_iter (P:positive->Type) +Definition PeanoView_iter (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p)) := (fix iter p (q:PeanoView p) : P p := - match q in PeanoView p return P p with + match q in PeanoView p return P p with | PeanoOne => a | PeanoSucc _ q => f _ (iter _ q) end). @@ -536,23 +557,23 @@ Definition PeanoView_iter (P:positive->Type) Require Import Eqdep_dec EqdepFacts. Theorem eq_dep_eq_positive : - forall (P:positive->Type) (p:positive) (x y:P p), + forall (P:positive->Type) (p:positive) (x y:P p), eq_dep positive P p x p y -> x = y. Proof. apply eq_dep_eq_dec. decide equality. Qed. -Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'. +Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'. Proof. - intros. + intros. induction q as [ | p q IHq ]. apply eq_dep_eq_positive. cut (1=1). pattern 1 at 1 2 5, q'. destruct q'. trivial. destruct p0; intros; discriminate. trivial. apply eq_dep_eq_positive. - cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. + cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. intro. destruct p; discriminate. intro. unfold p0 in H. apply Psucc_inj in H. generalize q'. rewrite H. intro. @@ -561,12 +582,12 @@ Proof. trivial. Qed. -Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p)) +Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p)) (p:positive) := PeanoView_iter P a f p (peanoView p). -Theorem Prect_succ : forall (P:positive->Type) (a:P 1) - (f:forall p, P p -> P (Psucc p)) (p:positive), +Theorem Prect_succ : forall (P:positive->Type) (a:P 1) + (f:forall p, P p -> P (Psucc p)) (p:positive), Prect P a f (Psucc p) = f _ (Prect P a f p). Proof. intros. @@ -575,7 +596,7 @@ Proof. trivial. Qed. -Theorem Prect_base : forall (P:positive->Type) (a:P 1) +Theorem Prect_base : forall (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p)), Prect P a f 1 = a. Proof. trivial. @@ -713,6 +734,29 @@ Proof. intros [p|p| ] [q|q| ] H; destr_eq H; auto. Qed. +(*********************************************************************) +(** Properties of boolean equality *) + +Theorem Peqb_refl : forall x:positive, Peqb x x = true. +Proof. + induction x; auto. +Qed. + +Theorem Peqb_true_eq : forall x y:positive, Peqb x y = true -> x=y. +Proof. + induction x; destruct y; simpl; intros; try discriminate. + f_equal; auto. + f_equal; auto. + reflexivity. +Qed. + +Theorem Peqb_eq : forall x y : positive, Peqb x y = true <-> x=y. +Proof. + split. apply Peqb_true_eq. + intros; subst; apply Peqb_refl. +Qed. + + (**********************************************************************) (** Properties of comparison on binary positive numbers *) @@ -735,12 +779,19 @@ Qed. Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q. Proof. - induction p; intros [q| q| ] H; simpl in *; auto; + induction p; intros [q| q| ] H; simpl in *; auto; try discriminate H; try (f_equal; auto; fail). destruct (Pcompare_not_Eq p q) as (H',_); elim H'; auto. destruct (Pcompare_not_Eq p q) as (_,H'); elim H'; auto. Qed. +Lemma Pcompare_eq_iff : forall p q:positive, (p ?= q) Eq = Eq <-> p = q. +Proof. + split. + apply Pcompare_Eq_eq. + intros; subst; apply Pcompare_refl. +Qed. + Lemma Pcompare_Gt_Lt : forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt. Proof. @@ -812,7 +863,7 @@ Lemma Pcompare_antisym : forall (p q:positive) (r:comparison), CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r). Proof. - induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto; + induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto; rewrite IHp; auto. Qed. @@ -840,6 +891,15 @@ Proof. symmetry; apply Pcompare_antisym. Qed. +Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq). +Proof. + intros. destruct ((p ?= q) Eq) as [ ]_eqn; constructor. + apply Pcompare_Eq_eq; auto. + auto. + apply ZC1; auto. +Qed. + + (** Comparison and the successor *) Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt. @@ -915,6 +975,14 @@ Proof. destruct (Pcompare_p_Sq n m) as (H',_); destruct (H' H); subst; auto. Qed. +Lemma Ple_lteq : forall p q, p <= q <-> p < q \/ p = q. +Proof. + unfold Ple, Plt. intros. + generalize (Pcompare_eq_iff p q). + destruct ((p ?= q) Eq); intuition; discriminate. +Qed. + + (**********************************************************************) (** Properties of subtraction on binary positive numbers *) @@ -940,14 +1008,14 @@ Qed. Theorem Pminus_mask_carry_spec : forall p q : positive, Pminus_mask_carry p q = Ppred_mask (Pminus_mask p q). Proof. - induction p as [p IHp|p IHp| ]; destruct q; simpl; + induction p as [p IHp|p IHp| ]; destruct q; simpl; try reflexivity; try rewrite IHp; destruct (Pminus_mask p q) as [|[r|r| ]|] || destruct p; auto. Qed. Theorem Pminus_succ_r : forall p q : positive, p - (Psucc q) = Ppred (p - q). Proof. - intros p q; unfold Pminus; + intros p q; unfold Pminus; rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. destruct (Pminus_mask p q) as [|[r|r| ]|]; auto. Qed. @@ -986,11 +1054,11 @@ Proof. induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto. Qed. -Lemma Pminus_mask_IsNeg : forall p q:positive, +Lemma Pminus_mask_IsNeg : forall p q:positive, Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg. Proof. - induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto; - try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H; + induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto; + try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H; specialize IHp with q. destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto. destruct (Pminus_mask p q); simpl; auto; try discriminate. @@ -1019,9 +1087,9 @@ Lemma Pminus_mask_Gt : Pminus_mask p q = IsPos h /\ q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)). Proof. - induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *; + induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *; try discriminate H. - (* p~1, q~1 *) + (* p~1, q~1 *) destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto. repeat split; auto; right. destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]]. @@ -1082,10 +1150,10 @@ Qed. (** Number of digits in a number *) -Fixpoint Psize (p:positive) : nat := - match p with +Fixpoint Psize (p:positive) : nat := + match p with | 1 => S O - | p~1 => S (Psize p) + | p~1 => S (Psize p) | p~0 => S (Psize p) end. diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 6ece00d7..53ba50ff 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: NArith.v 10751 2008-04-04 10:23:35Z herbelin $ *) +(* $Id$ *) (** Library for binary natural numbers *) diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v new file mode 100644 index 00000000..c5dd395b --- /dev/null +++ b/theories/NArith/NOrderedType.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* 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 BinNat Equalities Orders OrdersTac. + +Local Open Scope N_scope. + +(** * DecidableType structure for [N] binary natural numbers *) + +Module N_as_UBE <: UsualBoolEq. + Definition t := N. + Definition eq := @eq N. + Definition eqb := Neqb. + Definition eqb_eq := Neqb_eq. +End N_as_UBE. + +Module N_as_DT <: UsualDecidableTypeFull := Make_UDTF N_as_UBE. + +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) + + + +(** * OrderedType structure for [N] numbers *) + +Module N_as_OT <: OrderedTypeFull. + Include N_as_DT. + Definition lt := Nlt. + Definition le := Nle. + Definition compare := Ncompare. + + Instance lt_strorder : StrictOrder Nlt. + Proof. split; [ exact Nlt_irrefl | exact Nlt_trans ]. Qed. + + Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Nlt. + Proof. repeat red; intros; subst; auto. Qed. + + Definition le_lteq := Nle_lteq. + Definition compare_spec := Ncompare_spec. + +End N_as_OT. + +(** Note that [N_as_OT] can also be seen as a [UsualOrderedType] + and a [OrderedType] (and also as a [DecidableType]). *) + + + +(** * An [order] tactic for [N] numbers *) + +Module NOrder := OTF_to_OrderTac N_as_OT. +Ltac n_order := NOrder.order. + +(** Note that [n_order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) + diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index 5bd9a378..9540aace 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ndec.v 10739 2008-04-01 14:45:20Z herbelin $ i*) +(*i $Id$ i*) Require Import Bool. Require Import Sumbool. @@ -19,73 +19,49 @@ Require Import Ndigits. (** A boolean equality over [N] *) -Fixpoint Peqb (p1 p2:positive) {struct p2} : bool := - match p1, p2 with - | xH, xH => true - | xO p'1, xO p'2 => Peqb p'1 p'2 - | xI p'1, xI p'2 => Peqb p'1 p'2 - | _, _ => false - end. +Notation Peqb := Peqb (only parsing). (* Now in [BinPos] *) +Notation Neqb := Neqb (only parsing). (* Now in [BinNat] *) -Lemma Peqb_correct : forall p, Peqb p p = true. -Proof. -induction p; auto. -Qed. +Notation Peqb_correct := Peqb_refl (only parsing). -Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pcompare p p' Eq = Eq. +Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'. Proof. - induction p; destruct p'; simpl; intros; try discriminate; auto. + intros. now apply (Peqb_eq p p'). Qed. -Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'. +Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pcompare p p' Eq = Eq. Proof. - intros. - apply Pcompare_Eq_eq. - apply Peqb_Pcompare; auto. + intros. now rewrite Pcompare_eq_iff, <- Peqb_eq. Qed. Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true. -Proof. -intros; rewrite <- (Pcompare_Eq_eq _ _ H). -apply Peqb_correct. +Proof. + intros; now rewrite Peqb_eq, <- Pcompare_eq_iff. Qed. -Definition Neqb (a a':N) := - match a, a' with - | N0, N0 => true - | Npos p, Npos p' => Peqb p p' - | _, _ => false - end. - Lemma Neqb_correct : forall n, Neqb n n = true. Proof. - destruct n; trivial. - simpl; apply Peqb_correct. + intros; now rewrite Neqb_eq. Qed. Lemma Neqb_Ncompare : forall n n', Neqb n n' = true -> Ncompare n n' = Eq. Proof. - destruct n; destruct n'; simpl; intros; try discriminate; auto; apply Peqb_Pcompare; auto. + intros; now rewrite Ncompare_eq_correct, <- Neqb_eq. Qed. Lemma Ncompare_Neqb : forall n n', Ncompare n n' = Eq -> Neqb n n' = true. -Proof. -intros; rewrite <- (Ncompare_Eq_eq _ _ H). -apply Neqb_correct. +Proof. + intros; now rewrite Neqb_eq, <- Ncompare_eq_correct. Qed. Lemma Neqb_complete : forall a a', Neqb a a' = true -> a = a'. Proof. - intros. - apply Ncompare_Eq_eq. - apply Neqb_Ncompare; auto. + intros; now rewrite <- Neqb_eq. Qed. Lemma Neqb_comm : forall a a', Neqb a a' = Neqb a' a. Proof. - intros; apply bool_1; split; intros. - rewrite (Neqb_complete _ _ H); apply Neqb_correct. - rewrite (Neqb_complete _ _ H); apply Neqb_correct. + intros; apply eq_true_iff_eq. rewrite 2 Neqb_eq; auto with *. Qed. Lemma Nxor_eq_true : @@ -98,7 +74,8 @@ Lemma Nxor_eq_false : forall a a' p, Nxor a a' = Npos p -> Neqb a a' = false. Proof. intros. elim (sumbool_of_bool (Neqb a a')). intro H0. - rewrite (Neqb_complete a a' H0) in H. rewrite (Nxor_nilpotent a') in H. discriminate H. + rewrite (Neqb_complete a a' H0) in H. + rewrite (Nxor_nilpotent a') in H. discriminate H. trivial. Qed. @@ -107,7 +84,7 @@ Lemma Nodd_not_double : Nodd a -> forall a0, Neqb (Ndouble a0) a = false. Proof. intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0. - rewrite <- (Neqb_complete _ _ H0) in H. + rewrite <- (Neqb_complete _ _ H0) in H. unfold Nodd in H. rewrite (Ndouble_bit0 a0) in H. discriminate H. trivial. @@ -128,7 +105,7 @@ Lemma Neven_not_double_plus_one : Neven a -> forall a0, Neqb (Ndouble_plus_one a0) a = false. Proof. intros. elim (sumbool_of_bool (Neqb (Ndouble_plus_one a0) a)). intro H0. - rewrite <- (Neqb_complete _ _ H0) in H. + rewrite <- (Neqb_complete _ _ H0) in H. unfold Neven in H. rewrite (Ndouble_plus_one_bit0 a0) in H. discriminate H. @@ -149,7 +126,8 @@ Lemma Nbit0_neq : forall a a', Nbit0 a = false -> Nbit0 a' = true -> Neqb a a' = false. Proof. - intros. elim (sumbool_of_bool (Neqb a a')). intro H1. rewrite (Neqb_complete _ _ H1) in H. + intros. elim (sumbool_of_bool (Neqb a a')). intro H1. + rewrite (Neqb_complete _ _ H1) in H. rewrite H in H0. discriminate H0. trivial. Qed. @@ -166,7 +144,8 @@ Lemma Ndiv2_neq : Neqb (Ndiv2 a) (Ndiv2 a') = false -> Neqb a a' = false. Proof. intros. elim (sumbool_of_bool (Neqb a a')). intro H0. - rewrite (Neqb_complete _ _ H0) in H. rewrite (Neqb_correct (Ndiv2 a')) in H. discriminate H. + rewrite (Neqb_complete _ _ H0) in H. + rewrite (Neqb_correct (Ndiv2 a')) in H. discriminate H. trivial. Qed. @@ -354,6 +333,35 @@ Proof. trivial. Qed. +(* Nleb and Ncompare *) + +(* NB: No need to prove that Nleb a b = true <-> Ncompare a b <> Gt, + this statement is in fact Nleb_Nle! *) + +Lemma Nltb_Ncompare : forall a b, + Nleb a b = false <-> Ncompare a b = Gt. +Proof. + intros. + assert (IFF : forall x:bool, x = false <-> ~ x = true) + by (destruct x; intuition). + rewrite IFF, Nleb_Nle; unfold Nle. + destruct (Ncompare a b); split; intro H; auto; + elim H; discriminate. +Qed. + +Lemma Ncompare_Gt_Nltb : forall a b, + Ncompare a b = Gt -> Nleb a b = false. +Proof. + intros; apply <- Nltb_Ncompare; auto. +Qed. + +Lemma Ncompare_Lt_Nltb : forall a b, + Ncompare a b = Lt -> Nleb b a = false. +Proof. + intros a b H. + rewrite Nltb_Ncompare, <- Ncompare_antisym, H; auto. +Qed. + (* An alternate [min] function over [N] *) Definition Nmin' (a b:N) := if Nleb a b then a else b. @@ -362,8 +370,8 @@ Lemma Nmin_Nmin' : forall a b, Nmin a b = Nmin' a b. Proof. unfold Nmin, Nmin', Nleb; intros. rewrite nat_of_Ncompare. - generalize (leb_compare (nat_of_N a) (nat_of_N b)); - destruct (nat_compare (nat_of_N a) (nat_of_N b)); + generalize (leb_compare (nat_of_N a) (nat_of_N b)); + destruct (nat_compare (nat_of_N a) (nat_of_N b)); destruct (leb (nat_of_N a) (nat_of_N b)); intuition. lapply H1; intros; discriminate. lapply H1; intros; discriminate. @@ -392,7 +400,7 @@ Qed. Lemma Nmin_le_3 : forall a b c, Nleb a (Nmin b c) = true -> Nleb a b = true. Proof. - intros; rewrite Nmin_Nmin' in *. + intros; rewrite Nmin_Nmin' in *. unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. assumption. intro H0. rewrite H0 in H. apply Nltb_leb_weak. apply Nleb_ltb_trans with (b := c); assumption. @@ -401,7 +409,7 @@ Qed. Lemma Nmin_le_4 : forall a b c, Nleb a (Nmin b c) = true -> Nleb a c = true. Proof. - intros; rewrite Nmin_Nmin' in *. + intros; rewrite Nmin_Nmin' in *. unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. apply Nleb_trans with (b := b); assumption. intro H0. rewrite H0 in H. assumption. @@ -418,7 +426,7 @@ Qed. Lemma Nmin_lt_3 : forall a b c, Nleb (Nmin b c) a = false -> Nleb b a = false. Proof. - intros; rewrite Nmin_Nmin' in *. + intros; rewrite Nmin_Nmin' in *. unfold Nmin' in *. intros. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. assumption. intro H0. rewrite H0 in H. apply Nltb_trans with (b := c); assumption. @@ -427,7 +435,7 @@ Qed. Lemma Nmin_lt_4 : forall a b c, Nleb (Nmin b c) a = false -> Nleb c a = false. Proof. - intros; rewrite Nmin_Nmin' in *. + intros; rewrite Nmin_Nmin' in *. unfold Nmin' in *. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H. apply Nltb_leb_trans with (b := b); assumption. intro H0. rewrite H0 in H. assumption. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index fb32274e..b6c18e9b 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ndigits.v 11735 2009-01-02 17:22:31Z herbelin $ i*) +(*i $Id$ i*) Require Import Bool. Require Import Bvector. @@ -17,7 +17,7 @@ Require Import BinNat. (** [xor] *) -Fixpoint Pxor (p1 p2:positive) {struct p1} : N := +Fixpoint Pxor (p1 p2:positive) : N := match p1, p2 with | xH, xH => N0 | xH, xO p2 => Npos (xI p2) @@ -27,7 +27,7 @@ Fixpoint Pxor (p1 p2:positive) {struct p1} : N := | xO p1, xI p2 => Ndouble_plus_one (Pxor p1 p2) | xI p1, xH => Npos (xO p1) | xI p1, xO p2 => Ndouble_plus_one (Pxor p1 p2) - | xI p1, xI p2 => Ndouble (Pxor p1 p2) + | xI p1, xI p2 => Ndouble (Pxor p1 p2) end. Definition Nxor (n n':N) := @@ -65,7 +65,7 @@ Proof. simpl. rewrite IHp; reflexivity. Qed. -(** Checking whether a particular bit is set on not *) +(** Checking whether a particular bit is set on not *) Fixpoint Pbit (p:positive) : nat -> bool := match p with @@ -134,13 +134,13 @@ Qed. (** End of auxilliary results *) -(** This part is aimed at proving that if two numbers produce +(** This part is aimed at proving that if two numbers produce the same stream of bits, then they are equal. *) Lemma Nbit_faithful_1 : forall a:N, eqf (Nbit N0) (Nbit a) -> N0 = a. Proof. destruct a. trivial. - induction p as [p IHp| p IHp| ]; intro H. + induction p as [p IHp| p IHp| ]; intro H. absurd (N0 = Npos p). discriminate. exact (IHp (fun n => H (S n))). absurd (N0 = Npos p). discriminate. @@ -196,7 +196,7 @@ Proof. assert (Npos p = Npos p') by exact (IHp (Npos p') H0). inversion H1. reflexivity. assumption. - intros. apply Nbit_faithful_3. intros. + intros. apply Nbit_faithful_3. intros. assert (Npos p = Npos p') by exact (IHp (Npos p') H0). inversion H1. reflexivity. assumption. @@ -257,7 +257,7 @@ Proof. generalize (fun p1 p2 => H (Npos p1) (Npos p2)); clear H; intro H. unfold xorf in *. destruct a as [|p]. simpl Nbit; rewrite false_xorb. reflexivity. - destruct a' as [|p0]. + destruct a' as [|p0]. simpl Nbit; rewrite xorb_false. reflexivity. destruct p. destruct p0; simpl Nbit in *. rewrite <- H; simpl; case (Pxor p p0); trivial. @@ -273,13 +273,13 @@ Qed. Lemma Nxor_semantics : forall a a':N, eqf (Nbit (Nxor a a')) (xorf (Nbit a) (Nbit a')). Proof. - unfold eqf. intros; generalize a, a'. induction n. + unfold eqf. intros; generalize a, a'. induction n. apply Nxor_sem_5. apply Nxor_sem_6; assumption. Qed. -(** Consequences: +(** Consequences: - only equal numbers lead to a null xor - - xor is associative + - xor is associative *) Lemma Nxor_eq : forall a a':N, Nxor a a' = N0 -> a = a'. @@ -306,7 +306,7 @@ Proof. apply eqf_sym, Nxor_semantics. Qed. -(** Checking whether a number is odd, i.e. +(** Checking whether a number is odd, i.e. if its lower bit is set. *) Definition Nbit0 (n:N) := @@ -380,8 +380,8 @@ Lemma Nneg_bit0 : forall a a':N, Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a'). Proof. - intros. - rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false. + intros. + rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false. reflexivity. Qed. @@ -402,14 +402,14 @@ Lemma Nsame_bit0 : forall (a a':N) (p:positive), Nxor a a' = Npos (xO p) -> Nbit0 a = Nbit0 a'. Proof. - intros. rewrite <- (xorb_false (Nbit0 a)). + intros. rewrite <- (xorb_false (Nbit0 a)). assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity. rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. reflexivity. Qed. (** a lexicographic order on bits, starting from the lowest bit *) -Fixpoint Nless_aux (a a':N) (p:positive) {struct p} : bool := +Fixpoint Nless_aux (a a':N) (p:positive) : bool := match p with | xO p' => Nless_aux (Ndiv2 a) (Ndiv2 a') p' | _ => andb (negb (Nbit0 a)) (Nbit0 a') @@ -430,7 +430,7 @@ Proof. assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1. simpl. rewrite H, H0. reflexivity. - assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). + assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2. Qed. @@ -443,7 +443,7 @@ Proof. assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1. simpl. rewrite H, H0. reflexivity. - assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). + assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2. Qed. @@ -496,14 +496,14 @@ Qed. Lemma N0_less_1 : forall a, Nless N0 a = true -> {p : positive | a = Npos p}. Proof. - destruct a. intros. discriminate. + destruct a. discriminate. intros. exists p. reflexivity. Qed. Lemma N0_less_2 : forall a, Nless N0 a = false -> a = N0. Proof. induction a as [|p]; intro H. trivial. - elimtype False. induction p as [|p IHp|]; discriminate || simpl; auto using IHp. + exfalso. induction p as [|p IHp|]; discriminate || simpl; auto using IHp. Qed. Lemma Nless_trans : @@ -534,7 +534,7 @@ Proof. rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H. rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0). Qed. - + Lemma Nless_total : forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. Proof. @@ -558,7 +558,7 @@ Qed. (** Number of digits in a number *) -Definition Nsize (n:N) : nat := match n with +Definition Nsize (n:N) : nat := match n with | N0 => 0%nat | Npos p => Psize p end. @@ -566,35 +566,35 @@ Definition Nsize (n:N) : nat := match n with (** conversions between N and bit vectors. *) -Fixpoint P2Bv (p:positive) : Bvector (Psize p) := - match p return Bvector (Psize p) with +Fixpoint P2Bv (p:positive) : Bvector (Psize p) := + match p return Bvector (Psize p) with | xH => Bvect_true 1%nat | xO p => Bcons false (Psize p) (P2Bv p) | xI p => Bcons true (Psize p) (P2Bv p) end. Definition N2Bv (n:N) : Bvector (Nsize n) := - match n as n0 return Bvector (Nsize n0) with + match n as n0 return Bvector (Nsize n0) with | N0 => Bnil | Npos p => P2Bv p end. -Fixpoint Bv2N (n:nat)(bv:Bvector n) {struct bv} : N := - match bv with +Fixpoint Bv2N (n:nat)(bv:Bvector n) : N := + match bv with | Vnil => N0 | Vcons false n bv => Ndouble (Bv2N n bv) - | Vcons true n bv => Ndouble_plus_one (Bv2N n bv) + | Vcons true n bv => Ndouble_plus_one (Bv2N n bv) end. Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. -Proof. +Proof. destruct n. simpl; auto. induction p; simpl in *; auto; rewrite IHp; simpl; auto. Qed. -(** The opposite composition is not so simple: if the considered - bit vector has some zeros on its right, they will disappear during +(** The opposite composition is not so simple: if the considered + bit vector has some zeros on its right, they will disappear during the return [Bv2N] translation: *) Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n. @@ -603,16 +603,16 @@ induction n; intros. rewrite (V0_eq _ bv); simpl; auto. rewrite (VSn_eq _ _ bv); simpl. specialize IHn with (Vtail _ _ bv). -destruct (Vhead _ _ bv); - destruct (Bv2N n (Vtail bool n bv)); +destruct (Vhead _ _ bv); + destruct (Bv2N n (Vtail bool n bv)); simpl; auto with arith. Qed. (** In the previous lemma, we can only replace the inequality by an equality whenever the highest bit is non-null. *) -Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)), - Bsign _ bv = true <-> +Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)), + Bsign _ bv = true <-> Nsize (Bv2N _ bv) = (S n). Proof. induction n; intro. @@ -621,18 +621,18 @@ rewrite (V0_eq _ (Vtail _ _ bv)); simpl. destruct (Vhead _ _ bv); simpl; intuition; try discriminate. rewrite (VSn_eq _ _ bv); simpl. generalize (IHn (Vtail _ _ bv)); clear IHn. -destruct (Vhead _ _ bv); - destruct (Bv2N (S n) (Vtail bool (S n) bv)); +destruct (Vhead _ _ bv); + destruct (Bv2N (S n) (Vtail bool (S n) bv)); simpl; intuition; try discriminate. Qed. -(** To state nonetheless a second result about composition of - conversions, we define a conversion on a given number of bits : *) +(** To state nonetheless a second result about composition of + conversions, we define a conversion on a given number of bits : *) -Fixpoint N2Bv_gen (n:nat)(a:N) { struct n } : Bvector n := - match n return Bvector n with +Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n := + match n return Bvector n with | 0 => Bnil - | S n => match a with + | S n => match a with | N0 => Bvect_false (S n) | Npos xH => Bcons true _ (Bvect_false n) | Npos (xO p) => Bcons false _ (N2Bv_gen n (Npos p)) @@ -649,10 +649,10 @@ auto. induction p; simpl; intros; auto; congruence. Qed. -(** In fact, if [k] is large enough, [N2Bv_gen k a] contains all digits of +(** In fact, if [k] is large enough, [N2Bv_gen k a] contains all digits of [a] plus some zeros. *) -Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat), +Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat), N2Bv_gen (Nsize a + k) a = Vextend _ _ _ (N2Bv a) (Bvect_false k). Proof. destruct a; simpl. @@ -662,7 +662,7 @@ Qed. (** Here comes now the second composition result. *) -Lemma N2Bv_Bv2N : forall n (bv:Bvector n), +Lemma N2Bv_Bv2N : forall n (bv:Bvector n), N2Bv_gen n (Bv2N n bv) = bv. Proof. induction n; intros. @@ -670,36 +670,36 @@ rewrite (V0_eq _ bv); simpl; auto. rewrite (VSn_eq _ _ bv); simpl. generalize (IHn (Vtail _ _ bv)); clear IHn. unfold Bcons. -destruct (Bv2N _ (Vtail _ _ bv)); - destruct (Vhead _ _ bv); intro H; rewrite <- H; simpl; trivial; +destruct (Bv2N _ (Vtail _ _ bv)); + destruct (Vhead _ _ bv); intro H; rewrite <- H; simpl; trivial; induction n; simpl; auto. Qed. (** accessing some precise bits. *) -Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), +Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), Nbit0 (Bv2N _ bv) = Blow _ bv. Proof. intros. unfold Blow. rewrite (VSn_eq _ _ bv) at 1. simpl. -destruct (Bv2N n (Vtail bool n bv)); simpl; +destruct (Bv2N n (Vtail bool n bv)); simpl; destruct (Vhead bool n bv); auto. Qed. Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool. Proof. - induction 1. + induction bv in p |- *. intros. - elimtype False; inversion H. + exfalso; inversion H. intros. destruct p. exact a. apply (IHbv p); auto with arith. Defined. -Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n), +Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n), Bnth _ bv p H = Nbit (Bv2N _ bv) p. Proof. induction bv; intros. @@ -726,7 +726,7 @@ Qed. (** Xor is the same in the two worlds. *) -Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), +Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv'). Proof. induction n. @@ -735,7 +735,7 @@ rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto. intros. rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto. rewrite IHn. -destruct (Vhead bool n bv); destruct (Vhead bool n bv'); +destruct (Vhead bool n bv); destruct (Vhead bool n bv'); destruct (Bv2N n (Vtail bool n bv)); destruct (Bv2N n (Vtail bool n bv')); simpl; auto. Qed. diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index af90b8e7..92559ff6 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ndist.v 10739 2008-04-01 14:45:20Z herbelin $ i*) +(*i $Id$ i*) Require Import Arith. Require Import Min. @@ -34,7 +34,7 @@ Definition Nplength (a:N) := Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0. Proof. - simple induction a; trivial. + simple induction a; trivial. unfold Nplength in |- *; intros; discriminate H. Qed. @@ -42,7 +42,7 @@ Lemma Nplength_zeros : forall (a:N) (n:nat), Nplength a = ni n -> forall k:nat, k < n -> Nbit a k = false. Proof. - simple induction a; trivial. + simple induction a; trivial. simple induction p. simple induction n. intros. inversion H1. simple induction k. simpl in H1. discriminate H1. intros. simpl in H1. discriminate H1. @@ -116,11 +116,11 @@ Qed. Lemma ni_min_assoc : forall d d' d'':natinf, ni_min (ni_min d d') d'' = ni_min d (ni_min d' d''). Proof. - simple induction d; trivial. simple induction d'; trivial. + simple induction d; trivial. simple induction d'; trivial. simple induction d''; trivial. unfold ni_min in |- *. intro. cut (min (min n n0) n1 = min n (min n0 n1)). intro. rewrite H. reflexivity. - generalize n0 n1. elim n; trivial. + generalize n0 n1. elim n; trivial. simple induction n3; trivial. simple induction n5; trivial. intros. simpl in |- *. auto. Qed. @@ -250,10 +250,10 @@ Proof. Qed. -(** We define an ultrametric distance between [N] numbers: - $d(a,a')=1/2^pd(a,a')$, - where $pd(a,a')$ is the number of identical bits at the beginning - of $a$ and $a'$ (infinity if $a=a'$). +(** We define an ultrametric distance between [N] numbers: + $d(a,a')=1/2^pd(a,a')$, + where $pd(a,a')$ is the number of identical bits at the beginning + of $a$ and $a'$ (infinity if $a=a'$). Instead of working with $d$, we work with $pd$, namely [Npdist]: *) @@ -286,7 +286,7 @@ Qed. This follows from the fact that $a ~Ra~|a| = 1/2^{\texttt{Nplength}}(a))$ is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$, or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that - min $(\texttt{Nplength}(a), \texttt{Nplength}(b)) \leq + min $(\texttt{Nplength}(a), \texttt{Nplength}(b)) \leq \texttt{Nplength} (a~\texttt{xor}~ b)$ (lemma [Nplength_ultra]). *) diff --git a/theories/NArith/Nminmax.v b/theories/NArith/Nminmax.v new file mode 100644 index 00000000..475b4dfb --- /dev/null +++ b/theories/NArith/Nminmax.v @@ -0,0 +1,126 @@ +(************************************************************************) +(* 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 Orders BinNat Nnat NOrderedType GenericMinMax. + +(** * Maximum and Minimum of two [N] numbers *) + +Local Open Scope N_scope. + +(** The functions [Nmax] and [Nmin] implement indeed + a maximum and a minimum *) + +Lemma Nmax_l : forall x y, y<=x -> Nmax x y = x. +Proof. + unfold Nle, Nmax. intros x y. + generalize (Ncompare_eq_correct x y). rewrite <- (Ncompare_antisym x y). + destruct (x ?= y); intuition. +Qed. + +Lemma Nmax_r : forall x y, x<=y -> Nmax x y = y. +Proof. + unfold Nle, Nmax. intros x y. destruct (x ?= y); intuition. +Qed. + +Lemma Nmin_l : forall x y, x<=y -> Nmin x y = x. +Proof. + unfold Nle, Nmin. intros x y. destruct (x ?= y); intuition. +Qed. + +Lemma Nmin_r : forall x y, y<=x -> Nmin x y = y. +Proof. + unfold Nle, Nmin. intros x y. + generalize (Ncompare_eq_correct x y). rewrite <- (Ncompare_antisym x y). + destruct (x ?= y); intuition. +Qed. + +Module NHasMinMax <: HasMinMax N_as_OT. + Definition max := Nmax. + Definition min := Nmin. + Definition max_l := Nmax_l. + Definition max_r := Nmax_r. + Definition min_l := Nmin_l. + Definition min_r := Nmin_r. +End NHasMinMax. + +Module N. + +(** We obtain hence all the generic properties of max and min. *) + +Include UsualMinMaxProperties N_as_OT NHasMinMax. + +(** * Properties specific to the [positive] domain *) + +(** Simplifications *) + +Lemma max_0_l : forall n, Nmax 0 n = n. +Proof. + intros. unfold Nmax. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). + destruct (n ?= 0); intuition. +Qed. + +Lemma max_0_r : forall n, Nmax n 0 = n. +Proof. intros. rewrite N.max_comm. apply max_0_l. Qed. + +Lemma min_0_l : forall n, Nmin 0 n = 0. +Proof. + intros. unfold Nmin. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). + destruct (n ?= 0); intuition. +Qed. + +Lemma min_0_r : forall n, Nmin n 0 = 0. +Proof. intros. rewrite N.min_comm. apply min_0_l. Qed. + +(** Compatibilities (consequences of monotonicity) *) + +Lemma succ_max_distr : + forall n m, Nsucc (Nmax n m) = Nmax (Nsucc n) (Nsucc m). +Proof. + intros. symmetry. apply max_monotone. + intros x x'. unfold Nle. + rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. + simpl; auto. +Qed. + +Lemma succ_min_distr : forall n m, Nsucc (Nmin n m) = Nmin (Nsucc n) (Nsucc m). +Proof. + intros. symmetry. apply min_monotone. + intros x x'. unfold Nle. + rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. + simpl; auto. +Qed. + +Lemma plus_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m. +Proof. + intros. apply max_monotone. + intros x x'. unfold Nle. + rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. + rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. +Qed. + +Lemma plus_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p. +Proof. + intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p). + apply plus_max_distr_l. +Qed. + +Lemma plus_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m. +Proof. + intros. apply min_monotone. + intros x x'. unfold Nle. + rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. + rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. +Qed. + +Lemma plus_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p. +Proof. + intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p). + apply plus_min_distr_l. +Qed. + +End N.
\ No newline at end of file diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index bc3711ee..0016d035 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Nnat.v 10739 2008-04-01 14:45:20Z herbelin $ i*) +(*i $Id$ i*) Require Import Arith_base. Require Import Compare_dec. @@ -39,7 +39,7 @@ Definition N_of_nat (n:nat) := Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a. Proof. destruct a as [| p]. reflexivity. - simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *. + simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *. rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H. rewrite nat_of_P_inj with (1 := H). reflexivity. Qed. @@ -66,14 +66,14 @@ Proof. apply N_of_nat_of_N. Qed. -Lemma nat_of_Ndouble_plus_one : +Lemma nat_of_Ndouble_plus_one : forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)). Proof. destruct a; simpl nat_of_N; auto. apply nat_of_P_xI. Qed. -Lemma N_of_double_plus_one : +Lemma N_of_double_plus_one : forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n). Proof. intros. @@ -97,14 +97,14 @@ Proof. apply N_of_nat_of_N. Qed. -Lemma nat_of_Nplus : +Lemma nat_of_Nplus : forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a'). Proof. destruct a; destruct a'; simpl; auto. apply nat_of_P_plus_morphism. Qed. -Lemma N_of_plus : +Lemma N_of_plus : forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n'). Proof. intros. @@ -138,14 +138,14 @@ Proof. apply N_of_nat_of_N. Qed. -Lemma nat_of_Nmult : +Lemma nat_of_Nmult : forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a'). Proof. destruct a; destruct a'; simpl; auto. apply nat_of_P_mult_morphism. Qed. -Lemma N_of_mult : +Lemma N_of_mult : forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n'). Proof. intros. @@ -155,7 +155,7 @@ Proof. apply N_of_nat_of_N. Qed. -Lemma nat_of_Ndiv2 : +Lemma nat_of_Ndiv2 : forall a, nat_of_N (Ndiv2 a) = div2 (nat_of_N a). Proof. destruct a; simpl in *; auto. @@ -164,9 +164,9 @@ Proof. rewrite div2_double_plus_one; auto. rewrite nat_of_P_xO. rewrite div2_double; auto. -Qed. +Qed. -Lemma N_of_div2 : +Lemma N_of_div2 : forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n). Proof. intros. @@ -175,29 +175,19 @@ Proof. apply N_of_nat_of_N. Qed. -Lemma nat_of_Ncompare : +Lemma nat_of_Ncompare : forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a'). Proof. destruct a; destruct a'; simpl. - compute; auto. - generalize (lt_O_nat_of_P p). - unfold nat_compare. - destruct (lt_eq_lt_dec 0 (nat_of_P p)) as [[H|H]|H]; auto. - rewrite <- H; inversion 1. - intros; generalize (lt_trans _ _ _ H0 H); inversion 1. - generalize (lt_O_nat_of_P p). - unfold nat_compare. - destruct (lt_eq_lt_dec (nat_of_P p) 0) as [[H|H]|H]; auto. - intros; generalize (lt_trans _ _ _ H0 H); inversion 1. - rewrite H; inversion 1. - unfold nat_compare. - destruct (lt_eq_lt_dec (nat_of_P p) (nat_of_P p0)) as [[H|H]|H]; auto. - apply nat_of_P_lt_Lt_compare_complement_morphism; auto. - rewrite (nat_of_P_inj _ _ H); apply Pcompare_refl. - apply nat_of_P_gt_Gt_compare_complement_morphism; auto. -Qed. - -Lemma N_of_nat_compare : + reflexivity. + assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. + destruct nat_of_P; [inversion NZ|auto]. + assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. + destruct nat_of_P; [inversion NZ|auto]. + apply nat_of_P_compare_morphism. +Qed. + +Lemma N_of_nat_compare : forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n'). Proof. intros. @@ -210,8 +200,8 @@ Lemma nat_of_Nmin : forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). Proof. intros; unfold Nmin; rewrite nat_of_Ncompare. - unfold nat_compare. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + rewrite nat_compare_equiv; unfold nat_compare_alt. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; simpl; intros; symmetry; auto with arith. apply min_l; rewrite e; auto with arith. Qed. @@ -230,8 +220,8 @@ Lemma nat_of_Nmax : forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a'). Proof. intros; unfold Nmax; rewrite nat_of_Ncompare. - unfold nat_compare. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + rewrite nat_compare_equiv; unfold nat_compare_alt. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; simpl; intros; symmetry; auto with arith. apply max_r; rewrite e; auto with arith. Qed. @@ -331,17 +321,17 @@ Qed. Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n. Proof. destruct n; simpl; auto. -Qed. +Qed. Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p. Proof. destruct p; simpl; auto. -Qed. +Qed. Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z. Proof. destruct z; simpl; auto. -Qed. +Qed. Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z. Proof. @@ -358,22 +348,22 @@ Proof. destruct n; destruct m; auto. Qed. -Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). +Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). Proof. intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus. Qed. -Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). +Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). Proof. intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S. Qed. -Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). +Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). Proof. intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min. Qed. -Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). +Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). Proof. intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max. Qed. diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v new file mode 100644 index 00000000..9c0f8261 --- /dev/null +++ b/theories/NArith/POrderedType.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* 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 BinPos Equalities Orders OrdersTac. + +Local Open Scope positive_scope. + +(** * DecidableType structure for [positive] numbers *) + +Module Positive_as_UBE <: UsualBoolEq. + Definition t := positive. + Definition eq := @eq positive. + Definition eqb := Peqb. + Definition eqb_eq := Peqb_eq. +End Positive_as_UBE. + +Module Positive_as_DT <: UsualDecidableTypeFull + := Make_UDTF Positive_as_UBE. + +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) + + + +(** * OrderedType structure for [positive] numbers *) + +Module Positive_as_OT <: OrderedTypeFull. + Include Positive_as_DT. + Definition lt := Plt. + Definition le := Ple. + Definition compare p q := Pcompare p q Eq. + + Instance lt_strorder : StrictOrder Plt. + Proof. split; [ exact Plt_irrefl | exact Plt_trans ]. Qed. + + Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Plt. + Proof. repeat red; intros; subst; auto. Qed. + + Definition le_lteq := Ple_lteq. + Definition compare_spec := Pcompare_spec. + +End Positive_as_OT. + +(** Note that [Positive_as_OT] can also be seen as a [UsualOrderedType] + and a [OrderedType] (and also as a [DecidableType]). *) + + + +(** * An [order] tactic for positive numbers *) + +Module PositiveOrder := OTF_to_OrderTac Positive_as_OT. +Ltac p_order := PositiveOrder.order. + +(** Note that [p_order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) diff --git a/theories/NArith/Pminmax.v b/theories/NArith/Pminmax.v new file mode 100644 index 00000000..4cc48af6 --- /dev/null +++ b/theories/NArith/Pminmax.v @@ -0,0 +1,126 @@ +(************************************************************************) +(* 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 Orders BinPos Pnat POrderedType GenericMinMax. + +(** * Maximum and Minimum of two positive numbers *) + +Local Open Scope positive_scope. + +(** The functions [Pmax] and [Pmin] implement indeed + a maximum and a minimum *) + +Lemma Pmax_l : forall x y, y<=x -> Pmax x y = x. +Proof. + unfold Ple, Pmax. intros x y. + rewrite (ZC4 y x). generalize (Pcompare_eq_iff x y). + destruct ((x ?= y) Eq); intuition. +Qed. + +Lemma Pmax_r : forall x y, x<=y -> Pmax x y = y. +Proof. + unfold Ple, Pmax. intros x y. destruct ((x ?= y) Eq); intuition. +Qed. + +Lemma Pmin_l : forall x y, x<=y -> Pmin x y = x. +Proof. + unfold Ple, Pmin. intros x y. destruct ((x ?= y) Eq); intuition. +Qed. + +Lemma Pmin_r : forall x y, y<=x -> Pmin x y = y. +Proof. + unfold Ple, Pmin. intros x y. + rewrite (ZC4 y x). generalize (Pcompare_eq_iff x y). + destruct ((x ?= y) Eq); intuition. +Qed. + +Module PositiveHasMinMax <: HasMinMax Positive_as_OT. + Definition max := Pmax. + Definition min := Pmin. + Definition max_l := Pmax_l. + Definition max_r := Pmax_r. + Definition min_l := Pmin_l. + Definition min_r := Pmin_r. +End PositiveHasMinMax. + + +Module P. +(** We obtain hence all the generic properties of max and min. *) + +Include UsualMinMaxProperties Positive_as_OT PositiveHasMinMax. + +(** * Properties specific to the [positive] domain *) + +(** Simplifications *) + +Lemma max_1_l : forall n, Pmax 1 n = n. +Proof. + intros. unfold Pmax. rewrite ZC4. generalize (Pcompare_1 n). + destruct (n ?= 1); intuition. +Qed. + +Lemma max_1_r : forall n, Pmax n 1 = n. +Proof. intros. rewrite P.max_comm. apply max_1_l. Qed. + +Lemma min_1_l : forall n, Pmin 1 n = 1. +Proof. + intros. unfold Pmin. rewrite ZC4. generalize (Pcompare_1 n). + destruct (n ?= 1); intuition. +Qed. + +Lemma min_1_r : forall n, Pmin n 1 = 1. +Proof. intros. rewrite P.min_comm. apply min_1_l. Qed. + +(** Compatibilities (consequences of monotonicity) *) + +Lemma succ_max_distr : + forall n m, Psucc (Pmax n m) = Pmax (Psucc n) (Psucc m). +Proof. + intros. symmetry. apply max_monotone. + intros x x'. unfold Ple. + rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. + simpl; auto. +Qed. + +Lemma succ_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m). +Proof. + intros. symmetry. apply min_monotone. + intros x x'. unfold Ple. + rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. + simpl; auto. +Qed. + +Lemma plus_max_distr_l : forall n m p, Pmax (p + n) (p + m) = p + Pmax n m. +Proof. + intros. apply max_monotone. + intros x x'. unfold Ple. + rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. + rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. +Qed. + +Lemma plus_max_distr_r : forall n m p, Pmax (n + p) (m + p) = Pmax n m + p. +Proof. + intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p). + apply plus_max_distr_l. +Qed. + +Lemma plus_min_distr_l : forall n m p, Pmin (p + n) (p + m) = p + Pmin n m. +Proof. + intros. apply min_monotone. + intros x x'. unfold Ple. + rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. + rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. +Qed. + +Lemma plus_min_distr_r : forall n m p, Pmin (n + p) (m + p) = Pmin n m + p. +Proof. + intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p). + apply plus_min_distr_l. +Qed. + +End P.
\ No newline at end of file diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index 2c007398..0891dea2 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,12 +7,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Pnat.v 9883 2007-06-07 18:44:59Z letouzey $ i*) +(*i $Id$ i*) Require Import BinPos. (**********************************************************************) -(** Properties of the injection from binary positive numbers to Peano +(** Properties of the injection from binary positive numbers to Peano natural numbers *) (** Original development by Pierre Crégut, CNET, Lannion, France *) @@ -22,6 +23,10 @@ Require Import Gt. Require Import Plus. Require Import Mult. Require Import Minus. +Require Import Compare_dec. + +Local Open Scope positive_scope. +Local Open Scope nat_scope. (** [nat_of_P] is a morphism for addition *) @@ -46,7 +51,7 @@ Proof. intro x; induction x as [p IHp| p IHp| ]; intro y; [ destruct y as [p0| p0| ] | destruct y as [p0| p0| ] - | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; + | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; intro m; [ rewrite IHp; rewrite plus_assoc; trivial with arith | rewrite IHp; rewrite plus_assoc; trivial with arith @@ -71,11 +76,11 @@ intro x; induction x as [p IHp| p IHp| ]; intro y; | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; [ intros m; rewrite Pmult_nat_plus_carry_morphism; rewrite IHp; rewrite plus_assoc_reverse; rewrite plus_assoc_reverse; - rewrite (plus_permute m (Pmult_nat p (m + m))); + rewrite (plus_permute m (Pmult_nat p (m + m))); trivial with arith | intros m; rewrite IHp; apply plus_assoc | intros m; rewrite Pmult_nat_succ_morphism; - rewrite (plus_comm (m + Pmult_nat p (m + m))); + rewrite (plus_comm (m + Pmult_nat p (m + m))); apply plus_assoc_reverse | intros m; rewrite IHp; apply plus_permute | intros m; rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ]. @@ -106,7 +111,7 @@ Proof. intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism; trivial. Qed. - + (** [nat_of_P] is a morphism for multiplication *) Theorem nat_of_P_mult_morphism : @@ -129,11 +134,11 @@ Proof. intro y; induction y as [p H| p H| ]; [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *; simpl in |- *; change 2 with (1 + 1) in |- *; - rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1; + rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1; rewrite H1; auto with arith | destruct H as [x H2]; exists (x + S x); unfold nat_of_P in |- *; simpl in |- *; change 2 with (1 + 1) in |- *; - rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; + rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; rewrite H2; auto with arith | exists 0; auto with arith ]. Qed. @@ -161,7 +166,7 @@ Qed. *) Lemma nat_of_P_lt_Lt_compare_morphism : - forall p q:positive, (p ?= q)%positive Eq = Lt -> nat_of_P p < nat_of_P q. + forall p q:positive, (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q. Proof. intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ]; intro H2; @@ -178,7 +183,7 @@ intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ]; apply ZL7; apply H; assumption | simpl in |- *; discriminate H2 | unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; rewrite ZL6; - elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *; + elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *; apply lt_O_Sn | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm; @@ -193,29 +198,35 @@ Qed. *) Lemma nat_of_P_gt_Gt_compare_morphism : - forall p q:positive, (p ?= q)%positive Eq = Gt -> nat_of_P p > nat_of_P q. + forall p q:positive, (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q. Proof. -unfold gt in |- *; intro x; induction x as [p H| p H| ]; intro y; - destruct y as [q| q| ]; intro H2; - [ simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - apply lt_n_S; apply ZL7; apply H; assumption - | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - elim (Pcompare_Gt_Gt p q H2); - [ intros H3; apply lt_S; apply ZL7; apply H; assumption - | intros E; rewrite E; apply lt_n_Sn ] - | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p); - intros h H3; rewrite H3; simpl in |- *; apply lt_n_S; - apply lt_O_Sn - | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - apply ZL8; apply H; apply Pcompare_Lt_Gt; assumption - | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - apply ZL7; apply H; assumption - | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p); - intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm; - apply lt_n_S; apply lt_O_Sn - | simpl in |- *; discriminate H2 - | simpl in |- *; discriminate H2 - | simpl in |- *; discriminate H2 ]. +intros p q GT. unfold gt. +apply nat_of_P_lt_Lt_compare_morphism. +change ((q ?= p) (CompOpp Eq) = CompOpp Gt). +rewrite <- Pcompare_antisym, GT; auto. +Qed. + +(** [nat_of_P] is a morphism for [Pcompare] and [nat_compare] *) + +Lemma nat_of_P_compare_morphism : forall p q, + (p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q). +Proof. + intros p q; symmetry. + destruct ((p ?= q) Eq) as [ | | ]_eqn. + rewrite (Pcompare_Eq_eq p q); auto. + apply <- nat_compare_eq_iff; auto. + apply -> nat_compare_lt. apply nat_of_P_lt_Lt_compare_morphism; auto. + apply -> nat_compare_gt. apply nat_of_P_gt_Gt_compare_morphism; auto. +Qed. + +(** [nat_of_P] is hence injective. *) + +Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q. +Proof. +intros. +apply Pcompare_Eq_eq. +rewrite nat_of_P_compare_morphism. +apply <- nat_compare_eq_iff; auto. Qed. (** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed @@ -225,17 +236,10 @@ Qed. *) Lemma nat_of_P_lt_Lt_compare_complement_morphism : - forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q)%positive Eq = Lt. + forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt. Proof. -intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq)); - [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H; - absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ] - | intros H; elim H; - [ auto - | intros H1 H2; absurd (nat_of_P x < nat_of_P y); - [ apply lt_asym; change (nat_of_P x > nat_of_P y) in |- *; - apply nat_of_P_gt_Gt_compare_morphism; assumption - | assumption ] ] ]. + intros. rewrite nat_of_P_compare_morphism. + apply -> nat_compare_lt; auto. Qed. (** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed @@ -245,18 +249,13 @@ Qed. *) Lemma nat_of_P_gt_Gt_compare_complement_morphism : - forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q)%positive Eq = Gt. + forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt. Proof. -intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq)); - [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H; - absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ] - | intros H; elim H; - [ intros H1 H2; absurd (nat_of_P y < nat_of_P x); - [ apply lt_asym; apply nat_of_P_lt_Lt_compare_morphism; assumption - | assumption ] - | auto ] ]. + intros. rewrite nat_of_P_compare_morphism. + apply -> nat_compare_gt; auto. Qed. + (** [nat_of_P] is strictly positive *) Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n. @@ -301,25 +300,22 @@ Qed. Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p. Proof. - simple induction p. unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. - rewrite Pmult_nat_4_mult_2_permute. rewrite H. simpl in |- *. rewrite <- plus_Snm_nSm. reflexivity. - unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute. - rewrite H. reflexivity. - reflexivity. + intros. + change 2 with (nat_of_P 2). + rewrite <- nat_of_P_mult_morphism. + f_equal. Qed. Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p). Proof. - simple induction p. unfold nat_of_P in |- *. simpl in |- *. intro p0. intro. rewrite Pmult_nat_2_mult_2_permute. - rewrite Pmult_nat_4_mult_2_permute; injection H; intro H1; rewrite H1; - rewrite <- plus_Snm_nSm; reflexivity. - unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute. - injection H; intro H1; rewrite H1; reflexivity. - reflexivity. + intros. + change 2 with (nat_of_P 2). + rewrite <- nat_of_P_mult_morphism, <- nat_of_P_succ_morphism. + f_equal. Qed. (**********************************************************************) -(** Properties of the shifted injection from Peano natural numbers to +(** Properties of the shifted injection from Peano natural numbers to binary positive numbers *) (** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *) @@ -327,9 +323,9 @@ Qed. Theorem nat_of_P_o_P_of_succ_nat_eq_succ : forall n:nat, nat_of_P (P_of_succ_nat n) = S n. Proof. -intro m; induction m as [| n H]; - [ reflexivity - | simpl in |- *; rewrite nat_of_P_succ_morphism; rewrite H; auto ]. +induction n as [|n H]. +reflexivity. +simpl; rewrite nat_of_P_succ_morphism, H; auto. Qed. (** Miscellaneous lemmas on [P_of_succ_nat] *) @@ -337,17 +333,17 @@ Qed. Lemma ZL3 : forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n). Proof. -intro x; induction x as [| n H]; - [ simpl in |- *; auto with arith - | simpl in |- *; rewrite plus_comm; simpl in |- *; rewrite H; +induction n as [| n H]; simpl; + [ auto with arith + | rewrite plus_comm; simpl; rewrite H; rewrite xO_succ_permute; auto with arith ]. Qed. Lemma ZL5 : forall n:nat, P_of_succ_nat (S n + S n) = xI (P_of_succ_nat n). Proof. -intro x; induction x as [| n H]; simpl in |- *; +induction n as [| n H]; simpl; [ auto with arith - | rewrite <- plus_n_Sm; simpl in |- *; simpl in H; rewrite H; + | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H; auto with arith ]. Qed. @@ -356,19 +352,9 @@ Qed. Theorem P_of_succ_nat_o_nat_of_P_eq_succ : forall p:positive, P_of_succ_nat (nat_of_P p) = Psucc p. Proof. -intro x; induction x as [p H| p H| ]; - [ simpl in |- *; rewrite <- H; change 2 with (1 + 1) in |- *; - rewrite Pmult_nat_r_plus_morphism; elim (ZL4 p); - unfold nat_of_P in |- *; intros n H1; rewrite H1; - rewrite ZL3; auto with arith - | unfold nat_of_P in |- *; simpl in |- *; change 2 with (1 + 1) in |- *; - rewrite Pmult_nat_r_plus_morphism; - rewrite <- (Ppred_succ (P_of_succ_nat (Pmult_nat p 1 + Pmult_nat p 1))); - rewrite <- (Ppred_succ (xI p)); simpl in |- *; - rewrite <- H; elim (ZL4 p); unfold nat_of_P in |- *; - intros n H1; rewrite H1; rewrite ZL5; simpl in |- *; - trivial with arith - | unfold nat_of_P in |- *; simpl in |- *; auto with arith ]. +intros. +apply nat_of_P_inj. +rewrite nat_of_P_o_P_of_succ_nat_eq_succ, nat_of_P_succ_morphism; auto. Qed. (** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity @@ -377,45 +363,36 @@ Qed. Theorem pred_o_P_of_succ_nat_o_nat_of_P_eq_id : forall p:positive, Ppred (P_of_succ_nat (nat_of_P p)) = p. Proof. -intros x; rewrite P_of_succ_nat_o_nat_of_P_eq_succ; rewrite Ppred_succ; - trivial with arith. +intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ, Ppred_succ; auto. Qed. (**********************************************************************) -(** Extra properties of the injection from binary positive numbers to Peano +(** Extra properties of the injection from binary positive numbers to Peano natural numbers *) (** [nat_of_P] is a morphism for subtraction on positive numbers *) Theorem nat_of_P_minus_morphism : forall p q:positive, - (p ?= q)%positive Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q. + (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q. Proof. intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r; [ rewrite <- nat_of_P_plus_morphism; rewrite Pplus_minus; auto with arith | apply lt_le_weak; exact (nat_of_P_gt_Gt_compare_morphism x y H) ]. Qed. -(** [nat_of_P] is injective *) - -Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q. -Proof. -intros x y H; rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id x); - rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id y); - rewrite H; trivial with arith. -Qed. Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p. Proof. intros p q; elim (ZL4 p); elim (ZL4 q); intros h H1 i H2; rewrite H1; - rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S; + rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S; apply le_minus. Qed. Lemma ZL17 : forall p q:positive, nat_of_P p < nat_of_P (p + q). Proof. intros p q; rewrite nat_of_P_plus_morphism; unfold lt in |- *; elim (ZL4 q); - intros k H; rewrite H; rewrite plus_comm; simpl in |- *; + intros k H; rewrite H; rewrite plus_comm; simpl in |- *; apply le_n_S; apply le_plus_r. Qed. @@ -423,9 +400,9 @@ Qed. Lemma Pcompare_minus_r : forall p q r:positive, - (q ?= p)%positive Eq = Lt -> - (r ?= p)%positive Eq = Gt -> - (r ?= q)%positive Eq = Gt -> (r - p ?= r - q)%positive Eq = Lt. + (q ?= p) Eq = Lt -> + (r ?= p) Eq = Gt -> + (r ?= q) Eq = Gt -> (r - p ?= r - q) Eq = Lt. Proof. intros; apply nat_of_P_lt_Lt_compare_complement_morphism; rewrite nat_of_P_minus_morphism; @@ -434,7 +411,7 @@ intros; apply nat_of_P_lt_Lt_compare_complement_morphism; [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p); rewrite plus_assoc; rewrite le_plus_minus_r; [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l; - apply nat_of_P_lt_Lt_compare_morphism; + apply nat_of_P_lt_Lt_compare_morphism; assumption | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption ] @@ -446,9 +423,9 @@ Qed. Lemma Pcompare_minus_l : forall p q r:positive, - (q ?= p)%positive Eq = Lt -> - (p ?= r)%positive Eq = Gt -> - (q ?= r)%positive Eq = Gt -> (q - r ?= p - r)%positive Eq = Lt. + (q ?= p) Eq = Lt -> + (p ?= r) Eq = Gt -> + (q ?= r) Eq = Gt -> (q - r ?= p - r) Eq = Lt. Proof. intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism; rewrite nat_of_P_minus_morphism; @@ -469,8 +446,8 @@ Qed. Theorem Pmult_minus_distr_l : forall p q r:positive, - (q ?= r)%positive Eq = Gt -> - (p * (q - r))%positive = (p * q - p * r)%positive. + (q ?= r) Eq = Gt -> + (p * (q - r) = p * q - p * r)%positive. Proof. intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism; rewrite nat_of_P_minus_morphism; @@ -478,7 +455,7 @@ intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism; [ do 2 rewrite nat_of_P_mult_morphism; do 3 rewrite (mult_comm (nat_of_P x)); apply mult_minus_distr_r | apply nat_of_P_gt_Gt_compare_complement_morphism; - do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *; + do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *; elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l; exact (nat_of_P_gt_Gt_compare_morphism y z H) ] | assumption ]. diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget new file mode 100644 index 00000000..32f94f01 --- /dev/null +++ b/theories/NArith/vo.itarget @@ -0,0 +1,12 @@ +BinNat.vo +BinPos.vo +NArith.vo +Ndec.vo +Ndigits.vo +Ndist.vo +Nnat.vo +Pnat.vo +POrderedType.vo +Pminmax.vo +NOrderedType.vo +Nminmax.vo |