1 files changed, 115 insertions, 47 deletions

diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index e3293e70..a5f99cc6 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,10 +7,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: BinPos.v 11033 2008-06-01 22:56:50Z letouzey $ i*)
+(*i $Id$ i*)
 
 Unset Boxed Definitions.
 
+Declare ML Module "z_syntax_plugin".
+
 (**********************************************************************)
 (** Binary positive numbers *)
 
@@ -30,15 +33,15 @@ Bind Scope positive_scope with positive.
 Arguments Scope xO [positive_scope].
 Arguments Scope xI [positive_scope].
 
-(** Postfix notation for positive numbers, allowing to mimic 
-    the position of bits in a big-endian representation. 
-    For instance, we can write 1~1~0 instead of (xO (xI xH)) 
+(** Postfix notation for positive numbers, allowing to mimic
+    the position of bits in a big-endian representation.
+    For instance, we can write 1~1~0 instead of (xO (xI xH))
     for the number 6 (which is 110 in binary notation).
 *)
 
-Notation "p ~ 1" := (xI p) 
+Notation "p ~ 1" := (xI p)
  (at level 7, left associativity, format "p '~' '1'") : positive_scope.
-Notation "p ~ 0" := (xO p) 
+Notation "p ~ 0" := (xO p)
  (at level 7, left associativity, format "p '~' '0'") : positive_scope.
 
 Open Local Scope positive_scope.
@@ -74,7 +77,7 @@ Fixpoint Pplus (x y:positive) : positive :=
     | 1, q~0 => q~1
     | 1, 1 => 1~0
   end
-  
+
 with Pplus_carry (x y:positive) : positive :=
   match x, y with
     | p~1, q~1 => (Pplus_carry p q)~1
@@ -176,7 +179,7 @@ Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask :=
     | 1, 1 => IsNul
     | 1, _ => IsNeg
   end
-  
+
 with Pminus_mask_carry (x y:positive) {struct y} : positive_mask :=
   match x, y with
     | p~1, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
@@ -253,23 +256,41 @@ Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.
 
 
-Definition Pmin (p p' : positive) := match Pcompare p p' Eq with 
- | Lt | Eq => p 
+Definition Pmin (p p' : positive) := match Pcompare p p' Eq with
+ | Lt | Eq => p
  | Gt => p'
  end.
 
-Definition Pmax (p p' : positive) := match Pcompare p p' Eq with 
- | Lt | Eq => p' 
+Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
+ | Lt | Eq => p'
  | Gt => p
  end.
 
+(********************************************************************)
+(** Boolean equality *)
+
+Fixpoint Peqb (x y : positive) {struct y} : bool :=
+ match x, y with
+ | 1, 1 => true
+ | p~1, q~1 => Peqb p q
+ | p~0, q~0 => Peqb p q
+ | _, _ => false
+ end.
+
 (**********************************************************************)
-(** Miscellaneous properties of binary positive numbers *)
+(** Decidability of equality on binary positive numbers *)
+
+Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}.
+Proof.
+  decide equality.
+Defined.
 
-Lemma ZL11 : forall p:positive, p = 1 \/ p <> 1.
+(* begin hide *)
+Corollary ZL11 : forall p:positive, p = 1 \/ p <> 1.
 Proof.
-  intros x; case x; intros; (left; reflexivity) || (right; discriminate).
+  intro; edestruct positive_eq_dec; eauto.
 Qed.
+(* end hide *)
 
 (**********************************************************************)
 (** Properties of successor on binary positive numbers *)
@@ -371,14 +392,14 @@ Theorem Pplus_comm : forall p q:positive, p + q = q + p.
 Proof.
   induction p; destruct q; simpl; f_equal; auto.
   rewrite 2 Pplus_carry_spec; f_equal; auto.
-Qed. 
+Qed.
 
 (** Permutation of [Pplus] and [Psucc] *)
 
 Theorem Pplus_succ_permute_r :
   forall p q:positive, p + Psucc q = Psucc (p + q).
 Proof.
-  induction p; destruct q; simpl; f_equal; 
+  induction p; destruct q; simpl; f_equal;
    auto using Pplus_one_succ_r; rewrite Pplus_carry_spec; auto.
 Qed.
 
@@ -423,10 +444,10 @@ Qed.
 Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q.
 Proof.
   intros p q r; revert p q; induction r.
-  intros [p|p| ] [q|q| ] H; simpl; destr_eq H; 
-    f_equal; auto using Pplus_carry_plus; 
+  intros [p|p| ] [q|q| ] H; simpl; destr_eq H;
+    f_equal; auto using Pplus_carry_plus;
     contradict H; auto using Pplus_carry_no_neutral.
-  intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto; 
+  intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto;
     contradict H; auto using Pplus_no_neutral.
   intros p q H; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption.
 Qed.
@@ -456,11 +477,11 @@ Qed.
 Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r.
 Proof.
   induction p.
-  intros [q|q| ] [r|r| ]; simpl; f_equal; auto; 
-    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, 
+  intros [q|q| ] [r|r| ]; simpl; f_equal; auto;
+    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r,
      ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
   intros [q|q| ] [r|r| ]; simpl; f_equal; auto;
-    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, 
+    rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r,
      ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
   intros p r; rewrite <- 2 Pplus_one_succ_l, Pplus_succ_permute_l; auto.
 Qed.
@@ -484,7 +505,7 @@ Lemma Pplus_xO_double_minus_one :
   forall p q:positive, Pdouble_minus_one (p + q) = p~0 + Pdouble_minus_one q.
 Proof.
   induction p as [p IHp| p IHp| ]; destruct q; simpl;
-  rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI, 
+  rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI,
     ?Pplus_xI_double_minus_one; try reflexivity.
   rewrite IHp; auto.
   rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity.
@@ -494,7 +515,7 @@ Qed.
 
 Lemma Pplus_diag : forall p:positive, p + p = p~0.
 Proof.
-  induction p as [p IHp| p IHp| ]; simpl; 
+  induction p as [p IHp| p IHp| ]; simpl;
    try rewrite ?Pplus_carry_spec, ?IHp; reflexivity.
 Qed.
 
@@ -525,10 +546,10 @@ Fixpoint peanoView p : PeanoView p :=
     | p~1 => peanoView_xI p (peanoView p)
   end.
 
-Definition PeanoView_iter (P:positive->Type) 
+Definition PeanoView_iter (P:positive->Type)
   (a:P 1) (f:forall p, P p -> P (Psucc p)) :=
   (fix iter p (q:PeanoView p) : P p :=
-    match q in PeanoView p return P p with 
+    match q in PeanoView p return P p with
       | PeanoOne => a
       | PeanoSucc _ q => f _ (iter _ q)
     end).
@@ -536,23 +557,23 @@ Definition PeanoView_iter (P:positive->Type)
 Require Import Eqdep_dec EqdepFacts.
 
 Theorem eq_dep_eq_positive :
-  forall (P:positive->Type) (p:positive) (x y:P p), 
+  forall (P:positive->Type) (p:positive) (x y:P p),
     eq_dep positive P p x p y -> x = y.
 Proof.
   apply eq_dep_eq_dec.
   decide equality.
 Qed.
 
-Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.  
+Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.
 Proof.
-  intros. 
+  intros.
   induction q as [ | p q IHq ].
   apply eq_dep_eq_positive.
   cut (1=1). pattern 1 at 1 2 5, q'. destruct q'. trivial.
   destruct p0; intros; discriminate.
   trivial.
   apply eq_dep_eq_positive.
-  cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. 
+  cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'.
   intro. destruct p; discriminate.
   intro. unfold p0 in H. apply Psucc_inj in H.
   generalize q'. rewrite H. intro.
@@ -561,12 +582,12 @@ Proof.
   trivial.
 Qed.
 
-Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p)) 
+Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p))
   (p:positive) :=
   PeanoView_iter P a f p (peanoView p).
 
