From df7acfad0ce0270b62644a5e9f8709ed0e7936e6 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 2 Nov 2010 14:44:08 +0000 Subject: Move stuff about positive into a distinct PArith subdir Beware! after this, a ./configure must be done. It might also be a good idea to chase any phantom .vo remaining after a make clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 3 +- doc/refman/RefMan-lib.tex | 3 +- doc/stdlib/index-list.html.template | 41 +- doc/stdlib/make-library-files | 2 +- doc/stdlib/make-library-index | 2 +- interp/coqlib.ml | 4 +- plugins/nsatz/nsatz.ml4 | 6 +- plugins/rtauto/refl_tauto.ml | 2 +- plugins/syntax/z_syntax.ml | 2 +- theories/NArith/BinPos.v | 1260 ----------------------------------- theories/NArith/POrderedType.v | 60 -- theories/NArith/Pminmax.v | 126 ---- theories/NArith/Pnat.v | 460 ------------- theories/NArith/Psqrt.v | 123 ---- theories/NArith/intro.tex | 2 +- theories/NArith/vo.itarget | 5 - theories/PArith/BinPos.v | 1255 ++++++++++++++++++++++++++++++++++ theories/PArith/PArith.v | 15 + theories/PArith/POrderedType.v | 60 ++ theories/PArith/Pminmax.v | 126 ++++ theories/PArith/Pnat.v | 460 +++++++++++++ theories/PArith/Psqrt.v | 123 ++++ theories/PArith/intro.tex | 4 + theories/PArith/vo.itarget | 6 + theories/theories.itarget | 1 + toplevel/coqinit.ml | 1 + 26 files changed, 2095 insertions(+), 2057 deletions(-) delete mode 100644 theories/NArith/BinPos.v delete mode 100644 theories/NArith/POrderedType.v delete mode 100644 theories/NArith/Pminmax.v delete mode 100644 theories/NArith/Pnat.v delete mode 100644 theories/NArith/Psqrt.v create mode 100644 theories/PArith/BinPos.v create mode 100644 theories/PArith/PArith.v create mode 100644 theories/PArith/POrderedType.v create mode 100644 theories/PArith/Pminmax.v create mode 100644 theories/PArith/Pnat.v create mode 100644 theories/PArith/Psqrt.v create mode 100644 theories/PArith/intro.tex create mode 100644 theories/PArith/vo.itarget diff --git a/Makefile.common b/Makefile.common index 77e4d59f2..26484fcdd 100644 --- a/Makefile.common +++ b/Makefile.common @@ -260,6 +260,7 @@ STRUCTURESVO:=$(call cat_vo_itarget, theories/Structures) ARITHVO:=$(call cat_vo_itarget, theories/Arith) SORTINGVO:=$(call cat_vo_itarget, theories/Sorting) BOOLVO:=$(call cat_vo_itarget, theories/Bool) +PARITHVO:=$(call cat_vo_itarget, theories/PArith) NARITHVO:=$(call cat_vo_itarget, theories/NArith) ZARITHVO:=$(call cat_vo_itarget, theories/ZArith) QARITHVO:=$(call cat_vo_itarget, theories/QArith) @@ -278,7 +279,7 @@ CLASSESVO:=$(call cat_vo_itarget, theories/Classes) PROGRAMVO:=$(call cat_vo_itarget, theories/Program) THEORIESVO:=\ - $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ + $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(PARITHVO) $(NARITHVO) $(ZARITHVO) \ $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(MSETSVO) \ $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) \ $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO) diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 8847d058a..36549b7a0 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -809,7 +809,8 @@ subdirectories: \begin{tabular}{lp{12cm}} {\bf Logic} & Classical logic and dependent equality \\ {\bf Arith} & Basic Peano arithmetic \\ - {\bf NArith} & Basic positive integer arithmetic \\ + {\bf PArith} & Basic positive integer arithmetic \\ + {\bf NArith} & Basic binary natural number arithmetic \\ {\bf ZArith} & Basic relative integer arithmetic \\ {\bf Numbers} & Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2$^{31}$ binary words) \\ {\bf Bool} & Booleans (basic functions and results) \\ diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index a4feb012b..4f208c7da 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -130,22 +130,31 @@ through the Require Import command.

theories/Arith/Factorial.v theories/Arith/Wf_nat.v - -
NArith: + +
PArith: Binary positive integers
+
+ theories/PArith/BinPos.v + theories/PArith/Pnat.v + theories/PArith/POrderedType.v + theories/PArith/Pminmax.v + theories/PArith/Psqrt.v + (theories/PArith/PArith.v) +
+ +
NArith: + Binary natural numbers +
- theories/NArith/BinPos.v theories/NArith/BinNat.v - (theories/NArith/NArith.v) - theories/NArith/Pnat.v theories/NArith/Nnat.v theories/NArith/Ndigits.v theories/NArith/Ndist.v theories/NArith/Ndec.v theories/NArith/Ndiv_def.v - theories/NArith/POrderedType.v - theories/NArith/Pminmax.v + theories/NArith/Nsqrt_def.v + (theories/NArith/NArith.v)
ZArith: @@ -169,7 +178,8 @@ through the Require Import command.

theories/ZArith/Zhints.v (theories/ZArith/ZArith_base.v) theories/ZArith/Zcomplements.v - theories/ZArith/Zsqrt.v + theories/ZArith/Zsqrt_def.v + theories/ZArith/Zsqrt_compat.v theories/ZArith/Zpow_def.v theories/ZArith/Zpower.v theories/ZArith/Zdiv.v @@ -226,6 +236,8 @@ through the Require Import command.

theories/Numbers/NatInt/NZOrder.v theories/Numbers/NatInt/NZDomain.v theories/Numbers/NatInt/NZProperties.v + theories/Numbers/NatInt/NZPow.v + theories/Numbers/NatInt/NZSqrt.v
@@ -265,8 +277,11 @@ through the Require Import command.

theories/Numbers/Natural/Abstract/NStrongRec.v theories/Numbers/Natural/Abstract/NSub.v theories/Numbers/Natural/Abstract/NDiv.v + theories/Numbers/Natural/Abstract/NMaxMin.v + theories/Numbers/Natural/Abstract/NParity.v + theories/Numbers/Natural/Abstract/NPow.v + theories/Numbers/Natural/Abstract/NSqrt.v theories/Numbers/Natural/Abstract/NProperties.v - theories/Numbers/Natural/Abstract/NMinMax.v theories/Numbers/Natural/Binary/NBinary.v theories/Numbers/Natural/Peano/NPeano.v theories/Numbers/Natural/SpecViaZ/NSig.v @@ -288,12 +303,14 @@ through the Require Import command.

