# Library Coq.PArith.BinPos

Require Export BinNums.
Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid
Equalities Orders OrdersFacts GenericMinMax Le Plus.
Require Export BinPosDef.

# Binary positive numbers, operations and properties

Initial development by Pierre Crégut, CNET, Lannion, France
The type positive and its constructors xI and xO and xH are now defined in BinNums.v
Local Open Scope positive_scope.
Local Local
Every definitions and early properties about positive numbers are placed in a module Pos for qualification purpose.
Module Pos
<: UsualOrderedTypeFull
<: UsualDecidableTypeFull
<: TotalOrder.

# Definitions of operations, now in a separate file

Include BinPosDef.Pos.
In functor applications that follow, we only inline t and eq

# Logical Predicates

Definition eq := @Logic.eq positive.
Definition eq_equiv := @eq_equivalence positive.
Include BackportEq.
Definition lt x y := (x ?= y) = Lt.
Definition gt x y := (x ?= y) = Gt.
Definition le x y := (x ?= y) <> Gt.
Definition ge x y := (x ?= y) <> Lt.
Infix "<=" := le : positive_scope.
Infix "<" := lt : positive_scope.
Infix ">=" := ge : positive_scope.
Infix ">" := gt : 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.

# Properties of operations over positive numbers

## Decidability of equality on binary positive numbers

Lemma eq_dec : forall x y:positive, {x = y} + {x <> y}.

# Properties of successor on binary positive numbers

## Specification of xI in term of succ and xO

Lemma xI_succ_xO p : p~1 = succ p~0.
Lemma succ_discr p : p <> succ p.

## Successor and double

Lemma pred_double_spec p : pred_double p = pred (p~0).
Lemma succ_pred_double p : succ (pred_double p) = p~0.
Lemma pred_double_succ p : pred_double (succ p) = p~1.
Lemma double_succ p : (succ p)~0 = succ (succ p~0).
Lemma pred_double_xO_discr p : pred_double p <> p~0.

## Successor and predecessor

Lemma succ_not_1 p : succ p <> 1.
Lemma pred_succ p : pred (succ p) = p.
Lemma succ_pred_or p : p = 1 \/ succ (pred p) = p.
Lemma succ_pred p : p <> 1 -> succ (pred p) = p.

## Injectivity of successor

Lemma succ_inj p q : succ p = succ q -> p = q.

## Predecessor to N

Lemma pred_N_succ p : pred_N (succ p) = Npos p.

# Properties of addition on binary positive numbers

## Specification of succ in term of add

Lemma add_1_r p : p + 1 = succ p.
Lemma add_1_l p : 1 + p = succ p.

## Specification of add_carry

Theorem add_carry_spec p q : add_carry p q = succ (p + q).

## Commutativity

Theorem add_comm p q : p + q = q + p.

## Permutation of add and succ

Theorem add_succ_r p q : p + succ q = succ (p + q).
Theorem add_succ_l p q : succ p + q = succ (p + q).

## No neutral elements for addition

Lemma add_no_neutral p q : q + p <> p.

## Simplification

Lemma add_carry_add p q r s :
add_carry p r = add_carry q s -> p + r = q + s.
Lemma add_reg_r p q r : p + r = q + r -> p = q.
Lemma add_reg_l p q r : p + q = p + r -> q = r.
Lemma add_cancel_r p q r : p + r = q + r <-> p = q.
Lemma add_cancel_l p q r : r + p = r + q <-> p = q.
Lemma add_carry_reg_r p q r :
add_carry p r = add_carry q r -> p = q.
Lemma add_carry_reg_l p q r :
add_carry p q = add_carry p r -> q = r.

## Addition is associative

Theorem add_assoc p q r : p + (q + r) = p + q + r.

## Commutation of addition and double

Lemma add_xO p q : (p + q)~0 = p~0 + q~0.
Lemma add_xI_pred_double p q :
(p + q)~0 = p~1 + pred_double q.
Lemma add_xO_pred_double p q :
pred_double (p + q) = p~0 + pred_double q.

## Miscellaneous

Lemma add_diag p : p + p = p~0.

# Peano induction and recursion on binary positive positive numbers