-Theorem Prect_succ : forall (P:positive->Type) (a:P 1) 
-  (f:forall p, P p -> P (Psucc p)) (p:positive), 
+Theorem Prect_succ : forall (P:positive->Type) (a:P 1)
+  (f:forall p, P p -> P (Psucc p)) (p:positive),
   Prect P a f (Psucc p) = f _ (Prect P a f p).
 Proof.
   intros.
@@ -575,7 +596,7 @@ Proof.
   trivial.
 Qed.
 
-Theorem Prect_base : forall (P:positive->Type) (a:P 1) 
+Theorem Prect_base : forall (P:positive->Type) (a:P 1)
   (f:forall p, P p -> P (Psucc p)), Prect P a f 1 = a.
 Proof.
   trivial.
@@ -713,6 +734,29 @@ Proof.
   intros [p|p| ] [q|q| ] H; destr_eq H; auto.
 Qed.
 
+(*********************************************************************)
+(** Properties of boolean equality *)
+
+Theorem Peqb_refl : forall x:positive, Peqb x x = true.
+Proof.
+ induction x; auto.
+Qed.
+
+Theorem Peqb_true_eq : forall x y:positive, Peqb x y = true -> x=y.
+Proof.
+ induction x; destruct y; simpl; intros; try discriminate.
+ f_equal; auto.
+ f_equal; auto.
+ reflexivity.
+Qed.
+
+Theorem Peqb_eq : forall x y : positive, Peqb x y = true <-> x=y.
+Proof.
+ split. apply Peqb_true_eq.
+ intros; subst; apply Peqb_refl.
+Qed.
+
+
 (**********************************************************************)
 (** Properties of comparison on binary positive numbers *)
 