theories/Numbers/Integer/Abstract/ZLt.v theories/Numbers/Integer/Abstract/ZMul.v theories/Numbers/Integer/Abstract/ZMulOrder.v + theories/Numbers/Integer/Abstract/ZSgnAbs.v + theories/Numbers/Integer/Abstract/ZMaxMin.v + theories/Numbers/Integer/Abstract/ZParity.v + theories/Numbers/Integer/Abstract/ZPow.v + theories/Numbers/Integer/Abstract/ZProperties.v theories/Numbers/Integer/Abstract/ZDivEucl.v theories/Numbers/Integer/Abstract/ZDivFloor.v theories/Numbers/Integer/Abstract/ZDivTrunc.v - theories/Numbers/Integer/Abstract/ZProperties.v - theories/Numbers/Integer/Abstract/ZSgnAbs.v - theories/Numbers/Integer/Abstract/ZMinMax.v theories/Numbers/Integer/Binary/ZBinary.v theories/Numbers/Integer/NatPairs/ZNatPairs.v theories/Numbers/Integer/SpecViaZ/ZSig.v diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files index 39cedbec4..c071c4a2e 100755 --- a/doc/stdlib/make-library-files +++ b/doc/stdlib/make-library-files @@ -10,7 +10,7 @@ # En supposant que make fait son boulot, ca fait un tri topologique du # graphe des dépendances -LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers" +LIBDIRS="Arith PArith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes Numbers" rm -f library.files.ls.tmp (cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index c8782e93b..8e496fdd2 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -7,7 +7,7 @@ FILE=$1 cp -f $FILE.template tmp echo -n Building file index-list.prehtml ... -LIBDIRS="Init Logic Structures Bool Arith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" +LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" for k in $LIBDIRS; do i=theories/$k diff --git a/interp/coqlib.ml b/interp/coqlib.ml index bb555148f..d6ed355c9 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -91,10 +91,12 @@ let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s let arith_dir = ["Coq";"Arith"] let arith_modules = [arith_dir] +let parith_dir = ["Coq";"PArith"] + let narith_dir = ["Coq";"NArith"] let zarith_dir = ["Coq";"ZArith"] -let zarith_base_modules = [narith_dir;zarith_dir] +let zarith_base_modules = [parith_dir;narith_dir;zarith_dir] let init_dir = ["Coq";"Init"] let init_modules = [ diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 5070f89ed..b235b5821 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -189,9 +189,9 @@ let z0 = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Z0") let zpos = lazy (gen_constant "CC" ["ZArith";"BinInt"] "Zpos") let zneg = lazy(gen_constant "CC" ["ZArith";"BinInt"] "Zneg") -let pxI = lazy(gen_constant "CC" ["NArith";"BinPos"] "xI") -let pxO = lazy(gen_constant "CC" ["NArith";"BinPos"] "xO") -let pxH = lazy(gen_constant "CC" ["NArith";"BinPos"] "xH") +let pxI = lazy(gen_constant "CC" ["PArith";"BinPos"] "xI") +let pxO = lazy(gen_constant "CC" ["PArith";"BinPos"] "xO") +let pxH = lazy(gen_constant "CC" ["PArith";"BinPos"] "xH") let nN0 = lazy (gen_constant "CC" ["NArith";"BinNat"] "N0") let nNpos = lazy(gen_constant "CC" ["NArith";"BinNat"] "Npos") diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index cd4a7d3b0..a520ce2d4 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -36,7 +36,7 @@ let l_true_equals_true = [|data_constant "bool";data_constant "true"|])) let pos_constant = - Coqlib.gen_constant "refl_tauto" ["NArith";"BinPos"] + Coqlib.gen_constant "refl_tauto" ["PArith";"BinPos"] let l_xI = lazy (pos_constant "xI") let l_xO = lazy (pos_constant "xO") diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 15d11eca2..fb8de1f92 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -23,7 +23,7 @@ exception Non_closed_number open Libnames open Rawterm let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let positive_module = ["Coq";"NArith";"BinPos"] +let positive_module = ["Coq";"PArith";"BinPos"] let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) let positive_path = make_path positive_module "positive" diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v deleted file mode 100644 index d334d42e9..000000000 --- a/theories/NArith/BinPos.v +++ /dev/null @@ -1,1260 +0,0 @@ -(* -*- coding: utf-8 -*- *) -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* positive -| xO : positive -> positive -| xH : positive. - -(** Declare binding key for scope positive_scope *) - -Delimit Scope positive_scope with positive. - -(** Automatically open scope positive_scope for type positive, xO and xI *) - -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)) - for the number 6 (which is 110 in binary notation). -*) - -Notation "p ~ 1" := (xI p) - (at level 7, left associativity, format "p '~' '1'") : positive_scope. -Notation "p ~ 0" := (xO p) - (at level 7, left associativity, format "p '~' '0'") : positive_scope. - -Open Local Scope positive_scope. - -(* In the current file, [xH] cannot yet be written as [1], since the - interpretation of positive numerical constants is not available - yet. We fix this here with an ad-hoc temporary notation. *) - -Notation Local "1" := xH (at level 7). - -(** Successor *) - -Fixpoint Psucc (x:positive) : positive := - match x with - | p~1 => (Psucc p)~0 - | p~0 => p~1 - | 1 => 1~0 - end. - -(** Addition *) - -Set Boxed Definitions. - -Fixpoint Pplus (x y:positive) : positive := - match x, y with - | p~1, q~1 => (Pplus_carry p q)~0 - | p~1, q~0 => (Pplus p q)~1 - | p~1, 1 => (Psucc p)~0 - | p~0, q~1 => (Pplus p q)~1 - | p~0, q~0 => (Pplus p q)~0 - | p~0, 1 => p~1 - | 1, q~1 => (Psucc q)~0 - | 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 - | p~1, q~0 => (Pplus_carry p q)~0 - | p~1, 1 => (Psucc p)~1 - | p~0, q~1 => (Pplus_carry p q)~0 - | p~0, q~0 => (Pplus p q)~1 - | p~0, 1 => (Psucc p)~0 - | 1, q~1 => (Psucc q)~1 - | 1, q~0 => (Psucc q)~0 - | 1, 1 => 1~1 - end. - -Unset Boxed Definitions. - -Infix "+" := Pplus : positive_scope. - -Definition Piter_op {A}(op:A->A->A) := - fix iter (p:positive)(a:A) : A := - match p with - | 1 => a - | p~0 => iter p (op a a) - | p~1 => op a (iter p (op a a)) - end. - -Lemma Piter_op_succ : forall A (op:A->A->A), - (forall x y z, op x (op y z) = op (op x y) z) -> - forall p a, - Piter_op op (Psucc p) a = op a (Piter_op op p a). -Proof. - induction p; simpl; intros; trivial. - rewrite H. apply IHp. -Qed. - -(** From binary positive numbers to Peano natural numbers *) - -Definition Pmult_nat : positive -> nat -> nat := - Eval unfold Piter_op in (* for compatibility *) - Piter_op plus. - -Definition nat_of_P (x:positive) := Pmult_nat x (S O). - -(** From Peano natural numbers to binary positive numbers *) - -Fixpoint P_of_succ_nat (n:nat) : positive := - match n with - | O => 1 - | S x => Psucc (P_of_succ_nat x) - end. - -(** Operation x -> 2*x-1 *) - -Fixpoint Pdouble_minus_one (x:positive) : positive := - match x with - | p~1 => p~0~1 - | p~0 => (Pdouble_minus_one p)~1 - | 1 => 1 - end. - -(** Predecessor *) - -Definition Ppred (x:positive) := - match x with - | p~1 => p~0 - | p~0 => Pdouble_minus_one p - | 1 => 1 - end. - -(** An auxiliary type for subtraction *) - -Inductive positive_mask : Set := -| IsNul : positive_mask -| IsPos : positive -> positive_mask -| IsNeg : positive_mask. - -(** Operation x -> 2*x+1 *) - -Definition Pdouble_plus_one_mask (x:positive_mask) := - match x with - | IsNul => IsPos 1 - | IsNeg => IsNeg - | IsPos p => IsPos p~1 - end. - -(** Operation x -> 2*x *) - -Definition Pdouble_mask (x:positive_mask) := - match x with - | IsNul => IsNul - | IsNeg => IsNeg - | IsPos p => IsPos p~0 - end. - -(** Operation x -> 2*x-2 *) - -Definition Pdouble_minus_two (x:positive) := - match x with - | p~1 => IsPos p~0~0 - | p~0 => IsPos (Pdouble_minus_one p)~0 - | 1 => IsNul - end. - -(** Subtraction of binary positive numbers into a positive numbers mask *) - -Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask := - match x, y with - | p~1, q~1 => Pdouble_mask (Pminus_mask p q) - | p~1, q~0 => Pdouble_plus_one_mask (Pminus_mask p q) - | p~1, 1 => IsPos p~0 - | p~0, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q) - | p~0, q~0 => Pdouble_mask (Pminus_mask p q) - | p~0, 1 => IsPos (Pdouble_minus_one p) - | 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) - | p~1, q~0 => Pdouble_mask (Pminus_mask p q) - | p~1, 1 => IsPos (Pdouble_minus_one p) - | p~0, q~1 => Pdouble_mask (Pminus_mask_carry p q) - | p~0, q~0 => Pdouble_plus_one_mask (Pminus_mask_carry p q) - | p~0, 1 => Pdouble_minus_two p - | 1, _ => IsNeg - end. - -(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *) - -Definition Pminus (x y:positive) := - match Pminus_mask x y with - | IsPos z => z - | _ => 1 - end. - -Infix "-" := Pminus : positive_scope. - -(** Multiplication on binary positive numbers *) - -Fixpoint Pmult (x y:positive) : positive := - match x with - | p~1 => y + (Pmult p y)~0 - | p~0 => (Pmult p y)~0 - | 1 => y - end. - -Infix "*" := Pmult : positive_scope. - -(** Division by 2 rounded below but for 1 *) - -Definition Pdiv2 (z:positive) := - match z with - | 1 => 1 - | p~0 => p - | p~1 => p - end. - -Infix "/" := Pdiv2 : positive_scope. - -(** Comparison on binary positive numbers *) - -Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison := - match x, y with - | p~1, q~1 => Pcompare p q r - | p~1, q~0 => Pcompare p q Gt - | p~1, 1 => Gt - | p~0, q~1 => Pcompare p q Lt - | p~0, q~0 => Pcompare p q r - | p~0, 1 => Gt - | 1, q~1 => Lt - | 1, q~0 => Lt - | 1, 1 => r - end. - -Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope. - -Definition Plt (x y:positive) := (Pcompare x y Eq) = Lt. -Definition Pgt (x y:positive) := (Pcompare x y Eq) = Gt. -Definition Ple (x y:positive) := (Pcompare x y Eq) <> Gt. -Definition Pge (x y:positive) := (Pcompare x y Eq) <> Lt. - -Infix "<=" := Ple : positive_scope. -Infix "<" := Plt : positive_scope. -Infix ">=" := Pge : positive_scope. -Infix ">" := Pgt : positive_scope. - -Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope. -Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope. -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 - | Gt => p' - end. - -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. - -(**********************************************************************) -(** Decidability of equality on binary positive numbers *) - -Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -(* begin hide *) -Corollary ZL11 : forall p:positive, p = 1 \/ p <> 1. -Proof. - intro; edestruct positive_eq_dec; eauto. -Qed. -(* end hide *) - -(**********************************************************************) -(** Properties of successor on binary positive numbers *) - -(** Specification of [xI] in term of [Psucc] and [xO] *) - -Lemma xI_succ_xO : forall p:positive, p~1 = Psucc p~0. -Proof. - reflexivity. -Qed. - -Lemma Psucc_discr : forall p:positive, p <> Psucc p. -Proof. - destruct p; discriminate. -Qed. - -(** Successor and double *) - -Lemma Psucc_o_double_minus_one_eq_xO : - forall p:positive, Psucc (Pdouble_minus_one p) = p~0. -Proof. - induction p; simpl; f_equal; auto. -Qed. - -Lemma Pdouble_minus_one_o_succ_eq_xI : - forall p:positive, Pdouble_minus_one (Psucc p) = p~1. -Proof. - induction p; simpl; f_equal; auto. -Qed. - -Lemma xO_succ_permute : - forall p:positive, (Psucc p)~0 = Psucc (Psucc p~0). -Proof. - induction p; simpl; auto. -Qed. - -Lemma double_moins_un_xO_discr : - forall p:positive, Pdouble_minus_one p <> p~0. -Proof. - destruct p; discriminate. -Qed. - -(** Successor and predecessor *) - -Lemma Psucc_not_one : forall p:positive, Psucc p <> 1. -Proof. - destruct p; discriminate. -Qed. - -Lemma Ppred_succ : forall p:positive, Ppred (Psucc p) = p. -Proof. - intros [[p|p| ]|[p|p| ]| ]; simpl; auto. - f_equal; apply Pdouble_minus_one_o_succ_eq_xI. -Qed. - -Lemma Psucc_pred : forall p:positive, p = 1 \/ Psucc (Ppred p) = p. -Proof. - induction p; simpl; auto. - right; apply Psucc_o_double_minus_one_eq_xO. -Qed. - -Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). - -(** Injectivity of successor *) - -Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q. -Proof. - induction p; intros [q|q| ] H; simpl in *; destr_eq H; f_equal; auto. - elim (Psucc_not_one p); auto. - elim (Psucc_not_one q); auto. -Qed. - -(**********************************************************************) -(** Properties of addition on binary positive numbers *) - -(** Specification of [Psucc] in term of [Pplus] *) - -Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + 1. -Proof. - destruct p; reflexivity. -Qed. - -Lemma Pplus_one_succ_l : forall p:positive, Psucc p = 1 + p. -Proof. - destruct p; reflexivity. -Qed. - -(** Specification of [Pplus_carry] *) - -Theorem Pplus_carry_spec : - forall p q:positive, Pplus_carry p q = Psucc (p + q). -Proof. - induction p; destruct q; simpl; f_equal; auto. -Qed. - -(** Commutativity *) - -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. - -(** 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; - auto using Pplus_one_succ_r; rewrite Pplus_carry_spec; auto. -Qed. - -Theorem Pplus_succ_permute_l : - forall p q:positive, Psucc p + q = Psucc (p + q). -Proof. - intros p q; rewrite Pplus_comm, (Pplus_comm p); - apply Pplus_succ_permute_r. -Qed. - -Theorem Pplus_carry_pred_eq_plus : - forall p q:positive, q <> 1 -> Pplus_carry p (Ppred q) = p + q. -Proof. - intros p q H; rewrite Pplus_carry_spec, <- Pplus_succ_permute_r; f_equal. - destruct (Psucc_pred q); [ elim H; assumption | assumption ]. -Qed. - -(** No neutral for addition on strictly positive numbers *) - -Lemma Pplus_no_neutral : forall p q:positive, q + p <> p. -Proof. - induction p as [p IHp|p IHp| ]; intros [q|q| ] H; - destr_eq H; apply (IHp q H). -Qed. - -Lemma Pplus_carry_no_neutral : - forall p q:positive, Pplus_carry q p <> Psucc p. -Proof. - intros p q H; elim (Pplus_no_neutral p q). - apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption. -Qed. - -(** Simplification *) - -Lemma Pplus_carry_plus : - forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s. -Proof. - intros p q r s H; apply Psucc_inj; do 2 rewrite <- Pplus_carry_spec; - assumption. -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; - contradict H; auto using Pplus_carry_no_neutral. - 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. - -Lemma Pplus_reg_l : forall p q r:positive, p + q = p + r -> q = r. -Proof. - intros p q r H; apply Pplus_reg_r with (r:=p). - rewrite (Pplus_comm r), (Pplus_comm q); assumption. -Qed. - -Lemma Pplus_carry_reg_r : - forall p q r:positive, Pplus_carry p r = Pplus_carry q r -> p = q. -Proof. - intros p q r H; apply Pplus_reg_r with (r:=r); apply Pplus_carry_plus; - assumption. -Qed. - -Lemma Pplus_carry_reg_l : - forall p q r:positive, Pplus_carry p q = Pplus_carry p r -> q = r. -Proof. - intros p q r H; apply Pplus_reg_r with (r:=p); - rewrite (Pplus_comm r), (Pplus_comm q); apply Pplus_carry_plus; assumption. -Qed. - -(** Addition on positive is associative *) - -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, - ?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, - ?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. - -(** Commutation of addition with the double of a positive number *) - -Lemma Pplus_xO : forall m n : positive, (m + n)~0 = m~0 + n~0. -Proof. - destruct n; destruct m; simpl; auto. -Qed. - -Lemma Pplus_xI_double_minus_one : - forall p q:positive, (p + q)~0 = p~1 + Pdouble_minus_one q. -Proof. - intros; change (p~1) with (p~0 + 1). - rewrite <- Pplus_assoc, <- Pplus_one_succ_l, Psucc_o_double_minus_one_eq_xO. - reflexivity. -Qed. - -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, - ?Pplus_xI_double_minus_one; try reflexivity. - rewrite IHp; auto. - rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity. -Qed. - -(** Misc *) - -Lemma Pplus_diag : forall p:positive, p + p = p~0. -Proof. - induction p as [p IHp| p IHp| ]; simpl; - try rewrite ?Pplus_carry_spec, ?IHp; reflexivity. -Qed. - -(**********************************************************************) -(** Peano induction and recursion on binary positive positive numbers *) -(** (a nice proof from Conor McBride, see "The view from the left") *) - -Inductive PeanoView : positive -> Type := -| PeanoOne : PeanoView 1 -| PeanoSucc : forall p, PeanoView p -> PeanoView (Psucc p). - -Fixpoint peanoView_xO p (q:PeanoView p) : PeanoView (p~0) := - match q in PeanoView x return PeanoView (x~0) with - | PeanoOne => PeanoSucc _ PeanoOne - | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xO _ q)) - end. - -Fixpoint peanoView_xI p (q:PeanoView p) : PeanoView (p~1) := - match q in PeanoView x return PeanoView (x~1) with - | PeanoOne => PeanoSucc _ (PeanoSucc _ PeanoOne) - | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xI _ q)) - end. - -Fixpoint peanoView p : PeanoView p := - match p return PeanoView p with - | 1 => PeanoOne - | p~0 => peanoView_xO p (peanoView p) - | p~1 => peanoView_xI p (peanoView p) - end. - -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 - | PeanoOne => a - | PeanoSucc _ q => f _ (iter _ q) - end). - -Require Import Eqdep_dec EqdepFacts. - -Theorem eq_dep_eq_positive : - 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'. -Proof. - 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'. - intro. destruct p; discriminate. - intro. unfold p0 in H. apply Psucc_inj in H. - generalize q'. rewrite H. intro. - rewrite (IHq q'0). - trivial. - trivial. -Qed. - -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), - Prect P a f (Psucc p) = f _ (Prect P a f p). -Proof. - intros. - unfold Prect. - rewrite (PeanoViewUnique _ (peanoView (Psucc p)) (PeanoSucc _ (peanoView p))). - trivial. -Qed. - -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. -Qed. - -Definition Prec (P:positive->Set) := Prect P. - -(** Peano induction *) - -Definition Pind (P:positive->Prop) := Prect P. - -(** Peano case analysis *) - -Theorem Pcase : - forall P:positive -> Prop, - P 1 -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p. -Proof. - intros; apply Pind; auto. -Qed. - -(**********************************************************************) -(** Properties of multiplication on binary positive numbers *) - -(** One is right neutral for multiplication *) - -Lemma Pmult_1_r : forall p:positive, p * 1 = p. -Proof. - induction p; simpl; f_equal; auto. -Qed. - -(** Successor and multiplication *) - -Lemma Pmult_Sn_m : forall n m : positive, (Psucc n) * m = m + n * m. -Proof. - induction n as [n IHn | n IHn | ]; simpl; intro m. - rewrite IHn, Pplus_assoc, Pplus_diag, <-Pplus_xO; reflexivity. - reflexivity. - symmetry; apply Pplus_diag. -Qed. - -(** Right reduction properties for multiplication *) - -Lemma Pmult_xO_permute_r : forall p q:positive, p * q~0 = (p * q)~0. -Proof. - intros p q; induction p; simpl; do 2 (f_equal; auto). -Qed. - -Lemma Pmult_xI_permute_r : forall p q:positive, p * q~1 = p + (p * q)~0. -Proof. - intros p q; induction p as [p IHp|p IHp| ]; simpl; f_equal; auto. - rewrite IHp, 2 Pplus_assoc, (Pplus_comm p); reflexivity. -Qed. - -(** Commutativity of multiplication *) - -Theorem Pmult_comm : forall p q:positive, p * q = q * p. -Proof. - intros p q; induction q as [q IHq|q IHq| ]; simpl; try rewrite <- IHq; - auto using Pmult_xI_permute_r, Pmult_xO_permute_r, Pmult_1_r. -Qed. - -(** Distributivity of multiplication over addition *) - -Theorem Pmult_plus_distr_l : - forall p q r:positive, p * (q + r) = p * q + p * r. -Proof. - intros p q r; induction p as [p IHp|p IHp| ]; simpl. - rewrite IHp. set (m:=(p*q)~0). set (n:=(p*r)~0). - change ((p*q+p*r)~0) with (m+n). - rewrite 2 Pplus_assoc; f_equal. - rewrite <- 2 Pplus_assoc; f_equal. - apply Pplus_comm. - f_equal; auto. - reflexivity. -Qed. - -Theorem Pmult_plus_distr_r : - forall p q r:positive, (p + q) * r = p * r + q * r. -Proof. - intros p q r; do 3 rewrite Pmult_comm with (q:=r); apply Pmult_plus_distr_l. -Qed. - -(** Associativity of multiplication *) - -Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r. -Proof. - induction p as [p IHp| p IHp | ]; simpl; intros q r. - rewrite IHp; rewrite Pmult_plus_distr_r; reflexivity. - rewrite IHp; reflexivity. - reflexivity. -Qed. - -(** Parity properties of multiplication *) - -Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, p~1 * r <> q~0 * r. -Proof. - intros p q r; induction r; try discriminate. - rewrite 2 Pmult_xO_permute_r; intro H; destr_eq H; auto. -Qed. - -Lemma Pmult_xO_discr : forall p q:positive, p~0 * q <> q. -Proof. - intros p q; induction q; try discriminate. - rewrite Pmult_xO_permute_r; injection; assumption. -Qed. - -(** Simplification properties of multiplication *) - -Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q. -Proof. - induction p as [p IHp| p IHp| ]; intros [q|q| ] r H; - reflexivity || apply (f_equal (A:=positive)) || apply False_ind. - apply IHp with (r~0); simpl in *; - rewrite 2 Pmult_xO_permute_r; apply Pplus_reg_l with (1:=H). - apply Pmult_xI_mult_xO_discr with (1:=H). - simpl in H; rewrite Pplus_comm in H; apply Pplus_no_neutral with (1:=H). - symmetry in H; apply Pmult_xI_mult_xO_discr with (1:=H). - apply IHp with (r~0); simpl; rewrite 2 Pmult_xO_permute_r; assumption. - apply Pmult_xO_discr with (1:= H). - simpl in H; symmetry in H; rewrite Pplus_comm in H; - apply Pplus_no_neutral with (1:=H). - symmetry in H; apply Pmult_xO_discr with (1:=H). -Qed. - -Theorem Pmult_reg_l : forall p q r:positive, r * p = r * q -> p = q. -Proof. - intros p q r H; apply Pmult_reg_r with (r:=r). - rewrite (Pmult_comm p), (Pmult_comm q); assumption. -Qed. - -(** Inversion of multiplication *) - -Lemma Pmult_1_inversion_l : forall p q:positive, p * q = 1 -> p = 1. -Proof. - intros [p|p| ] [q|q| ] H; destr_eq H; auto. -Qed. - -(** Square *) - -Lemma Psquare_xO : forall p, p~0 * p~0 = (p*p)~0~0. -Proof. - intros. simpl. now rewrite Pmult_comm. -Qed. - -Lemma Psquare_xI : forall p, p~1 * p~1 = (p*p+p)~0~1. -Proof. - intros. simpl. rewrite Pmult_comm. simpl. f_equal. - rewrite Pplus_assoc, Pplus_diag. simpl. now rewrite Pplus_comm. -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 *) - -Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq. - induction p; auto. -Qed. - -(* A generalization of Pcompare_refl *) - -Theorem Pcompare_refl_id : forall (p : positive) (r : comparison), (p ?= p) r = r. - induction p; auto. -Qed. - -Theorem Pcompare_not_Eq : - forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq. -Proof. - induction p as [p IHp| p IHp| ]; intros [q| q| ]; split; simpl; auto; - discriminate || (elim (IHp q); auto). -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; - 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. - induction p; intros [q|q| ] H; simpl; auto; discriminate. -Qed. - -Lemma Pcompare_eq_Lt : - forall p q : positive, (p ?= q) Eq = Lt <-> (p ?= q) Gt = Lt. -Proof. - intros p q; split; [| apply Pcompare_Gt_Lt]. - revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate. -Qed. - -Lemma Pcompare_Lt_Gt : - forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt. -Proof. - induction p; intros [q|q| ] H; simpl; auto; discriminate. -Qed. - -Lemma Pcompare_eq_Gt : - forall p q : positive, (p ?= q) Eq = Gt <-> (p ?= q) Lt = Gt. -Proof. - intros p q; split; [| apply Pcompare_Lt_Gt]. - revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate. -Qed. - -Lemma Pcompare_Lt_Lt : - forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q. -Proof. - induction p as [p IHp| p IHp| ]; intros [q|q| ] H; simpl in *; auto; - destruct (IHp q H); subst; auto. -Qed. - -Lemma Pcompare_Lt_eq_Lt : - forall p q:positive, (p ?= q) Lt = Lt <-> (p ?= q) Eq = Lt \/ p = q. -Proof. - intros p q; split; [apply Pcompare_Lt_Lt |]. - intros [H|H]; [|subst; apply Pcompare_refl_id]. - revert q H; induction p; intros [q|q| ] H; simpl in *; - auto; discriminate. -Qed. - -Lemma Pcompare_Gt_Gt : - forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q. -Proof. - induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto; - destruct (IHp q H); subst; auto. -Qed. - -Lemma Pcompare_Gt_eq_Gt : - forall p q:positive, (p ?= q) Gt = Gt <-> (p ?= q) Eq = Gt \/ p = q. -Proof. - intros p q; split; [apply Pcompare_Gt_Gt |]. - intros [H|H]; [|subst; apply Pcompare_refl_id]. - revert q H; induction p; intros [q|q| ] H; simpl in *; - auto; discriminate. -Qed. - -Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt. -Proof. - destruct r; auto. -Qed. - -Ltac ElimPcompare c1 c2 := - elim (Dcompare ((c1 ?= c2) Eq)); - [ idtac | let x := fresh "H" in (intro x; case x; clear x) ]. - -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; - rewrite IHp; auto. -Qed. - -Lemma ZC1 : forall p q:positive, (p ?= q) Eq = Gt -> (q ?= p) Eq = Lt. -Proof. - intros p q H; change Eq with (CompOpp Eq). - rewrite <- Pcompare_antisym, H; reflexivity. -Qed. - -Lemma ZC2 : forall p q:positive, (p ?= q) Eq = Lt -> (q ?= p) Eq = Gt. -Proof. - intros p q H; change Eq with (CompOpp Eq). - rewrite <- Pcompare_antisym, H; reflexivity. -Qed. - -Lemma ZC3 : forall p q:positive, (p ?= q) Eq = Eq -> (q ?= p) Eq = Eq. -Proof. - intros p q H; change Eq with (CompOpp Eq). - rewrite <- Pcompare_antisym, H; reflexivity. -Qed. - -Lemma ZC4 : forall p q:positive, (p ?= q) Eq = CompOpp ((q ?= p) Eq). -Proof. - intros; change Eq at 1 with (CompOpp Eq). - 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. -Proof. - induction p; simpl in *; - [ elim (Pcompare_eq_Lt p (Psucc p)); auto | - apply Pcompare_refl_id | reflexivity]. -Qed. - -Theorem Pcompare_p_Sq : forall p q : positive, - (p ?= Psucc q) Eq = Lt <-> (p ?= q) Eq = Lt \/ p = q. -Proof. - intros p q; split. - (* -> *) - revert p q; induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; - try (left; reflexivity); try (right; reflexivity). - destruct (IHp q (Pcompare_Gt_Lt _ _ H)); subst; auto. - destruct (Pcompare_eq_Lt p q); auto. - destruct p; discriminate. - left; destruct (IHp q H); - [ elim (Pcompare_Lt_eq_Lt p q); auto | subst; apply Pcompare_refl_id]. - destruct (Pcompare_Lt_Lt p q H); subst; auto. - destruct p; discriminate. - (* <- *) - intros [H|H]; [|subst; apply Pcompare_p_Sp]. - revert q H; induction p; intros [q|q| ] H; simpl in *; - auto; try discriminate. - destruct (Pcompare_eq_Lt p (Psucc q)); auto. - apply Pcompare_Gt_Lt; auto. - destruct (Pcompare_Lt_Lt p q H); subst; auto using Pcompare_p_Sp. - destruct (Pcompare_Lt_eq_Lt p q); auto. -Qed. - -(** 1 is the least positive number *) - -Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt. -Proof. - destruct p; discriminate. -Qed. - -(** Properties of the strict order on positive numbers *) - -Lemma Plt_1 : forall p, ~ p < 1. -Proof. - exact Pcompare_1. -Qed. - -Lemma Plt_1_succ : forall n, 1 < Psucc n. -Proof. - intros. apply Pcompare_p_Sq. destruct n; auto. -Qed. - -Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m. -Proof. - unfold Plt; intros n m H; apply <- Pcompare_p_Sq; auto. -Qed. - -Lemma Psucc_lt_compat : forall n m, n < m <-> Psucc n < Psucc m. -Proof. - unfold Plt. induction n; destruct m; simpl; auto; split; try easy; intros. - now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, IHn, Pcompare_Gt_Lt. - now apply Pcompare_eq_Lt, IHn, Pcompare_p_Sq, Pcompare_Lt_eq_Lt. - destruct (Psucc n); discriminate. - now apply Pcompare_eq_Lt, Pcompare_p_Sq, Pcompare_Lt_eq_Lt. - now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, Pcompare_Gt_Lt. - destruct n; discriminate. - apply Plt_1_succ. - destruct m; auto. -Qed. - -Lemma Plt_irrefl : forall p : positive, ~ p < p. -Proof. - unfold Plt; intro p; rewrite Pcompare_refl; discriminate. -Qed. - -Lemma Plt_trans : forall n m p : positive, n < m -> m < p -> n < p. -Proof. - intros n m p; induction p using Pind; intros H H0. - elim (Plt_1 _ H0). - apply Plt_lt_succ. - destruct (Pcompare_p_Sq m p) as (H',_); destruct (H' H0); subst; auto. -Qed. - -Theorem Plt_ind : forall (A : positive -> Prop) (n : positive), - A (Psucc n) -> - (forall m : positive, n < m -> A m -> A (Psucc m)) -> - forall m : positive, n < m -> A m. -Proof. - intros A n AB AS m. induction m using Pind; intros H. - elim (Plt_1 _ H). - 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. - -(** Strict order and operations *) - -Lemma Pplus_lt_mono_l : forall p q r, q p+q < p+r. -Proof. - induction p using Prect. - intros q r. rewrite <- 2 Pplus_one_succ_l. apply Psucc_lt_compat. - intros q r. rewrite 2 Pplus_succ_permute_l. - eapply iff_trans; [ eapply IHp | eapply Psucc_lt_compat ]. -Qed. - -Lemma Pplus_lt_mono : forall p q r s, p r p+r p*q < p*r. -Proof. - induction p using Prect; auto. - intros q r H. rewrite 2 Pmult_Sn_m. - apply Pplus_lt_mono; auto. -Qed. - -Lemma Pmult_lt_mono : forall p q r s, p r p*r < q*s. -Proof. - intros. apply Plt_trans with (p*s). - now apply Pmult_lt_mono_l. - rewrite (Pmult_comm p), (Pmult_comm q). now apply Pmult_lt_mono_l. -Qed. - -Lemma Plt_plus_r : forall p q, p < p+q. -Proof. - induction q using Prect. - rewrite <- Pplus_one_succ_r. apply Pcompare_p_Sp. - apply Plt_trans with (p+q); auto. - apply Pplus_lt_mono_l, Pcompare_p_Sp. -Qed. - -Lemma Plt_not_plus_l : forall p q, ~ p+q < p. -Proof. - intros p q H. elim (Plt_irrefl p). - apply Plt_trans with (p+q); auto using Plt_plus_r. -Qed. - - -(**********************************************************************) -(** Properties of subtraction on binary positive numbers *) - -Lemma Ppred_minus : forall p, Ppred p = Pminus p 1. -Proof. - destruct p; auto. -Qed. - -Definition Ppred_mask (p : positive_mask) := -match p with -| IsPos 1 => IsNul -| IsPos q => IsPos (Ppred q) -| IsNul => IsNeg -| IsNeg => IsNeg -end. - -Lemma Pminus_mask_succ_r : - forall p q : positive, Pminus_mask p (Psucc q) = Pminus_mask_carry p q. -Proof. - induction p ; destruct q; simpl; f_equal; auto; destruct p; auto. -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; - 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; - rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. - destruct (Pminus_mask p q) as [|[r|r| ]|]; auto. -Qed. - -Lemma double_eq_zero_inversion : - forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul. -Proof. - destruct p; simpl; intros; trivial; discriminate. -Qed. - -Lemma double_plus_one_zero_discr : - forall p:positive_mask, Pdouble_plus_one_mask p <> IsNul. -Proof. - destruct p; discriminate. -Qed. - -Lemma double_plus_one_eq_one_inversion : - forall p:positive_mask, Pdouble_plus_one_mask p = IsPos 1 -> p = IsNul. -Proof. - destruct p; simpl; intros; trivial; discriminate. -Qed. - -Lemma double_eq_one_discr : - forall p:positive_mask, Pdouble_mask p <> IsPos 1. -Proof. - destruct p; discriminate. -Qed. - -Theorem Pminus_mask_diag : forall p:positive, Pminus_mask p p = IsNul. -Proof. - induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto. -Qed. - -Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg. -Proof. - induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto. -Qed. - -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; - specialize IHp with q. - destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto. - destruct (Pminus_mask p q); simpl; auto; try discriminate. - destruct (Pminus_mask_carry p q); simpl; auto; try discriminate. - destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto. -Qed. - -Lemma ZL10 : - forall p q:positive, - Pminus_mask p q = IsPos 1 -> Pminus_mask_carry p q = IsNul. -Proof. - induction p; intros [q|q| ] H; simpl in *; try discriminate. - elim (double_eq_one_discr _ H). - rewrite (double_plus_one_eq_one_inversion _ H); auto. - rewrite (double_plus_one_eq_one_inversion _ H); auto. - elim (double_eq_one_discr _ H). - destruct p; simpl; auto; discriminate. -Qed. - -(** Properties of subtraction valid only for x>y *) - -Lemma Pminus_mask_Gt : - forall p q:positive, - (p ?= q) Eq = Gt -> - exists h : positive, - 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 *; - try discriminate H. - (* 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|]]. - rewrite ZL10; subst; auto. - rewrite W; simpl; destruct r; auto; elim NE; auto. - (* p~1, q~0 *) - destruct (Pcompare_Gt_Gt _ _ H) as [H'|H']; clear H; rename H' into H. - destruct (IHp q H) as (r & U & V & W); exists (r~1); rewrite ?U, ?V; auto. - exists 1; subst; rewrite Pminus_mask_diag; auto. - (* p~1, 1 *) - exists (p~0); auto. - (* p~0, q~1 *) - destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as (r & U & V & W). - destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]]. - exists 1; subst; rewrite ZL10, Pplus_one_succ_r; auto. - exists ((Ppred r)~1); rewrite W, Pplus_carry_pred_eq_plus, V; auto. - (* p~0, q~0 *) - 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|]]. - rewrite ZL10; subst; auto. - rewrite W; simpl; destruct r; auto; elim NE; auto. - (* p~0, 1 *) - exists (Pdouble_minus_one p); repeat split; destruct p; simpl; auto. - rewrite Psucc_o_double_minus_one_eq_xO; auto. -Qed. - -Theorem Pplus_minus : - forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p. -Proof. - intros p q H; destruct (Pminus_mask_Gt p q H) as (r & U & V & _). - unfold Pminus; rewrite U; simpl; auto. -Qed. - -(** When x Pminus_mask p q = IsNeg. -Proof. - unfold Plt; induction p as [p IHp|p IHp| ]; destruct q; simpl; intros; - try discriminate; try rewrite IHp; auto. - apply Pcompare_Gt_Lt; auto. - destruct (Pcompare_Lt_Lt _ _ H). - rewrite Pminus_mask_IsNeg; simpl; auto. - subst; rewrite Pminus_mask_carry_diag; auto. -Qed. - -Lemma Pminus_Lt : forall p q:positive, p p-q = 1. -Proof. - intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto. -Qed. - -(** The substraction of x by x returns 1 *) - -Lemma Pminus_Eq : forall p:positive, p-p = 1. -Proof. - intros; unfold Pminus; rewrite Pminus_mask_diag; auto. -Qed. - -(** Number of digits in a number *) - -Fixpoint Psize (p:positive) : nat := - match p with - | 1 => S O - | p~1 => S (Psize p) - | p~0 => S (Psize p) - end. - -Lemma Psize_monotone : forall p q, (p?=q) Eq = Lt -> (Psize p <= Psize q)%nat. -Proof. - assert (le0 : forall n, (0<=n)%nat) by (induction n; auto). - assert (leS : forall n m, (n<=m -> S n <= S m)%nat) by (induction 1; auto). - induction p; destruct q; simpl; auto; intros; try discriminate. - intros; generalize (Pcompare_Gt_Lt _ _ H); auto. - intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto. -Qed. - - - - - diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v deleted file mode 100644 index 1c4cde6f5..000000000 --- a/theories/NArith/POrderedType.v +++ /dev/null @@ -1,60 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 deleted file mode 100644 index 2f753a4c9..000000000 --- a/theories/NArith/Pminmax.v +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 deleted file mode 100644 index 715c4484d..000000000 --- a/theories/NArith/Pnat.v +++ /dev/null @@ -1,460 +0,0 @@ -(* -*- coding: utf-8 -*- *) -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* n + n < m + m. -Proof. -intros m n H; apply lt_trans with (m := m + n); - [ apply plus_lt_compat_l with (1 := H) - | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. -Qed. - -Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m. -Proof. -intros m n H; apply le_lt_trans with (m := m + n); - [ change (m + m < m + n) in |- *; apply plus_lt_compat_l with (1 := H) - | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. -Qed. - -(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed - from [compare] on [positive]) - - Part 1: [lt] on [positive] is finer than [lt] on [nat] -*) - -Lemma nat_of_P_lt_Lt_compare_morphism : - 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; - [ unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; do 2 rewrite ZL6; - apply ZL7; apply H; simpl in H2; assumption - | unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; apply ZL8; - apply H; simpl in H2; apply Pcompare_Gt_Lt; assumption - | simpl in |- *; discriminate H2 - | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - elim (Pcompare_Lt_Lt p q H2); - [ intros H3; apply lt_S; apply ZL7; apply H; apply H3 - | intros E; rewrite E; apply lt_n_Sn ] - | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - 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 |- *; - 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; - apply lt_n_S; apply lt_O_Sn - | simpl in |- *; discriminate H2 ]. -Qed. - -(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed - from [compare] on [positive]) - - Part 1: [gt] on [positive] is finer than [gt] on [nat] -*) - -Lemma nat_of_P_gt_Gt_compare_morphism : - forall p q:positive, (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q. -Proof. -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 - from [compare] on [positive]) - - Part 2: [lt] on [nat] is finer than [lt] on [positive] -*) - -Lemma nat_of_P_lt_Lt_compare_complement_morphism : - forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt. -Proof. - 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 - from [compare] on [positive]) - - Part 2: [gt] on [nat] is finer than [gt] on [positive] -*) - -Lemma nat_of_P_gt_Gt_compare_complement_morphism : - forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt. -Proof. - 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. -induction p; simpl in |- *; auto with arith. -intro m; apply le_trans with (m + m); auto with arith. -Qed. - -Lemma lt_O_nat_of_P : forall p:positive, 0 < nat_of_P p. -intro; unfold nat_of_P in |- *; apply lt_le_trans with 1; auto with arith. -apply le_Pmult_nat. -Qed. - -(** Pmult_nat permutes with multiplication *) - -Lemma Pmult_nat_mult_permute : - forall (p:positive) (n m:nat), Pmult_nat p (m * n) = m * Pmult_nat p n. -Proof. - simple induction p. intros. simpl in |- *. rewrite mult_plus_distr_l. rewrite <- (mult_plus_distr_l m n n). - rewrite (H (n + n) m). reflexivity. - intros. simpl in |- *. rewrite <- (mult_plus_distr_l m n n). apply H. - trivial. -Qed. - -Lemma Pmult_nat_2_mult_2_permute : - forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1. -Proof. - intros. rewrite <- Pmult_nat_mult_permute. reflexivity. -Qed. - -Lemma Pmult_nat_4_mult_2_permute : - forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2. -Proof. - intros. rewrite <- Pmult_nat_mult_permute. reflexivity. -Qed. - -(** Mapping of xH, xO and xI through [nat_of_P] *) - -Lemma nat_of_P_xH : nat_of_P 1 = 1. -Proof. - reflexivity. -Qed. - -Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p. -Proof. - 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. - 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 - binary positive numbers *) - -(** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *) - -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. -induction n as [|n H]. -reflexivity. -simpl; rewrite nat_of_P_succ_morphism, H; auto. -Qed. - -(** Miscellaneous lemmas on [P_of_succ_nat] *) - -Lemma ZL3 : - forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n). -Proof. -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. -induction n as [| n H]; simpl; - [ auto with arith - | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H; - auto with arith ]. -Qed. - -(** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *) - -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. -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 - on [positive] *) - -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; 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 - 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) 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. - - -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; - 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 |- *; - apply le_n_S; apply le_plus_r. -Qed. - -(** Comparison and subtraction *) - -Lemma Pcompare_minus_r : - forall p q r:positive, - (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; - [ rewrite nat_of_P_minus_morphism; - [ apply plus_lt_reg_l with (p := nat_of_P q); rewrite le_plus_minus_r; - [ 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; - assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; - assumption ] - | assumption ] - | assumption ]. -Qed. - -Lemma Pcompare_minus_l : - forall p q r:positive, - (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; - [ rewrite nat_of_P_minus_morphism; - [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z); - rewrite le_plus_minus_r; - [ rewrite le_plus_minus_r; - [ apply nat_of_P_lt_Lt_compare_morphism; assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; - assumption ] - | assumption ] - | assumption ]. -Qed. - -(** Distributivity of multiplication over subtraction *) - -Theorem Pmult_minus_distr_l : - forall p q 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; - [ rewrite nat_of_P_minus_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 |- *; - 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 ]. -Qed. diff --git a/theories/NArith/Psqrt.v b/theories/NArith/Psqrt.v deleted file mode 100644 index 1d85f14a2..000000000 --- a/theories/NArith/Psqrt.v +++ /dev/null @@ -1,123 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* false | _ => true end. - -(** A Square Root function for positive numbers *) - -(** We procede by blocks of two digits : if p is written qbb' - then sqrt(p) will be sqrt(q)~0 or sqrt(q)~1. - For deciding easily in which case we are, we store the remainder - (as a positive_mask, since it can be null). - Instead of copy-pasting the following code four times, we - factorize as an auxiliary function, with f and g being either - xO or xI depending of the initial digits. - NB: (Pminus_mask (g (f 1)) 4) is a hack, morally it's g (f 0). -*) - -Definition Psqrtrem_step (f g:positive->positive) p := - match p with - | (s, IsPos r) => - let s' := s~0~1 in - let r' := g (f r) in - if Pleb s' r' then (s~1, Pminus_mask r' s') - else (s~0, IsPos r') - | (s,_) => (s~0, Pminus_mask (g (f 1)) 4) - end. - -Fixpoint Psqrtrem p : positive * positive_mask := - match p with - | 1 => (1,IsNul) - | 2 => (1,IsPos 1) - | 3 => (1,IsPos 2) - | p~0~0 => Psqrtrem_step xO xO (Psqrtrem p) - | p~0~1 => Psqrtrem_step xO xI (Psqrtrem p) - | p~1~0 => Psqrtrem_step xI xO (Psqrtrem p) - | p~1~1 => Psqrtrem_step xI xI (Psqrtrem p) - end. - -Definition Psqrt p := fst (Psqrtrem p). - -(** An inductive relation for specifying sqrt results *) - -Inductive PSQRT : positive*positive_mask -> positive -> Prop := - | PSQRT_exact : forall s x, x=s*s -> PSQRT (s,IsNul) x - | PSQRT_approx : forall s r x, x=s*s+r -> r <= s~0 -> PSQRT (s,IsPos r) x. - -(** Correctness proofs *) - -Lemma Psqrtrem_step_spec : forall f g p x, - (f=xO \/ f=xI) -> (g=xO \/ g=xI) -> - PSQRT p x -> PSQRT (Psqrtrem_step f g p) (g (f x)). -Proof. -intros f g _ _ Hf Hg [ s _ -> | s r _ -> Hr ]. -(* exact *) -unfold Psqrtrem_step. -destruct Hf,Hg; subst; simpl Pminus_mask; - constructor; try discriminate; now rewrite Psquare_xO. -(* approx *) -assert (Hfg : forall p q, g (f (p+q)) = p~0~0 + g (f q)) - by (intros; destruct Hf, Hg; now subst). -unfold Psqrtrem_step. unfold Pleb. -case Pcompare_spec; [intros EQ | intros LT | intros GT]. -(* - EQ *) -rewrite <- EQ. rewrite Pminus_mask_diag. -destruct Hg; subst g; try discriminate. -destruct Hf; subst f; try discriminate. -injection EQ; clear EQ; intros <-. -constructor. now rewrite Psquare_xI. -(* - LT *) -destruct (Pminus_mask_Gt (g (f r)) (s~0~1)) as (y & -> & H & _). -change Eq with (CompOpp Eq). now rewrite <- Pcompare_antisym, LT. -constructor. -rewrite Hfg, <- H. now rewrite Psquare_xI, Pplus_assoc. -apply Ple_lteq, Pcompare_p_Sq in Hr; change (r < s~1) in Hr. -apply Ple_lteq, Pcompare_p_Sq; change (y < s~1~1). -apply Pplus_lt_mono_l with (s~0~1). -rewrite H. simpl. rewrite Pplus_carry_spec, Pplus_diag. simpl. -set (s1:=s~1) in *; clearbody s1. -destruct Hf,Hg; subst; red; simpl; - apply Hr || apply Pcompare_eq_Lt, Hr. -(* - GT *) -constructor. -rewrite Hfg. now rewrite Psquare_xO. -apply Ple_lteq, Pcompare_p_Sq, GT. -Qed. - -Lemma Psqrtrem_spec : forall p, PSQRT (Psqrtrem p) p. -Proof. -fix 1. - destruct p; try destruct p; try (constructor; easy); - apply Psqrtrem_step_spec; auto. -Qed. - -Lemma Psqrt_spec : forall p, - let s := Psqrt p in s*s <= p < (Psucc s)*(Psucc s). -Proof. - intros p. simpl. - assert (H:=Psqrtrem_spec p). - unfold Psqrt in *. destruct Psqrtrem as (s,rm); simpl. - inversion_clear H; subst. - (* exact *) - split. red. rewrite Pcompare_refl. discriminate. - apply Pmult_lt_mono; apply Pcompare_p_Sp. - (* approx *) - split. - apply Ple_lteq; left. apply Plt_plus_r. - rewrite (Pplus_one_succ_l). - rewrite Pmult_plus_distr_r, !Pmult_plus_distr_l. - rewrite !Pmult_1_r. simpl (1*s). - rewrite <- Pplus_assoc, (Pplus_assoc s s), Pplus_diag, Pplus_assoc. - rewrite (Pplus_comm (_+_)). apply Pplus_lt_mono_l. - rewrite <- Pplus_one_succ_l. now apply Pcompare_p_Sq, Ple_lteq. -Qed. diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex index 83eed970e..bf39bc36c 100644 --- a/theories/NArith/intro.tex +++ b/theories/NArith/intro.tex @@ -1,4 +1,4 @@ -\section{Binary positive and non negative integers : NArith}\label{NArith} +\section{Binary natural numbers : NArith}\label{NArith} Here are defined various arithmetical notions and their properties, similar to those of {\tt Arith}. diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget index 0caf0b249..1797b25e4 100644 --- a/theories/NArith/vo.itarget +++ b/theories/NArith/vo.itarget @@ -1,13 +1,8 @@ BinNat.vo -BinPos.vo NArith.vo Ndec.vo Ndigits.vo Ndist.vo Nnat.vo Ndiv_def.vo -Pnat.vo -POrderedType.vo -Pminmax.vo -Psqrt.vo Nsqrt_def.vo diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v new file mode 100644 index 000000000..663233c57 --- /dev/null +++ b/theories/PArith/BinPos.v @@ -0,0 +1,1255 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* positive +| xO : positive -> positive +| xH : positive. + +(** Declare binding key for scope positive_scope *) + +Delimit Scope positive_scope with positive. + +(** Automatically open scope positive_scope for type positive, xO and xI *) + +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)) + for the number 6 (which is 110 in binary notation). +*) + +Notation "p ~ 1" := (xI p) + (at level 7, left associativity, format "p '~' '1'") : positive_scope. +Notation "p ~ 0" := (xO p) + (at level 7, left associativity, format "p '~' '0'") : positive_scope. + +Open Local Scope positive_scope. + +(* In the current file, [xH] cannot yet be written as [1], since the + interpretation of positive numerical constants is not available + yet. We fix this here with an ad-hoc temporary notation. *) + +Notation Local "1" := xH (at level 7). + +(** Successor *) + +Fixpoint Psucc (x:positive) : positive := + match x with + | p~1 => (Psucc p)~0 + | p~0 => p~1 + | 1 => 1~0 + end. + +(** Addition *) + +Set Boxed Definitions. + +Fixpoint Pplus (x y:positive) : positive := + match x, y with + | p~1, q~1 => (Pplus_carry p q)~0 + | p~1, q~0 => (Pplus p q)~1 + | p~1, 1 => (Psucc p)~0 + | p~0, q~1 => (Pplus p q)~1 + | p~0, q~0 => (Pplus p q)~0 + | p~0, 1 => p~1 + | 1, q~1 => (Psucc q)~0 + | 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 + | p~1, q~0 => (Pplus_carry p q)~0 + | p~1, 1 => (Psucc p)~1 + | p~0, q~1 => (Pplus_carry p q)~0 + | p~0, q~0 => (Pplus p q)~1 + | p~0, 1 => (Psucc p)~0 + | 1, q~1 => (Psucc q)~1 + | 1, q~0 => (Psucc q)~0 + | 1, 1 => 1~1 + end. + +Unset Boxed Definitions. + +Infix "+" := Pplus : positive_scope. + +Definition Piter_op {A}(op:A->A->A) := + fix iter (p:positive)(a:A) : A := + match p with + | 1 => a + | p~0 => iter p (op a a) + | p~1 => op a (iter p (op a a)) + end. + +Lemma Piter_op_succ : forall A (op:A->A->A), + (forall x y z, op x (op y z) = op (op x y) z) -> + forall p a, + Piter_op op (Psucc p) a = op a (Piter_op op p a). +Proof. + induction p; simpl; intros; trivial. + rewrite H. apply IHp. +Qed. + +(** From binary positive numbers to Peano natural numbers *) + +Definition Pmult_nat : positive -> nat -> nat := + Eval unfold Piter_op in (* for compatibility *) + Piter_op plus. + +Definition nat_of_P (x:positive) := Pmult_nat x (S O). + +(** From Peano natural numbers to binary positive numbers *) + +Fixpoint P_of_succ_nat (n:nat) : positive := + match n with + | O => 1 + | S x => Psucc (P_of_succ_nat x) + end. + +(** Operation x -> 2*x-1 *) + +Fixpoint Pdouble_minus_one (x:positive) : positive := + match x with + | p~1 => p~0~1 + | p~0 => (Pdouble_minus_one p)~1 + | 1 => 1 + end. + +(** Predecessor *) + +Definition Ppred (x:positive) := + match x with + | p~1 => p~0 + | p~0 => Pdouble_minus_one p + | 1 => 1 + end. + +(** An auxiliary type for subtraction *) + +Inductive positive_mask : Set := +| IsNul : positive_mask +| IsPos : positive -> positive_mask +| IsNeg : positive_mask. + +(** Operation x -> 2*x+1 *) + +Definition Pdouble_plus_one_mask (x:positive_mask) := + match x with + | IsNul => IsPos 1 + | IsNeg => IsNeg + | IsPos p => IsPos p~1 + end. + +(** Operation x -> 2*x *) + +Definition Pdouble_mask (x:positive_mask) := + match x with + | IsNul => IsNul + | IsNeg => IsNeg + | IsPos p => IsPos p~0 + end. + +(** Operation x -> 2*x-2 *) + +Definition Pdouble_minus_two (x:positive) := + match x with + | p~1 => IsPos p~0~0 + | p~0 => IsPos (Pdouble_minus_one p)~0 + | 1 => IsNul + end. + +(** Subtraction of binary positive numbers into a positive numbers mask *) + +Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask := + match x, y with + | p~1, q~1 => Pdouble_mask (Pminus_mask p q) + | p~1, q~0 => Pdouble_plus_one_mask (Pminus_mask p q) + | p~1, 1 => IsPos p~0 + | p~0, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q) + | p~0, q~0 => Pdouble_mask (Pminus_mask p q) + | p~0, 1 => IsPos (Pdouble_minus_one p) + | 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) + | p~1, q~0 => Pdouble_mask (Pminus_mask p q) + | p~1, 1 => IsPos (Pdouble_minus_one p) + | p~0, q~1 => Pdouble_mask (Pminus_mask_carry p q) + | p~0, q~0 => Pdouble_plus_one_mask (Pminus_mask_carry p q) + | p~0, 1 => Pdouble_minus_two p + | 1, _ => IsNeg + end. + +(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *) + +Definition Pminus (x y:positive) := + match Pminus_mask x y with + | IsPos z => z + | _ => 1 + end. + +Infix "-" := Pminus : positive_scope. + +(** Multiplication on binary positive numbers *) + +Fixpoint Pmult (x y:positive) : positive := + match x with + | p~1 => y + (Pmult p y)~0 + | p~0 => (Pmult p y)~0 + | 1 => y + end. + +Infix "*" := Pmult : positive_scope. + +(** Division by 2 rounded below but for 1 *) + +Definition Pdiv2 (z:positive) := + match z with + | 1 => 1 + | p~0 => p + | p~1 => p + end. + +Infix "/" := Pdiv2 : positive_scope. + +(** Comparison on binary positive numbers *) + +Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison := + match x, y with + | p~1, q~1 => Pcompare p q r + | p~1, q~0 => Pcompare p q Gt + | p~1, 1 => Gt + | p~0, q~1 => Pcompare p q Lt + | p~0, q~0 => Pcompare p q r + | p~0, 1 => Gt + | 1, q~1 => Lt + | 1, q~0 => Lt + | 1, 1 => r + end. + +Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope. + +Definition Plt (x y:positive) := (Pcompare x y Eq) = Lt. +Definition Pgt (x y:positive) := (Pcompare x y Eq) = Gt. +Definition Ple (x y:positive) := (Pcompare x y Eq) <> Gt. +Definition Pge (x y:positive) := (Pcompare x y Eq) <> Lt. + +Infix "<=" := Ple : positive_scope. +Infix "<" := Plt : positive_scope. +Infix ">=" := Pge : positive_scope. +Infix ">" := Pgt : positive_scope. + +Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope. +Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope. +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 + | Gt => p' + end. + +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. + +(**********************************************************************) +(** Decidability of equality on binary positive numbers *) + +Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +(* begin hide *) +Corollary ZL11 : forall p:positive, p = 1 \/ p <> 1. +Proof. + intro; edestruct positive_eq_dec; eauto. +Qed. +(* end hide *) + +(**********************************************************************) +(** Properties of successor on binary positive numbers *) + +(** Specification of [xI] in term of [Psucc] and [xO] *) + +Lemma xI_succ_xO : forall p:positive, p~1 = Psucc p~0. +Proof. + reflexivity. +Qed. + +Lemma Psucc_discr : forall p:positive, p <> Psucc p. +Proof. + destruct p; discriminate. +Qed. + +(** Successor and double *) + +Lemma Psucc_o_double_minus_one_eq_xO : + forall p:positive, Psucc (Pdouble_minus_one p) = p~0. +Proof. + induction p; simpl; f_equal; auto. +Qed. + +Lemma Pdouble_minus_one_o_succ_eq_xI : + forall p:positive, Pdouble_minus_one (Psucc p) = p~1. +Proof. + induction p; simpl; f_equal; auto. +Qed. + +Lemma xO_succ_permute : + forall p:positive, (Psucc p)~0 = Psucc (Psucc p~0). +Proof. + induction p; simpl; auto. +Qed. + +Lemma double_moins_un_xO_discr : + forall p:positive, Pdouble_minus_one p <> p~0. +Proof. + destruct p; discriminate. +Qed. + +(** Successor and predecessor *) + +Lemma Psucc_not_one : forall p:positive, Psucc p <> 1. +Proof. + destruct p; discriminate. +Qed. + +Lemma Ppred_succ : forall p:positive, Ppred (Psucc p) = p. +Proof. + intros [[p|p| ]|[p|p| ]| ]; simpl; auto. + f_equal; apply Pdouble_minus_one_o_succ_eq_xI. +Qed. + +Lemma Psucc_pred : forall p:positive, p = 1 \/ Psucc (Ppred p) = p. +Proof. + induction p; simpl; auto. + right; apply Psucc_o_double_minus_one_eq_xO. +Qed. + +Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). + +(** Injectivity of successor *) + +Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q. +Proof. + induction p; intros [q|q| ] H; simpl in *; destr_eq H; f_equal; auto. + elim (Psucc_not_one p); auto. + elim (Psucc_not_one q); auto. +Qed. + +(**********************************************************************) +(** Properties of addition on binary positive numbers *) + +(** Specification of [Psucc] in term of [Pplus] *) + +Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + 1. +Proof. + destruct p; reflexivity. +Qed. + +Lemma Pplus_one_succ_l : forall p:positive, Psucc p = 1 + p. +Proof. + destruct p; reflexivity. +Qed. + +(** Specification of [Pplus_carry] *) + +Theorem Pplus_carry_spec : + forall p q:positive, Pplus_carry p q = Psucc (p + q). +Proof. + induction p; destruct q; simpl; f_equal; auto. +Qed. + +(** Commutativity *) + +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. + +(** 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; + auto using Pplus_one_succ_r; rewrite Pplus_carry_spec; auto. +Qed. + +Theorem Pplus_succ_permute_l : + forall p q:positive, Psucc p + q = Psucc (p + q). +Proof. + intros p q; rewrite Pplus_comm, (Pplus_comm p); + apply Pplus_succ_permute_r. +Qed. + +Theorem Pplus_carry_pred_eq_plus : + forall p q:positive, q <> 1 -> Pplus_carry p (Ppred q) = p + q. +Proof. + intros p q H; rewrite Pplus_carry_spec, <- Pplus_succ_permute_r; f_equal. + destruct (Psucc_pred q); [ elim H; assumption | assumption ]. +Qed. + +(** No neutral for addition on strictly positive numbers *) + +Lemma Pplus_no_neutral : forall p q:positive, q + p <> p. +Proof. + induction p as [p IHp|p IHp| ]; intros [q|q| ] H; + destr_eq H; apply (IHp q H). +Qed. + +Lemma Pplus_carry_no_neutral : + forall p q:positive, Pplus_carry q p <> Psucc p. +Proof. + intros p q H; elim (Pplus_no_neutral p q). + apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption. +Qed. + +(** Simplification *) + +Lemma Pplus_carry_plus : + forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s. +Proof. + intros p q r s H; apply Psucc_inj; do 2 rewrite <- Pplus_carry_spec; + assumption. +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; + contradict H; auto using Pplus_carry_no_neutral. + 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. + +Lemma Pplus_reg_l : forall p q r:positive, p + q = p + r -> q = r. +Proof. + intros p q r H; apply Pplus_reg_r with (r:=p). + rewrite (Pplus_comm r), (Pplus_comm q); assumption. +Qed. + +Lemma Pplus_carry_reg_r : + forall p q r:positive, Pplus_carry p r = Pplus_carry q r -> p = q. +Proof. + intros p q r H; apply Pplus_reg_r with (r:=r); apply Pplus_carry_plus; + assumption. +Qed. + +Lemma Pplus_carry_reg_l : + forall p q r:positive, Pplus_carry p q = Pplus_carry p r -> q = r. +Proof. + intros p q r H; apply Pplus_reg_r with (r:=p); + rewrite (Pplus_comm r), (Pplus_comm q); apply Pplus_carry_plus; assumption. +Qed. + +(** Addition on positive is associative *) + +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, + ?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, + ?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. + +(** Commutation of addition with the double of a positive number *) + +Lemma Pplus_xO : forall m n : positive, (m + n)~0 = m~0 + n~0. +Proof. + destruct n; destruct m; simpl; auto. +Qed. + +Lemma Pplus_xI_double_minus_one : + forall p q:positive, (p + q)~0 = p~1 + Pdouble_minus_one q. +Proof. + intros; change (p~1) with (p~0 + 1). + rewrite <- Pplus_assoc, <- Pplus_one_succ_l, Psucc_o_double_minus_one_eq_xO. + reflexivity. +Qed. + +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, + ?Pplus_xI_double_minus_one; try reflexivity. + rewrite IHp; auto. + rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity. +Qed. + +(** Misc *) + +Lemma Pplus_diag : forall p:positive, p + p = p~0. +Proof. + induction p as [p IHp| p IHp| ]; simpl; + try rewrite ?Pplus_carry_spec, ?IHp; reflexivity. +Qed. + +(**********************************************************************) +(** Peano induction and recursion on binary positive positive numbers *) +(** (a nice proof from Conor McBride, see "The view from the left") *) + +Inductive PeanoView : positive -> Type := +| PeanoOne : PeanoView 1 +| PeanoSucc : forall p, PeanoView p -> PeanoView (Psucc p). + +Fixpoint peanoView_xO p (q:PeanoView p) : PeanoView (p~0) := + match q in PeanoView x return PeanoView (x~0) with + | PeanoOne => PeanoSucc _ PeanoOne + | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xO _ q)) + end. + +Fixpoint peanoView_xI p (q:PeanoView p) : PeanoView (p~1) := + match q in PeanoView x return PeanoView (x~1) with + | PeanoOne => PeanoSucc _ (PeanoSucc _ PeanoOne) + | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xI _ q)) + end. + +Fixpoint peanoView p : PeanoView p := + match p return PeanoView p with + | 1 => PeanoOne + | p~0 => peanoView_xO p (peanoView p) + | p~1 => peanoView_xI p (peanoView p) + end. + +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 + | PeanoOne => a + | PeanoSucc _ q => f _ (iter _ q) + end). + +Require Import Eqdep_dec EqdepFacts. + +Theorem eq_dep_eq_positive : + 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'. +Proof. + 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'. + intro. destruct p; discriminate. + intro. unfold p0 in H. apply Psucc_inj in H. + generalize q'. rewrite H. intro. + rewrite (IHq q'0). + trivial. + trivial. +Qed. + +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), + Prect P a f (Psucc p) = f _ (Prect P a f p). +Proof. + intros. + unfold Prect. + rewrite (PeanoViewUnique _ (peanoView (Psucc p)) (PeanoSucc _ (peanoView p))). + trivial. +Qed. + +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. +Qed. + +Definition Prec (P:positive->Set) := Prect P. + +(** Peano induction *) + +Definition Pind (P:positive->Prop) := Prect P. + +(** Peano case analysis *) + +Theorem Pcase : + forall P:positive -> Prop, + P 1 -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p. +Proof. + intros; apply Pind; auto. +Qed. + +(**********************************************************************) +(** Properties of multiplication on binary positive numbers *) + +(** One is right neutral for multiplication *) + +Lemma Pmult_1_r : forall p:positive, p * 1 = p. +Proof. + induction p; simpl; f_equal; auto. +Qed. + +(** Successor and multiplication *) + +Lemma Pmult_Sn_m : forall n m : positive, (Psucc n) * m = m + n * m. +Proof. + induction n as [n IHn | n IHn | ]; simpl; intro m. + rewrite IHn, Pplus_assoc, Pplus_diag, <-Pplus_xO; reflexivity. + reflexivity. + symmetry; apply Pplus_diag. +Qed. + +(** Right reduction properties for multiplication *) + +Lemma Pmult_xO_permute_r : forall p q:positive, p * q~0 = (p * q)~0. +Proof. + intros p q; induction p; simpl; do 2 (f_equal; auto). +Qed. + +Lemma Pmult_xI_permute_r : forall p q:positive, p * q~1 = p + (p * q)~0. +Proof. + intros p q; induction p as [p IHp|p IHp| ]; simpl; f_equal; auto. + rewrite IHp, 2 Pplus_assoc, (Pplus_comm p); reflexivity. +Qed. + +(** Commutativity of multiplication *) + +Theorem Pmult_comm : forall p q:positive, p * q = q * p. +Proof. + intros p q; induction q as [q IHq|q IHq| ]; simpl; try rewrite <- IHq; + auto using Pmult_xI_permute_r, Pmult_xO_permute_r, Pmult_1_r. +Qed. + +(** Distributivity of multiplication over addition *) + +Theorem Pmult_plus_distr_l : + forall p q r:positive, p * (q + r) = p * q + p * r. +Proof. + intros p q r; induction p as [p IHp|p IHp| ]; simpl. + rewrite IHp. set (m:=(p*q)~0). set (n:=(p*r)~0). + change ((p*q+p*r)~0) with (m+n). + rewrite 2 Pplus_assoc; f_equal. + rewrite <- 2 Pplus_assoc; f_equal. + apply Pplus_comm. + f_equal; auto. + reflexivity. +Qed. + +Theorem Pmult_plus_distr_r : + forall p q r:positive, (p + q) * r = p * r + q * r. +Proof. + intros p q r; do 3 rewrite Pmult_comm with (q:=r); apply Pmult_plus_distr_l. +Qed. + +(** Associativity of multiplication *) + +Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r. +Proof. + induction p as [p IHp| p IHp | ]; simpl; intros q r. + rewrite IHp; rewrite Pmult_plus_distr_r; reflexivity. + rewrite IHp; reflexivity. + reflexivity. +Qed. + +(** Parity properties of multiplication *) + +Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, p~1 * r <> q~0 * r. +Proof. + intros p q r; induction r; try discriminate. + rewrite 2 Pmult_xO_permute_r; intro H; destr_eq H; auto. +Qed. + +Lemma Pmult_xO_discr : forall p q:positive, p~0 * q <> q. +Proof. + intros p q; induction q; try discriminate. + rewrite Pmult_xO_permute_r; injection; assumption. +Qed. + +(** Simplification properties of multiplication *) + +Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q. +Proof. + induction p as [p IHp| p IHp| ]; intros [q|q| ] r H; + reflexivity || apply (f_equal (A:=positive)) || apply False_ind. + apply IHp with (r~0); simpl in *; + rewrite 2 Pmult_xO_permute_r; apply Pplus_reg_l with (1:=H). + apply Pmult_xI_mult_xO_discr with (1:=H). + simpl in H; rewrite Pplus_comm in H; apply Pplus_no_neutral with (1:=H). + symmetry in H; apply Pmult_xI_mult_xO_discr with (1:=H). + apply IHp with (r~0); simpl; rewrite 2 Pmult_xO_permute_r; assumption. + apply Pmult_xO_discr with (1:= H). + simpl in H; symmetry in H; rewrite Pplus_comm in H; + apply Pplus_no_neutral with (1:=H). + symmetry in H; apply Pmult_xO_discr with (1:=H). +Qed. + +Theorem Pmult_reg_l : forall p q r:positive, r * p = r * q -> p = q. +Proof. + intros p q r H; apply Pmult_reg_r with (r:=r). + rewrite (Pmult_comm p), (Pmult_comm q); assumption. +Qed. + +(** Inversion of multiplication *) + +Lemma Pmult_1_inversion_l : forall p q:positive, p * q = 1 -> p = 1. +Proof. + intros [p|p| ] [q|q| ] H; destr_eq H; auto. +Qed. + +(** Square *) + +Lemma Psquare_xO : forall p, p~0 * p~0 = (p*p)~0~0. +Proof. + intros. simpl. now rewrite Pmult_comm. +Qed. + +Lemma Psquare_xI : forall p, p~1 * p~1 = (p*p+p)~0~1. +Proof. + intros. simpl. rewrite Pmult_comm. simpl. f_equal. + rewrite Pplus_assoc, Pplus_diag. simpl. now rewrite Pplus_comm. +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 *) + +Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq. + induction p; auto. +Qed. + +(* A generalization of Pcompare_refl *) + +Theorem Pcompare_refl_id : forall (p : positive) (r : comparison), (p ?= p) r = r. + induction p; auto. +Qed. + +Theorem Pcompare_not_Eq : + forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq. +Proof. + induction p as [p IHp| p IHp| ]; intros [q| q| ]; split; simpl; auto; + discriminate || (elim (IHp q); auto). +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; + 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. + induction p; intros [q|q| ] H; simpl; auto; discriminate. +Qed. + +Lemma Pcompare_eq_Lt : + forall p q : positive, (p ?= q) Eq = Lt <-> (p ?= q) Gt = Lt. +Proof. + intros p q; split; [| apply Pcompare_Gt_Lt]. + revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate. +Qed. + +Lemma Pcompare_Lt_Gt : + forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt. +Proof. + induction p; intros [q|q| ] H; simpl; auto; discriminate. +Qed. + +Lemma Pcompare_eq_Gt : + forall p q : positive, (p ?= q) Eq = Gt <-> (p ?= q) Lt = Gt. +Proof. + intros p q; split; [| apply Pcompare_Lt_Gt]. + revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate. +Qed. + +Lemma Pcompare_Lt_Lt : + forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q. +Proof. + induction p as [p IHp| p IHp| ]; intros [q|q| ] H; simpl in *; auto; + destruct (IHp q H); subst; auto. +Qed. + +Lemma Pcompare_Lt_eq_Lt : + forall p q:positive, (p ?= q) Lt = Lt <-> (p ?= q) Eq = Lt \/ p = q. +Proof. + intros p q; split; [apply Pcompare_Lt_Lt |]. + intros [H|H]; [|subst; apply Pcompare_refl_id]. + revert q H; induction p; intros [q|q| ] H; simpl in *; + auto; discriminate. +Qed. + +Lemma Pcompare_Gt_Gt : + forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q. +Proof. + induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto; + destruct (IHp q H); subst; auto. +Qed. + +Lemma Pcompare_Gt_eq_Gt : + forall p q:positive, (p ?= q) Gt = Gt <-> (p ?= q) Eq = Gt \/ p = q. +Proof. + intros p q; split; [apply Pcompare_Gt_Gt |]. + intros [H|H]; [|subst; apply Pcompare_refl_id]. + revert q H; induction p; intros [q|q| ] H; simpl in *; + auto; discriminate. +Qed. + +Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt. +Proof. + destruct r; auto. +Qed. + +Ltac ElimPcompare c1 c2 := + elim (Dcompare ((c1 ?= c2) Eq)); + [ idtac | let x := fresh "H" in (intro x; case x; clear x) ]. + +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; + rewrite IHp; auto. +Qed. + +Lemma ZC1 : forall p q:positive, (p ?= q) Eq = Gt -> (q ?= p) Eq = Lt. +Proof. + intros p q H; change Eq with (CompOpp Eq). + rewrite <- Pcompare_antisym, H; reflexivity. +Qed. + +Lemma ZC2 : forall p q:positive, (p ?= q) Eq = Lt -> (q ?= p) Eq = Gt. +Proof. + intros p q H; change Eq with (CompOpp Eq). + rewrite <- Pcompare_antisym, H; reflexivity. +Qed. + +Lemma ZC3 : forall p q:positive, (p ?= q) Eq = Eq -> (q ?= p) Eq = Eq. +Proof. + intros p q H; change Eq with (CompOpp Eq). + rewrite <- Pcompare_antisym, H; reflexivity. +Qed. + +Lemma ZC4 : forall p q:positive, (p ?= q) Eq = CompOpp ((q ?= p) Eq). +Proof. + intros; change Eq at 1 with (CompOpp Eq). + 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. +Proof. + induction p; simpl in *; + [ elim (Pcompare_eq_Lt p (Psucc p)); auto | + apply Pcompare_refl_id | reflexivity]. +Qed. + +Theorem Pcompare_p_Sq : forall p q : positive, + (p ?= Psucc q) Eq = Lt <-> (p ?= q) Eq = Lt \/ p = q. +Proof. + intros p q; split. + (* -> *) + revert p q; induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; + try (left; reflexivity); try (right; reflexivity). + destruct (IHp q (Pcompare_Gt_Lt _ _ H)); subst; auto. + destruct (Pcompare_eq_Lt p q); auto. + destruct p; discriminate. + left; destruct (IHp q H); + [ elim (Pcompare_Lt_eq_Lt p q); auto | subst; apply Pcompare_refl_id]. + destruct (Pcompare_Lt_Lt p q H); subst; auto. + destruct p; discriminate. + (* <- *) + intros [H|H]; [|subst; apply Pcompare_p_Sp]. + revert q H; induction p; intros [q|q| ] H; simpl in *; + auto; try discriminate. + destruct (Pcompare_eq_Lt p (Psucc q)); auto. + apply Pcompare_Gt_Lt; auto. + destruct (Pcompare_Lt_Lt p q H); subst; auto using Pcompare_p_Sp. + destruct (Pcompare_Lt_eq_Lt p q); auto. +Qed. + +(** 1 is the least positive number *) + +Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt. +Proof. + destruct p; discriminate. +Qed. + +(** Properties of the strict order on positive numbers *) + +Lemma Plt_1 : forall p, ~ p < 1. +Proof. + exact Pcompare_1. +Qed. + +Lemma Plt_1_succ : forall n, 1 < Psucc n. +Proof. + intros. apply Pcompare_p_Sq. destruct n; auto. +Qed. + +Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m. +Proof. + unfold Plt; intros n m H; apply <- Pcompare_p_Sq; auto. +Qed. + +Lemma Psucc_lt_compat : forall n m, n < m <-> Psucc n < Psucc m. +Proof. + unfold Plt. induction n; destruct m; simpl; auto; split; try easy; intros. + now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, IHn, Pcompare_Gt_Lt. + now apply Pcompare_eq_Lt, IHn, Pcompare_p_Sq, Pcompare_Lt_eq_Lt. + destruct (Psucc n); discriminate. + now apply Pcompare_eq_Lt, Pcompare_p_Sq, Pcompare_Lt_eq_Lt. + now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, Pcompare_Gt_Lt. + destruct n; discriminate. + apply Plt_1_succ. + destruct m; auto. +Qed. + +Lemma Plt_irrefl : forall p : positive, ~ p < p. +Proof. + unfold Plt; intro p; rewrite Pcompare_refl; discriminate. +Qed. + +Lemma Plt_trans : forall n m p : positive, n < m -> m < p -> n < p. +Proof. + intros n m p; induction p using Pind; intros H H0. + elim (Plt_1 _ H0). + apply Plt_lt_succ. + destruct (Pcompare_p_Sq m p) as (H',_); destruct (H' H0); subst; auto. +Qed. + +Theorem Plt_ind : forall (A : positive -> Prop) (n : positive), + A (Psucc n) -> + (forall m : positive, n < m -> A m -> A (Psucc m)) -> + forall m : positive, n < m -> A m. +Proof. + intros A n AB AS m. induction m using Pind; intros H. + elim (Plt_1 _ H). + 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. + +(** Strict order and operations *) + +Lemma Pplus_lt_mono_l : forall p q r, q p+q < p+r. +Proof. + induction p using Prect. + intros q r. rewrite <- 2 Pplus_one_succ_l. apply Psucc_lt_compat. + intros q r. rewrite 2 Pplus_succ_permute_l. + eapply iff_trans; [ eapply IHp | eapply Psucc_lt_compat ]. +Qed. + +Lemma Pplus_lt_mono : forall p q r s, p r p+r p*q < p*r. +Proof. + induction p using Prect; auto. + intros q r H. rewrite 2 Pmult_Sn_m. + apply Pplus_lt_mono; auto. +Qed. + +Lemma Pmult_lt_mono : forall p q r s, p r p*r < q*s. +Proof. + intros. apply Plt_trans with (p*s). + now apply Pmult_lt_mono_l. + rewrite (Pmult_comm p), (Pmult_comm q). now apply Pmult_lt_mono_l. +Qed. + +Lemma Plt_plus_r : forall p q, p < p+q. +Proof. + induction q using Prect. + rewrite <- Pplus_one_succ_r. apply Pcompare_p_Sp. + apply Plt_trans with (p+q); auto. + apply Pplus_lt_mono_l, Pcompare_p_Sp. +Qed. + +Lemma Plt_not_plus_l : forall p q, ~ p+q < p. +Proof. + intros p q H. elim (Plt_irrefl p). + apply Plt_trans with (p+q); auto using Plt_plus_r. +Qed. + + +(**********************************************************************) +(** Properties of subtraction on binary positive numbers *) + +Lemma Ppred_minus : forall p, Ppred p = Pminus p 1. +Proof. + destruct p; auto. +Qed. + +Definition Ppred_mask (p : positive_mask) := +match p with +| IsPos 1 => IsNul +| IsPos q => IsPos (Ppred q) +| IsNul => IsNeg +| IsNeg => IsNeg +end. + +Lemma Pminus_mask_succ_r : + forall p q : positive, Pminus_mask p (Psucc q) = Pminus_mask_carry p q. +Proof. + induction p ; destruct q; simpl; f_equal; auto; destruct p; auto. +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; + 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; + rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. + destruct (Pminus_mask p q) as [|[r|r| ]|]; auto. +Qed. + +Lemma double_eq_zero_inversion : + forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul. +Proof. + destruct p; simpl; intros; trivial; discriminate. +Qed. + +Lemma double_plus_one_zero_discr : + forall p:positive_mask, Pdouble_plus_one_mask p <> IsNul. +Proof. + destruct p; discriminate. +Qed. + +Lemma double_plus_one_eq_one_inversion : + forall p:positive_mask, Pdouble_plus_one_mask p = IsPos 1 -> p = IsNul. +Proof. + destruct p; simpl; intros; trivial; discriminate. +Qed. + +Lemma double_eq_one_discr : + forall p:positive_mask, Pdouble_mask p <> IsPos 1. +Proof. + destruct p; discriminate. +Qed. + +Theorem Pminus_mask_diag : forall p:positive, Pminus_mask p p = IsNul. +Proof. + induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto. +Qed. + +Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg. +Proof. + induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto. +Qed. + +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; + specialize IHp with q. + destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto. + destruct (Pminus_mask p q); simpl; auto; try discriminate. + destruct (Pminus_mask_carry p q); simpl; auto; try discriminate. + destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto. +Qed. + +Lemma ZL10 : + forall p q:positive, + Pminus_mask p q = IsPos 1 -> Pminus_mask_carry p q = IsNul. +Proof. + induction p; intros [q|q| ] H; simpl in *; try discriminate. + elim (double_eq_one_discr _ H). + rewrite (double_plus_one_eq_one_inversion _ H); auto. + rewrite (double_plus_one_eq_one_inversion _ H); auto. + elim (double_eq_one_discr _ H). + destruct p; simpl; auto; discriminate. +Qed. + +(** Properties of subtraction valid only for x>y *) + +Lemma Pminus_mask_Gt : + forall p q:positive, + (p ?= q) Eq = Gt -> + exists h : positive, + 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 *; + try discriminate H. + (* 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|]]. + rewrite ZL10; subst; auto. + rewrite W; simpl; destruct r; auto; elim NE; auto. + (* p~1, q~0 *) + destruct (Pcompare_Gt_Gt _ _ H) as [H'|H']; clear H; rename H' into H. + destruct (IHp q H) as (r & U & V & W); exists (r~1); rewrite ?U, ?V; auto. + exists 1; subst; rewrite Pminus_mask_diag; auto. + (* p~1, 1 *) + exists (p~0); auto. + (* p~0, q~1 *) + destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as (r & U & V & W). + destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]]. + exists 1; subst; rewrite ZL10, Pplus_one_succ_r; auto. + exists ((Ppred r)~1); rewrite W, Pplus_carry_pred_eq_plus, V; auto. + (* p~0, q~0 *) + 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|]]. + rewrite ZL10; subst; auto. + rewrite W; simpl; destruct r; auto; elim NE; auto. + (* p~0, 1 *) + exists (Pdouble_minus_one p); repeat split; destruct p; simpl; auto. + rewrite Psucc_o_double_minus_one_eq_xO; auto. +Qed. + +Theorem Pplus_minus : + forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p. +Proof. + intros p q H; destruct (Pminus_mask_Gt p q H) as (r & U & V & _). + unfold Pminus; rewrite U; simpl; auto. +Qed. + +(** When x Pminus_mask p q = IsNeg. +Proof. + unfold Plt; induction p as [p IHp|p IHp| ]; destruct q; simpl; intros; + try discriminate; try rewrite IHp; auto. + apply Pcompare_Gt_Lt; auto. + destruct (Pcompare_Lt_Lt _ _ H). + rewrite Pminus_mask_IsNeg; simpl; auto. + subst; rewrite Pminus_mask_carry_diag; auto. +Qed. + +Lemma Pminus_Lt : forall p q:positive, p p-q = 1. +Proof. + intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto. +Qed. + +(** The substraction of x by x returns 1 *) + +Lemma Pminus_Eq : forall p:positive, p-p = 1. +Proof. + intros; unfold Pminus; rewrite Pminus_mask_diag; auto. +Qed. + +(** Number of digits in a number *) + +Fixpoint Psize (p:positive) : nat := + match p with + | 1 => S O + | p~1 => S (Psize p) + | p~0 => S (Psize p) + end. + +Lemma Psize_monotone : forall p q, (p?=q) Eq = Lt -> (Psize p <= Psize q)%nat. +Proof. + assert (le0 : forall n, (0<=n)%nat) by (induction n; auto). + assert (leS : forall n m, (n<=m -> S n <= S m)%nat) by (induction 1; auto). + induction p; destruct q; simpl; auto; intros; try discriminate. + intros; generalize (Pcompare_Gt_Lt _ _ H); auto. + intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto. +Qed. diff --git a/theories/PArith/PArith.v b/theories/PArith/PArith.v new file mode 100644 index 000000000..f453af386 --- /dev/null +++ b/theories/PArith/PArith.v @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/PArith/Pminmax.v b/theories/PArith/Pminmax.v new file mode 100644 index 000000000..2f753a4c9 --- /dev/null +++ b/theories/PArith/Pminmax.v @@ -0,0 +1,126 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/PArith/Pnat.v b/theories/PArith/Pnat.v new file mode 100644 index 000000000..715c4484d --- /dev/null +++ b/theories/PArith/Pnat.v @@ -0,0 +1,460 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* n + n < m + m. +Proof. +intros m n H; apply lt_trans with (m := m + n); + [ apply plus_lt_compat_l with (1 := H) + | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. +Qed. + +Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m. +Proof. +intros m n H; apply le_lt_trans with (m := m + n); + [ change (m + m < m + n) in |- *; apply plus_lt_compat_l with (1 := H) + | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. +Qed. + +(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed + from [compare] on [positive]) + + Part 1: [lt] on [positive] is finer than [lt] on [nat] +*) + +Lemma nat_of_P_lt_Lt_compare_morphism : + 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; + [ unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; do 2 rewrite ZL6; + apply ZL7; apply H; simpl in H2; assumption + | unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; apply ZL8; + apply H; simpl in H2; apply Pcompare_Gt_Lt; assumption + | simpl in |- *; discriminate H2 + | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; + elim (Pcompare_Lt_Lt p q H2); + [ intros H3; apply lt_S; apply ZL7; apply H; apply H3 + | intros E; rewrite E; apply lt_n_Sn ] + | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; + 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 |- *; + 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; + apply lt_n_S; apply lt_O_Sn + | simpl in |- *; discriminate H2 ]. +Qed. + +(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed + from [compare] on [positive]) + + Part 1: [gt] on [positive] is finer than [gt] on [nat] +*) + +Lemma nat_of_P_gt_Gt_compare_morphism : + forall p q:positive, (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q. +Proof. +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 + from [compare] on [positive]) + + Part 2: [lt] on [nat] is finer than [lt] on [positive] +*) + +Lemma nat_of_P_lt_Lt_compare_complement_morphism : + forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt. +Proof. + 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 + from [compare] on [positive]) + + Part 2: [gt] on [nat] is finer than [gt] on [positive] +*) + +Lemma nat_of_P_gt_Gt_compare_complement_morphism : + forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt. +Proof. + 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. +induction p; simpl in |- *; auto with arith. +intro m; apply le_trans with (m + m); auto with arith. +Qed. + +Lemma lt_O_nat_of_P : forall p:positive, 0 < nat_of_P p. +intro; unfold nat_of_P in |- *; apply lt_le_trans with 1; auto with arith. +apply le_Pmult_nat. +Qed. + +(** Pmult_nat permutes with multiplication *) + +Lemma Pmult_nat_mult_permute : + forall (p:positive) (n m:nat), Pmult_nat p (m * n) = m * Pmult_nat p n. +Proof. + simple induction p. intros. simpl in |- *. rewrite mult_plus_distr_l. rewrite <- (mult_plus_distr_l m n n). + rewrite (H (n + n) m). reflexivity. + intros. simpl in |- *. rewrite <- (mult_plus_distr_l m n n). apply H. + trivial. +Qed. + +Lemma Pmult_nat_2_mult_2_permute : + forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1. +Proof. + intros. rewrite <- Pmult_nat_mult_permute. reflexivity. +Qed. + +Lemma Pmult_nat_4_mult_2_permute : + forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2. +Proof. + intros. rewrite <- Pmult_nat_mult_permute. reflexivity. +Qed. + +(** Mapping of xH, xO and xI through [nat_of_P] *) + +Lemma nat_of_P_xH : nat_of_P 1 = 1. +Proof. + reflexivity. +Qed. + +Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p. +Proof. + 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. + 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 + binary positive numbers *) + +(** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *) + +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. +induction n as [|n H]. +reflexivity. +simpl; rewrite nat_of_P_succ_morphism, H; auto. +Qed. + +(** Miscellaneous lemmas on [P_of_succ_nat] *) + +Lemma ZL3 : + forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n). +Proof. +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. +induction n as [| n H]; simpl; + [ auto with arith + | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H; + auto with arith ]. +Qed. + +(** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *) + +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. +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 + on [positive] *) + +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; 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 + 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) 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. + + +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; + 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 |- *; + apply le_n_S; apply le_plus_r. +Qed. + +(** Comparison and subtraction *) + +Lemma Pcompare_minus_r : + forall p q r:positive, + (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; + [ rewrite nat_of_P_minus_morphism; + [ apply plus_lt_reg_l with (p := nat_of_P q); rewrite le_plus_minus_r; + [ 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; + assumption + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; + apply ZC1; assumption ] + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; + assumption ] + | assumption ] + | assumption ]. +Qed. + +Lemma Pcompare_minus_l : + forall p q r:positive, + (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; + [ rewrite nat_of_P_minus_morphism; + [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z); + rewrite le_plus_minus_r; + [ rewrite le_plus_minus_r; + [ apply nat_of_P_lt_Lt_compare_morphism; assumption + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; + apply ZC1; assumption ] + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; + assumption ] + | assumption ] + | assumption ]. +Qed. + +(** Distributivity of multiplication over subtraction *) + +Theorem Pmult_minus_distr_l : + forall p q 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; + [ rewrite nat_of_P_minus_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 |- *; + 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 ]. +Qed. diff --git a/theories/PArith/Psqrt.v b/theories/PArith/Psqrt.v new file mode 100644 index 000000000..1d85f14a2 --- /dev/null +++ b/theories/PArith/Psqrt.v @@ -0,0 +1,123 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* false | _ => true end. + +(** A Square Root function for positive numbers *) + +(** We procede by blocks of two digits : if p is written qbb' + then sqrt(p) will be sqrt(q)~0 or sqrt(q)~1. + For deciding easily in which case we are, we store the remainder + (as a positive_mask, since it can be null). + Instead of copy-pasting the following code four times, we + factorize as an auxiliary function, with f and g being either + xO or xI depending of the initial digits. + NB: (Pminus_mask (g (f 1)) 4) is a hack, morally it's g (f 0). +*) + +Definition Psqrtrem_step (f g:positive->positive) p := + match p with + | (s, IsPos r) => + let s' := s~0~1 in + let r' := g (f r) in + if Pleb s' r' then (s~1, Pminus_mask r' s') + else (s~0, IsPos r') + | (s,_) => (s~0, Pminus_mask (g (f 1)) 4) + end. + +Fixpoint Psqrtrem p : positive * positive_mask := + match p with + | 1 => (1,IsNul) + | 2 => (1,IsPos 1) + | 3 => (1,IsPos 2) + | p~0~0 => Psqrtrem_step xO xO (Psqrtrem p) + | p~0~1 => Psqrtrem_step xO xI (Psqrtrem p) + | p~1~0 => Psqrtrem_step xI xO (Psqrtrem p) + | p~1~1 => Psqrtrem_step xI xI (Psqrtrem p) + end. + +Definition Psqrt p := fst (Psqrtrem p). + +(** An inductive relation for specifying sqrt results *) + +Inductive PSQRT : positive*positive_mask -> positive -> Prop := + | PSQRT_exact : forall s x, x=s*s -> PSQRT (s,IsNul) x + | PSQRT_approx : forall s r x, x=s*s+r -> r <= s~0 -> PSQRT (s,IsPos r) x. + +(** Correctness proofs *) + +Lemma Psqrtrem_step_spec : forall f g p x, + (f=xO \/ f=xI) -> (g=xO \/ g=xI) -> + PSQRT p x -> PSQRT (Psqrtrem_step f g p) (g (f x)). +Proof. +intros f g _ _ Hf Hg [ s _ -> | s r _ -> Hr ]. +(* exact *) +unfold Psqrtrem_step. +destruct Hf,Hg; subst; simpl Pminus_mask; + constructor; try discriminate; now rewrite Psquare_xO. +(* approx *) +assert (Hfg : forall p q, g (f (p+q)) = p~0~0 + g (f q)) + by (intros; destruct Hf, Hg; now subst). +unfold Psqrtrem_step. unfold Pleb. +case Pcompare_spec; [intros EQ | intros LT | intros GT]. +(* - EQ *) +rewrite <- EQ. rewrite Pminus_mask_diag. +destruct Hg; subst g; try discriminate. +destruct Hf; subst f; try discriminate. +injection EQ; clear EQ; intros <-. +constructor. now rewrite Psquare_xI. +(* - LT *) +destruct (Pminus_mask_Gt (g (f r)) (s~0~1)) as (y & -> & H & _). +change Eq with (CompOpp Eq). now rewrite <- Pcompare_antisym, LT. +constructor. +rewrite Hfg, <- H. now rewrite Psquare_xI, Pplus_assoc. +apply Ple_lteq, Pcompare_p_Sq in Hr; change (r < s~1) in Hr. +apply Ple_lteq, Pcompare_p_Sq; change (y < s~1~1). +apply Pplus_lt_mono_l with (s~0~1). +rewrite H. simpl. rewrite Pplus_carry_spec, Pplus_diag. simpl. +set (s1:=s~1) in *; clearbody s1. +destruct Hf,Hg; subst; red; simpl; + apply Hr || apply Pcompare_eq_Lt, Hr. +(* - GT *) +constructor. +rewrite Hfg. now rewrite Psquare_xO. +apply Ple_lteq, Pcompare_p_Sq, GT. +Qed. + +Lemma Psqrtrem_spec : forall p, PSQRT (Psqrtrem p) p. +Proof. +fix 1. + destruct p; try destruct p; try (constructor; easy); + apply Psqrtrem_step_spec; auto. +Qed. + +Lemma Psqrt_spec : forall p, + let s := Psqrt p in s*s <= p < (Psucc s)*(Psucc s). +Proof. + intros p. simpl. + assert (H:=Psqrtrem_spec p). + unfold Psqrt in *. destruct Psqrtrem as (s,rm); simpl. + inversion_clear H; subst. + (* exact *) + split. red. rewrite Pcompare_refl. discriminate. + apply Pmult_lt_mono; apply Pcompare_p_Sp. + (* approx *) + split. + apply Ple_lteq; left. apply Plt_plus_r. + rewrite (Pplus_one_succ_l). + rewrite Pmult_plus_distr_r, !Pmult_plus_distr_l. + rewrite !Pmult_1_r. simpl (1*s). + rewrite <- Pplus_assoc, (Pplus_assoc s s), Pplus_diag, Pplus_assoc. + rewrite (Pplus_comm (_+_)). apply Pplus_lt_mono_l. + rewrite <- Pplus_one_succ_l. now apply Pcompare_p_Sq, Ple_lteq. +Qed. diff --git a/theories/PArith/intro.tex b/theories/PArith/intro.tex new file mode 100644 index 000000000..ffce881ed --- /dev/null +++ b/theories/PArith/intro.tex @@ -0,0 +1,4 @@ +\section{Binary positive integers : PArith}\label{PArith} + +Here are defined various arithmetical notions and their properties, +similar to those of {\tt Arith}. diff --git a/theories/PArith/vo.itarget b/theories/PArith/vo.itarget new file mode 100644 index 000000000..e9139da8a --- /dev/null +++ b/theories/PArith/vo.itarget @@ -0,0 +1,6 @@ +BinPos.vo +Pnat.vo +POrderedType.vo +Pminmax.vo +Psqrt.vo +PArith.vo \ No newline at end of file diff --git a/theories/theories.itarget b/theories/theories.itarget index afc3554b1..7cc4e09a9 100644 --- a/theories/theories.itarget +++ b/theories/theories.itarget @@ -7,6 +7,7 @@ Structures/vo.otarget Init/vo.otarget Lists/vo.otarget Logic/vo.otarget +PArith/vo.otarget NArith/vo.otarget Numbers/vo.otarget Program/vo.otarget diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 26a5cb36f..a62510b68 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -77,6 +77,7 @@ let theories_dirs_map = [ "theories/Relations", "Relations" ; "theories/Numbers", "Numbers" ; "theories/QArith", "QArith" ; + "theories/PArith", "PArith" ; "theories/NArith", "NArith" ; "theories/ZArith", "ZArith" ; "theories/Arith", "Arith" ; -- cgit v1.2.3