The Peano-like recursor function for positive (due to Daniel Schepler)
Fixpoint peano_rect (P:positive->Type) (a:P 1)
(f: forall p:positive, P p -> P (succ p)) (p:positive) : P p :=
let f2 := peano_rect (fun p:positive => P (p~0)) (f _ a)
(fun (p:positive) (x:P (p~0)) => f _ (f _ x))
in
match p with
| q~1 => f _ (f2 q)
| q~0 => f2 q
| 1 => a
end.
Theorem peano_rect_succ (P:positive->Type) (a:P 1)
(f:forall p, P p -> P (succ p)) (p:positive) :
peano_rect P a f (succ p) = f _ (peano_rect P a f p).
Theorem peano_rect_base (P:positive->Type) (a:P 1)
(f:forall p, P p -> P (succ p)) :
peano_rect P a f 1 = a.
Definition peano_rec (P:positive->Set) := peano_rect P.
Peano induction
Definition peano_ind (P:positive->Prop) := peano_rect P.
Peano case analysis
Theorem peano_case :
forall P:positive -> Prop,
P 1 -> (forall n:positive, P (succ n)) -> forall p:positive, P p.
Earlier, the Peano-like recursor was built and proved in a way due to Conor McBride, see "The view from the left"
Inductive PeanoView : positive -> Type :=
| PeanoOne : PeanoView 1
| PeanoSucc : forall p, PeanoView p -> PeanoView (succ 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 (succ 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).
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.
Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.
Lemma peano_equiv (P:positive->Type) (a:P 1) (f:forall p, P p -> P (succ p)) p :
PeanoView_iter P a f p (peanoView p) = peano_rect P a f p.

# Properties of multiplication on binary positive numbers

## One is neutral for multiplication

Lemma mul_1_l p : 1 * p = p.
Lemma mul_1_r p : p * 1 = p.

## Right reduction properties for multiplication

Lemma mul_xO_r p q : p * q~0 = (p * q)~0.
Lemma mul_xI_r p q : p * q~1 = p + (p * q)~0.

## Commutativity of multiplication

Theorem mul_comm p q : p * q = q * p.

## Distributivity of multiplication over addition

Theorem mul_add_distr_l p q r :
p * (q + r) = p * q + p * r.
Theorem mul_add_distr_r p q r :
(p + q) * r = p * r + q * r.

## Associativity of multiplication

Theorem mul_assoc p q r : p * (q * r) = p * q * r.

## Successor and multiplication

Lemma mul_succ_l p q : (succ p) * q = q + p * q.
Lemma mul_succ_r p q : p * (succ q) = p + p * q.

## Parity properties of multiplication

Lemma mul_xI_mul_xO_discr p q r : p~1 * r <> q~0 * r.
Lemma mul_xO_discr p q : p~0 * q <> q.

## Simplification properties of multiplication

Theorem mul_reg_r p q r : p * r = q * r -> p = q.
Theorem mul_reg_l p q r : r * p = r * q -> p = q.
Lemma mul_cancel_r p q r : p * r = q * r <-> p = q.
Lemma mul_cancel_l p q r : r * p = r * q <-> p = q.

## Inversion of multiplication

Lemma mul_eq_1_l p q : p * q = 1 -> p = 1.
Lemma mul_eq_1_r p q : p * q = 1 -> q = 1.
Notation mul_eq_1 := mul_eq_1_l.

## Square

Lemma square_xO p : p~0 * p~0 = (p*p)~0~0.
Lemma square_xI p : p~1 * p~1 = (p*p+p)~0~1.

## Properties of iter

Lemma iter_swap_gen : forall A B (f:A->B)(g:A->A)(h:B->B),
(forall a, f (g a) = h (f a)) -> forall p a,
f (iter p g a) = iter p h (f a).
Theorem iter_swap :
forall p (A:Type) (f:A -> A) (x:A),
iter p f (f x) = f (iter p f x).
Theorem iter_succ :
forall p (A:Type) (f:A -> A) (x:A),
iter (succ p) f x = f (iter p f x).
Theorem iter_add :
forall p q (A:Type) (f:A -> A) (x:A),
iter (p+q) f x = iter p f (iter q f x).
Theorem iter_invariant :
forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop),
(forall x:A, Inv x -> Inv (f x)) ->
forall x:A, Inv x -> Inv (iter p f x).

## Properties of power

Lemma pow_1_r p : p^1 = p.
Lemma pow_succ_r p q : p^(succ q) = p * p^q.

## Properties of square

Lemma square_spec p : square p = p * p.

## Properties of sub_mask

Lemma sub_mask_succ_r p q :
sub_mask p (succ q) = sub_mask_carry p q.
Theorem sub_mask_carry_spec p q :
sub_mask_carry p q = pred_mask (sub_mask p q).
Inductive SubMaskSpec (p q : positive) : mask -> Prop :=
| SubIsNul : p = q -> SubMaskSpec p q IsNul
| SubIsPos : forall r, q + r = p -> SubMaskSpec p q (IsPos r)
| SubIsNeg : forall r, p + r = q -> SubMaskSpec p q IsNeg.
Theorem sub_mask_spec p q : SubMaskSpec p q (sub_mask p q).
Theorem sub_mask_nul_iff p q : sub_mask p q = IsNul <-> p = q.
Theorem sub_mask_diag p : sub_mask p p = IsNul.
Lemma sub_mask_add p q r : sub_mask p q = IsPos r -> q + r = p.
Lemma sub_mask_add_diag_l p q : sub_mask (p+q) p = IsPos q.
Lemma sub_mask_pos_iff p q r : sub_mask p q = IsPos r <-> q + r = p.
Lemma sub_mask_add_diag_r p q : sub_mask p (p+q) = IsNeg.
Lemma sub_mask_neg_iff p q : sub_mask p q = IsNeg <-> exists r, p + r = q.

# Properties of boolean comparisons

Theorem eqb_eq p q : (p =? q) = true <-> p=q.
Theorem ltb_lt p q : (p <? q) = true <-> p < q.
Theorem leb_le p q : (p <=? q) = true <-> p <= q.
More about eqb
Include BoolEqualityFacts.