@@ -735,12 +779,19 @@ Qed.
 
 Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.
 Proof.
-  induction p; intros [q| q| ] H; simpl in *; auto; 
+  induction p; intros [q| q| ] H; simpl in *; auto;
    try discriminate H; try (f_equal; auto; fail).
   destruct (Pcompare_not_Eq p q) as (H',_); elim H'; auto.
   destruct (Pcompare_not_Eq p q) as (_,H'); elim H'; auto.
 Qed.
 
+Lemma Pcompare_eq_iff : forall p q:positive, (p ?= q) Eq = Eq <-> p = q.
+Proof.
+  split.
+  apply Pcompare_Eq_eq.
+  intros; subst; apply Pcompare_refl.
+Qed.
+
 Lemma Pcompare_Gt_Lt :
   forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt.
 Proof.
@@ -812,7 +863,7 @@ Lemma Pcompare_antisym :
   forall (p q:positive) (r:comparison),
     CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r).
 Proof.
-  induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto; 
+  induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto;
    rewrite IHp; auto.
 Qed.
 
@@ -840,6 +891,15 @@ Proof.
   symmetry; apply Pcompare_antisym.
 Qed.
 
+Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq).
+Proof.
+  intros. destruct ((p ?= q) Eq) as [ ]_eqn; constructor.
+  apply Pcompare_Eq_eq; auto.
+  auto.
+  apply ZC1; auto.
+Qed.
+
+
 (** Comparison and the successor *)
 
 Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.
@@ -915,6 +975,14 @@ Proof.
   destruct (Pcompare_p_Sq n m) as (H',_); destruct (H' H); subst; auto.
 Qed.
 
+Lemma Ple_lteq : forall p q, p <= q <-> p < q \/ p = q.
+Proof.
+  unfold Ple, Plt. intros.
+  generalize (Pcompare_eq_iff p q).
+  destruct ((p ?= q) Eq); intuition; discriminate.
+Qed.
+
+
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)
 
@@ -940,14 +1008,14 @@ Qed.
 Theorem Pminus_mask_carry_spec :
   forall p q : positive, Pminus_mask_carry p q = Ppred_mask (Pminus_mask p q).
 Proof.
-  induction p as [p IHp|p IHp| ]; destruct q; simpl; 
+  induction p as [p IHp|p IHp| ]; destruct q; simpl;
    try reflexivity; try rewrite IHp;
    destruct (Pminus_mask p q) as [|[r|r| ]|] || destruct p; auto.
 Qed.
 
 Theorem Pminus_succ_r : forall p q : positive, p - (Psucc q) = Ppred (p - q).
 Proof.
-  intros p q; unfold Pminus; 
+  intros p q; unfold Pminus;
   rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
   destruct (Pminus_mask p q) as [|[r|r| ]|]; auto.
 Qed.
@@ -986,11 +1054,11 @@ Proof.
   induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto.
 Qed.
 
-Lemma Pminus_mask_IsNeg : forall p q:positive, 
+Lemma Pminus_mask_IsNeg : forall p q:positive,
  Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg.
 Proof.
-  induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto; 
-   try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H; 
+  induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto;
+   try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H;
    specialize IHp with q.
   destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto.
   destruct (Pminus_mask p q); simpl; auto; try discriminate.
@@ -1019,9 +1087,9 @@ Lemma Pminus_mask_Gt :
       Pminus_mask p q = IsPos h /\
       q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)).
 Proof.
-  induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *; 
+  induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *;
    try discriminate H.
-  (* p~1, q~1 *) 
+  (* p~1, q~1 *)
   destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto.
   repeat split; auto; right.
   destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
@@ -1082,10 +1150,10 @@ Qed.
 
 (** Number of digits in a number *)
 
-Fixpoint Psize (p:positive) : nat := 
-  match p with 
+Fixpoint Psize (p:positive) : nat :=
+  match p with
     | 1 => S O
-    | p~1 => S (Psize p) 
+    | p~1 => S (Psize p)
     | p~0 => S (Psize p)
   end.