From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- theories/NArith/BinPos.v | 162 +++++++++++++++++++++++++++++++++-------------- 1 file changed, 115 insertions(+), 47 deletions(-) (limited to 'theories/NArith/BinPos.v') 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 *) (* 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. -- cgit v1.2.3