# Properties of comparison on binary positive numbers

First, we express compare_cont in term of compare
Definition switch_Eq c c' :=
match c' with
| Eq => c
| Lt => Lt
| Gt => Gt
end.
Lemma compare_cont_spec p q c :
compare_cont p q c = switch_Eq c (p ?= q).
From this general result, we now describe particular cases of compare_cont p q c = c' :

- When c=Eq, this is directly compare
- When c<>Eq, we'll show first that c'<>Eq
- That leaves only 4 lemmas for c and c' being Lt or Gt

Theorem compare_cont_Eq p q c :
compare_cont p q c = Eq -> c = Eq.
Lemma compare_cont_Lt_Gt p q :
compare_cont p q Lt = Gt <-> p > q.
Lemma compare_cont_Lt_Lt p q :
compare_cont p q Lt = Lt <-> p <= q.
Lemma compare_cont_Gt_Lt p q :
compare_cont p q Gt = Lt <-> p < q.
Lemma compare_cont_Gt_Gt p q :
compare_cont p q Gt = Gt <-> p >= q.
We can express recursive equations for compare
Lemma compare_xO_xO p q : (p~0 ?= q~0) = (p ?= q).
Lemma compare_xI_xI p q : (p~1 ?= q~1) = (p ?= q).
Lemma compare_xI_xO p q :
(p~1 ?= q~0) = switch_Eq Gt (p ?= q).
Lemma compare_xO_xI p q :
(p~0 ?= q~1) = switch_Eq Lt (p ?= q).
Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare.
Ltac simpl_compare := autorewrite with compare.
Ltac simpl_compare_in H := autorewrite with compare in H.
Relation between compare and sub_mask
Definition mask2cmp (p:mask) : comparison :=
match p with
| IsNul => Eq
| IsPos _ => Gt
| IsNeg => Lt
end.
Lemma compare_sub_mask p q : (p ?= q) = mask2cmp (sub_mask p q).
Alternative characterisation of strict order in term of addition
Lemma lt_iff_add p q : p < q <-> exists r, p + r = q.
Lemma gt_iff_add p q : p > q <-> exists r, q + r = p.
Basic facts about compare_cont
Theorem compare_cont_refl p c :
compare_cont p p c = c.
Lemma compare_cont_antisym p q c :
CompOpp (compare_cont p q c) = compare_cont q p (CompOpp c).
Basic facts about compare
Lemma compare_eq_iff p q : (p ?= q) = Eq <-> p = q.
Lemma compare_antisym p q : (q ?= p) = CompOpp (p ?= q).
Lemma compare_lt_iff p q : (p ?= q) = Lt <-> p < q.
Lemma compare_le_iff p q : (p ?= q) <> Gt <-> p <= q.
More properties about compare and boolean comparisons, including compare_spec and lt_irrefl and lt_eq_cases.
Include BoolOrderFacts.
Definition le_lteq := lt_eq_cases.

## Facts about gt and ge

The predicates lt and le are now favored in the statements of theorems, the use of gt and ge is hence not recommended. We provide here the bare minimal results to related them with lt and le.
Lemma gt_lt_iff p q : p > q <-> q < p.
Lemma gt_lt p q : p > q -> q < p.
Lemma lt_gt p q : p < q -> q > p.
Lemma ge_le_iff p q : p >= q <-> q <= p.
Lemma ge_le p q : p >= q -> q <= p.
Lemma le_ge p q : p <= q -> q >= p.

## Comparison and the successor

Lemma compare_succ_r p q :
switch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q).
Lemma compare_succ_l p q :
switch_Eq Lt (succ p ?= q) = switch_Eq Gt (p ?= q).
Theorem lt_succ_r p q : p < succ q <-> p <= q.
Lemma lt_succ_diag_r p : p < succ p.
Lemma compare_succ_succ p q : (succ p ?= succ q) = (p ?= q).

## 1 is the least positive number

Lemma le_1_l p : 1 <= p.
Lemma nlt_1_r p : ~ p < 1.
Lemma lt_1_succ p : 1 < succ p.

## Properties of the order

Lemma le_nlt p q : p <= q <-> ~ q < p.
Lemma lt_nle p q : p < q <-> ~ q <= p.
Lemma lt_le_incl p q : p<q -> p<=q.
Lemma lt_lt_succ n m : n < m -> n < succ m.
Lemma succ_lt_mono n m : n < m <-> succ n < succ m.
Lemma succ_le_mono n m : n <= m <-> succ n <= succ m.
Lemma lt_trans n m p : n < m -> m < p -> n < p.
Theorem lt_ind : forall (A : positive -> Prop) (n : positive),
A (succ n) ->
(forall m : positive, n < m -> A m -> A (succ m)) ->
forall m : positive, n < m -> A m.
Instance lt_strorder : StrictOrder lt.
Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) lt.
Lemma lt_total p q : p < q \/ p = q \/ q < p.
Lemma le_refl p : p <= p.
Lemma le_lt_trans n m p : n <= m -> m < p -> n < p.
Lemma lt_le_trans n m p : n < m -> m <= p -> n < p.
Lemma le_trans n m p : n <= m -> m <= p -> n <= p.
Lemma le_succ_l n m : succ n <= m <-> n < m.
Lemma le_antisym p q : p <= q -> q <= p -> p = q.
Instance le_preorder : PreOrder le.
Instance le_partorder : PartialOrder Logic.eq le.

