1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: BinPos.v 11033 2008-06-01 22:56:50Z letouzey $ i*)
11
Unset Boxed Definitions.
13
(**********************************************************************)
14
(** Binary positive numbers *)
16
(** Original development by Pierre Crégut, CNET, Lannion, France *)
18
Inductive positive : Set :=
19
| xI : positive -> positive
20
| xO : positive -> positive
23
(** Declare binding key for scope positive_scope *)
25
Delimit Scope positive_scope with positive.
27
(** Automatically open scope positive_scope for type positive, xO and xI *)
29
Bind Scope positive_scope with positive.
30
Arguments Scope xO [positive_scope].
31
Arguments Scope xI [positive_scope].
33
(** Postfix notation for positive numbers, allowing to mimic
34
the position of bits in a big-endian representation.
35
For instance, we can write 1~1~0 instead of (xO (xI xH))
36
for the number 6 (which is 110 in binary notation).
39
Notation "p ~ 1" := (xI p)
40
(at level 7, left associativity, format "p '~' '1'") : positive_scope.
41
Notation "p ~ 0" := (xO p)
42
(at level 7, left associativity, format "p '~' '0'") : positive_scope.
44
Open Local Scope positive_scope.
46
(* In the current file, [xH] cannot yet be written as [1], since the
47
interpretation of positive numerical constants is not available
48
yet. We fix this here with an ad-hoc temporary notation. *)
50
Notation Local "1" := xH (at level 7).
54
Fixpoint Psucc (x:positive) : positive :=
63
Set Boxed Definitions.
65
Fixpoint Pplus (x y:positive) : positive :=
67
| p~1, q~1 => (Pplus_carry p q)~0
68
| p~1, q~0 => (Pplus p q)~1
69
| p~1, 1 => (Psucc p)~0
70
| p~0, q~1 => (Pplus p q)~1
71
| p~0, q~0 => (Pplus p q)~0
73
| 1, q~1 => (Psucc q)~0
78
with Pplus_carry (x y:positive) : positive :=
80
| p~1, q~1 => (Pplus_carry p q)~1
81
| p~1, q~0 => (Pplus_carry p q)~0
82
| p~1, 1 => (Psucc p)~1
83
| p~0, q~1 => (Pplus_carry p q)~0
84
| p~0, q~0 => (Pplus p q)~1
85
| p~0, 1 => (Psucc p)~0
86
| 1, q~1 => (Psucc q)~1
87
| 1, q~0 => (Psucc q)~0
91
Unset Boxed Definitions.
93
Infix "+" := Pplus : positive_scope.
95
(** From binary positive numbers to Peano natural numbers *)
97
Fixpoint Pmult_nat (x:positive) (pow2:nat) : nat :=
99
| p~1 => (pow2 + Pmult_nat p (pow2 + pow2))%nat
100
| p~0 => Pmult_nat p (pow2 + pow2)%nat
104
Definition nat_of_P (x:positive) := Pmult_nat x (S O).
106
(** From Peano natural numbers to binary positive numbers *)
108
Fixpoint P_of_succ_nat (n:nat) : positive :=
111
| S x => Psucc (P_of_succ_nat x)
114
(** Operation x -> 2*x-1 *)
116
Fixpoint Pdouble_minus_one (x:positive) : positive :=
119
| p~0 => (Pdouble_minus_one p)~1
125
Definition Ppred (x:positive) :=
128
| p~0 => Pdouble_minus_one p
132
(** An auxiliary type for subtraction *)
134
Inductive positive_mask : Set :=
135
| IsNul : positive_mask
136
| IsPos : positive -> positive_mask
137
| IsNeg : positive_mask.
139
(** Operation x -> 2*x+1 *)
141
Definition Pdouble_plus_one_mask (x:positive_mask) :=
145
| IsPos p => IsPos p~1
148
(** Operation x -> 2*x *)
150
Definition Pdouble_mask (x:positive_mask) :=
154
| IsPos p => IsPos p~0
157
(** Operation x -> 2*x-2 *)
159
Definition Pdouble_minus_two (x:positive) :=
162
| p~0 => IsPos (Pdouble_minus_one p)~0
166
(** Subtraction of binary positive numbers into a positive numbers mask *)
168
Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask :=
170
| p~1, q~1 => Pdouble_mask (Pminus_mask p q)
171
| p~1, q~0 => Pdouble_plus_one_mask (Pminus_mask p q)
172
| p~1, 1 => IsPos p~0
173
| p~0, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
174
| p~0, q~0 => Pdouble_mask (Pminus_mask p q)
175
| p~0, 1 => IsPos (Pdouble_minus_one p)
180
with Pminus_mask_carry (x y:positive) {struct y} : positive_mask :=
182
| p~1, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
183
| p~1, q~0 => Pdouble_mask (Pminus_mask p q)
184
| p~1, 1 => IsPos (Pdouble_minus_one p)
185
| p~0, q~1 => Pdouble_mask (Pminus_mask_carry p q)
186
| p~0, q~0 => Pdouble_plus_one_mask (Pminus_mask_carry p q)
187
| p~0, 1 => Pdouble_minus_two p
191
(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *)
193
Definition Pminus (x y:positive) :=
194
match Pminus_mask x y with
199
Infix "-" := Pminus : positive_scope.
201
(** Multiplication on binary positive numbers *)
203
Fixpoint Pmult (x y:positive) : positive :=
205
| p~1 => y + (Pmult p y)~0
206
| p~0 => (Pmult p y)~0
210
Infix "*" := Pmult : positive_scope.
212
(** Division by 2 rounded below but for 1 *)
214
Definition Pdiv2 (z:positive) :=
221
Infix "/" := Pdiv2 : positive_scope.
223
(** Comparison on binary positive numbers *)
225
Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison :=
227
| p~1, q~1 => Pcompare p q r
228
| p~1, q~0 => Pcompare p q Gt
230
| p~0, q~1 => Pcompare p q Lt
231
| p~0, q~0 => Pcompare p q r
238
Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
240
Definition Plt (x y:positive) := (Pcompare x y Eq) = Lt.
241
Definition Pgt (x y:positive) := (Pcompare x y Eq) = Gt.
242
Definition Ple (x y:positive) := (Pcompare x y Eq) <> Gt.
243
Definition Pge (x y:positive) := (Pcompare x y Eq) <> Lt.
245
Infix "<=" := Ple : positive_scope.
246
Infix "<" := Plt : positive_scope.
247
Infix ">=" := Pge : positive_scope.
248
Infix ">" := Pgt : positive_scope.
250
Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
251
Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
252
Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
253
Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.
256
Definition Pmin (p p' : positive) := match Pcompare p p' Eq with
261
Definition Pmax (p p' : positive) := match Pcompare p p' Eq with
266
(**********************************************************************)
267
(** Miscellaneous properties of binary positive numbers *)
269
Lemma ZL11 : forall p:positive, p = 1 \/ p <> 1.
271
intros x; case x; intros; (left; reflexivity) || (right; discriminate).
274
(**********************************************************************)
275
(** Properties of successor on binary positive numbers *)
277
(** Specification of [xI] in term of [Psucc] and [xO] *)
279
Lemma xI_succ_xO : forall p:positive, p~1 = Psucc p~0.
284
Lemma Psucc_discr : forall p:positive, p <> Psucc p.
286
destruct p; discriminate.
289
(** Successor and double *)
291
Lemma Psucc_o_double_minus_one_eq_xO :
292
forall p:positive, Psucc (Pdouble_minus_one p) = p~0.
294
induction p; simpl; f_equal; auto.
297
Lemma Pdouble_minus_one_o_succ_eq_xI :
298
forall p:positive, Pdouble_minus_one (Psucc p) = p~1.
300
induction p; simpl; f_equal; auto.
303
Lemma xO_succ_permute :
304
forall p:positive, (Psucc p)~0 = Psucc (Psucc p~0).
306
induction p; simpl; auto.
309
Lemma double_moins_un_xO_discr :
310
forall p:positive, Pdouble_minus_one p <> p~0.
312
destruct p; discriminate.
315
(** Successor and predecessor *)
317
Lemma Psucc_not_one : forall p:positive, Psucc p <> 1.
319
destruct p; discriminate.
322
Lemma Ppred_succ : forall p:positive, Ppred (Psucc p) = p.
324
intros [[p|p| ]|[p|p| ]| ]; simpl; auto.
325
f_equal; apply Pdouble_minus_one_o_succ_eq_xI.
328
Lemma Psucc_pred : forall p:positive, p = 1 \/ Psucc (Ppred p) = p.
330
induction p; simpl; auto.
331
right; apply Psucc_o_double_minus_one_eq_xO.
334
Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)).
336
(** Injectivity of successor *)
338
Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q.
340
induction p; intros [q|q| ] H; simpl in *; destr_eq H; f_equal; auto.
341
elim (Psucc_not_one p); auto.
342
elim (Psucc_not_one q); auto.
345
(**********************************************************************)
346
(** Properties of addition on binary positive numbers *)
348
(** Specification of [Psucc] in term of [Pplus] *)
350
Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + 1.
352
destruct p; reflexivity.
355
Lemma Pplus_one_succ_l : forall p:positive, Psucc p = 1 + p.
357
destruct p; reflexivity.
360
(** Specification of [Pplus_carry] *)
362
Theorem Pplus_carry_spec :
363
forall p q:positive, Pplus_carry p q = Psucc (p + q).
365
induction p; destruct q; simpl; f_equal; auto.
370
Theorem Pplus_comm : forall p q:positive, p + q = q + p.
372
induction p; destruct q; simpl; f_equal; auto.
373
rewrite 2 Pplus_carry_spec; f_equal; auto.
376
(** Permutation of [Pplus] and [Psucc] *)
378
Theorem Pplus_succ_permute_r :
379
forall p q:positive, p + Psucc q = Psucc (p + q).
381
induction p; destruct q; simpl; f_equal;
382
auto using Pplus_one_succ_r; rewrite Pplus_carry_spec; auto.
385
Theorem Pplus_succ_permute_l :
386
forall p q:positive, Psucc p + q = Psucc (p + q).
388
intros p q; rewrite Pplus_comm, (Pplus_comm p);
389
apply Pplus_succ_permute_r.
392
Theorem Pplus_carry_pred_eq_plus :
393
forall p q:positive, q <> 1 -> Pplus_carry p (Ppred q) = p + q.
395
intros p q H; rewrite Pplus_carry_spec, <- Pplus_succ_permute_r; f_equal.
396
destruct (Psucc_pred q); [ elim H; assumption | assumption ].
399
(** No neutral for addition on strictly positive numbers *)
401
Lemma Pplus_no_neutral : forall p q:positive, q + p <> p.
403
induction p as [p IHp|p IHp| ]; intros [q|q| ] H;
404
destr_eq H; apply (IHp q H).
407
Lemma Pplus_carry_no_neutral :
408
forall p q:positive, Pplus_carry q p <> Psucc p.
410
intros p q H; elim (Pplus_no_neutral p q).
411
apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption.
414
(** Simplification *)
416
Lemma Pplus_carry_plus :
417
forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s.
419
intros p q r s H; apply Psucc_inj; do 2 rewrite <- Pplus_carry_spec;
423
Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q.
425
intros p q r; revert p q; induction r.
426
intros [p|p| ] [q|q| ] H; simpl; destr_eq H;
427
f_equal; auto using Pplus_carry_plus;
428
contradict H; auto using Pplus_carry_no_neutral.
429
intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto;
430
contradict H; auto using Pplus_no_neutral.
431
intros p q H; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption.
434
Lemma Pplus_reg_l : forall p q r:positive, p + q = p + r -> q = r.
436
intros p q r H; apply Pplus_reg_r with (r:=p).
437
rewrite (Pplus_comm r), (Pplus_comm q); assumption.
440
Lemma Pplus_carry_reg_r :
441
forall p q r:positive, Pplus_carry p r = Pplus_carry q r -> p = q.
443
intros p q r H; apply Pplus_reg_r with (r:=r); apply Pplus_carry_plus;
447
Lemma Pplus_carry_reg_l :
448
forall p q r:positive, Pplus_carry p q = Pplus_carry p r -> q = r.
450
intros p q r H; apply Pplus_reg_r with (r:=p);
451
rewrite (Pplus_comm r), (Pplus_comm q); apply Pplus_carry_plus; assumption.
454
(** Addition on positive is associative *)
456
Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r.
459
intros [q|q| ] [r|r| ]; simpl; f_equal; auto;
460
rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r,
461
?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
462
intros [q|q| ] [r|r| ]; simpl; f_equal; auto;
463
rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r,
464
?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto.
465
intros p r; rewrite <- 2 Pplus_one_succ_l, Pplus_succ_permute_l; auto.
468
(** Commutation of addition with the double of a positive number *)
470
Lemma Pplus_xO : forall m n : positive, (m + n)~0 = m~0 + n~0.
472
destruct n; destruct m; simpl; auto.
475
Lemma Pplus_xI_double_minus_one :
476
forall p q:positive, (p + q)~0 = p~1 + Pdouble_minus_one q.
478
intros; change (p~1) with (p~0 + 1).
479
rewrite <- Pplus_assoc, <- Pplus_one_succ_l, Psucc_o_double_minus_one_eq_xO.
483
Lemma Pplus_xO_double_minus_one :
484
forall p q:positive, Pdouble_minus_one (p + q) = p~0 + Pdouble_minus_one q.
486
induction p as [p IHp| p IHp| ]; destruct q; simpl;
487
rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI,
488
?Pplus_xI_double_minus_one; try reflexivity.
490
rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity.
495
Lemma Pplus_diag : forall p:positive, p + p = p~0.
497
induction p as [p IHp| p IHp| ]; simpl;
498
try rewrite ?Pplus_carry_spec, ?IHp; reflexivity.
501
(**********************************************************************)
502
(** Peano induction and recursion on binary positive positive numbers *)
503
(** (a nice proof from Conor McBride, see "The view from the left") *)
505
Inductive PeanoView : positive -> Type :=
506
| PeanoOne : PeanoView 1
507
| PeanoSucc : forall p, PeanoView p -> PeanoView (Psucc p).
509
Fixpoint peanoView_xO p (q:PeanoView p) : PeanoView (p~0) :=
510
match q in PeanoView x return PeanoView (x~0) with
511
| PeanoOne => PeanoSucc _ PeanoOne
512
| PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xO _ q))
515
Fixpoint peanoView_xI p (q:PeanoView p) : PeanoView (p~1) :=
516
match q in PeanoView x return PeanoView (x~1) with
517
| PeanoOne => PeanoSucc _ (PeanoSucc _ PeanoOne)
518
| PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xI _ q))
521
Fixpoint peanoView p : PeanoView p :=
522
match p return PeanoView p with
524
| p~0 => peanoView_xO p (peanoView p)
525
| p~1 => peanoView_xI p (peanoView p)
528
Definition PeanoView_iter (P:positive->Type)
529
(a:P 1) (f:forall p, P p -> P (Psucc p)) :=
530
(fix iter p (q:PeanoView p) : P p :=
531
match q in PeanoView p return P p with
533
| PeanoSucc _ q => f _ (iter _ q)
536
Require Import Eqdep_dec EqdepFacts.
538
Theorem eq_dep_eq_positive :
539
forall (P:positive->Type) (p:positive) (x y:P p),
540
eq_dep positive P p x p y -> x = y.
546
Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.
549
induction q as [ | p q IHq ].
550
apply eq_dep_eq_positive.
551
cut (1=1). pattern 1 at 1 2 5, q'. destruct q'. trivial.
552
destruct p0; intros; discriminate.
554
apply eq_dep_eq_positive.
555
cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'.
556
intro. destruct p; discriminate.
557
intro. unfold p0 in H. apply Psucc_inj in H.
558
generalize q'. rewrite H. intro.
564
Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p))
566
PeanoView_iter P a f p (peanoView p).
568
Theorem Prect_succ : forall (P:positive->Type) (a:P 1)
569
(f:forall p, P p -> P (Psucc p)) (p:positive),
570
Prect P a f (Psucc p) = f _ (Prect P a f p).
574
rewrite (PeanoViewUnique _ (peanoView (Psucc p)) (PeanoSucc _ (peanoView p))).
578
Theorem Prect_base : forall (P:positive->Type) (a:P 1)
579
(f:forall p, P p -> P (Psucc p)), Prect P a f 1 = a.
584
Definition Prec (P:positive->Set) := Prect P.
586
(** Peano induction *)
588
Definition Pind (P:positive->Prop) := Prect P.
590
(** Peano case analysis *)
593
forall P:positive -> Prop,
594
P 1 -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p.
596
intros; apply Pind; auto.
599
(**********************************************************************)
600
(** Properties of multiplication on binary positive numbers *)
602
(** One is right neutral for multiplication *)
604
Lemma Pmult_1_r : forall p:positive, p * 1 = p.
606
induction p; simpl; f_equal; auto.
609
(** Successor and multiplication *)
611
Lemma Pmult_Sn_m : forall n m : positive, (Psucc n) * m = m + n * m.
613
induction n as [n IHn | n IHn | ]; simpl; intro m.
614
rewrite IHn, Pplus_assoc, Pplus_diag, <-Pplus_xO; reflexivity.
616
symmetry; apply Pplus_diag.
619
(** Right reduction properties for multiplication *)
621
Lemma Pmult_xO_permute_r : forall p q:positive, p * q~0 = (p * q)~0.
623
intros p q; induction p; simpl; do 2 (f_equal; auto).
626
Lemma Pmult_xI_permute_r : forall p q:positive, p * q~1 = p + (p * q)~0.
628
intros p q; induction p as [p IHp|p IHp| ]; simpl; f_equal; auto.
629
rewrite IHp, 2 Pplus_assoc, (Pplus_comm p); reflexivity.
632
(** Commutativity of multiplication *)
634
Theorem Pmult_comm : forall p q:positive, p * q = q * p.
636
intros p q; induction q as [q IHq|q IHq| ]; simpl; try rewrite <- IHq;
637
auto using Pmult_xI_permute_r, Pmult_xO_permute_r, Pmult_1_r.
640
(** Distributivity of multiplication over addition *)
642
Theorem Pmult_plus_distr_l :
643
forall p q r:positive, p * (q + r) = p * q + p * r.
645
intros p q r; induction p as [p IHp|p IHp| ]; simpl.
646
rewrite IHp. set (m:=(p*q)~0). set (n:=(p*r)~0).
647
change ((p*q+p*r)~0) with (m+n).
648
rewrite 2 Pplus_assoc; f_equal.
649
rewrite <- 2 Pplus_assoc; f_equal.
655
Theorem Pmult_plus_distr_r :
656
forall p q r:positive, (p + q) * r = p * r + q * r.
658
intros p q r; do 3 rewrite Pmult_comm with (q:=r); apply Pmult_plus_distr_l.
661
(** Associativity of multiplication *)
663
Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r.
665
induction p as [p IHp| p IHp | ]; simpl; intros q r.
666
rewrite IHp; rewrite Pmult_plus_distr_r; reflexivity.
667
rewrite IHp; reflexivity.
671
(** Parity properties of multiplication *)
673
Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, p~1 * r <> q~0 * r.
675
intros p q r; induction r; try discriminate.
676
rewrite 2 Pmult_xO_permute_r; intro H; destr_eq H; auto.
679
Lemma Pmult_xO_discr : forall p q:positive, p~0 * q <> q.
681
intros p q; induction q; try discriminate.
682
rewrite Pmult_xO_permute_r; injection; assumption.
685
(** Simplification properties of multiplication *)
687
Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q.
689
induction p as [p IHp| p IHp| ]; intros [q|q| ] r H;
690
reflexivity || apply (f_equal (A:=positive)) || apply False_ind.
691
apply IHp with (r~0); simpl in *;
692
rewrite 2 Pmult_xO_permute_r; apply Pplus_reg_l with (1:=H).
693
apply Pmult_xI_mult_xO_discr with (1:=H).
694
simpl in H; rewrite Pplus_comm in H; apply Pplus_no_neutral with (1:=H).
695
symmetry in H; apply Pmult_xI_mult_xO_discr with (1:=H).
696
apply IHp with (r~0); simpl; rewrite 2 Pmult_xO_permute_r; assumption.
697
apply Pmult_xO_discr with (1:= H).
698
simpl in H; symmetry in H; rewrite Pplus_comm in H;
699
apply Pplus_no_neutral with (1:=H).
700
symmetry in H; apply Pmult_xO_discr with (1:=H).
703
Theorem Pmult_reg_l : forall p q r:positive, r * p = r * q -> p = q.
705
intros p q r H; apply Pmult_reg_r with (r:=r).
706
rewrite (Pmult_comm p), (Pmult_comm q); assumption.
709
(** Inversion of multiplication *)
711
Lemma Pmult_1_inversion_l : forall p q:positive, p * q = 1 -> p = 1.
713
intros [p|p| ] [q|q| ] H; destr_eq H; auto.
716
(**********************************************************************)
717
(** Properties of comparison on binary positive numbers *)
719
Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq.
723
(* A generalization of Pcompare_refl *)
725
Theorem Pcompare_refl_id : forall (p : positive) (r : comparison), (p ?= p) r = r.
729
Theorem Pcompare_not_Eq :
730
forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq.
732
induction p as [p IHp| p IHp| ]; intros [q| q| ]; split; simpl; auto;
733
discriminate || (elim (IHp q); auto).
736
Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q.
738
induction p; intros [q| q| ] H; simpl in *; auto;
739
try discriminate H; try (f_equal; auto; fail).
740
destruct (Pcompare_not_Eq p q) as (H',_); elim H'; auto.
741
destruct (Pcompare_not_Eq p q) as (_,H'); elim H'; auto.
744
Lemma Pcompare_Gt_Lt :
745
forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt.
747
induction p; intros [q|q| ] H; simpl; auto; discriminate.
750
Lemma Pcompare_eq_Lt :
751
forall p q : positive, (p ?= q) Eq = Lt <-> (p ?= q) Gt = Lt.
753
intros p q; split; [| apply Pcompare_Gt_Lt].
754
revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate.
757
Lemma Pcompare_Lt_Gt :
758
forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt.
760
induction p; intros [q|q| ] H; simpl; auto; discriminate.
763
Lemma Pcompare_eq_Gt :
764
forall p q : positive, (p ?= q) Eq = Gt <-> (p ?= q) Lt = Gt.
766
intros p q; split; [| apply Pcompare_Lt_Gt].
767
revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate.
770
Lemma Pcompare_Lt_Lt :
771
forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q.
773
induction p as [p IHp| p IHp| ]; intros [q|q| ] H; simpl in *; auto;
774
destruct (IHp q H); subst; auto.
777
Lemma Pcompare_Lt_eq_Lt :
778
forall p q:positive, (p ?= q) Lt = Lt <-> (p ?= q) Eq = Lt \/ p = q.
780
intros p q; split; [apply Pcompare_Lt_Lt |].
781
intros [H|H]; [|subst; apply Pcompare_refl_id].
782
revert q H; induction p; intros [q|q| ] H; simpl in *;
786
Lemma Pcompare_Gt_Gt :
787
forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q.
789
induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto;
790
destruct (IHp q H); subst; auto.
793
Lemma Pcompare_Gt_eq_Gt :
794
forall p q:positive, (p ?= q) Gt = Gt <-> (p ?= q) Eq = Gt \/ p = q.
796
intros p q; split; [apply Pcompare_Gt_Gt |].
797
intros [H|H]; [|subst; apply Pcompare_refl_id].
798
revert q H; induction p; intros [q|q| ] H; simpl in *;
802
Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt.
807
Ltac ElimPcompare c1 c2 :=
808
elim (Dcompare ((c1 ?= c2) Eq));
809
[ idtac | let x := fresh "H" in (intro x; case x; clear x) ].
811
Lemma Pcompare_antisym :
812
forall (p q:positive) (r:comparison),
813
CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r).
815
induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto;
819
Lemma ZC1 : forall p q:positive, (p ?= q) Eq = Gt -> (q ?= p) Eq = Lt.
821
intros p q H; change Eq with (CompOpp Eq).
822
rewrite <- Pcompare_antisym, H; reflexivity.
825
Lemma ZC2 : forall p q:positive, (p ?= q) Eq = Lt -> (q ?= p) Eq = Gt.
827
intros p q H; change Eq with (CompOpp Eq).
828
rewrite <- Pcompare_antisym, H; reflexivity.
831
Lemma ZC3 : forall p q:positive, (p ?= q) Eq = Eq -> (q ?= p) Eq = Eq.
833
intros p q H; change Eq with (CompOpp Eq).
834
rewrite <- Pcompare_antisym, H; reflexivity.
837
Lemma ZC4 : forall p q:positive, (p ?= q) Eq = CompOpp ((q ?= p) Eq).
839
intros; change Eq at 1 with (CompOpp Eq).
840
symmetry; apply Pcompare_antisym.
843
(** Comparison and the successor *)
845
Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt.
847
induction p; simpl in *;
848
[ elim (Pcompare_eq_Lt p (Psucc p)); auto |
849
apply Pcompare_refl_id | reflexivity].
852
Theorem Pcompare_p_Sq : forall p q : positive,
853
(p ?= Psucc q) Eq = Lt <-> (p ?= q) Eq = Lt \/ p = q.
857
revert p q; induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *;
858
try (left; reflexivity); try (right; reflexivity).
859
destruct (IHp q (Pcompare_Gt_Lt _ _ H)); subst; auto.
860
destruct (Pcompare_eq_Lt p q); auto.
861
destruct p; discriminate.
862
left; destruct (IHp q H);
863
[ elim (Pcompare_Lt_eq_Lt p q); auto | subst; apply Pcompare_refl_id].
864
destruct (Pcompare_Lt_Lt p q H); subst; auto.
865
destruct p; discriminate.
867
intros [H|H]; [|subst; apply Pcompare_p_Sp].
868
revert q H; induction p; intros [q|q| ] H; simpl in *;
869
auto; try discriminate.
870
destruct (Pcompare_eq_Lt p (Psucc q)); auto.
871
apply Pcompare_Gt_Lt; auto.
872
destruct (Pcompare_Lt_Lt p q H); subst; auto using Pcompare_p_Sp.
873
destruct (Pcompare_Lt_eq_Lt p q); auto.
876
(** 1 is the least positive number *)
878
Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt.
880
destruct p; discriminate.
883
(** Properties of the strict order on positive numbers *)
885
Lemma Plt_1 : forall p, ~ p < 1.
890
Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m.
892
unfold Plt; intros n m H; apply <- Pcompare_p_Sq; auto.
895
Lemma Plt_irrefl : forall p : positive, ~ p < p.
897
unfold Plt; intro p; rewrite Pcompare_refl; discriminate.
900
Lemma Plt_trans : forall n m p : positive, n < m -> m < p -> n < p.
902
intros n m p; induction p using Pind; intros H H0.
905
destruct (Pcompare_p_Sq m p) as (H',_); destruct (H' H0); subst; auto.
908
Theorem Plt_ind : forall (A : positive -> Prop) (n : positive),
910
(forall m : positive, n < m -> A m -> A (Psucc m)) ->
911
forall m : positive, n < m -> A m.
913
intros A n AB AS m. induction m using Pind; intros H.
915
destruct (Pcompare_p_Sq n m) as (H',_); destruct (H' H); subst; auto.
918
(**********************************************************************)
919
(** Properties of subtraction on binary positive numbers *)
921
Lemma Ppred_minus : forall p, Ppred p = Pminus p 1.
926
Definition Ppred_mask (p : positive_mask) :=
929
| IsPos q => IsPos (Ppred q)
934
Lemma Pminus_mask_succ_r :
935
forall p q : positive, Pminus_mask p (Psucc q) = Pminus_mask_carry p q.
937
induction p ; destruct q; simpl; f_equal; auto; destruct p; auto.
940
Theorem Pminus_mask_carry_spec :
941
forall p q : positive, Pminus_mask_carry p q = Ppred_mask (Pminus_mask p q).
943
induction p as [p IHp|p IHp| ]; destruct q; simpl;
944
try reflexivity; try rewrite IHp;
945
destruct (Pminus_mask p q) as [|[r|r| ]|] || destruct p; auto.
948
Theorem Pminus_succ_r : forall p q : positive, p - (Psucc q) = Ppred (p - q).
950
intros p q; unfold Pminus;
951
rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
952
destruct (Pminus_mask p q) as [|[r|r| ]|]; auto.
955
Lemma double_eq_zero_inversion :
956
forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul.
958
destruct p; simpl; intros; trivial; discriminate.
961
Lemma double_plus_one_zero_discr :
962
forall p:positive_mask, Pdouble_plus_one_mask p <> IsNul.
964
destruct p; discriminate.
967
Lemma double_plus_one_eq_one_inversion :
968
forall p:positive_mask, Pdouble_plus_one_mask p = IsPos 1 -> p = IsNul.
970
destruct p; simpl; intros; trivial; discriminate.
973
Lemma double_eq_one_discr :
974
forall p:positive_mask, Pdouble_mask p <> IsPos 1.
976
destruct p; discriminate.
979
Theorem Pminus_mask_diag : forall p:positive, Pminus_mask p p = IsNul.
981
induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto.
984
Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg.
986
induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto.
989
Lemma Pminus_mask_IsNeg : forall p q:positive,
990
Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg.
992
induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto;
993
try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H;
994
specialize IHp with q.
995
destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto.
996
destruct (Pminus_mask p q); simpl; auto; try discriminate.
997
destruct (Pminus_mask_carry p q); simpl; auto; try discriminate.
998
destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto.
1002
forall p q:positive,
1003
Pminus_mask p q = IsPos 1 -> Pminus_mask_carry p q = IsNul.
1005
induction p; intros [q|q| ] H; simpl in *; try discriminate.
1006
elim (double_eq_one_discr _ H).
1007
rewrite (double_plus_one_eq_one_inversion _ H); auto.
1008
rewrite (double_plus_one_eq_one_inversion _ H); auto.
1009
elim (double_eq_one_discr _ H).
1010
destruct p; simpl; auto; discriminate.
1013
(** Properties of subtraction valid only for x>y *)
1015
Lemma Pminus_mask_Gt :
1016
forall p q:positive,
1018
exists h : positive,
1019
Pminus_mask p q = IsPos h /\
1020
q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)).
1022
induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *;
1025
destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto.
1026
repeat split; auto; right.
1027
destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
1028
rewrite ZL10; subst; auto.
1029
rewrite W; simpl; destruct r; auto; elim NE; auto.
1031
destruct (Pcompare_Gt_Gt _ _ H) as [H'|H']; clear H; rename H' into H.
1032
destruct (IHp q H) as (r & U & V & W); exists (r~1); rewrite ?U, ?V; auto.
1033
exists 1; subst; rewrite Pminus_mask_diag; auto.
1037
destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as (r & U & V & W).
1038
destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
1039
exists 1; subst; rewrite ZL10, Pplus_one_succ_r; auto.
1040
exists ((Ppred r)~1); rewrite W, Pplus_carry_pred_eq_plus, V; auto.
1042
destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto.
1043
repeat split; auto; right.
1044
destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]].
1045
rewrite ZL10; subst; auto.
1046
rewrite W; simpl; destruct r; auto; elim NE; auto.
1048
exists (Pdouble_minus_one p); repeat split; destruct p; simpl; auto.
1049
rewrite Psucc_o_double_minus_one_eq_xO; auto.
1052
Theorem Pplus_minus :
1053
forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p.
1055
intros p q H; destruct (Pminus_mask_Gt p q H) as (r & U & V & _).
1056
unfold Pminus; rewrite U; simpl; auto.
1059
(** When x<y, the substraction of x by y returns 1 *)
1061
Lemma Pminus_mask_Lt : forall p q:positive, p<q -> Pminus_mask p q = IsNeg.
1063
unfold Plt; induction p as [p IHp|p IHp| ]; destruct q; simpl; intros;
1064
try discriminate; try rewrite IHp; auto.
1065
apply Pcompare_Gt_Lt; auto.
1066
destruct (Pcompare_Lt_Lt _ _ H).
1067
rewrite Pminus_mask_IsNeg; simpl; auto.
1068
subst; rewrite Pminus_mask_carry_diag; auto.
1071
Lemma Pminus_Lt : forall p q:positive, p<q -> p-q = 1.
1073
intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto.
1076
(** The substraction of x by x returns 1 *)
1078
Lemma Pminus_Eq : forall p:positive, p-p = 1.
1080
intros; unfold Pminus; rewrite Pminus_mask_diag; auto.
1083
(** Number of digits in a number *)
1085
Fixpoint Psize (p:positive) : nat :=
1088
| p~1 => S (Psize p)
1089
| p~0 => S (Psize p)
1092
Lemma Psize_monotone : forall p q, (p?=q) Eq = Lt -> (Psize p <= Psize q)%nat.
1094
assert (le0 : forall n, (0<=n)%nat) by (induction n; auto).
1095
assert (leS : forall n m, (n<=m -> S n <= S m)%nat) by (induction 1; auto).
1096
induction p; destruct q; simpl; auto; intros; try discriminate.
1097
intros; generalize (Pcompare_Gt_Lt _ _ H); auto.
1098
intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto.
added
removed
theories/NArith/BinPos.v