## Comparison and addition

Lemma add_compare_mono_l p q r : (p+q ?= p+r) = (q ?= r).
Lemma add_compare_mono_r p q r : (q+p ?= r+p) = (q ?= r).

## Order and addition

Lemma lt_add_diag_r p q : p < p + q.
Lemma add_lt_mono_l p q r : q<r <-> p+q < p+r.
Lemma add_lt_mono_r p q r : q<r <-> q+p < r+p.
Lemma add_lt_mono p q r s : p<q -> r<s -> p+r<q+s.
Lemma add_le_mono_l p q r : q<=r <-> p+q<=p+r.
Lemma add_le_mono_r p q r : q<=r <-> q+p<=r+p.
Lemma add_le_mono p q r s : p<=q -> r<=s -> p+r <= q+s.

## Comparison and multiplication

Lemma mul_compare_mono_l p q r : (p*q ?= p*r) = (q ?= r).
Lemma mul_compare_mono_r p q r : (q*p ?= r*p) = (q ?= r).

## Order and multiplication

Lemma mul_lt_mono_l p q r : q<r <-> p*q < p*r.
Lemma mul_lt_mono_r p q r : q<r <-> q*p < r*p.
Lemma mul_lt_mono p q r s : p<q -> r<s -> p*r < q*s.
Lemma mul_le_mono_l p q r : q<=r <-> p*q<=p*r.
Lemma mul_le_mono_r p q r : q<=r <-> q*p<=r*p.
Lemma mul_le_mono p q r s : p<=q -> r<=s -> p*r <= q*s.
Lemma lt_add_r p q : p < p+q.
Lemma lt_not_add_l p q : ~ p+q < p.
Lemma pow_gt_1 n p : 1<n -> 1<n^p.

# Properties of subtraction on binary positive numbers

Lemma sub_1_r p : sub p 1 = pred p.
Lemma pred_sub p : pred p = sub p 1.
Theorem sub_succ_r p q : p - (succ q) = pred (p - q).

## Properties of subtraction without underflow

Lemma sub_mask_pos' p q :
q < p -> exists r, sub_mask p q = IsPos r /\ q + r = p.
Lemma sub_mask_pos p q :
q < p -> exists r, sub_mask p q = IsPos r.
Theorem sub_add p q : q < p -> (p-q)+q = p.
Lemma add_sub p q : (p+q)-q = p.
Lemma mul_sub_distr_l p q r : r<q -> p*(q-r) = p*q-p*r.
Lemma mul_sub_distr_r p q r : q<p -> (p-q)*r = p*r-q*r.
Lemma sub_lt_mono_l p q r: q<p -> p<r -> r-p < r-q.
Lemma sub_compare_mono_l p q r :
q<p -> r<p -> (p-q ?= p-r) = (r ?= q).
Lemma sub_compare_mono_r p q r :
p<q -> p<r -> (q-p ?= r-p) = (q ?= r).
Lemma sub_lt_mono_r p q r : q<p -> r<q -> q-r < p-r.
Lemma sub_decr n m : m<n -> n-m < n.
Lemma add_sub_assoc p q r : r<q -> p+(q-r) = p+q-r.
Lemma sub_add_distr p q r : q+r < p -> p-(q+r) = p-q-r.
Lemma sub_sub_distr p q r : r<q -> q-r < p -> p-(q-r) = p+r-q.
Recursive equations for sub
Lemma sub_xO_xO n m : m<n -> n~0 - m~0 = (n-m)~0.
Lemma sub_xI_xI n m : m<n -> n~1 - m~1 = (n-m)~0.
Lemma sub_xI_xO n m : m<n -> n~1 - m~0 = (n-m)~1.
Lemma sub_xO_xI n m : n~0 - m~1 = pred_double (n-m).
Properties of subtraction with underflow
Lemma sub_mask_neg_iff' p q : sub_mask p q = IsNeg <-> p < q.
Lemma sub_mask_neg p q : p<q -> sub_mask p q = IsNeg.
Lemma sub_le p q : p<=q -> p-q = 1.
Lemma sub_lt p q : p<q -> p-q = 1.
Lemma sub_diag p : p-p = 1.

## Results concerning size and size_nat

Lemma size_nat_monotone p q : p<q -> (size_nat p <= size_nat q)%nat.
Lemma size_gt p : p < 2^(size p).
Lemma size_le p : 2^(size p) <= p~0.

## Properties of min and max

First, the specification
Lemma max_l : forall x y, y<=x -> max x y = x.
Lemma max_r : forall x y, x<=y -> max x y = y.
Lemma min_l : forall x y, x<=y -> min x y = x.
Lemma min_r : forall x y, y<=x -> min x y = y.
We hence obtain all the generic properties of min and max.
Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
Ltac order := Private_Tac.order.
Minimum, maximum and constant one
Lemma max_1_l n : max 1 n = n.
Lemma max_1_r n : max n 1 = n.
Lemma min_1_l n : min 1 n = 1.
Lemma min_1_r n : min n 1 = 1.
Minimum, maximum and operations (consequences of monotonicity)
Lemma succ_max_distr n m : succ (max n m) = max (succ n) (succ m).
Lemma succ_min_distr n m : succ (min n m) = min (succ n) (succ m).
Lemma add_max_distr_l n m p : max (p + n) (p + m) = p + max n m.
Lemma add_max_distr_r n m p : max (n + p) (m + p) = max n m + p.
Lemma add_min_distr_l n m p : min (p + n) (p + m) = p + min n m.
Lemma add_min_distr_r n m p : min (n + p) (m + p) = min n m + p.
Lemma mul_max_distr_l n m p : max (p * n) (p * m) = p * max n m.
Lemma mul_max_distr_r n m p : max (n * p) (m * p) = max n m * p.
Lemma mul_min_distr_l n m p : min (p * n) (p * m) = p * min n m.
Lemma mul_min_distr_r n m p : min (n * p) (m * p) = min n m * p.

## Results concerning iter_op

Lemma iter_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,
iter_op op (succ p) a = op a (iter_op op p a).

## Results about of_nat and of_succ_nat

Lemma of_nat_succ (n:nat) : of_succ_nat n = of_nat (S n).
Lemma pred_of_succ_nat (n:nat) : pred (of_succ_nat n) = of_nat n.
Lemma succ_of_nat (n:nat) : n<>O -> succ (of_nat n) = of_succ_nat n.

## Correctness proofs for the square root function

Inductive SqrtSpec : positive*mask -> positive -> Prop :=
| SqrtExact s x : x=s*s -> SqrtSpec (s,IsNul) x
| SqrtApprox s r x : x=s*s+r -> r <= s~0 -> SqrtSpec (s,IsPos r) x.
Lemma sqrtrem_step_spec f g p x :
(f=xO \/ f=xI) -> (g=xO \/ g=xI) ->
SqrtSpec p x -> SqrtSpec (sqrtrem_step f g p) (g (f x)).
Lemma sqrtrem_spec p : SqrtSpec (sqrtrem p) p.
Lemma sqrt_spec p :
let s := sqrt p in s*s <= p < (succ s)*(succ s).

## Correctness proofs for the gcd function

Lemma divide_add_cancel_l p q r : (p | r) -> (p | q + r) -> (p | q).
Lemma divide_xO_xI p q r : (p | q~0) -> (p | r~1) -> (p | q).
Lemma divide_xO_xO p q : (p~0|q~0) <-> (p|q).
Lemma divide_mul_l p q r : (p|q) -> (p|q*r).
Lemma divide_mul_r p q r : (p|r) -> (p|q*r).
The first component of ggcd is gcd
Lemma ggcdn_gcdn : forall n a b,
fst (ggcdn n a b) = gcdn n a b.
Lemma ggcd_gcd : forall a b, fst (ggcd a b) = gcd a b.
The other components of ggcd are indeed the correct factors.
Ltac destr_pggcdn IHn :=
match goal with |- context [ ggcdn _ ?x ?y ] =>
generalize (IHn x y); destruct ggcdn as (g,(u,v)); simpl
end.
Lemma ggcdn_correct_divisors : forall n a b,
let '(g,(aa,bb)) := ggcdn n a b in
a = g*aa /\ b = g*bb.
Lemma ggcd_correct_divisors : forall a b,
let '(g,(aa,bb)) := ggcd a b in
a=g*aa /\ b=g*bb.
We can use this fact to prove a part of the gcd correctness
Lemma gcd_divide_l : forall a b, (gcd a b | a).
Lemma gcd_divide_r : forall a b, (gcd a b | b).
We now prove directly that gcd is the greatest amongst common divisors
Lemma gcdn_greatest : forall n a b, (size_nat a + size_nat b <= n)%nat ->
forall p, (p|a) -> (p|b) -> (p|gcdn n a b).
Lemma gcd_greatest : forall a b p, (p|a) -> (p|b) -> (p|gcd a b).
As a consequence, the rests after division by gcd are relatively prime
Lemma ggcd_greatest : forall a b,
let (aa,bb) := snd (ggcd a b) in
forall p, (p|aa) -> (p|bb) -> p=1.
End Pos.
Exportation of notations
Infix "+" := Pos.add : positive_scope.
Infix "-" := Pos.sub : positive_scope.
Infix "*" := Pos.mul : positive_scope.
Infix "^" := Pos.pow : positive_scope.
Infix "?=" := Pos.compare (at level 70, no associativity) : positive_scope.
Infix "=?" := Pos.eqb (at level 70, no associativity) : positive_scope.
Infix "<=?" := Pos.leb (at level 70, no associativity) : positive_scope.
Infix "<?" := Pos.ltb (at level 70, no associativity) : positive_scope.
Infix "<=" := Pos.le : positive_scope.
Infix "<" := Pos.lt : positive_scope.
Infix ">=" := Pos.ge : positive_scope.
Infix ">" := Pos.gt : 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.
Notation "( p | q )" := (Pos.divide p q) (at level 0) : positive_scope.
Compatibility notations
Notation positive := positive (only parsing).
Notation positive_rect := positive_rect (only parsing).
Notation positive_rec := positive_rec (only parsing).
Notation positive_ind := positive_ind (only parsing).
Notation xI := xI (only parsing).
Notation xO := xO (only parsing).
Notation xH := xH (only parsing).
Notation IsNul := Pos.IsNul (only parsing).
Notation IsPos := Pos.IsPos (only parsing).
Notation IsNeg := Pos.IsNeg (only parsing).
Notation Psucc := Pos.succ (compat "8.3").
Notation Pplus := Pos.add (compat "8.3").
Notation Pplus_carry := Pos.add_carry (compat "8.3").
Notation Ppred := Pos.pred (compat "8.3").
Notation Piter_op := Pos.iter_op (compat "8.3").
Notation Piter_op_succ := Pos.iter_op_succ (compat "8.3").
Notation Pmult_nat := (Pos.iter_op plus) (compat "8.3").
Notation nat_of_P := Pos.to_nat (compat "8.3").
Notation P_of_succ_nat := Pos.of_succ_nat (compat "8.3").
Notation Pdouble_minus_one := Pos.pred_double (compat "8.3").
Notation positive_mask := Pos.mask (compat "8.3").
Notation positive_mask_rect := Pos.mask_rect (compat "8.3").
Notation positive_mask_ind := Pos.mask_ind (compat "8.3").
Notation positive_mask_rec := Pos.mask_rec (compat "8.3").
Notation Pdouble_plus_one_mask := Pos.succ_double_mask (compat "8.3").
Notation Pdouble_mask := Pos.double_mask (compat "8.3").
Notation Pdouble_minus_two := Pos.double_pred_mask (compat "8.3").
Notation Pminus_mask := Pos.sub_mask (compat "8.3").
Notation Pminus_mask_carry := Pos.sub_mask_carry (compat "8.3").
Notation Pminus := Pos.sub (compat "8.3").
Notation Pmult := Pos.mul (compat "8.3").
Notation iter_pos := @Pos.iter (compat "8.3").
Notation Ppow := Pos.pow (compat "8.3").
Notation Pdiv2 := Pos.div2 (compat "8.3").
Notation Pdiv2_up := Pos.div2_up (compat "8.3").
Notation Psize := Pos.size_nat (compat "8.3").
Notation Psize_pos := Pos.size (compat "8.3").
Notation Pcompare := Pos.compare_cont (compat "8.3").
Notation Plt := Pos.lt (compat "8.3").
Notation Pgt := Pos.gt (compat "8.3").
Notation Ple := Pos.le (compat "8.3").
Notation Pge := Pos.ge (compat "8.3").
Notation Pmin := Pos.min (compat "8.3").
Notation Pmax := Pos.max (compat "8.3").
Notation Peqb := Pos.eqb (compat "8.3").
Notation positive_eq_dec := Pos.eq_dec (compat "8.3").
Notation xI_succ_xO := Pos.xI_succ_xO (compat "8.3").
Notation Psucc_discr := Pos.succ_discr (compat "8.3").
Notation Psucc_o_double_minus_one_eq_xO :=
Pos.succ_pred_double (compat "8.3").
Notation Pdouble_minus_one_o_succ_eq_xI :=
Pos.pred_double_succ (compat "8.3").
Notation xO_succ_permute := Pos.double_succ (compat "8.3").
Notation double_moins_un_xO_discr :=
Pos.pred_double_xO_discr (compat "8.3").
Notation Psucc_not_one := Pos.succ_not_1 (compat "8.3").
Notation Ppred_succ := Pos.pred_succ (compat "8.3").
Notation Psucc_pred := Pos.succ_pred_or (compat "8.3").
Notation Psucc_inj := Pos.succ_inj (compat "8.3").
Notation Pplus_carry_spec := Pos.add_carry_spec (compat "8.3").
Notation Pplus_comm := Pos.add_comm (compat "8.3").
Notation Pplus_succ_permute_r := Pos.add_succ_r (compat "8.3").
Notation Pplus_succ_permute_l := Pos.add_succ_l (compat "8.3").
Notation Pplus_no_neutral := Pos.add_no_neutral (compat "8.3").
Notation Pplus_carry_plus := Pos.add_carry_add (compat "8.3").
Notation Pplus_reg_r := Pos.add_reg_r (compat "8.3").
Notation Pplus_reg_l := Pos.add_reg_l (compat "8.3").
Notation Pplus_carry_reg_r := Pos.add_carry_reg_r (compat "8.3").
Notation Pplus_carry_reg_l := Pos.add_carry_reg_l (compat "8.3").
Notation Pplus_assoc := Pos.add_assoc (compat "8.3").
Notation Pplus_xO := Pos.add_xO (compat "8.3").
Notation Pplus_xI_double_minus_one := Pos.add_xI_pred_double (compat "8.3").
Notation Pplus_xO_double_minus_one := Pos.add_xO_pred_double (compat "8.3").
Notation Pplus_diag := Pos.add_diag (compat "8.3").
Notation PeanoView := Pos.PeanoView (compat "8.3").
Notation PeanoOne := Pos.PeanoOne (compat "8.3").
Notation PeanoSucc := Pos.PeanoSucc (compat "8.3").
Notation PeanoView_rect := Pos.PeanoView_rect (compat "8.3").
Notation PeanoView_ind := Pos.PeanoView_ind (compat "8.3").
Notation PeanoView_rec := Pos.PeanoView_rec (compat "8.3").
Notation peanoView_xO := Pos.peanoView_xO (compat "8.3").
Notation peanoView_xI := Pos.peanoView_xI (compat "8.3").
Notation peanoView := Pos.peanoView (compat "8.3").
Notation PeanoView_iter := Pos.PeanoView_iter (compat "8.3").
Notation eq_dep_eq_positive := Pos.eq_dep_eq_positive (compat "8.3").
Notation PeanoViewUnique := Pos.PeanoViewUnique (compat "8.3").
Notation Prect := Pos.peano_rect (compat "8.3").
Notation Prect_succ := Pos.peano_rect_succ (compat "8.3").
Notation Prect_base := Pos.peano_rect_base (compat "8.3").
Notation Prec := Pos.peano_rec (compat "8.3").
Notation Pind := Pos.peano_ind (compat "8.3").
Notation Pcase := Pos.peano_case (compat "8.3").
Notation Pmult_1_r := Pos.mul_1_r (compat "8.3").
Notation Pmult_Sn_m := Pos.mul_succ_l (compat "8.3").
Notation Pmult_xO_permute_r := Pos.mul_xO_r (compat "8.3").
Notation Pmult_xI_permute_r := Pos.mul_xI_r (compat "8.3").
Notation Pmult_comm := Pos.mul_comm (compat "8.3").
Notation Pmult_plus_distr_l := Pos.mul_add_distr_l (compat "8.3").
Notation Pmult_plus_distr_r := Pos.mul_add_distr_r (compat "8.3").
Notation Pmult_assoc := Pos.mul_assoc (compat "8.3").
Notation Pmult_xI_mult_xO_discr := Pos.mul_xI_mul_xO_discr (compat "8.3").
Notation Pmult_xO_discr := Pos.mul_xO_discr (compat "8.3").
Notation Pmult_reg_r := Pos.mul_reg_r (compat "8.3").
Notation Pmult_reg_l := Pos.mul_reg_l (compat "8.3").
Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (compat "8.3").
Notation Psquare_xO := Pos.square_xO (compat "8.3").
Notation Psquare_xI := Pos.square_xI (compat "8.3").
Notation iter_pos_swap_gen := Pos.iter_swap_gen (compat "8.3").
Notation iter_pos_swap := Pos.iter_swap (compat "8.3").
Notation iter_pos_succ := Pos.iter_succ (compat "8.3").
Notation iter_pos_plus := Pos.iter_add (compat "8.3").
Notation iter_pos_invariant := Pos.iter_invariant (compat "8.3").
Notation Ppow_1_r := Pos.pow_1_r (compat "8.3").
Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.3").
Notation Peqb_refl := Pos.eqb_refl (compat "8.3").
Notation Peqb_eq := Pos.eqb_eq (compat "8.3").
Notation Pcompare_refl_id := Pos.compare_cont_refl (compat "8.3").
Notation Pcompare_eq_iff := Pos.compare_eq_iff (compat "8.3").
Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (compat "8.3").
Notation Pcompare_eq_Lt := Pos.compare_lt_iff (compat "8.3").
Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (compat "8.3").
Notation Pcompare_antisym := Pos.compare_cont_antisym (compat "8.3").
Notation ZC1 := Pos.gt_lt (compat "8.3").
Notation ZC2 := Pos.lt_gt (compat "8.3").
Notation Pcompare_spec := Pos.compare_spec (compat "8.3").
Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (compat "8.3").
Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.3").
Notation Pcompare_1 := Pos.nlt_1_r (compat "8.3").
Notation Plt_1 := Pos.nlt_1_r (compat "8.3").
Notation Plt_1_succ := Pos.lt_1_succ (compat "8.3").
Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.3").
Notation Plt_irrefl := Pos.lt_irrefl (compat "8.3").
Notation Plt_trans := Pos.lt_trans (compat "8.3").
Notation Plt_ind := Pos.lt_ind (compat "8.3").
Notation Ple_lteq := Pos.le_lteq (compat "8.3").
Notation Ple_refl := Pos.le_refl (compat "8.3").
Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.3").
Notation Plt_le_trans := Pos.lt_le_trans (compat "8.3").
Notation Ple_trans := Pos.le_trans (compat "8.3").
Notation Plt_succ_r := Pos.lt_succ_r (compat "8.3").
Notation Ple_succ_l := Pos.le_succ_l (compat "8.3").
Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (compat "8.3").
Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (compat "8.3").
Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (compat "8.3").
Notation Pplus_lt_mono_r := Pos.add_lt_mono_r (compat "8.3").
Notation Pplus_lt_mono := Pos.add_lt_mono (compat "8.3").
Notation Pplus_le_mono_l := Pos.add_le_mono_l (compat "8.3").
Notation Pplus_le_mono_r := Pos.add_le_mono_r (compat "8.3").
Notation Pplus_le_mono := Pos.add_le_mono (compat "8.3").
Notation Pmult_compare_mono_l := Pos.mul_compare_mono_l (compat "8.3").
Notation Pmult_compare_mono_r := Pos.mul_compare_mono_r (compat "8.3").
Notation Pmult_lt_mono_l := Pos.mul_lt_mono_l (compat "8.3").
Notation Pmult_lt_mono_r := Pos.mul_lt_mono_r (compat "8.3").
Notation Pmult_lt_mono := Pos.mul_lt_mono (compat "8.3").
Notation Pmult_le_mono_l := Pos.mul_le_mono_l (compat "8.3").
Notation Pmult_le_mono_r := Pos.mul_le_mono_r (compat "8.3").
Notation Pmult_le_mono := Pos.mul_le_mono (compat "8.3").
Notation Plt_plus_r := Pos.lt_add_r (compat "8.3").
Notation Plt_not_plus_l := Pos.lt_not_add_l (compat "8.3").
Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.3").
Notation Ppred_mask := Pos.pred_mask (compat "8.3").
Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (compat "8.3").
Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (compat "8.3").
Notation Pminus_succ_r := Pos.sub_succ_r (compat "8.3").
Notation Pminus_mask_diag := Pos.sub_mask_diag (compat "8.3").
Notation Pplus_minus_eq := Pos.add_sub (compat "8.3").
Notation Pmult_minus_distr_l := Pos.mul_sub_distr_l (compat "8.3").
Notation Pminus_lt_mono_l := Pos.sub_lt_mono_l (compat "8.3").
Notation Pminus_compare_mono_l := Pos.sub_compare_mono_l (compat "8.3").
Notation Pminus_compare_mono_r := Pos.sub_compare_mono_r (compat "8.3").
Notation Pminus_lt_mono_r := Pos.sub_lt_mono_r (compat "8.3").
Notation Pminus_decr := Pos.sub_decr (compat "8.3").
Notation Pminus_xI_xI := Pos.sub_xI_xI (compat "8.3").
Notation Pplus_minus_assoc := Pos.add_sub_assoc (compat "8.3").
Notation Pminus_plus_distr := Pos.sub_add_distr (compat "8.3").
Notation Pminus_minus_distr := Pos.sub_sub_distr (compat "8.3").
Notation Pminus_mask_Lt := Pos.sub_mask_neg (compat "8.3").
Notation Pminus_Lt := Pos.sub_lt (compat "8.3").
Notation Pminus_Eq := Pos.sub_diag (compat "8.3").
Notation Psize_monotone := Pos.size_nat_monotone (compat "8.3").
Notation Psize_pos_gt := Pos.size_gt (compat "8.3").
Notation Psize_pos_le := Pos.size_le (compat "8.3").
More complex compatibility facts, expressed as lemmas (to preserve scopes for instance)
Lemma Peqb_true_eq x y : Pos.eqb x y = true -> x=y.
Lemma Pcompare_eq_Gt p q : (p ?= q) = Gt <-> p > q.
Lemma Pplus_one_succ_r p : Pos.succ p = p + 1.
Lemma Pplus_one_succ_l p : Pos.succ p = 1 + p.
Lemma Pcompare_refl p : Pos.compare_cont p p Eq = Eq.
Lemma Pcompare_Eq_eq : forall p q, Pos.compare_cont p q Eq = Eq -> p = q.
Lemma ZC4 p q : Pos.compare_cont p q Eq = CompOpp (Pos.compare_cont q p Eq).
Lemma Ppred_minus p : Pos.pred p = p - 1.
Lemma Pminus_mask_Gt p q :
p > q ->
exists h : positive,
Pos.sub_mask p q = IsPos h /\
q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = IsPos (Pos.pred h)).
Lemma Pplus_minus : forall p q, p > q -> q+(p-q) = p.
Discontinued results of little interest and little/zero use in user contributions:
Pplus_carry_no_neutral Pplus_carry_pred_eq_plus Pcompare_not_Eq Pcompare_Lt_Lt Pcompare_Lt_eq_Lt Pcompare_Gt_Gt Pcompare_Gt_eq_Gt Psucc_lt_compat Psucc_le_compat ZC3 Pcompare_p_Sq Pminus_mask_carry_diag Pminus_mask_IsNeg ZL10 ZL11 double_eq_zero_inversion double_plus_one_zero_discr double_plus_one_eq_one_inversion double_eq_one_discr
Infix "/" := Pdiv2 : positive_scope.
Old stuff, to remove someday
Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt.
Incompatibilities :

- (_ ?= _)%positive expects no arg now, and designates Pos.compare which is convertible but syntactically distinct to Pos.compare_cont .. .. Eq.
- Pmult_nat cannot be unfolded (unfold Pos.iter_op instead).