Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. Style: centered; floating; windowed.
(* -*- coding: utf-8 -*- *) (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Export BinNums. Require Import Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax Le Plus. Require Export BinPosDef. (**********************************************************************)
(**********************************************************************)
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.
Every definitions and early properties about positive numbers
are placed in a module Pos for qualification purpose.
Module Pos
<: UsualOrderedTypeFull
<: UsualDecidableTypeFull
<: TotalOrder.
Include BinPosDef.Pos.
In functor applications that follow, we only inline t and eq
Set Inline Level 30.
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. (**********************************************************************)
forall x y : positive, {x = y} + {x <> y}decide equality. Defined. (**********************************************************************)forall x y : positive, {x = y} + {x <> y}
p:positivep~1 = succ p~0reflexivity. Qed.p:positivep~1 = succ p~0p:positivep <> succ pnow destruct p. Qed.p:positivep <> succ p
p:positivepred_double p = pred p~0reflexivity. Qed.p:positivepred_double p = pred p~0p:positivesucc (pred_double p) = p~0induction p; simpl; now f_equal. Qed.p:positivesucc (pred_double p) = p~0p:positivepred_double (succ p) = p~1induction p; simpl; now f_equal. Qed.p:positivepred_double (succ p) = p~1p:positive(succ p)~0 = succ (succ p~0)now destruct p. Qed.p:positive(succ p)~0 = succ (succ p~0)p:positivepred_double p <> p~0now destruct p. Qed.p:positivepred_double p <> p~0
p:positivesucc p <> 1now destruct p. Qed.p:positivesucc p <> 1p:positivepred (succ p) = pp:positivepred (succ p) = papply pred_double_succ. Qed.p:positivepred_double (succ p) = p~1p:positivep = 1 \/ succ (pred p) = pp:positivep = 1 \/ succ (pred p) = pright; apply succ_pred_double. Qed.p:positivep~0 = 1 \/ succ (pred_double p) = p~0p:positivep <> 1 -> succ (pred p) = pp:positivep <> 1 -> succ (pred p) = pp:positiveH:p~0 <> 1succ (pred_double p) = p~0H:1 <> 12 = 1now destruct H. Qed.H:1 <> 12 = 1
p, q:positivesucc p = succ q -> p = qp, q:positivesucc p = succ q -> p = qp:positiveforall q : positive, succ p = succ q -> p = qp:positiveIHp:forall q : positive, succ p = succ q -> p = qH:succ p = 1p~1 = 1q:positiveH:1 = succ q1 = q~1elim (succ_not_1 q); auto. Qed.q:positiveH:1 = succ q1 = q~1
p:positivepred_N (succ p) = Npos pp:positivepred_N (succ p) = Npos pp:positiveNpos (pred_double (succ p)) = Npos p~1apply pred_double_succ. Qed. (**********************************************************************)p:positivepred_double (succ p) = p~1
p:positivep + 1 = succ pnow destruct p. Qed.p:positivep + 1 = succ pp:positive1 + p = succ pnow destruct p. Qed.p:positive1 + p = succ p
p, q:positiveadd_carry p q = succ (p + q)p, q:positiveadd_carry p q = succ (p + q)induction p; destruct q; simpl; now f_equal. Qed.p:positiveforall q : positive, add_carry p q = succ (p + q)
p, q:positivep + q = q + pp, q:positivep + q = q + pp:positiveforall q : positive, p + q = q + prewrite 2 add_carry_spec; now f_equal. Qed.p:positiveIHp:forall q0 : positive, p + q0 = q0 + pq:positiveadd_carry p q = add_carry q p
p, q:positivep + succ q = succ (p + q)p, q:positivep + succ q = succ (p + q)induction p; destruct q; simpl; f_equal; auto using add_1_r; rewrite add_carry_spec; auto. Qed.p:positiveforall q : positive, p + succ q = succ (p + q)p, q:positivesucc p + q = succ (p + q)p, q:positivesucc p + q = succ (p + q)apply add_succ_r. Qed.p, q:positiveq + succ p = succ (q + p)
p, q:positiveq + p <> pp, q:positiveq + p <> pinduction p as [p IHp|p IHp| ]; intros [q|q| ] H; destr_eq H; apply (IHp q H). Qed.p:positiveforall q : positive, q + p <> p
p, q, r, s:positiveadd_carry p r = add_carry q s -> p + r = q + sintros H; apply succ_inj; now rewrite <- 2 add_carry_spec. Qed.p, q, r, s:positiveadd_carry p r = add_carry q s -> p + r = q + sp, q, r:positivep + r = q + r -> p = qp, q, r:positivep + r = q + r -> p = qr:positiveforall p q : positive, p + r = q + r -> p = qr:positiveIHr:forall p q : positive, p + r = q + r -> p = qforall p q : positive, p + r~1 = q + r~1 -> p = qr:positiveIHr:forall p q : positive, p + r = q + r -> p = qforall p q : positive, p + r~0 = q + r~0 -> p = qforall p q : positive, p + 1 = q + 1 -> p = qr:positiveIHr:forall p q : positive, p + r = q + r -> p = qforall p q : positive, p + r~0 = q + r~0 -> p = qforall p q : positive, p + 1 = q + 1 -> p = qforall p q : positive, p + 1 = q + 1 -> p = qp, q:positiveH:p + 1 = q + 1p = qnow rewrite <- 2 add_1_r. Qed.p, q:positiveH:p + 1 = q + 1succ p = succ qp, q, r:positivep + q = p + r -> q = rp, q, r:positivep + q = p + r -> q = rnow apply add_reg_r. Qed.p, q, r:positiveq + p = r + p -> q = rp, q, r:positivep + r = q + r <-> p = qp, q, r:positivep + r = q + r <-> p = qp, q, r:positivep + r = q + r -> p = qp, q, r:positivep = q -> p + r = q + rcongruence. Qed.p, q, r:positivep = q -> p + r = q + rp, q, r:positiver + p = r + q <-> p = qp, q, r:positiver + p = r + q <-> p = qp, q, r:positiver + p = r + q -> p = qp, q, r:positivep = q -> r + p = r + qcongruence. Qed.p, q, r:positivep = q -> r + p = r + qp, q, r:positiveadd_carry p r = add_carry q r -> p = qp, q, r:positiveadd_carry p r = add_carry q r -> p = qapply add_reg_r with (r:=r); now apply add_carry_add. Qed.p, q, r:positiveH:add_carry p r = add_carry q rp = qp, q, r:positiveadd_carry p q = add_carry p r -> q = rintros H; apply add_reg_r with (r:=p); rewrite (add_comm r), (add_comm q); now apply add_carry_add. Qed.p, q, r:positiveadd_carry p q = add_carry p r -> q = r
p, q, r:positivep + (q + r) = p + q + rp, q, r:positivep + (q + r) = p + q + rp:positiveforall q r : positive, p + (q + r) = p + q + rp:positiveIHp:forall q r : positive, p + (q + r) = p + q + rforall q r : positive, p~1 + (q + r) = p~1 + q + rp:positiveIHp:forall q r : positive, p + (q + r) = p + q + rforall q r : positive, p~0 + (q + r) = p~0 + q + rforall q r : positive, 1 + (q + r) = 1 + q + rp:positiveIHp:forall q r : positive, p + (q + r) = p + q + rforall q r : positive, p~0 + (q + r) = p~0 + q + rforall q r : positive, 1 + (q + r) = 1 + q + rintros q r; rewrite 2 add_1_l, add_succ_l; auto. Qed.forall q r : positive, 1 + (q + r) = 1 + q + r
p, q:positive(p + q)~0 = p~0 + q~0now destruct p, q. Qed.p, q:positive(p + q)~0 = p~0 + q~0p, q:positive(p + q)~0 = p~1 + pred_double qp, q:positive(p + q)~0 = p~1 + pred_double qnow rewrite <- add_assoc, add_1_l, succ_pred_double. Qed.p, q:positive(p + q)~0 = p~0 + 1 + pred_double qp, q:positivepred_double (p + q) = p~0 + pred_double qp, q:positivepred_double (p + q) = p~0 + pred_double qp:positiveforall q : positive, pred_double (p + q) = p~0 + pred_double qp:positiveIHp:forall q0 : positive, pred_double (p + q0) = p~0 + pred_double q0q:positive(pred_double (p + q))~1 = match pred_double q with | q0~1 => (p + q0)~1 | q0~0 => (p + q0)~0 | 1 => p~1 end~1q:positiveq~0~1 = match pred_double q with | q0~1 => (succ q0)~0 | q0~0 => q0~1 | 1 => 2 end~1q:positiveq~0~1 = match pred_double q with | q0~1 => (succ q0)~0 | q0~0 => q0~1 | 1 => 2 end~1reflexivity. Qed.q:positive(1 + pred_double q)~1 = match pred_double q with | q0~1 => (succ q0)~0 | q0~0 => q0~1 | 1 => 2 end~1
p:positivep + p = p~0induction p as [p IHp| p IHp| ]; simpl; now rewrite ?add_carry_spec, ?IHp. Qed. (**********************************************************************)p:positivep + p = p~0
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.P:positive -> Typea:P 1f:forall p0 : positive, P p0 -> P (succ p0)p:positivepeano_rect P a f (succ p) = f p (peano_rect P a f p)P:positive -> Typea:P 1f:forall p0 : positive, P p0 -> P (succ p0)p:positivepeano_rect P a f (succ p) = f p (peano_rect P a f p)p:positiveforall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), peano_rect P a f (succ p) = f p (peano_rect P a f p)p:positiveIHp:forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), peano_rect P a f (succ p) = f p (peano_rect P a f p)forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), peano_rect P a f (succ p~1) = f p~1 (peano_rect P a f p~1)p:positiveIHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), peano_rect P0 a0 f0 (succ p) = f0 p (peano_rect P0 a0 f0 p)P:positive -> Typea:P 1f:forall p0 : positive, P p0 -> P (succ p0)peano_rect P a f (succ p~1) = f p~1 (peano_rect P a f p~1)now rewrite IHp. Qed.p:positiveIHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), peano_rect P0 a0 f0 (succ p) = f0 p (peano_rect P0 a0 f0 p)P:positive -> Typea:P 1f:forall p0 : positive, P p0 -> P (succ p0)peano_rect (fun p0 : positive => P p0~0) (f 1 a) (fun (p0 : positive) (x : P p0~0) => f p0~1 (f p0~0 x)) (succ p) = f p~1 (f p~0 (peano_rect (fun p0 : positive => P p0~0) (f 1 a) (fun (p0 : positive) (x : P p0~0) => f p0~1 (f p0~0 x)) p))P:positive -> Typea:P 1f:forall p : positive, P p -> P (succ p)peano_rect P a f 1 = atrivial. Qed. Definition peano_rec (P:positive->Set) := peano_rect P.P:positive -> Typea:P 1f:forall p : positive, P p -> P (succ p)peano_rect P a f 1 = a
Peano induction
Definition peano_ind (P:positive->Prop) := peano_rect P.
Peano case analysis
forall P : positive -> Prop, P 1 -> (forall n : positive, P (succ n)) -> forall p : positive, P pintros; apply peano_ind; auto. Qed.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).forall (P : positive -> Type) (p : positive) (x y : P p), eq_dep positive P p x p y -> x = yforall (P : positive -> Type) (p : positive) (x y : P p), eq_dep positive P p x p y -> x = ydecide equality. Qed.forall x y : positive, {x = y} + {x <> y}forall (p : positive) (q q' : PeanoView p), q = q'forall (p : positive) (q q' : PeanoView p), q = q'p:positiveq, q':PeanoView pq = q'q':PeanoView 1PeanoOne = q'p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0PeanoSucc p q = q'q':PeanoView 1eq_dep positive PeanoView 1 PeanoOne 1 q'p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0PeanoSucc p q = q'q':PeanoView 11 = 1 -> eq_dep positive PeanoView 1 PeanoOne 1 q'q':PeanoView 11 = 1p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0PeanoSucc p q = q'q':PeanoView 1(fun (p : positive) (p0 : PeanoView p) => p = 1 -> eq_dep positive PeanoView 1 PeanoOne p p0) 1 q'q':PeanoView 11 = 1p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0PeanoSucc p q = q'1 = 1 -> eq_dep positive PeanoView 1 PeanoOne 1 PeanoOnep:positiveq':PeanoView psucc p = 1 -> eq_dep positive PeanoView 1 PeanoOne (succ p) (PeanoSucc p q')q':PeanoView 11 = 1p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0PeanoSucc p q = q'p:positiveq':PeanoView psucc p = 1 -> eq_dep positive PeanoView 1 PeanoOne (succ p) (PeanoSucc p q')q':PeanoView 11 = 1p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0PeanoSucc p q = q'q':PeanoView 11 = 1p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0PeanoSucc p q = q'p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0PeanoSucc p q = q'p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p) q'p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p) q'p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0(fun (p0 : positive) (p1 : PeanoView p0) => p0 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) p0 p1) (succ p) q'p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pIHq:forall q' : PeanoView p, q = q'1 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) 1 PeanoOnep:positiveq:PeanoView pp0:positiveq':PeanoView p0IHq:forall q'0 : PeanoView p, q = q'0succ p0 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pIHq:forall q' : PeanoView p, q = q'H:1 = succ peq_dep positive PeanoView (succ p) (PeanoSucc p q) 1 PeanoOnep:positiveq:PeanoView pp0:positiveq':PeanoView p0IHq:forall q'0 : PeanoView p, q = q'0succ p0 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pp0:positiveq':PeanoView p0IHq:forall q'0 : PeanoView p, q = q'0succ p0 = succ p -> eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pp0:positiveq':PeanoView p0IHq:forall q'0 : PeanoView p, q = q'0H:succ p0 = succ peq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pp0:positiveq':PeanoView p0IHq:forall q'0 : PeanoView p, q = q'0H:p0 = peq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q')p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pp0:positiveq':PeanoView p0IHq:forall q'0 : PeanoView p, q = q'0H:p0 = pforall q'0 : PeanoView p0, eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p0) (PeanoSucc p0 q'0)p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pp0:positiveq':PeanoView p0IHq:forall q'0 : PeanoView p, q = q'0H:p0 = pforall q'0 : PeanoView p, eq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p) (PeanoSucc p q'0)p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pp0:positiveq':PeanoView p0IHq:forall q'1 : PeanoView p, q = q'1H:p0 = pq'0:PeanoView peq_dep positive PeanoView (succ p) (PeanoSucc p q) (succ p) (PeanoSucc p q'0)p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pp:positiveq:PeanoView pp0:positiveq':PeanoView p0IHq:forall q'1 : PeanoView p, q = q'1H:p0 = pq'0:PeanoView peq_dep positive PeanoView (succ p) (PeanoSucc p q'0) (succ p) (PeanoSucc p q'0)p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ ptrivial. Qed.p:positiveq:PeanoView pq':PeanoView (succ p)IHq:forall q'0 : PeanoView p, q = q'0succ p = succ pP:positive -> Typea:P 1f:forall p0 : positive, P p0 -> P (succ p0)p:positivePeanoView_iter P a f p (peanoView p) = peano_rect P a f pP:positive -> Typea:P 1f:forall p0 : positive, P p0 -> P (succ p0)p:positivePeanoView_iter P a f p (peanoView p) = peano_rect P a f pp:positiveforall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), PeanoView_iter P a f p (peanoView p) = peano_rect P a f pforall (P : positive -> Type) (a : P 1) (f : forall p : positive, P p -> P (succ p)), PeanoView_iter P a f 1 (peanoView 1) = peano_rect P a f 1p:positiveIHp:forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), PeanoView_iter P a f p (peanoView p) = peano_rect P a f pforall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), PeanoView_iter P a f (succ p) (peanoView (succ p)) = peano_rect P a f (succ p)p:positiveIHp:forall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), PeanoView_iter P a f p (peanoView p) = peano_rect P a f pforall (P : positive -> Type) (a : P 1) (f : forall p0 : positive, P p0 -> P (succ p0)), PeanoView_iter P a f (succ p) (peanoView (succ p)) = peano_rect P a f (succ p)p:positiveIHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), PeanoView_iter P0 a0 f0 p (peanoView p) = peano_rect P0 a0 f0 pP:positive -> Typea:P 1f:forall p0 : positive, P p0 -> P (succ p0)PeanoView_iter P a f (succ p) (peanoView (succ p)) = peano_rect P a f (succ p)p:positiveIHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), PeanoView_iter P0 a0 f0 p (peanoView p) = peano_rect P0 a0 f0 pP:positive -> Typea:P 1f:forall p0 : positive, P p0 -> P (succ p0)PeanoView_iter P a f (succ p) (peanoView (succ p)) = f p (peano_rect P a f p)simpl; now f_equal. Qed. (**********************************************************************)p:positiveIHp:forall (P0 : positive -> Type) (a0 : P0 1) (f0 : forall p0 : positive, P0 p0 -> P0 (succ p0)), PeanoView_iter P0 a0 f0 p (peanoView p) = peano_rect P0 a0 f0 pP:positive -> Typea:P 1f:forall p0 : positive, P p0 -> P (succ p0)PeanoView_iter P a f (succ p) (PeanoSucc p (peanoView p)) = f p (peano_rect P a f p)
p:positive1 * p = preflexivity. Qed.p:positive1 * p = pp:positivep * 1 = pinduction p; simpl; now f_equal. Qed.p:positivep * 1 = p
p, q:positivep * q~0 = (p * q)~0induction p; simpl; f_equal; f_equal; trivial. Qed.p, q:positivep * q~0 = (p * q)~0p, q:positivep * q~1 = p + (p * q)~0p, q:positivep * q~1 = p + (p * q)~0now rewrite IHp, 2 add_assoc, (add_comm p). Qed.p, q:positiveIHp:p * q~1 = p + (p * q)~0q + p * q~1 = p + (q + (p * q)~0)
p, q:positivep * q = q * pinduction q as [q IHq|q IHq| ]; simpl; rewrite <- ? IHq; auto using mul_xI_r, mul_xO_r, mul_1_r. Qed.p, q:positivep * q = q * p
p, q, r:positivep * (q + r) = p * q + p * rp, q, r:positivep * (q + r) = p * q + p * rp, q, r:positiveIHp:p * (q + r) = p * q + p * rq + r + (p * (q + r))~0 = q + (p * q)~0 + (r + (p * r)~0)p, q, r:positiveIHp:p * (q + r) = p * q + p * r(p * (q + r))~0 = (p * q + p * r)~0q, r:positiveq + r = q + rp, q, r:positiveIHp:p * (q + r) = p * q + p * rq + r + (p * q + p * r)~0 = q + (p * q)~0 + (r + (p * r)~0)p, q, r:positiveIHp:p * (q + r) = p * q + p * r(p * (q + r))~0 = (p * q + p * r)~0q, r:positiveq + r = q + rp, q, r:positiveIHp:p * (q + r) = p * q + p * rm:=(p * q)~0:positiveq + r + (p * q + p * r)~0 = q + m + (r + (p * r)~0)p, q, r:positiveIHp:p * (q + r) = p * q + p * r(p * (q + r))~0 = (p * q + p * r)~0q, r:positiveq + r = q + rp, q, r:positiveIHp:p * (q + r) = p * q + p * rm:=(p * q)~0:positiven:=(p * r)~0:positiveq + r + (p * q + p * r)~0 = q + m + (r + n)p, q, r:positiveIHp:p * (q + r) = p * q + p * r(p * (q + r))~0 = (p * q + p * r)~0q, r:positiveq + r = q + rp, q, r:positiveIHp:p * (q + r) = p * q + p * rm:=(p * q)~0:positiven:=(p * r)~0:positiveq + r + (m + n) = q + m + (r + n)p, q, r:positiveIHp:p * (q + r) = p * q + p * r(p * (q + r))~0 = (p * q + p * r)~0q, r:positiveq + r = q + rp, q, r:positiveIHp:p * (q + r) = p * q + p * rm:=(p * q)~0:positiven:=(p * r)~0:positiveq + r + m = q + m + rp, q, r:positiveIHp:p * (q + r) = p * q + p * r(p * (q + r))~0 = (p * q + p * r)~0q, r:positiveq + r = q + rp, q, r:positiveIHp:p * (q + r) = p * q + p * rm:=(p * q)~0:positiven:=(p * r)~0:positiver + m = m + rp, q, r:positiveIHp:p * (q + r) = p * q + p * r(p * (q + r))~0 = (p * q + p * r)~0q, r:positiveq + r = q + rp, q, r:positiveIHp:p * (q + r) = p * q + p * r(p * (q + r))~0 = (p * q + p * r)~0q, r:positiveq + r = q + rreflexivity. Qed.q, r:positiveq + r = q + rp, q, r:positive(p + q) * r = p * r + q * rrewrite 3 (mul_comm _ r); apply mul_add_distr_l. Qed.p, q, r:positive(p + q) * r = p * r + q * r
p, q, r:positivep * (q * r) = p * q * rp, q, r:positivep * (q * r) = p * q * rnow rewrite mul_add_distr_r. Qed.p, q, r:positiveIHp:p * (q * r) = p * q * rq * r + (p * q * r)~0 = (q + (p * q)~0) * r
p, q:positivesucc p * q = q + p * qp, q:positivesucc p * q = q + p * qp, q:positiveIHp:succ p * q = q + p * q(succ p * q)~0 = q + (q + (p * q)~0)q:positiveq~0 = q + qsymmetry; apply add_diag. Qed.q:positiveq~0 = q + qp, q:positivep * succ q = p + p * qp, q:positivep * succ q = p + p * qp, q:positivep + q * p = p + p * qapply mul_comm. Qed.p, q:positiveq * p = p * q
p, q, r:positivep~1 * r <> q~0 * rp, q, r:positivep~1 * r <> q~0 * rrewrite 2 mul_xO_r; intro H; destr_eq H; auto. Qed.p, q, r:positiveIHr:p~1 * r <> q~0 * rp~1 * r~0 <> q~0 * r~0p, q:positivep~0 * q <> qp, q:positivep~0 * q <> qrewrite mul_xO_r; injection; auto. Qed.p, q:positiveIHq:p~0 * q <> qp~0 * q~0 <> q~0
p, q, r:positivep * r = q * r -> p = qp, q, r:positivep * r = q * r -> p = qp:positiveforall q r : positive, p * r = q * r -> p = qp:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~1 * r = q~1 * rp = qp:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~1 * r = 1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~1 * r = q~1 * rp * r~0 = q * r~0p:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~1 * r = 1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:r + (p * r)~0 = r + (q * r)~0p * r~0 = q * r~0p:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~1 * r = 1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:r + (p * r)~0 = r + (q * r)~0(p * r)~0 = (q * r)~0p:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~1 * r = 1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~1 * r = 1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positivep~1 * r <> q~0 * rp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~1 * r = 1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~1 * r = 1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positivep~1 * r <> 1 * rp:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiver + (p * r)~0 <> rp:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positive(p * r)~0 + r <> rp:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~1 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:q~1 * r = p~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveq~1 * r <> p~0 * rp:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp = qp:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp * r~0 = q * r~0p:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q0 r0 : positive, p * r0 = q0 * r0 -> p = q0q, r:positiveH:p~0 * r = q~0 * rp * r~0 = q * r~0p:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positiveH:p~0 * r = 1 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalsep:positiveIHp:forall q r0 : positive, p * r0 = q * r0 -> p = qr:positivep~0 * r <> 1 * rq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalseq, r:positiveH:1 * r = q~1 * rFalseq, r:positiveH:1 * r = q~0 * rFalseq, r:positiveH:q~1 * r = 1 * rFalseq, r:positiveH:1 * r = q~0 * rFalseq, r:positiveq~1 * r <> 1 * rq, r:positiveH:1 * r = q~0 * rFalseq, r:positiver + (q * r)~0 <> rq, r:positiveH:1 * r = q~0 * rFalseq, r:positive(q * r)~0 + r <> rq, r:positiveH:1 * r = q~0 * rFalseq, r:positiveH:1 * r = q~0 * rFalseq, r:positiveH:q~0 * r = 1 * rFalseapply mul_xO_discr. Qed.q, r:positiveq~0 * r <> 1 * rp, q, r:positiver * p = r * q -> p = qp, q, r:positiver * p = r * q -> p = qapply mul_reg_r. Qed.p, q, r:positivep * r = q * r -> p = qp, q, r:positivep * r = q * r <-> p = qp, q, r:positivep * r = q * r <-> p = qp, q, r:positivep * r = q * r -> p = qp, q, r:positivep = q -> p * r = q * rcongruence. Qed.p, q, r:positivep = q -> p * r = q * rp, q, r:positiver * p = r * q <-> p = qp, q, r:positiver * p = r * q <-> p = qp, q, r:positiver * p = r * q -> p = qp, q, r:positivep = q -> r * p = r * qcongruence. Qed.p, q, r:positivep = q -> r * p = r * q
p, q:positivep * q = 1 -> p = 1now destruct p, q. Qed.p, q:positivep * q = 1 -> p = 1p, q:positivep * q = 1 -> q = 1now destruct p, q. Qed. Notation mul_eq_1 := mul_eq_1_l.p, q:positivep * q = 1 -> q = 1
p:positivep~0 * p~0 = (p * p)~0~0p:positivep~0 * p~0 = (p * p)~0~0now rewrite mul_comm. Qed.p:positive(p * p~0)~0 = (p * p)~0~0p:positivep~1 * p~1 = (p * p + p)~0~1p:positivep~1 * p~1 = (p * p + p)~0~1p:positive(p + p * p~1)~1 = (p * p + p)~0~1p:positive(p + p~1 * p)~1 = (p * p + p)~0~1p:positive(p + (p + (p * p)~0))~1 = (p * p + p)~0~1p:positivep + (p + (p * p)~0) = (p * p + p)~0p:positivep~0 + (p * p)~0 = (p * p + p)~0now rewrite add_comm. Qed.p:positive(p + p * p)~0 = (p * p + p)~0
forall (A B : Type) (f : A -> B) (g : A -> A) (h : B -> B), (forall a : A, f (g a) = h (f a)) -> forall (p : positive) (a : A), f (iter g a p) = iter h (f a) pinduction p; simpl; intros; now rewrite ?H, ?IHp. Qed.forall (A B : Type) (f : A -> B) (g : A -> A) (h : B -> B), (forall a : A, f (g a) = h (f a)) -> forall (p : positive) (a : A), f (iter g a p) = iter h (f a) pforall (p : positive) (A : Type) (f : A -> A) (x : A), iter f (f x) p = f (iter f x p)forall (p : positive) (A : Type) (f : A -> A) (x : A), iter f (f x) p = f (iter f x p)p:positiveA:Typef:A -> Ax:Aiter f (f x) p = f (iter f x p)now apply iter_swap_gen. Qed.p:positiveA:Typef:A -> Ax:Af (iter f x p) = iter f (f x) pforall (p : positive) (A : Type) (f : A -> A) (x : A), iter f x (succ p) = f (iter f x p)forall (p : positive) (A : Type) (f : A -> A) (x : A), iter f x (succ p) = f (iter f x p)now rewrite !IHp, iter_swap. Qed.p:positiveIHp:forall (A0 : Type) (f0 : A0 -> A0) (x0 : A0), iter f0 x0 (succ p) = f0 (iter f0 x0 p)A:Typef:A -> Ax:Aiter f (iter f x (succ p)) (succ p) = f (f (iter f (iter f x p) p))forall (p q : positive) (A : Type) (f : A -> A) (x : A), iter f x (p + q) = iter f (iter f x q) pforall (p q : positive) (A : Type) (f : A -> A) (x : A), iter f x (p + q) = iter f (iter f x q) pq:positiveA:Typef:A -> Ax:Aiter f x (1 + q) = iter f (iter f x q) 1p:positiveIHp:forall (q0 : positive) (A0 : Type) (f0 : A0 -> A0) (x0 : A0), iter f0 x0 (p + q0) = iter f0 (iter f0 x0 q0) pq:positiveA:Typef:A -> Ax:Aiter f x (succ p + q) = iter f (iter f x q) (succ p)now rewrite add_succ_l, !iter_succ, IHp. Qed.p:positiveIHp:forall (q0 : positive) (A0 : Type) (f0 : A0 -> A0) (x0 : A0), iter f0 x0 (p + q0) = iter f0 (iter f0 x0 q0) pq:positiveA:Typef:A -> Ax:Aiter f x (succ p + q) = iter f (iter f x q) (succ p)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 f x p)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 f x p)p:positiveIHp:forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f x p)forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (f (iter f (iter f x p) p))p:positiveIHp:forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f x p)forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f (iter f x p) p)p:positiveIHp:forall (A0 : Type) (f0 : A0 -> A0) (Inv0 : A0 -> Prop), (forall x0 : A0, Inv0 x0 -> Inv0 (f0 x0)) -> forall x0 : A0, Inv0 x0 -> Inv0 (iter f0 x0 p)A:Typef:A -> AInv:A -> PropH:forall x0 : A, Inv x0 -> Inv (f x0)x:AH0:Inv xInv (f (iter f (iter f x p) p))p:positiveIHp:forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f x p)forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f (iter f x p) p)p:positiveIHp:forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f x p)forall (A : Type) (f : A -> A) (Inv : A -> Prop), (forall x : A, Inv x -> Inv (f x)) -> forall x : A, Inv x -> Inv (iter f (iter f x p) p)apply IHp, IHp; trivial. Qed.p:positiveIHp:forall (A0 : Type) (f0 : A0 -> A0) (Inv0 : A0 -> Prop), (forall x0 : A0, Inv0 x0 -> Inv0 (f0 x0)) -> forall x0 : A0, Inv0 x0 -> Inv0 (iter f0 x0 p)A:Typef:A -> AInv:A -> PropH:forall x0 : A, Inv x0 -> Inv (f x0)x:AH0:Inv xInv (iter f (iter f x p) p)
p:positivep ^ 1 = pp:positivep ^ 1 = pp:positiveiter (mul p) 1 1 = pnow rewrite mul_comm. Qed.p:positivep * 1 = pp, q:positivep ^ succ q = p * p ^ qp, q:positivep ^ succ q = p * p ^ qnow rewrite iter_succ. Qed.p, q:positiveiter (mul p) 1 (succ q) = p * iter (mul p) 1 q
p:positivesquare p = p * pp:positivesquare p = p * pp:positiveIHp:square p = p * psquare p~1 = p~1 * p~1p:positiveIHp:square p = p * psquare p~0 = p~0 * p~0square 1 = 1 * 1p:positiveIHp:square p = p * psquare p~1 = p~1 * p~1p:positiveIHp:square p = p * psquare p~1 = (p * p + p)~0~1now rewrite IHp.p:positiveIHp:square p = p * p(square p + p)~0~1 = (p * p + p)~0~1p:positiveIHp:square p = p * psquare p~0 = p~0 * p~0p:positiveIHp:square p = p * psquare p~0 = (p * p)~0~0now rewrite IHp.p:positiveIHp:square p = p * p(square p)~0~0 = (p * p)~0~0trivial. Qed.square 1 = 1 * 1
p, q:positivesub_mask p (succ q) = sub_mask_carry p qp, q:positivesub_mask p (succ q) = sub_mask_carry p qinduction p; destruct q; simpl; f_equal; trivial; now destruct p. Qed.p:positiveforall q : positive, sub_mask p (succ q) = sub_mask_carry p qp, q:positivesub_mask_carry p q = pred_mask (sub_mask p q)p, q:positivesub_mask_carry p q = pred_mask (sub_mask p q)induction p as [p IHp|p IHp| ]; destruct q; simpl; try reflexivity; rewrite ?IHp; destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto. Qed. 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.p:positiveforall q : positive, sub_mask_carry p q = pred_mask (sub_mask p q)p, q:positiveSubMaskSpec p q (sub_mask p q)p, q:positiveSubMaskSpec p q (sub_mask p q)p:positiveforall q : positive, SubMaskSpec p q (sub_mask p q)(* p~1 q~1 *)p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~1 q~1 (double_mask (sub_mask p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~1 q~0 (succ_double_mask (sub_mask p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegp:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positiveSubMaskSpec p~1 (p + r)~1 (double_mask IsNeg)p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~1 q~0 (succ_double_mask (sub_mask p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNeg(* p~1 q~0 *)p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~1 q~0 (succ_double_mask (sub_mask p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegp:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positiveSubMaskSpec p~1 (p + r)~0 (succ_double_mask IsNeg)p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegp:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positivep~1 + pred_double r = (p + r)~0p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegp:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positive(p + r)~0 = p~1 + pred_double rp:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNeg(* p~0 q~1 *)p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~1 (succ_double_mask (sub_mask_carry p q))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegp:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~1 (succ_double_mask (pred_mask (sub_mask p q)))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegq:positiveIHp:forall q0 : positive, SubMaskSpec q q0 (sub_mask q q0)SubMaskSpec q~0 q~1 (succ_double_mask (pred_mask IsNul))q, r:positiveIHp:forall q0 : positive, SubMaskSpec (q + r) q0 (sub_mask (q + r) q0)SubMaskSpec (q + r)~0 q~1 (succ_double_mask (pred_mask (IsPos r)))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positiveSubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegq, r:positiveIHp:forall q0 : positive, SubMaskSpec (q + r) q0 (sub_mask (q + r) q0)SubMaskSpec (q + r)~0 q~1 (succ_double_mask (pred_mask (IsPos r)))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positiveSubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegq, r:positiveIHp:forall q0 : positive, SubMaskSpec (q + r~1) q0 (sub_mask (q + r~1) q0)(add_carry q r~0)~0 = (q + r~1)~0q, r:positiveIHp:forall q0 : positive, SubMaskSpec (q + r~0) q0 (sub_mask (q + r~0) q0)(add_carry q (pred_double r))~0 = (q + r~0)~0q:positiveIHp:forall q0 : positive, SubMaskSpec (q + 1) q0 (sub_mask (q + 1) q0)(succ q)~0 = (q + 1)~0p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positiveSubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegq, r:positiveIHp:forall q0 : positive, SubMaskSpec (q + r~0) q0 (sub_mask (q + r~0) q0)(add_carry q (pred_double r))~0 = (q + r~0)~0q:positiveIHp:forall q0 : positive, SubMaskSpec (q + 1) q0 (sub_mask (q + 1) q0)(succ q)~0 = (q + 1)~0p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positiveSubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegq:positiveIHp:forall q0 : positive, SubMaskSpec (q + 1) q0 (sub_mask (q + 1) q0)(succ q)~0 = (q + 1)~0p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positiveSubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegp:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positiveSubMaskSpec p~0 (p + r)~1 (succ_double_mask (pred_mask IsNeg))p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNeg(* p~0 q~0 *)p:positiveIHp:forall q0 : positive, SubMaskSpec p q0 (sub_mask p q0)q:positiveSubMaskSpec p~0 q~0 (double_mask (sub_mask p q))p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNegp:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)r:positiveSubMaskSpec p~0 (p + r)~0 (double_mask IsNeg)p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNeg(* p~0 1 *)p:positiveIHp:forall q : positive, SubMaskSpec p q (sub_mask p q)1 + pred_double p = p~0q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNeg(* 1 q~1 *)q:positiveSubMaskSpec 1 q~1 IsNegq:positiveSubMaskSpec 1 q~0 IsNeg(* 1 q~0 *)q:positiveSubMaskSpec 1 q~0 IsNegnow rewrite add_1_l, succ_pred_double. Qed.q:positive1 + pred_double q = q~0p, q:positivesub_mask p q = IsNul <-> p = qp, q:positivesub_mask p q = IsNul <-> p = qp, q:positivesub_mask p q = IsNul -> p = qp, q:positivep = q -> sub_mask p q = IsNulp, q:positivep = q -> sub_mask p q = IsNulinduction p; simpl; now rewrite ?IHp. Qed.p:positivesub_mask p p = IsNulp:positivesub_mask p p = IsNulnow apply sub_mask_nul_iff. Qed.p:positivesub_mask p p = IsNulp, q, r:positivesub_mask p q = IsPos r -> q + r = pcase sub_mask_spec; congruence. Qed.p, q, r:positivesub_mask p q = IsPos r -> q + r = pp, q:positivesub_mask (p + q) p = IsPos qp, q:positivesub_mask (p + q) p = IsPos qp, q:positivep + q = p -> IsNul = IsPos qp, q:positiveforall r : positive, p + r = p + q -> IsPos r = IsPos qp, q:positiveforall r : positive, p + q + r = p -> IsNeg = IsPos qp, q:positiveH:p + q = pIsNul = IsPos qp, q:positiveforall r : positive, p + r = p + q -> IsPos r = IsPos qp, q:positiveforall r : positive, p + q + r = p -> IsNeg = IsPos qp, q:positiveH:q + p = pIsNul = IsPos qp, q:positiveforall r : positive, p + r = p + q -> IsPos r = IsPos qp, q:positiveforall r : positive, p + q + r = p -> IsNeg = IsPos qp, q:positiveforall r : positive, p + r = p + q -> IsPos r = IsPos qp, q:positiveforall r : positive, p + q + r = p -> IsNeg = IsPos qp, q, r:positiveH:p + r = p + qIsPos r = IsPos qp, q:positiveforall r : positive, p + q + r = p -> IsNeg = IsPos qp, q, r:positiveH:r = qIsPos r = IsPos qp, q:positiveforall r : positive, p + q + r = p -> IsNeg = IsPos qp, q:positiveforall r : positive, p + q + r = p -> IsNeg = IsPos qp, q, r:positiveH:p + q + r = pIsNeg = IsPos qelim (add_no_neutral _ _ H). Qed.p, q, r:positiveH:q + r + p = pIsNeg = IsPos qp, q, r:positivesub_mask p q = IsPos r <-> q + r = pp, q, r:positivesub_mask p q = IsPos r <-> q + r = pp, q, r:positivesub_mask p q = IsPos r -> q + r = pp, q, r:positiveq + r = p -> sub_mask p q = IsPos rintros <-; apply sub_mask_add_diag_l. Qed.p, q, r:positiveq + r = p -> sub_mask p q = IsPos rp, q:positivesub_mask p (p + q) = IsNegp, q:positivesub_mask p (p + q) = IsNegp, q:positivep = p + q -> IsNul = IsNegp, q:positiveforall r : positive, p + q + r = p -> IsPos r = IsNegp, q:positiveH:p = p + qIsNul = IsNegp, q:positiveforall r : positive, p + q + r = p -> IsPos r = IsNegp, q:positiveH:q + p = pIsNul = IsNegp, q:positiveforall r : positive, p + q + r = p -> IsPos r = IsNegp, q:positiveforall r : positive, p + q + r = p -> IsPos r = IsNegp, q, r:positiveH:p + q + r = pIsPos r = IsNegelim (add_no_neutral _ _ H). Qed.p, q, r:positiveH:q + r + p = pIsPos r = IsNegp, q:positivesub_mask p q = IsNeg <-> (exists r : positive, p + r = q)p, q:positivesub_mask p q = IsNeg <-> (exists r : positive, p + r = q)p, q:positivesub_mask p q = IsNeg -> exists r : positive, p + r = qp, q:positive(exists r : positive, p + r = q) -> sub_mask p q = IsNegp, q:positiveforall r : positive, p + r = q -> IsNeg = IsNeg -> exists r0 : positive, p + r0 = qp, q:positive(exists r : positive, p + r = q) -> sub_mask p q = IsNegp, q:positive(exists r : positive, p + r = q) -> sub_mask p q = IsNegapply sub_mask_add_diag_r. Qed. (*********************************************************************)p, r:positivesub_mask p (p + r) = IsNeg
p, q:positive(p =? q) = true <-> p = qp, q:positive(p =? q) = true <-> p = qinduction p; destruct q; simpl; rewrite ?IHp; split; congruence. Qed.p:positiveforall q : positive, (p =? q) = true <-> p = qp, q:positive(p <? q) = true <-> p < qp, q:positive(p <? q) = true <-> p < qdestruct compare; easy'. Qed.p, q:positivematch p ?= q with | Lt => true | _ => false end = true <-> (p ?= q) = Ltp, q:positive(p <=? q) = true <-> p <= qp, q:positive(p <=? q) = true <-> p <= qdestruct compare; easy'. Qed.p, q:positivematch p ?= q with | Gt => false | _ => true end = true <-> (p ?= q) <> Gt
More about eqb
Include BoolEqualityFacts. (**********************************************************************)
First, we express compare_cont in term of compare
Definition switch_Eq c c' := match c' with | Eq => c | Lt => Lt | Gt => Gt end.p, q:positivec:comparisoncompare_cont c p q = switch_Eq c (p ?= q)p, q:positivec:comparisoncompare_cont c p q = switch_Eq c (p ?= q)p, q:positivec:comparisoncompare_cont c p q = switch_Eq c (compare_cont Eq p q)p:positiveforall (q : positive) (c : comparison), compare_cont c p q = switch_Eq c (compare_cont Eq p q)p:positiveIHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)q:positiveforall c : comparison, compare_cont Gt p q = switch_Eq c (compare_cont Gt p q)p:positiveIHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)q:positiveforall c : comparison, compare_cont Lt p q = switch_Eq c (compare_cont Lt p q)p:positiveIHp:forall (q0 : positive) (c0 : comparison), compare_cont c0 p q0 = switch_Eq c0 (compare_cont Eq p q0)q:positivec:comparisoncompare_cont Gt p q = switch_Eq c (compare_cont Gt p q)p:positiveIHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)q:positiveforall c : comparison, compare_cont Lt p q = switch_Eq c (compare_cont Lt p q)p:positiveIHp:forall (q0 : positive) (c0 : comparison), compare_cont c0 p q0 = switch_Eq c0 (compare_cont Eq p q0)q:positivec:comparisonswitch_Eq Gt (switch_Eq Eq (compare_cont Eq p q)) = switch_Eq c (switch_Eq Gt (switch_Eq Eq (compare_cont Eq p q)))p:positiveIHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)q:positiveforall c : comparison, compare_cont Lt p q = switch_Eq c (compare_cont Lt p q)p:positiveIHp:forall (q0 : positive) (c : comparison), compare_cont c p q0 = switch_Eq c (compare_cont Eq p q0)q:positiveforall c : comparison, compare_cont Lt p q = switch_Eq c (compare_cont Lt p q)p:positiveIHp:forall (q0 : positive) (c0 : comparison), compare_cont c0 p q0 = switch_Eq c0 (compare_cont Eq p q0)q:positivec:comparisoncompare_cont Lt p q = switch_Eq c (compare_cont Lt p q)now destruct (compare_cont Eq p q). Qed.p:positiveIHp:forall (q0 : positive) (c0 : comparison), compare_cont c0 p q0 = switch_Eq c0 (compare_cont Eq p q0)q:positivec:comparisonswitch_Eq Lt (switch_Eq Eq (compare_cont Eq p q)) = switch_Eq c (switch_Eq Lt (switch_Eq Eq (compare_cont Eq 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
p, q:positivec:comparisoncompare_cont c p q = Eq -> c = Eqp, q:positivec:comparisoncompare_cont c p q = Eq -> c = Eqnow destruct (p ?= q). Qed.p, q:positivec:comparisonswitch_Eq c (p ?= q) = Eq -> c = Eqp, q:positivecompare_cont Lt p q = Gt <-> p > qp, q:positivecompare_cont Lt p q = Gt <-> p > qp, q:positiveswitch_Eq Lt (p ?= q) = Gt <-> p > qdestruct (p ?= q); now split. Qed.p, q:positiveswitch_Eq Lt (p ?= q) = Gt <-> (p ?= q) = Gtp, q:positivecompare_cont Lt p q = Lt <-> p <= qp, q:positivecompare_cont Lt p q = Lt <-> p <= qp, q:positiveswitch_Eq Lt (p ?= q) = Lt <-> p <= qdestruct (p ?= q); easy'. Qed.p, q:positiveswitch_Eq Lt (p ?= q) = Lt <-> (p ?= q) <> Gtp, q:positivecompare_cont Gt p q = Lt <-> p < qp, q:positivecompare_cont Gt p q = Lt <-> p < qp, q:positiveswitch_Eq Gt (p ?= q) = Lt <-> p < qdestruct (p ?= q); now split. Qed.p, q:positiveswitch_Eq Gt (p ?= q) = Lt <-> (p ?= q) = Ltp, q:positivecompare_cont Gt p q = Gt <-> p >= qp, q:positivecompare_cont Gt p q = Gt <-> p >= qp, q:positiveswitch_Eq Gt (p ?= q) = Gt <-> p >= qdestruct (p ?= q); easy'. Qed.p, q:positiveswitch_Eq Gt (p ?= q) = Gt <-> (p ?= q) <> Ltp, q:positivecompare_cont Lt p q <> Lt <-> p > qp, q:positivecompare_cont Lt p q <> Lt <-> p > qp, q:positive~ p <= q <-> p > qnow destruct compare_cont; split; try apply comparison_eq_stable. Qed.p, q:positive~ compare_cont Eq p q <> Gt <-> compare_cont Eq p q = Gtp, q:positivecompare_cont Lt p q <> Gt <-> p <= qapply not_iff_compat, compare_cont_Lt_Gt. Qed.p, q:positivecompare_cont Lt p q <> Gt <-> p <= qp, q:positivecompare_cont Gt p q <> Lt <-> p >= qapply not_iff_compat, compare_cont_Gt_Lt. Qed.p, q:positivecompare_cont Gt p q <> Lt <-> p >= qp, q:positivecompare_cont Gt p q <> Gt <-> p < qp, q:positivecompare_cont Gt p q <> Gt <-> p < qp, q:positive~ p >= q <-> p < qnow destruct compare_cont; split; try apply comparison_eq_stable. Qed.p, q:positive~ compare_cont Eq p q <> Lt <-> compare_cont Eq p q = Lt
We can express recursive equations for compare
p, q:positive(p~0 ?= q~0) = (p ?= q)reflexivity. Qed.p, q:positive(p~0 ?= q~0) = (p ?= q)p, q:positive(p~1 ?= q~1) = (p ?= q)reflexivity. Qed.p, q:positive(p~1 ?= q~1) = (p ?= q)p, q:positive(p~1 ?= q~0) = switch_Eq Gt (p ?= q)exact (compare_cont_spec p q Gt). Qed.p, q:positive(p~1 ?= q~0) = switch_Eq Gt (p ?= q)p, q:positive(p~0 ?= q~1) = switch_Eq Lt (p ?= q)exact (compare_cont_spec p q Lt). Qed. 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.p, q:positive(p~0 ?= q~1) = switch_Eq Lt (p ?= q)
Relation between compare and sub_mask
Definition mask2cmp (p:mask) : comparison := match p with | IsNul => Eq | IsPos _ => Gt | IsNeg => Lt end.p, q:positive(p ?= q) = mask2cmp (sub_mask p q)p, q:positive(p ?= q) = mask2cmp (sub_mask p q)induction p as [p IHp| p IHp| ]; intros [q|q| ]; simpl; trivial; specialize (IHp q); rewrite ?sub_mask_carry_spec; destruct (sub_mask p q) as [|r|]; simpl in *; try clear r; try destruct r; simpl; trivial; simpl_compare; now rewrite IHp. Qed.p:positiveforall q : positive, (p ?= q) = mask2cmp (sub_mask p q)
Alternative characterisation of strict order in term of addition
p, q:positivep < q <-> (exists r : positive, p + r = q)p, q:positivep < q <-> (exists r : positive, p + r = q)p, q:positive(p ?= q) = Lt <-> (exists r : positive, p + r = q)destruct sub_mask; now split. Qed.p, q:positivemask2cmp (sub_mask p q) = Lt <-> sub_mask p q = IsNegp, q:positivep > q <-> (exists r : positive, q + r = p)p, q:positivep > q <-> (exists r : positive, q + r = p)p, q:positive(p ?= q) = Gt <-> (exists r : positive, q + r = p)p, q:positivemask2cmp (sub_mask p q) = Gt <-> (exists r : positive, q + r = p)p, q:positivemask2cmp (sub_mask p q) = Gt -> exists r : positive, q + r = pp, q:positive(exists r : positive, q + r = p) -> mask2cmp (sub_mask p q) = Gtp, q, r:positiveHr:sub_mask p q = IsPos rexists r0 : positive, q + r0 = pp, q:positive(exists r : positive, q + r = p) -> mask2cmp (sub_mask p q) = Gtp, q, r:positiveHr:sub_mask p q = IsPos rq + r = pp, q:positive(exists r : positive, q + r = p) -> mask2cmp (sub_mask p q) = Gtp, q:positive(exists r : positive, q + r = p) -> mask2cmp (sub_mask p q) = Gtp, q, r:positiveHr:q + r = pmask2cmp (sub_mask p q) = Gtnow rewrite Hr. Qed.p, q, r:positiveHr:sub_mask p q = IsPos rmask2cmp (sub_mask p q) = Gt
Basic facts about compare_cont
p:positivec:comparisoncompare_cont c p p = cnow induction p. Qed.p:positivec:comparisoncompare_cont c p p = cp, q:positivec:comparisonCompOpp (compare_cont c p q) = compare_cont (CompOpp c) q pp, q:positivec:comparisonCompOpp (compare_cont c p q) = compare_cont (CompOpp c) q pinduction p as [p IHp|p IHp| ]; intros [q|q| ] c; simpl; trivial; apply IHp. Qed.p:positiveforall (q : positive) (c : comparison), CompOpp (compare_cont c p q) = compare_cont (CompOpp c) q p
Basic facts about compare
p, q:positive(p ?= q) = Eq <-> p = qp, q:positive(p ?= q) = Eq <-> p = qdestruct sub_mask; now split. Qed.p, q:positivemask2cmp (sub_mask p q) = Eq <-> sub_mask p q = IsNulp, q:positive(q ?= p) = CompOpp (p ?= q)p, q:positive(q ?= p) = CompOpp (p ?= q)now rewrite compare_cont_antisym. Qed.p, q:positivecompare_cont Eq q p = CompOpp (compare_cont Eq p q)p, q:positive(p ?= q) = Lt <-> p < qreflexivity. Qed.p, q:positive(p ?= q) = Lt <-> p < qp, q:positive(p ?= q) <> Gt <-> p <= qreflexivity. Qed.p, q:positive(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.
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.
p, q:positivep > q <-> q < pp, q:positivep > q <-> q < pnow rewrite compare_antisym, CompOpp_iff. Qed.p, q:positive(p ?= q) = Gt <-> (q ?= p) = Ltp, q:positivep > q -> q < papply gt_lt_iff. Qed.p, q:positivep > q -> q < pp, q:positivep < q -> q > papply gt_lt_iff. Qed.p, q:positivep < q -> q > pp, q:positivep >= q <-> q <= pp, q:positivep >= q <-> q <= pnow rewrite compare_antisym, CompOpp_iff. Qed.p, q:positive(p ?= q) <> Lt <-> (q ?= p) <> Gtp, q:positivep >= q -> q <= papply ge_le_iff. Qed.p, q:positivep >= q -> q <= pp, q:positivep <= q -> q >= papply ge_le_iff. Qed.p, q:positivep <= q -> q >= p
p, q:positiveswitch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q)p, q:positiveswitch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q)induction p as [p IH|p IH| ]; intros [q|q| ]; simpl; simpl_compare; rewrite ?IH; trivial; (now destruct compare) || (now destruct p). Qed.p:positiveforall q : positive, switch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q)p, q:positiveswitch_Eq Lt (succ p ?= q) = switch_Eq Gt (p ?= q)p, q:positiveswitch_Eq Lt (succ p ?= q) = switch_Eq Gt (p ?= q)p, q:positiveswitch_Eq Lt (CompOpp (q ?= succ p)) = switch_Eq Gt (CompOpp (q ?= p))now do 2 destruct compare. Qed.p, q:positiveswitch_Eq Gt (q ?= succ p) = switch_Eq Lt (q ?= p) -> switch_Eq Lt (CompOpp (q ?= succ p)) = switch_Eq Gt (CompOpp (q ?= p))p, q:positivep < succ q <-> p <= qp, q:positivep < succ q <-> p <= qp, q:positive(p ?= succ q) = Lt <-> (p ?= q) <> Gtdo 2 destruct compare; try discriminate; now split. Qed.p, q:positiveswitch_Eq Gt (p ?= succ q) = switch_Eq Lt (p ?= q) -> (p ?= succ q) = Lt <-> (p ?= q) <> Gtp:positivep < succ pp:positivep < succ pp:positiveexists r : positive, p + r = succ papply add_1_r. Qed.p:positivep + 1 = succ pp, q:positive(succ p ?= succ q) = (p ?= q)p, q:positive(succ p ?= succ q) = (p ?= q)induction p; destruct q; simpl; simpl_compare; trivial; apply compare_succ_l || apply compare_succ_r || (now destruct p) || (now destruct q). Qed.p:positiveforall q : positive, (succ p ?= succ q) = (p ?= q)
p:positive1 <= pnow destruct p. Qed.p:positive1 <= pp:positive~ p < 1now destruct p. Qed.p:positive~ p < 1p:positive1 < succ papply lt_succ_r, le_1_l. Qed.p:positive1 < succ p
p, q:positivep <= q <-> ~ q < pnow rewrite <- ge_le_iff. Qed.p, q:positivep <= q <-> ~ q < pp, q:positivep < q <-> ~ q <= pp, q:positivep < q <-> ~ q <= pp, q:positivep < q <-> ~ q <= pp, q:positive(p ?= q) = Lt <-> ~ (q ?= p) <> Gtdestruct compare; split; auto; easy'. Qed.p, q:positiveCompOpp (q ?= p) = Lt <-> ~ (q ?= p) <> Gtp, q:positivep < q -> p <= qp, q:positivep < q -> p <= qp, q:positiveH:p < qp <= qnow left. Qed.p, q:positiveH:p < qp < q \/ p = qn, m:positiven < m -> n < succ mn, m:positiven < m -> n < succ mnow apply lt_succ_r, lt_le_incl. Qed.n, m:positiveH:n < mn < succ mn, m:positiven < m <-> succ n < succ mn, m:positiven < m <-> succ n < succ mnow rewrite compare_succ_succ. Qed.n, m:positive(n ?= m) = Lt <-> (succ n ?= succ m) = Ltn, m:positiven <= m <-> succ n <= succ mn, m:positiven <= m <-> succ n <= succ mnow rewrite compare_succ_succ. Qed.n, m:positive(n ?= m) <> Gt <-> (succ n ?= succ m) <> Gtn, m, p:positiven < m -> m < p -> n < pn, m, p:positiven < m -> m < p -> n < pn, m, p:positive(exists r : positive, n + r = m) -> (exists r : positive, m + r = p) -> exists r : positive, n + r = pn, m, p, r:positiveHr:n + r = ms:positiveHs:m + s = pexists r0 : positive, n + r0 = pnow rewrite add_assoc, Hr, Hs. Qed.n, m, p, r:positiveHr:n + r = ms:positiveHs:m + s = pn + (r + s) = pforall (A : positive -> Prop) (n : positive), A (succ n) -> (forall m : positive, n < m -> A m -> A (succ m)) -> forall m : positive, n < m -> A mforall (A : positive -> Prop) (n : positive), A (succ n) -> (forall m : positive, n < m -> A m -> A (succ m)) -> forall m : positive, n < m -> A mA:positive -> Propn:positiveAB:A (succ n)AS:forall m0 : positive, n < m0 -> A m0 -> A (succ m0)m:positiven < m -> A mA:positive -> Propn:positiveAB:A (succ n)AS:forall m : positive, n < m -> A m -> A (succ m)H:n < 1A 1A:positive -> Propn:positiveAB:A (succ n)AS:forall m0 : positive, n < m0 -> A m0 -> A (succ m0)m:positiveIHm:n < m -> A mH:n < succ mA (succ m)A:positive -> Propn:positiveAB:A (succ n)AS:forall m0 : positive, n < m0 -> A m0 -> A (succ m0)m:positiveIHm:n < m -> A mH:n < succ mA (succ m)destruct H as [H|H]; subst; auto. Qed.A:positive -> Propn:positiveAB:A (succ n)AS:forall m0 : positive, n < m0 -> A m0 -> A (succ m0)m:positiveIHm:n < m -> A mH:n < m \/ n = mA (succ m)StrictOrder ltStrictOrder ltIrreflexive ltTransitive ltexact lt_trans. Qed.Transitive ltProper (Logic.eq ==> Logic.eq ==> iff) ltProper (Logic.eq ==> Logic.eq ==> iff) ltforall x y : positive, x = y -> forall x0 y0 : positive, x0 = y0 -> (x < x0 -> y < y0) /\ (y < y0 -> x < x0)subst; auto. Qed.x, y:positiveH:x = yx0, y0:positiveH0:x0 = y0(x < x0 -> y < y0) /\ (y < y0 -> x < x0)p, q:positivep < q \/ p = q \/ q < pcase (compare_spec p q); intuition. Qed.p, q:positivep < q \/ p = q \/ q < pp:positivep <= pp:positivep <= pp:positivep <= pnow rewrite compare_refl. Qed.p:positive(p ?= p) <> Gtn, m, p:positiven <= m -> m < p -> n < pn, m, p:positiven <= m -> m < p -> n < pn, m, p:positiveH:n <= mH':m < pn < pn, m, p:positiveH:n < m \/ n = mH':m < pn < pn, m, p:positiveH:n < mH':m < pn < pn, m, p:positiveH:n = mH':m < pn < pnow subst. Qed.n, m, p:positiveH:n = mH':m < pn < pn, m, p:positiven < m -> m <= p -> n < pn, m, p:positiven < m -> m <= p -> n < pn, m, p:positiveH:n < mH':m <= pn < pn, m, p:positiveH:n < mH':m < p \/ m = pn < pn, m, p:positiveH:n < mH0:m < pn < pn, m, p:positiveH:n < mH0:m = pn < pnow subst. Qed.n, m, p:positiveH:n < mH0:m = pn < pn, m, p:positiven <= m -> m <= p -> n <= pn, m, p:positiven <= m -> m <= p -> n <= pn, m, p:positiveH:n <= mH':m <= pn <= pn, m, p:positiveH:n < m \/ n = mH':m <= pn <= pn, m, p:positiveH:n < mH':m <= pn <= pn, m, p:positiveH:n = mH':m <= pn <= pn, m, p:positiveH:n < mH':m <= pn < pn, m, p:positiveH:n = mH':m <= pn <= pnow subst. Qed.n, m, p:positiveH:n = mH':m <= pn <= pn, m:positivesucc n <= m <-> n < mn, m:positivesucc n <= m <-> n < mn, m:positivesucc n < succ m <-> n < mapply succ_lt_mono. Qed.n, m:positiven < m <-> succ n < succ mp, q:positivep <= q -> q <= p -> p = qp, q:positivep <= q -> q <= p -> p = qp, q:positiveH:p < qq <= p -> p = qp, q:positiveH:p < qH0:q < pp = qnow transitivity q. Qed.p, q:positiveH:p < qH0:q < pp < pPreOrder lePreOrder leReflexive leTransitive leexact le_trans. Qed.Transitive lePartialOrder Logic.eq lePartialOrder Logic.eq lex, y:positivepointwise_lifting iff Tnil (x = y) (relation_conjunction le (Basics.flip le) x y)x, y:positivex = y <-> x <= y <= xx, y:positivex = y -> x <= y <= xx, y:positivex <= y <= x -> x = ydestruct 1; now apply le_antisym. Qed.x, y:positivex <= y <= x -> x = y
p, q, r:positive(p + q ?= p + r) = (q ?= r)p, q, r:positive(p + q ?= p + r) = (q ?= r)forall p q r : positive, (p + q ?= p + r) = (q ?= r)q, r:positive(1 + q ?= 1 + r) = (q ?= r)p:positiveIHp:forall q0 r0 : positive, (p + q0 ?= p + r0) = (q0 ?= r0)q, r:positive(succ p + q ?= succ p + r) = (q ?= r)q, r:positive(succ q ?= succ r) = (q ?= r)p:positiveIHp:forall q0 r0 : positive, (p + q0 ?= p + r0) = (q0 ?= r0)q, r:positive(succ p + q ?= succ p + r) = (q ?= r)now rewrite 2 add_succ_l, compare_succ_succ. Qed.p:positiveIHp:forall q0 r0 : positive, (p + q0 ?= p + r0) = (q0 ?= r0)q, r:positive(succ p + q ?= succ p + r) = (q ?= r)p, q, r:positive(q + p ?= r + p) = (q ?= r)p, q, r:positive(q + p ?= r + p) = (q ?= r)apply add_compare_mono_l. Qed.p, q, r:positive(p + q ?= p + r) = (q ?= r)
p, q:positivep < p + qp, q:positivep < p + qnow exists q. Qed.p, q:positiveexists r : positive, p + r = p + qp, q, r:positiveq < r <-> p + q < p + rp, q, r:positiveq < r <-> p + q < p + rp, q, r:positive(q ?= r) = Lt <-> (p + q ?= p + r) = Ltapply iff_refl. Qed.p, q, r:positive(q ?= r) = Lt <-> (q ?= r) = Ltp, q, r:positiveq < r <-> q + p < r + pp, q, r:positiveq < r <-> q + p < r + pp, q, r:positive(q ?= r) = Lt <-> (q + p ?= r + p) = Ltapply iff_refl. Qed.p, q, r:positive(q ?= r) = Lt <-> (q ?= r) = Ltp, q, r, s:positivep < q -> r < s -> p + r < q + sp, q, r, s:positivep < q -> r < s -> p + r < q + sp, q, r, s:positiveH:p < qH0:r < sp + r < q + sp, q, r, s:positiveH:p < qH0:r < sp + r < p + sp, q, r, s:positiveH:p < qH0:r < sp + s < q + snow apply add_lt_mono_r. Qed.p, q, r, s:positiveH:p < qH0:r < sp + s < q + sp, q, r:positiveq <= r <-> p + q <= p + rp, q, r:positiveq <= r <-> p + q <= p + rp, q, r:positive(q ?= r) <> Gt <-> (p + q ?= p + r) <> Gtapply iff_refl. Qed.p, q, r:positive(q ?= r) <> Gt <-> (q ?= r) <> Gtp, q, r:positiveq <= r <-> q + p <= r + pp, q, r:positiveq <= r <-> q + p <= r + pp, q, r:positive(q ?= r) <> Gt <-> (q + p ?= r + p) <> Gtapply iff_refl. Qed.p, q, r:positive(q ?= r) <> Gt <-> (q ?= r) <> Gtp, q, r, s:positivep <= q -> r <= s -> p + r <= q + sp, q, r, s:positivep <= q -> r <= s -> p + r <= q + sp, q, r, s:positiveH:p <= qH0:r <= sp + r <= q + sp, q, r, s:positiveH:p <= qH0:r <= sp + r <= p + sp, q, r, s:positiveH:p <= qH0:r <= sp + s <= q + snow apply add_le_mono_r. Qed.p, q, r, s:positiveH:p <= qH0:r <= sp + s <= q + s
p, q, r:positive(p * q ?= p * r) = (q ?= r)p, q, r:positive(p * q ?= p * r) = (q ?= r)p:positiveforall q r : positive, (p * q ?= p * r) = (q ?= r)p:positiveIHp:forall q r : positive, (p * q ?= p * r) = (q ?= r)forall q r : positive, (q + (p * q)~0 ?= r + (p * r)~0) = (q ?= r)p:positiveIHp:forall q0 r0 : positive, (p * q0 ?= p * r0) = (q0 ?= r0)q, r:positive(q + (p * q)~0 ?= r + (p * r)~0) = (q ?= r)p, q, r:positiveIHp:(p * q ?= p * r) = (q ?= r)(q + (p * q)~0 ?= r + (p * r)~0) = (q ?= r)p, q, r:positiveIHp:(p * q ?= p * r) = EqH:q = r(q + (p * q)~0 ?= r + (p * r)~0) = Eqp, q, r:positiveIHp:(p * q ?= p * r) = LtH:q < r(q + (p * q)~0 ?= r + (p * r)~0) = Ltp, q, r:positiveIHp:(p * q ?= p * r) = GtH:r < q(q + (p * q)~0 ?= r + (p * r)~0) = Gtp, r:positiveIHp:(p * r ?= p * r) = Eq(r + (p * r)~0 ?= r + (p * r)~0) = Eqp, q, r:positiveIHp:(p * q ?= p * r) = LtH:q < r(q + (p * q)~0 ?= r + (p * r)~0) = Ltp, q, r:positiveIHp:(p * q ?= p * r) = GtH:r < q(q + (p * q)~0 ?= r + (p * r)~0) = Gtp, q, r:positiveIHp:(p * q ?= p * r) = LtH:q < r(q + (p * q)~0 ?= r + (p * r)~0) = Ltp, q, r:positiveIHp:(p * q ?= p * r) = GtH:r < q(q + (p * q)~0 ?= r + (p * r)~0) = Gtnow apply lt_gt, add_lt_mono, gt_lt. Qed.p, q, r:positiveIHp:(p * q ?= p * r) = GtH:r < q(q + (p * q)~0 ?= r + (p * r)~0) = Gtp, q, r:positive(q * p ?= r * p) = (q ?= r)p, q, r:positive(q * p ?= r * p) = (q ?= r)apply mul_compare_mono_l. Qed.p, q, r:positive(p * q ?= p * r) = (q ?= r)
p, q, r:positiveq < r <-> p * q < p * rp, q, r:positiveq < r <-> p * q < p * rp, q, r:positive(q ?= r) = Lt <-> (p * q ?= p * r) = Ltapply iff_refl. Qed.p, q, r:positive(q ?= r) = Lt <-> (q ?= r) = Ltp, q, r:positiveq < r <-> q * p < r * pp, q, r:positiveq < r <-> q * p < r * pp, q, r:positive(q ?= r) = Lt <-> (q * p ?= r * p) = Ltapply iff_refl. Qed.p, q, r:positive(q ?= r) = Lt <-> (q ?= r) = Ltp, q, r, s:positivep < q -> r < s -> p * r < q * sp, q, r, s:positivep < q -> r < s -> p * r < q * sp, q, r, s:positiveH:p < qH0:r < sp * r < q * sp, q, r, s:positiveH:p < qH0:r < sp * r < p * sp, q, r, s:positiveH:p < qH0:r < sp * s < q * snow apply mul_lt_mono_r. Qed.p, q, r, s:positiveH:p < qH0:r < sp * s < q * sp, q, r:positiveq <= r <-> p * q <= p * rp, q, r:positiveq <= r <-> p * q <= p * rp, q, r:positive(q ?= r) <> Gt <-> (p * q ?= p * r) <> Gtapply iff_refl. Qed.p, q, r:positive(q ?= r) <> Gt <-> (q ?= r) <> Gtp, q, r:positiveq <= r <-> q * p <= r * pp, q, r:positiveq <= r <-> q * p <= r * pp, q, r:positive(q ?= r) <> Gt <-> (q * p ?= r * p) <> Gtapply iff_refl. Qed.p, q, r:positive(q ?= r) <> Gt <-> (q ?= r) <> Gtp, q, r, s:positivep <= q -> r <= s -> p * r <= q * sp, q, r, s:positivep <= q -> r <= s -> p * r <= q * sp, q, r, s:positiveH:p <= qH0:r <= sp * r <= q * sp, q, r, s:positiveH:p <= qH0:r <= sp * r <= p * sp, q, r, s:positiveH:p <= qH0:r <= sp * s <= q * snow apply mul_le_mono_r. Qed.p, q, r, s:positiveH:p <= qH0:r <= sp * s <= q * sp, q:positivep < p + qp, q:positivep < p + qp:positivep < p + 1p, q:positiveIHq:p < p + qp < p + succ qp:positivep < succ pp, q:positiveIHq:p < p + qp < p + succ qp, q:positiveIHq:p < p + qp < p + succ qapply add_lt_mono_l, lt_succ_diag_r. Qed.p, q:positiveIHq:p < p + qp + q < p + succ qp, q:positive~ p + q < pp, q:positive~ p + q < pp, q:positiveH:p + q < pFalseapply lt_trans with (p+q); auto using lt_add_r. Qed.p, q:positiveH:p + q < pp < pn, p:positive1 < n -> 1 < n ^ pn, p:positive1 < n -> 1 < n ^ pn, p:positiveH:1 < n1 < n ^ pn:positiveH:1 < n1 < n ^ 1n, p:positiveH:1 < nIHp:1 < n ^ p1 < n ^ succ pn, p:positiveH:1 < nIHp:1 < n ^ p1 < n ^ succ pn, p:positiveH:1 < nIHp:1 < n ^ p1 < n * n ^ pn, p:positiveH:1 < nIHp:1 < n ^ p1 < n * 1n, p:positiveH:1 < nIHp:1 < n ^ pn * 1 < n * n ^ pnow apply mul_lt_mono_l. Qed. (**********************************************************************)n, p:positiveH:1 < nIHp:1 < n ^ pn * 1 < n * n ^ p
p:positivep - 1 = pred pnow destruct p. Qed.p:positivep - 1 = pred pp:positivepred p = p - 1p:positivepred p = p - 1apply sub_1_r. Qed.p:positivep - 1 = pred pp, q:positivep - succ q = pred (p - q)p, q:positivep - succ q = pred (p - q)destruct (sub_mask p q) as [|[r|r| ]|]; auto. Qed.p, q:positivematch pred_mask (sub_mask p q) with | IsPos z => z | _ => 1 end = pred match sub_mask p q with | IsPos z => z | _ => 1 end
p, q:positiveq < p -> exists r : positive, sub_mask p q = IsPos r /\ q + r = pp, q:positiveq < p -> exists r : positive, sub_mask p q = IsPos r /\ q + r = pp, q:positive(exists r : positive, q + r = p) -> exists r : positive, sub_mask p q = IsPos r /\ q + r = pp, q, r:positiveHr:q + r = pexists r0 : positive, sub_mask p q = IsPos r0 /\ q + r0 = pp, q, r:positiveHr:q + r = psub_mask p q = IsPos r /\ q + r = pnow apply sub_mask_pos_iff. Qed.p, q, r:positiveHr:q + r = psub_mask p q = IsPos rp, q:positiveq < p -> exists r : positive, sub_mask p q = IsPos rp, q:positiveq < p -> exists r : positive, sub_mask p q = IsPos rp, q:positiveH:q < pexists r : positive, sub_mask p q = IsPos rnow exists r. Qed.p, q:positiveH:q < pr:positiveHr:sub_mask p q = IsPos rexists r0 : positive, sub_mask p q = IsPos r0p, q:positiveq < p -> p - q + q = pp, q:positiveq < p -> p - q + q = pp, q:positiveH:q < pp - q + q = pp, q:positiveH:q < pr:positiveU:sub_mask p q = IsPos rp - q + q = pp, q:positiveH:q < pr:positiveU:sub_mask p q = IsPos rmatch sub_mask p q with | IsPos z => z | _ => 1 end + q = pp, q:positiveH:q < pr:positiveU:sub_mask p q = IsPos rr + q = pnow apply sub_mask_add. Qed.p, q:positiveH:q < pr:positiveU:sub_mask p q = IsPos rq + r = pp, q:positivep + q - q = pp, q:positivep + q - q = pp, q:positivep + q - q = pp, q:positivep + q - q + q = p + qp, q:positiveq < p + qapply lt_add_r. Qed.p, q:positiveq < q + pp, q, r:positiver < q -> p * (q - r) = p * q - p * rp, q, r:positiver < q -> p * (q - r) = p * q - p * rp, q, r:positiveH:r < qp * (q - r) = p * q - p * rp, q, r:positiveH:r < qp * (q - r) + p * r = p * q - p * r + p * rp, q, r:positiveH:r < qp * (q - r + r) = p * q - p * r + p * rp, q, r:positiveH:r < qp * q = p * q - p * r + p * rp, q, r:positiveH:r < qp * q - p * r + p * r = p * qnow apply mul_lt_mono_l. Qed.p, q, r:positiveH:r < qp * r < p * qp, q, r:positiveq < p -> (p - q) * r = p * r - q * rp, q, r:positiveq < p -> (p - q) * r = p * r - q * rp, q, r:positiveH:q < p(p - q) * r = p * r - q * rnow apply mul_sub_distr_l. Qed.p, q, r:positiveH:q < pr * (p - q) = r * p - r * qp, q, r:positiveq < p -> p < r -> r - p < r - qp, q, r:positiveq < p -> p < r -> r - p < r - qp, q, r:positiveHqp:q < pHpr:p < rr - p < r - qp, q, r:positiveHqp:q < pHpr:p < rr - p + p < r - q + pp, q, r:positiveHqp:q < pHpr:p < rr < r - q + pp, q, r:positiveHqp:q < pHpr:p < rr <= r - q + qp, q, r:positiveHqp:q < pHpr:p < rr - q + q < r - q + pp, q, r:positiveHqp:q < pHpr:p < rr <= rp, q, r:positiveHqp:q < pHpr:p < rr - q + q < r - q + pnow apply add_lt_mono_l. Qed.p, q, r:positiveHqp:q < pHpr:p < rr - q + q < r - q + pp, q, r:positiveq < p -> r < p -> (p - q ?= p - r) = (r ?= q)p, q, r:positiveq < p -> r < p -> (p - q ?= p - r) = (r ?= q)p, q, r:positiveHqp:q < pHrp:r < p(p - q ?= p - r) = (r ?= q)p, q, r:positiveHqp:q < pHrp:r < pH:r = q(p - q ?= p - r) = Eqp, q, r:positiveHqp:q < pHrp:r < pH:r < q(p - q ?= p - r) = Ltp, q, r:positiveHqp:q < pHrp:r < pH:q < r(p - q ?= p - r) = Gtp, q:positiveHqp, Hrp:q < p(p - q ?= p - q) = Eqp, q, r:positiveHqp:q < pHrp:r < pH:r < q(p - q ?= p - r) = Ltp, q, r:positiveHqp:q < pHrp:r < pH:q < r(p - q ?= p - r) = Gtp, q, r:positiveHqp:q < pHrp:r < pH:r < q(p - q ?= p - r) = Ltp, q, r:positiveHqp:q < pHrp:r < pH:q < r(p - q ?= p - r) = Gtapply lt_gt, sub_lt_mono_l; trivial. Qed.p, q, r:positiveHqp:q < pHrp:r < pH:q < r(p - q ?= p - r) = Gtp, q, r:positivep < q -> p < r -> (q - p ?= r - p) = (q ?= r)p, q, r:positivep < q -> p < r -> (q - p ?= r - p) = (q ?= r)rewrite <- (add_compare_mono_r p), 2 sub_add; trivial. Qed.p, q, r:positiveH:p < qH0:p < r(q - p ?= r - p) = (q ?= r)p, q, r:positiveq < p -> r < q -> q - r < p - rp, q, r:positiveq < p -> r < q -> q - r < p - rp, q, r:positiveH:q < pH0:r < qq - r < p - rp, q, r:positiveH:q < pH0:r < q(q - r ?= p - r) = Ltnow apply lt_trans with q. Qed.p, q, r:positiveH:q < pH0:r < qr < pn, m:positivem < n -> n - m < nn, m:positivem < n -> n - m < nn, m:positiveH:m < nn - m < nn, m:positiveH:m < nn - m + m < n + mapply lt_add_r. Qed.n, m:positiveH:m < nn < n + mp, q, r:positiver < q -> p + (q - r) = p + q - rp, q, r:positiver < q -> p + (q - r) = p + q - rp, q, r:positiveH:r < qp + (q - r) = p + q - rp, q, r:positiveH:r < qp + (q - r) + r = p + q - r + rp, q, r:positiveH:r < qr < p + qapply lt_trans with q; trivial using lt_add_r. Qed.p, q, r:positiveH:r < qr < q + pp, q, r:positiveq + r < p -> p - (q + r) = p - q - rp, q, r:positiveq + r < p -> p - (q + r) = p - q - rp, q, r:positiveH:q + r < pp - (q + r) = p - q - rp, q, r:positiveH:q + r < pH0:q < pp - (q + r) = p - q - rp, q, r:positiveH:r + q < pH0:q < pp - (r + q) = p - q - rp, q, r:positiveH:r + q < pH0:q < pp - (r + q) + (r + q) = p - q - r + (r + q)p, q, r:positiveH:r + q < pH0:q < pp = p - q - r + (r + q)p, q, r:positiveH:r + q < pH0:q < pr < p - qrewrite sub_add; trivial. Qed.p, q, r:positiveH:r + q < pH0:q < pr + q < p - q + qp, q, r:positiver < q -> q - r < p -> p - (q - r) = p + r - qp, q, r:positiver < q -> q - r < p -> p - (q - r) = p + r - qp, q, r:positiveH:r < qH0:q - r < pp - (q - r) = p + r - qp, q, r:positiveH:r < qH0:q - r < pp - (q - r) + (q - r + r) = p + r - q + (q - r + r)p, q, r:positiveH:r < qH0:q - r < pq < p + rnow apply add_lt_mono_r. Qed.p, q, r:positiveH:r < qH0:q - r < pq - r + r < p + r
Recursive equations for sub
n, m:positivem < n -> n~0 - m~0 = (n - m)~0n, m:positivem < n -> n~0 - m~0 = (n - m)~0n, m:positiveH:m < nn~0 - m~0 = (n - m)~0n, m:positiveH:m < nmatch sub_mask n~0 m~0 with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~0now destruct (sub_mask_pos n m H) as (p, ->). Qed.n, m:positiveH:m < nmatch double_mask (sub_mask n m) with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~0n, m:positivem < n -> n~1 - m~1 = (n - m)~0n, m:positivem < n -> n~1 - m~1 = (n - m)~0n, m:positiveH:m < nn~1 - m~1 = (n - m)~0n, m:positiveH:m < nmatch sub_mask n~1 m~1 with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~0now destruct (sub_mask_pos n m H) as (p, ->). Qed.n, m:positiveH:m < nmatch double_mask (sub_mask n m) with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~0n, m:positivem < n -> n~1 - m~0 = (n - m)~1n, m:positivem < n -> n~1 - m~0 = (n - m)~1n, m:positiveH:m < nn~1 - m~0 = (n - m)~1n, m:positiveH:m < nmatch sub_mask n~1 m~0 with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~1now destruct (sub_mask_pos n m) as (p, ->). Qed.n, m:positiveH:m < nmatch succ_double_mask (sub_mask n m) with | IsPos z => z | _ => 1 end = match sub_mask n m with | IsPos z => z | _ => 1 end~1n, m:positiven~0 - m~1 = pred_double (n - m)n, m:positiven~0 - m~1 = pred_double (n - m)n, m:positivematch sub_mask n~0 m~1 with | IsPos z => z | _ => 1 end = pred_double match sub_mask n m with | IsPos z => z | _ => 1 endn, m:positivematch succ_double_mask (sub_mask_carry n m) with | IsPos z => z | _ => 1 end = pred_double match sub_mask n m with | IsPos z => z | _ => 1 endnow destruct (sub_mask n m) as [|[r|r|]|]. Qed.n, m:positivematch succ_double_mask (pred_mask (sub_mask n m)) with | IsPos z => z | _ => 1 end = pred_double match sub_mask n m with | IsPos z => z | _ => 1 end
Properties of subtraction with underflow
p, q:positivesub_mask p q = IsNeg <-> p < qp, q:positivesub_mask p q = IsNeg <-> p < qapply sub_mask_neg_iff. Qed.p, q:positivesub_mask p q = IsNeg <-> (exists r : positive, p + r = q)p, q:positivep < q -> sub_mask p q = IsNegapply sub_mask_neg_iff'. Qed.p, q:positivep < q -> sub_mask p q = IsNegp, q:positivep <= q -> p - q = 1p, q:positivep <= q -> p - q = 1p, q:positive(p ?= q) <> Gt -> match sub_mask p q with | IsPos z => z | _ => 1 end = 1destruct sub_mask; easy'. Qed.p, q:positivemask2cmp (sub_mask p q) <> Gt -> match sub_mask p q with | IsPos z => z | _ => 1 end = 1p, q:positivep < q -> p - q = 1p, q:positivep < q -> p - q = 1now apply sub_le, lt_le_incl. Qed.p, q:positiveH:p < qp - q = 1p:positivep - p = 1p:positivep - p = 1now rewrite sub_mask_diag. Qed.p:positivematch sub_mask p p with | IsPos z => z | _ => 1 end = 1
p, q:positivep < q -> (size_nat p <= size_nat q)%natp, q:positivep < q -> (size_nat p <= size_nat q)%natp, q:positivele0:forall n : nat, (0 <= n)%natp < q -> (size_nat p <= size_nat q)%natp, q:positivele0:forall n : nat, (0 <= n)%natleS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%natp < q -> (size_nat p <= size_nat q)%natp:positivele0:forall n : nat, (0 <= n)%natleS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%natforall q : positive, p < q -> (size_nat p <= size_nat q)%natp:positivele0:forall n : nat, (0 <= n)%natleS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%natIHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%natq:positiveH:switch_Eq Gt (p ?= q) = Lt(size_nat p <= size_nat q)%natp:positivele0:forall n : nat, (0 <= n)%natleS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%natIHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%natq:positiveH:switch_Eq Lt (p ?= q) = Lt(size_nat p <= size_nat q)%natp:positivele0:forall n : nat, (0 <= n)%natleS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%natIHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%natq:positiveH:switch_Eq Gt (p ?= q) = Ltp < qp:positivele0:forall n : nat, (0 <= n)%natleS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%natIHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%natq:positiveH:switch_Eq Lt (p ?= q) = Lt(size_nat p <= size_nat q)%natp:positivele0:forall n : nat, (0 <= n)%natleS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%natIHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%natq:positiveH:switch_Eq Gt (p ?= q) = Lt(p ?= q) = Ltp:positivele0:forall n : nat, (0 <= n)%natleS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%natIHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%natq:positiveH:switch_Eq Lt (p ?= q) = Lt(size_nat p <= size_nat q)%natdestruct (compare_spec p q); subst; now auto. Qed.p:positivele0:forall n : nat, (0 <= n)%natleS:forall n m : nat, (n <= m)%nat -> (S n <= S m)%natIHp:forall q0 : positive, p < q0 -> (size_nat p <= size_nat q0)%natq:positiveH:switch_Eq Lt (p ?= q) = Lt(size_nat p <= size_nat q)%natp:positivep < 2 ^ size pp:positivep < 2 ^ size pp:positiveIHp:p < 2 ^ size pp~1 < 2 * 2 ^ size pnow apply le_succ_l. Qed.p:positiveIHp:succ p <= 2 ^ size pp~1 < 2 * 2 ^ size pp:positive2 ^ size p <= p~0p:positive2 ^ size p <= p~0p:positiveIHp:2 ^ size p <= p~02 * 2 ^ size p <= p~1~0p:positiveIHp:2 ^ size p <= p~02 ^ size p <= p~1p:positiveIHp:2 ^ size p <= p~02 ^ size p < p~1apply lt_succ_r, IHp. Qed.p:positiveIHp:2 ^ size p <= p~02 ^ size p < succ p~0
First, the specification
forall x y : positive, y <= x -> max x y = xforall x y : positive, y <= x -> max x y = xx, y:positiveH:y <= xmax x y = xx, y:positiveH:y <= xmatch x ?= y with | Gt => x | _ => y end = xx, y:positiveH:y <= xx < y -> y = xx, y:positiveH:y <= xH':x < yy = xnow elim H. Qed.x, y:positiveH:~ x < yH':x < yy = xforall x y : positive, x <= y -> max x y = yforall x y : positive, x <= y -> max x y = yforall x y : positive, (x ?= y) <> Gt -> match x ?= y with | Gt => x | _ => y end = ydestruct compare; easy'. Qed.x, y:positive(x ?= y) <> Gt -> match x ?= y with | Gt => x | _ => y end = yforall x y : positive, x <= y -> min x y = xforall x y : positive, x <= y -> min x y = xforall x y : positive, (x ?= y) <> Gt -> match x ?= y with | Gt => y | _ => x end = xdestruct compare; easy'. Qed.x, y:positive(x ?= y) <> Gt -> match x ?= y with | Gt => y | _ => x end = xforall x y : positive, y <= x -> min x y = yforall x y : positive, y <= x -> min x y = yx, y:positiveH:y <= xmin x y = yx, y:positiveH:y <= xmatch x ?= y with | Gt => y | _ => x end = yx, y:positiveH:y <= xx < y -> x = yx, y:positiveH:y <= xH':x < yx = ynow elim H'. Qed.x, y:positiveH:~ x < yH':x < yx = 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
n:positivemax 1 n = nn:positivemax 1 n = nn:positivematch 1 ?= n with | Gt => 1 | _ => n end = nn:positiven < 1 -> 1 = nn:positiveH:n < 11 = nn:positiveH:~ 1 <= n1 = napply le_1_l. Qed.n:positiveH:~ 1 <= n1 <= nn:positivemax n 1 = nn:positivemax n 1 = napply max_1_l. Qed.n:positivemax 1 n = nn:positivemin 1 n = 1n:positivemin 1 n = 1n:positivematch 1 ?= n with | Gt => n | _ => 1 end = 1n:positiven < 1 -> n = 1n:positiveH:n < 1n = 1n:positiveH:~ 1 <= nn = 1apply le_1_l. Qed.n:positiveH:~ 1 <= n1 <= nn:positivemin n 1 = 1n:positivemin n 1 = 1apply min_1_l. Qed.n:positivemin 1 n = 1
Minimum, maximum and operations (consequences of monotonicity)
n, m:positivesucc (max n m) = max (succ n) (succ m)n, m:positivesucc (max n m) = max (succ n) (succ m)n, m:positivemax (succ n) (succ m) = succ (max n m)n, m:positiveProper (le ==> le) succapply succ_le_mono. Qed.n, m, x, x':positivex <= x' -> succ x <= succ x'n, m:positivesucc (min n m) = min (succ n) (succ m)n, m:positivesucc (min n m) = min (succ n) (succ m)n, m:positivemin (succ n) (succ m) = succ (min n m)n, m:positiveProper (le ==> le) succapply succ_le_mono. Qed.n, m, x, x':positivex <= x' -> succ x <= succ x'n, m, p:positivemax (p + n) (p + m) = p + max n mn, m, p:positivemax (p + n) (p + m) = p + max n mn, m, p:positiveProper (le ==> le) (add p)apply add_le_mono_l. Qed.n, m, p, x, x':positivex <= x' -> p + x <= p + x'n, m, p:positivemax (n + p) (m + p) = max n m + pn, m, p:positivemax (n + p) (m + p) = max n m + papply add_max_distr_l. Qed.n, m, p:positivemax (p + n) (p + m) = p + max n mn, m, p:positivemin (p + n) (p + m) = p + min n mn, m, p:positivemin (p + n) (p + m) = p + min n mn, m, p:positiveProper (le ==> le) (add p)apply add_le_mono_l. Qed.n, m, p, x, x':positivex <= x' -> p + x <= p + x'n, m, p:positivemin (n + p) (m + p) = min n m + pn, m, p:positivemin (n + p) (m + p) = min n m + papply add_min_distr_l. Qed.n, m, p:positivemin (p + n) (p + m) = p + min n mn, m, p:positivemax (p * n) (p * m) = p * max n mn, m, p:positivemax (p * n) (p * m) = p * max n mn, m, p:positiveProper (le ==> le) (mul p)apply mul_le_mono_l. Qed.n, m, p, x, x':positivex <= x' -> p * x <= p * x'n, m, p:positivemax (n * p) (m * p) = max n m * pn, m, p:positivemax (n * p) (m * p) = max n m * papply mul_max_distr_l. Qed.n, m, p:positivemax (p * n) (p * m) = p * max n mn, m, p:positivemin (p * n) (p * m) = p * min n mn, m, p:positivemin (p * n) (p * m) = p * min n mn, m, p:positiveProper (le ==> le) (mul p)apply mul_le_mono_l. Qed.n, m, p, x, x':positivex <= x' -> p * x <= p * x'n, m, p:positivemin (n * p) (m * p) = min n m * pn, m, p:positivemin (n * p) (m * p) = min n m * papply mul_min_distr_l. Qed.n, m, p:positivemin (p * n) (p * m) = p * min n m
forall (A : Type) (op : A -> A -> A), (forall x y z : A, op x (op y z) = op (op x y) z) -> forall (p : positive) (a : A), iter_op op (succ p) a = op a (iter_op op p a)forall (A : Type) (op : A -> A -> A), (forall x y z : A, op x (op y z) = op (op x y) z) -> forall (p : positive) (a : A), iter_op op (succ p) a = op a (iter_op op p a)A:Typeop:A -> A -> AH:forall x y z : A, op x (op y z) = op (op x y) zp:positiveIHp:forall a0 : A, iter_op op (succ p) a0 = op a0 (iter_op op p a0)a:Aiter_op op (succ p) (op a a) = op a (op a (iter_op op p (op a a)))apply IHp. Qed.A:Typeop:A -> A -> AH:forall x y z : A, op x (op y z) = op (op x y) zp:positiveIHp:forall a0 : A, iter_op op (succ p) a0 = op a0 (iter_op op p a0)a:Aiter_op op (succ p) (op a a) = op (op a a) (iter_op op p (op a a))
n:natof_succ_nat n = of_nat (S n)n:natof_succ_nat n = of_nat (S n)of_succ_nat 0 = of_nat 1n:natIHn:of_succ_nat n = of_nat (S n)of_succ_nat (S n) = of_nat (S (S n))n:natIHn:of_succ_nat n = of_nat (S n)of_succ_nat (S n) = of_nat (S (S n))n:natIHn:of_succ_nat n = of_nat (S n)succ (of_succ_nat n) = succ match n with | 0%nat => 1 | S _ => succ (of_nat n) endnow rewrite IHn. Qed.n:natIHn:of_succ_nat n = of_nat (S n)of_succ_nat n = match n with | 0%nat => 1 | S _ => succ (of_nat n) endn:natpred (of_succ_nat n) = of_nat nn:natpred (of_succ_nat n) = of_nat npred (of_succ_nat 0) = of_nat 0n:natpred (of_succ_nat (S n)) = of_nat (S n)n:natpred (of_succ_nat (S n)) = of_nat (S n)n:natpred (succ (of_succ_nat n)) = of_nat (S n)apply of_nat_succ. Qed.n:natof_succ_nat n = of_nat (S n)n:natn <> 0%nat -> succ (of_nat n) = of_succ_nat nn:natn <> 0%nat -> succ (of_nat n) = of_succ_nat nn:natn <> 0%nat -> succ (of_nat n) = of_nat (S n)now destruct 1. Qed.0%nat <> 0%nat -> succ (of_nat 0) = of_nat 1
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.f, g:positive -> positivep:(positive * mask)%typex:positivef = xO \/ f = xI -> g = xO \/ g = xI -> SqrtSpec p x -> SqrtSpec (sqrtrem_step f g p) (g (f x))f, g:positive -> positivep:(positive * mask)%typex:positivef = xO \/ f = xI -> g = xO \/ g = xI -> SqrtSpec p x -> SqrtSpec (sqrtrem_step f g p) (g (f x))(* exact *)f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs:positiveSqrtSpec (sqrtrem_step f g (s, IsNul)) (g (f (s * s)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0SqrtSpec (sqrtrem_step f g (s, IsPos r)) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs:positiveSqrtSpec (s~0, sub_mask (g (f 1)) 4) (g (f (s * s)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0SqrtSpec (sqrtrem_step f g (s, IsPos r)) (g (f (s * s + r)))(* approx *)f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0SqrtSpec (sqrtrem_step f g (s, IsPos r)) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)SqrtSpec (sqrtrem_step f g (s, IsPos r)) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)SqrtSpec (if match s~0~1 ?= g (f r) with | Gt => false | _ => true end then (s~1, sub_mask (g (f r)) s~0~1) else (s~0, IsPos (g (f r)))) (g (f (s * s + r)))(* - EQ *)f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)EQ:s~0~1 = g (f r)SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)EQ:s~0~1 = g (f r)SqrtSpec (s~1, IsNul) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)EQ:s~0~1 = g (f r)g (f (s * s + r)) = s~1 * s~1f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIs, r:positiveHr:r <= s~0EQ:s~0 = f rHfg:forall p0 q : positive, (f (p0 + q))~1 = p0~0~0 + (f q)~1(f (s * s + r))~1 = s~1 * s~1f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))p:(positive * mask)%typex, s, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, (p0 + q)~0~1 = p0~0~0 + q~0~1EQ:s = r(s * s + r)~0~1 = s~1 * s~1f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))p:(positive * mask)%typex, r:positiveHr:r <= r~0Hfg:forall p0 q : positive, (p0 + q)~0~1 = p0~0~0 + q~0~1(r * r + r)~0~1 = r~1 * r~1f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))(* - LT *)f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)SqrtSpec (s~1, sub_mask (g (f r)) s~0~1) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)SqrtSpec (s~1, IsPos y) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)g (f (s * s + r)) = s~1 * s~1 + yf, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)y <= s~1~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)(s * s)~0~0 + (s~0~1 + y) = s~1 * s~1 + yf, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)y <= s~1~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)y <= s~1~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)y <= s~1~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r < succ s~0LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)y <= s~1~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r < s~1LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)y <= s~1~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r < s~1LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)g (f r) < s~0~1 + succ s~1~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r < s~1LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)g (f r) < (add_carry s s)~0~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r < s~1LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)g (f r) < (succ s~0)~0~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r < s~1LT:s~0~1 < g (f r)y:positiveH:s~0~1 + y = g (f r)g (f r) < s~1~0~0f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))(* - GT *)f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1SqrtSpec (s~0, IsPos (g (f r))) (g (f (s * s + r)))f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1g (f (s * s + r)) = s~0 * s~0 + g (f r)f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1g (f r) <= s~0~0apply lt_succ_r, GT. Qed.f, g:positive -> positivep:(positive * mask)%typex:positiveHf:f = xO \/ f = xIHg:g = xO \/ g = xIs, r:positiveHr:r <= s~0Hfg:forall p0 q : positive, g (f (p0 + q)) = p0~0~0 + g (f q)GT:g (f r) < s~0~1g (f r) <= s~0~0p:positiveSqrtSpec (sqrtrem p) pp:positiveSqrtSpec (sqrtrem p) pforall p : positive, SqrtSpec (sqrtrem p) pdestruct p; try destruct p; try (constructor; easy); apply sqrtrem_step_spec; auto. Qed.sqrtrem_spec:forall p : positive, SqrtSpec (sqrtrem p) pforall p : positive, SqrtSpec (sqrtrem p) pp:positivelet s := sqrt p in s * s <= p < succ s * succ sp:positivelet s := sqrt p in s * s <= p < succ s * succ sp:positivesqrt p * sqrt p <= p < succ (sqrt p) * succ (sqrt p)p:positiveH:SqrtSpec (sqrtrem p) psqrt p * sqrt p <= p < succ (sqrt p) * succ (sqrt p)p:positiveH:SqrtSpec (sqrtrem p) pfst (sqrtrem p) * fst (sqrtrem p) <= p < succ (fst (sqrtrem p)) * succ (fst (sqrtrem p))p, s:positiverm:maskH:SqrtSpec (s, rm) ps * s <= p < succ s * succ s(* exact *)s:positiverm:masks * s <= s * s < succ s * succ ss:positiverm:maskr:positiveH1:r <= s~0s * s <= s * s + r < succ s * succ ss:positiverm:masks * s <= s * ss:positiverm:masks * s < succ s * succ ss:positiverm:maskr:positiveH1:r <= s~0s * s <= s * s + r < succ s * succ ss:positiverm:masks * s < succ s * succ ss:positiverm:maskr:positiveH1:r <= s~0s * s <= s * s + r < succ s * succ s(* approx *)s:positiverm:maskr:positiveH1:r <= s~0s * s <= s * s + r < succ s * succ ss:positiverm:maskr:positiveH1:r <= s~0s * s <= s * s + rs:positiverm:maskr:positiveH1:r <= s~0s * s + r < succ s * succ ss:positiverm:maskr:positiveH1:r <= s~0s * s + r < succ s * succ ss:positiverm:maskr:positiveH1:r <= s~0s * s + r < 1 + s + (s + s * s)s:positiverm:maskr:positiveH1:r <= s~0r + s * s < 1 + s + s + s * snow rewrite <- add_assoc, add_diag, add_1_l, lt_succ_r. Qed.s:positiverm:maskr:positiveH1:r <= s~0r < 1 + s + s
p, q, r:positive(p | r) -> (p | q + r) -> (p | q)p, q, r:positive(p | r) -> (p | q + r) -> (p | q)p, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * p(p | q)p, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * pq = (t - s) * pp, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * pq = t * p - s * pp, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * ps < tp, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * pq = q + r - rp, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * ps < tp, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * pq + r - r = qp, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * ps < tp, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * ps < tp, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * ps * p < t * papply lt_add_r. Qed.p, q, r, s:positiveHs:r = s * pt:positiveHt:q + r = t * pr < r + qp, q, r:positive(p | q~0) -> (p | r~1) -> (p | q)p, q, r:positive(p | q~0) -> (p | r~1) -> (p | q)p, q, r, s:positiveHs:q~0 = s * pt:positiveHt:r~1 = t * p(p | q)p, q, r, s:positiveHs:q~0 = s * p~1t:positiveHt:r~1 = t * p~1(p~1 | q)p, q, r, s:positiveHs:q~0 = s * p~0t:positiveHt:r~1 = t * p~0(p~0 | q)q, r, s:positiveHs:q~0 = s * 1t:positiveHt:r~1 = t * 1(1 | q)p, q, r, s:positiveHs:q~0 = s~0 * p~1t:positiveHt:r~1 = t * p~1(p~1 | q)p, q, r, s:positiveHs:q~0 = s * p~0t:positiveHt:r~1 = t * p~0(p~0 | q)q, r, s:positiveHs:q~0 = s * 1t:positiveHt:r~1 = t * 1(1 | q)p, q, r, s:positiveHs:q~0 = (s * p~1)~0t:positiveHt:r~1 = t * p~1(p~1 | q)p, q, r, s:positiveHs:q~0 = s * p~0t:positiveHt:r~1 = t * p~0(p~0 | q)q, r, s:positiveHs:q~0 = s * 1t:positiveHt:r~1 = t * 1(1 | q)p, q, r, s:positiveHs:q = s * p~1t:positiveHt:r~1 = t * p~1(p~1 | q)p, q, r, s:positiveHs:q~0 = s * p~0t:positiveHt:r~1 = t * p~0(p~0 | q)q, r, s:positiveHs:q~0 = s * 1t:positiveHt:r~1 = t * 1(1 | q)p, q, r, s:positiveHs:q~0 = s * p~0t:positiveHt:r~1 = t * p~0(p~0 | q)q, r, s:positiveHs:q~0 = s * 1t:positiveHt:r~1 = t * 1(1 | q)exists q; now rewrite mul_1_r. Qed.q, r, s:positiveHs:q~0 = s * 1t:positiveHt:r~1 = t * 1(1 | q)p, q:positive(p~0 | q~0) <-> (p | q)p, q:positive(p~0 | q~0) <-> (p | q)p, q, r:positiveH:q~0 = r * p~0(p | q)p, q, r:positiveH:q = r * p(p~0 | q~0)p, q, r:positiveH:q~0 = (r * p)~0(p | q)p, q, r:positiveH:q = r * p(p~0 | q~0)p, q, r:positiveH:q = r * p(p | q)p, q, r:positiveH:q = r * p(p~0 | q~0)p, q, r:positiveH:q = r * p(p~0 | q~0)p, q, r:positiveH:q = r * pq~0 = r * p~0f_equal; auto. Qed.p, q, r:positiveH:q = r * pq~0 = (r * p)~0p, q, r:positive(p | q) -> (p | q * r)p, q, r:positive(p | q) -> (p | q * r)p, q, r, s:positiveH:q = s * p(p | q * r)p, q, r, s:positiveH:q = s * pq * r = s * r * pnow f_equal. Qed.p, q, r, s:positiveH:q = s * pq * r = s * p * rp, q, r:positive(p | r) -> (p | q * r)p, q, r:positive(p | r) -> (p | q * r)apply divide_mul_l. Qed.p, q, r:positive(p | r) -> (p | r * q)
The first component of ggcd is gcd
forall (n : nat) (a b : positive), fst (ggcdn n a b) = gcdn n a bforall (n : nat) (a b : positive), fst (ggcdn n a b) = gcdn n a bforall a b : positive, fst (ggcdn 0 a b) = gcdn 0 a bn:natIHn:forall a b : positive, fst (ggcdn n a b) = gcdn n a bforall a b : positive, fst (ggcdn (S n) a b) = gcdn (S n) a bdestruct a, b; simpl; auto; try case compare_spec; simpl; trivial; rewrite <- IHn; destruct ggcdn as (g,(u,v)); simpl; auto. Qed.n:natIHn:forall a b : positive, fst (ggcdn n a b) = gcdn n a bforall a b : positive, fst (ggcdn (S n) a b) = gcdn (S n) a bforall a b : positive, fst (ggcd a b) = gcd a bforall a b : positive, fst (ggcd a b) = gcd a bforall a b : positive, fst (ggcdn (size_nat a + size_nat b) a b) = gcdn (size_nat a + size_nat b) a bapply ggcdn_gcdn. Qed.a, b:positivefst (ggcdn (size_nat a + size_nat b) a b) = gcdn (size_nat a + size_nat b) 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.forall (n : nat) (a b : positive), let '(g, (aa, bb)) := ggcdn n a b in a = g * aa /\ b = g * bbforall (n : nat) (a b : positive), let '(g, (aa, bb)) := ggcdn n a b in a = g * aa /\ b = g * bbforall a b : positive, let '(g, (aa, bb)) := ggcdn 0 a b in a = g * aa /\ b = g * bbn:natIHn:forall a b : positive, let '(g, (aa, bb)) := ggcdn n a b in a = g * aa /\ b = g * bbforall a b : positive, let '(g, (aa, bb)) := ggcdn (S n) a b in a = g * aa /\ b = g * bbn:natIHn:forall a b : positive, let '(g, (aa, bb)) := ggcdn n a b in a = g * aa /\ b = g * bbforall a b : positive, let '(g, (aa, bb)) := ggcdn (S n) a b in a = g * aa /\ b = g * bb(* Eq *)n:natIHn:forall a0 b0 : positive, let '(g, (aa, bb)) := ggcdn n a0 b0 in a0 = g * aa /\ b0 = g * bba, b:positivea = b -> a~1 = a~1 * 1 /\ b~1 = a~1 * 1n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveb - a = g * u /\ a~1 = g * v -> a < b -> a~1 = g * v /\ b~1 = g * (v + u~0)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a b0 : positive, let '(g, (aa, bb)) := ggcdn n a b0 in a = g * aa /\ b0 = g * bbb:positiveb~1 = b~1 * 1 /\ b~1 = b~1 * 1n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveb - a = g * u /\ a~1 = g * v -> a < b -> a~1 = g * v /\ b~1 = g * (v + u~0)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0(* Lt *)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveb - a = g * u /\ a~1 = g * v -> a < b -> a~1 = g * v /\ b~1 = g * (v + u~0)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':b - a = g * uH:a~1 = g * vLT:a < bb~1 = g * (v + u~0)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':b - a = g * uH:a~1 = g * vLT:a < bb~1 = a~1 + (b - a)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':b - a = g * uH:a~1 = g * vLT:a < bb~1 = (a + (b - a))~1n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':b - a = g * uH:a~1 = g * vLT:a < bb = a + (b - a)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':b - a = g * uH:a~1 = g * vLT:a < ba + (b - a) = bn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':b - a = g * uH:a~1 = g * vLT:a < bb - a + a = bn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0(* Gt *)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea - b = g * u /\ b~1 = g * v -> b < a -> a~1 = g * (v + u~0) /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':a - b = g * uH:b~1 = g * vLT:b < aa~1 = g * (v + u~0)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':a - b = g * uH:b~1 = g * vLT:b < aa~1 = b~1 + (a - b)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':a - b = g * uH:b~1 = g * vLT:b < aa~1 = (b + (a - b))~1n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':a - b = g * uH:b~1 = g * vLT:b < aa = b + (a - b)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':a - b = g * uH:b~1 = g * vLT:b < ab + (a - b) = an:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH':a - b = g * uH:b~1 = g * vLT:b < aa - b + b = an:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0(* Then... *)n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea~1 = g * u /\ b = g * v -> a~1 = g * u /\ b~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH:a~1 = g * uH':b = g * vb~0 = g * v~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b~1 = g * v -> a~0 = g * u~0 /\ b~1 = g * vn:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positiveH:a = g * uH':b~1 = g * va~0 = g * u~0n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0intros (H,H'); split; subst; auto. Qed.n:natIHn:forall a0 b0 : positive, let '(g0, (aa, bb)) := ggcdn n a0 b0 in a0 = g0 * aa /\ b0 = g0 * bba, b, g, u, v:positivea = g * u /\ b = g * v -> a~0 = (g * u)~0 /\ b~0 = (g * v)~0forall a b : positive, let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bbforall a b : positive, let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bbforall a b : positive, let '(g, (aa, bb)) := ggcdn (size_nat a + size_nat b) a b in a = g * aa /\ b = g * bbapply ggcdn_correct_divisors. Qed.a, b:positivelet '(g, (aa, bb)) := ggcdn (size_nat a + size_nat b) a b in a = g * aa /\ b = g * bb
We can use this fact to prove a part of the gcd correctness
forall a b : positive, (gcd a b | a)forall a b : positive, (gcd a b | a)a, b:positive(gcd a b | a)a, b:positive(fst (ggcd a b) | a)a, b:positive(let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb) -> (fst (ggcd a b) | a)a, b, g, aa, bb:positivea = g * aa /\ b = g * bb -> (g | a)a, b, g, aa, bb:positiveH:a = g * aa(g | a)now rewrite mul_comm. Qed.a, b, g, aa, bb:positiveH:a = g * aaa = aa * gforall a b : positive, (gcd a b | b)forall a b : positive, (gcd a b | b)a, b:positive(gcd a b | b)a, b:positive(fst (ggcd a b) | b)a, b:positive(let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb) -> (fst (ggcd a b) | b)a, b, g, aa, bb:positivea = g * aa /\ b = g * bb -> (g | b)a, b, g, aa, bb:positiveH:b = g * bb(g | b)now rewrite mul_comm. Qed.a, b, g, aa, bb:positiveH:b = g * bbb = bb * g
We now prove directly that gcd is the greatest amongst common divisors
forall (n : nat) (a b : positive), (size_nat a + size_nat b <= n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn n a b)forall (n : nat) (a b : positive), (size_nat a + size_nat b <= n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn n a b)forall a b : positive, (size_nat a + size_nat b <= 0)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn 0 a b)n:natIHn:forall a b : positive, (size_nat a + size_nat b <= n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn n a b)forall a b : positive, (size_nat a + size_nat b <= S n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn (S n) a b)n:natIHn:forall a b : positive, (size_nat a + size_nat b <= n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn n a b)forall a b : positive, (size_nat a + size_nat b <= S n)%nat -> forall p : positive, (p | a) -> (p | b) -> (p | gcdn (S n) a b)(* Lt *)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positivea < b -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (b - a) a~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | gcdn n (b - a) a~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(size_nat (b - a) + size_nat a~1 <= n)%natn:nata, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | b - a)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:a < bLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(size_nat (b - a) + size_nat a~1 <= n)%natn:nata, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | b - a)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:a < bLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(size_nat (b - a) + size_nat a~1 <= size_nat a + S (size_nat b))%natn:nata, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | b - a)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:a < bLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(size_nat a~1 + size_nat (b - a) <= S (size_nat a) + size_nat b)%natn:nata, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | b - a)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:a < bLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(size_nat (b - a) <= size_nat b)%natn:nata, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | b - a)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | b - a)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | (b - a)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:a < bLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | (b - a)~0 + a~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)(* Gt *)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveb < a -> (S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~1) -> (p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLT:b < aLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | gcdn n (a - b) b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:b < aLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(size_nat (a - b) + size_nat b~1 <= n)%natn:nata, b:positiveLT:b < aLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | a - b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:b < aLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(size_nat (a - b) + size_nat b~1 <= n)%natn:nata, b:positiveLT:b < aLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | a - b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:b < aLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(size_nat (a - b) + size_nat b~1 <= size_nat a + S (size_nat b))%natn:nata, b:positiveLT:b < aLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | a - b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:b < aLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(size_nat (a - b) <= size_nat a)%natn:nata, b:positiveLT:b < aLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | a - b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:b < aLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | a - b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:b < aLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | (a - b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLT:b < aLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~1)(p | (a - b)~0 + b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)(* a~1 b~0 *)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~1) -> (p | b~0) -> (p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~0)(p | gcdn n a~1 b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~0)(size_nat a~1 + size_nat b <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~0)(p | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~0)(size_nat a~1 + size_nat b <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~0)(p | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~0)(S (size_nat a + size_nat b) <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~0)(p | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~1)Hp2:(p | b~0)(p | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)(* a~0 b~1 *)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~1) -> (p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~0)Hp2:(p | b~1)(p | gcdn n a b~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~0)Hp2:(p | b~1)(size_nat a + size_nat b~1 <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~0)Hp2:(p | b~1)(p | a)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~0)Hp2:(p | b~1)(size_nat a + S (size_nat b) <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~0)Hp2:(p | b~1)(p | a)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~0)Hp2:(p | b~1)(p | a)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)(* a~0 b~0 *)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positive(S (size_nat a + S (size_nat b)) <= S n)%nat -> forall p : positive, (p | a~0) -> (p | b~0) -> (p | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p | a~0)Hp2:(p | b~0)(p | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | 2 * gcdn n a b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | gcdn n a b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(size_nat a + size_nat b <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | a)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(size_nat a + size_nat b <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | a)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(S (size_nat a + size_nat b) <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | a)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | a)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | p~1)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~1 | a~0)Hp2:(p~1 | b~0)(p~1 | p~1)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p~0 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p0 : positive, (p0 | a0) -> (p0 | b0) -> (p0 | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | gcdn n a b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(size_nat a + size_nat b <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | a)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(size_nat a + size_nat b <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | a)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(size_nat a + S (size_nat b) <= n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(S (size_nat a + size_nat b) <= n)%natn:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | a)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | a)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:nata, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natp:positiveHp1:(p~0 | a~0)Hp2:(p~0 | b~0)(p | b)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(1 | (gcdn n a b)~0)now rewrite mul_1_r. Qed.n:natIHn:forall a0 b0 : positive, (size_nat a0 + size_nat b0 <= n)%nat -> forall p : positive, (p | a0) -> (p | b0) -> (p | gcdn n a0 b0)a, b:positiveLE:(S (size_nat a + S (size_nat b)) <= S n)%natHp1:(1 | a~0)Hp2:(1 | b~0)(gcdn n a b)~0 = (gcdn n a b)~0 * 1forall a b p : positive, (p | a) -> (p | b) -> (p | gcd a b)forall a b p : positive, (p | a) -> (p | b) -> (p | gcd a b)apply gcdn_greatest; auto. Qed.a, b, p:positiveH:(p | a)H0:(p | b)(p | gcd a b)
As a consequence, the rests after division by gcd are relatively prime
forall a b : positive, let (aa, bb) := snd (ggcd a b) in forall p : positive, (p | aa) -> (p | bb) -> p = 1forall a b : positive, let (aa, bb) := snd (ggcd a b) in forall p : positive, (p | aa) -> (p | bb) -> p = 1a, b:positivelet (aa, bb) := snd (ggcd a b) in forall p : positive, (p | aa) -> (p | bb) -> p = 1a, b:positive(forall p : positive, (p | a) -> (p | b) -> (p | gcd a b)) -> (let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb) -> let (aa, bb) := snd (ggcd a b) in forall p : positive, (p | aa) -> (p | bb) -> p = 1a, b:positive(forall p : positive, (p | a) -> (p | b) -> (p | fst (ggcd a b))) -> (let '(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb) -> let (aa, bb) := snd (ggcd a b) in forall p : positive, (p | aa) -> (p | bb) -> p = 1a, b, g, aa, bb:positive(forall p : positive, (p | a) -> (p | b) -> (p | g)) -> a = g * aa /\ b = g * bb -> forall p : positive, (p | aa) -> (p | bb) -> p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)(g * p | g)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)H':(g * p | g)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)(g * p | g * aa)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)(g * p | g * bb)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)H':(g * p | g)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p, r:positiveHr:aa = r * pHp2:(p | bb)(g * p | g * aa)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)(g * p | g * bb)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)H':(g * p | g)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p, r:positiveHr:aa = r * pHp2:(p | bb)g * aa = r * (g * p)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)(g * p | g * bb)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)H':(g * p | g)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)(g * p | g * bb)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)H':(g * p | g)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)r:positiveHr:bb = r * p(g * p | g * bb)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)H':(g * p | g)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)r:positiveHr:bb = r * pg * bb = r * (g * p)g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)H':(g * p | g)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)H':(g * p | g)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)q:positiveH':g = q * (g * p)p = 1g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)q:positiveH':g = q * p * gp = 1now apply mul_reg_r with g. Qed. End Pos. Bind Scope positive_scope with Pos.t positive.g, aa, bb:positiveH:forall p0 : positive, (p0 | g * aa) -> (p0 | g * bb) -> (p0 | g)p:positiveHp1:(p | aa)Hp2:(p | bb)q:positiveH':g = q * p * gq * p = 1
Exportation of notations
Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. 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 Pplus := Pos.add (only parsing). Notation Pplus_carry := Pos.add_carry (only parsing). Notation Pmult_nat := (Pos.iter_op plus) (only parsing). Notation nat_of_P := Pos.to_nat (only parsing). Notation P_of_succ_nat := Pos.of_succ_nat (only parsing). Notation Pdouble_minus_one := Pos.pred_double (only parsing). Notation positive_mask := Pos.mask (only parsing). Notation positive_mask_rect := Pos.mask_rect (only parsing). Notation positive_mask_ind := Pos.mask_ind (only parsing). Notation positive_mask_rec := Pos.mask_rec (only parsing). Notation Pdouble_plus_one_mask := Pos.succ_double_mask (only parsing). Notation Pdouble_minus_two := Pos.double_pred_mask (only parsing). Notation Pminus_mask := Pos.sub_mask (only parsing). Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing). Notation Pminus := Pos.sub (only parsing). Notation Pmult := Pos.mul (only parsing). Notation iter_pos := @Pos.iter (only parsing). Notation Psize := Pos.size_nat (only parsing). Notation Psize_pos := Pos.size (only parsing). Notation Pcompare x y m := (Pos.compare_cont m x y) (only parsing). Notation positive_eq_dec := Pos.eq_dec (only parsing). Notation xI_succ_xO := Pos.xI_succ_xO (only parsing). Notation Psucc_o_double_minus_one_eq_xO := Pos.succ_pred_double (only parsing). Notation Pdouble_minus_one_o_succ_eq_xI := Pos.pred_double_succ (only parsing). Notation xO_succ_permute := Pos.double_succ (only parsing). Notation double_moins_un_xO_discr := Pos.pred_double_xO_discr (only parsing). Notation Psucc_not_one := Pos.succ_not_1 (only parsing). Notation Psucc_pred := Pos.succ_pred_or (only parsing). Notation Pplus_carry_spec := Pos.add_carry_spec (only parsing). Notation Pplus_comm := Pos.add_comm (only parsing). Notation Pplus_succ_permute_r := Pos.add_succ_r (only parsing). Notation Pplus_succ_permute_l := Pos.add_succ_l (only parsing). Notation Pplus_no_neutral := Pos.add_no_neutral (only parsing). Notation Pplus_carry_plus := Pos.add_carry_add (only parsing). Notation Pplus_reg_r := Pos.add_reg_r (only parsing). Notation Pplus_reg_l := Pos.add_reg_l (only parsing). Notation Pplus_carry_reg_r := Pos.add_carry_reg_r (only parsing). Notation Pplus_carry_reg_l := Pos.add_carry_reg_l (only parsing). Notation Pplus_assoc := Pos.add_assoc (only parsing). Notation Pplus_xO := Pos.add_xO (only parsing). Notation Pplus_xI_double_minus_one := Pos.add_xI_pred_double (only parsing). Notation Pplus_xO_double_minus_one := Pos.add_xO_pred_double (only parsing). Notation Pplus_diag := Pos.add_diag (only parsing). Notation PeanoView := Pos.PeanoView (only parsing). Notation PeanoOne := Pos.PeanoOne (only parsing). Notation PeanoSucc := Pos.PeanoSucc (only parsing). Notation PeanoView_rect := Pos.PeanoView_rect (only parsing). Notation PeanoView_ind := Pos.PeanoView_ind (only parsing). Notation PeanoView_rec := Pos.PeanoView_rec (only parsing). Notation peanoView_xO := Pos.peanoView_xO (only parsing). Notation peanoView_xI := Pos.peanoView_xI (only parsing). Notation peanoView := Pos.peanoView (only parsing). Notation PeanoView_iter := Pos.PeanoView_iter (only parsing). Notation eq_dep_eq_positive := Pos.eq_dep_eq_positive (only parsing). Notation PeanoViewUnique := Pos.PeanoViewUnique (only parsing). Notation Prect := Pos.peano_rect (only parsing). Notation Prect_succ := Pos.peano_rect_succ (only parsing). Notation Prect_base := Pos.peano_rect_base (only parsing). Notation Prec := Pos.peano_rec (only parsing). Notation Pind := Pos.peano_ind (only parsing). Notation Pcase := Pos.peano_case (only parsing). Notation Pmult_1_r := Pos.mul_1_r (only parsing). Notation Pmult_Sn_m := Pos.mul_succ_l (only parsing). Notation Pmult_xO_permute_r := Pos.mul_xO_r (only parsing). Notation Pmult_xI_permute_r := Pos.mul_xI_r (only parsing). Notation Pmult_comm := Pos.mul_comm (only parsing). Notation Pmult_plus_distr_l := Pos.mul_add_distr_l (only parsing). Notation Pmult_plus_distr_r := Pos.mul_add_distr_r (only parsing). Notation Pmult_assoc := Pos.mul_assoc (only parsing). Notation Pmult_xI_mult_xO_discr := Pos.mul_xI_mul_xO_discr (only parsing). Notation Pmult_xO_discr := Pos.mul_xO_discr (only parsing). Notation Pmult_reg_r := Pos.mul_reg_r (only parsing). Notation Pmult_reg_l := Pos.mul_reg_l (only parsing). Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (only parsing). Notation iter_pos_swap_gen := Pos.iter_swap_gen (only parsing). Notation iter_pos_swap := Pos.iter_swap (only parsing). Notation iter_pos_succ := Pos.iter_succ (only parsing). Notation iter_pos_plus := Pos.iter_add (only parsing). Notation iter_pos_invariant := Pos.iter_invariant (only parsing). Notation Pcompare_refl_id := Pos.compare_cont_refl (only parsing). Notation Pcompare_eq_iff := Pos.compare_eq_iff (only parsing). Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (only parsing). Notation Pcompare_eq_Lt := Pos.compare_lt_iff (only parsing). Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (only parsing). Notation Pcompare_antisym := Pos.compare_cont_antisym (only parsing). Notation ZC1 := Pos.gt_lt (only parsing). Notation ZC2 := Pos.lt_gt (only parsing). Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (only parsing). Notation Pcompare_1 := Pos.nlt_1_r (only parsing). Notation Plt_1 := Pos.nlt_1_r (only parsing). Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (only parsing). Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (only parsing). Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (only parsing). Notation Pplus_lt_mono_r := Pos.add_lt_mono_r (only parsing). Notation Pplus_lt_mono := Pos.add_lt_mono (only parsing). Notation Pplus_le_mono_l := Pos.add_le_mono_l (only parsing). Notation Pplus_le_mono_r := Pos.add_le_mono_r (only parsing). Notation Pplus_le_mono := Pos.add_le_mono (only parsing). Notation Pmult_compare_mono_l := Pos.mul_compare_mono_l (only parsing). Notation Pmult_compare_mono_r := Pos.mul_compare_mono_r (only parsing). Notation Pmult_lt_mono_l := Pos.mul_lt_mono_l (only parsing). Notation Pmult_lt_mono_r := Pos.mul_lt_mono_r (only parsing). Notation Pmult_lt_mono := Pos.mul_lt_mono (only parsing). Notation Pmult_le_mono_l := Pos.mul_le_mono_l (only parsing). Notation Pmult_le_mono_r := Pos.mul_le_mono_r (only parsing). Notation Pmult_le_mono := Pos.mul_le_mono (only parsing). Notation Plt_plus_r := Pos.lt_add_r (only parsing). Notation Plt_not_plus_l := Pos.lt_not_add_l (only parsing). Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (only parsing). Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (only parsing). Notation Pminus_succ_r := Pos.sub_succ_r (only parsing). Notation Pminus_mask_diag := Pos.sub_mask_diag (only parsing). Notation Pplus_minus_eq := Pos.add_sub (only parsing). Notation Pmult_minus_distr_l := Pos.mul_sub_distr_l (only parsing). Notation Pminus_lt_mono_l := Pos.sub_lt_mono_l (only parsing). Notation Pminus_compare_mono_l := Pos.sub_compare_mono_l (only parsing). Notation Pminus_compare_mono_r := Pos.sub_compare_mono_r (only parsing). Notation Pminus_lt_mono_r := Pos.sub_lt_mono_r (only parsing). Notation Pminus_decr := Pos.sub_decr (only parsing). Notation Pminus_xI_xI := Pos.sub_xI_xI (only parsing). Notation Pplus_minus_assoc := Pos.add_sub_assoc (only parsing). Notation Pminus_plus_distr := Pos.sub_add_distr (only parsing). Notation Pminus_minus_distr := Pos.sub_sub_distr (only parsing). Notation Pminus_mask_Lt := Pos.sub_mask_neg (only parsing). Notation Pminus_Lt := Pos.sub_lt (only parsing). Notation Pminus_Eq := Pos.sub_diag (only parsing). Notation Psize_monotone := Pos.size_nat_monotone (only parsing). Notation Psize_pos_gt := Pos.size_gt (only parsing). Notation Psize_pos_le := Pos.size_le (only parsing).
More complex compatibility facts, expressed as lemmas
(to preserve scopes for instance)
x, y:BinNums.positive(x =? y) = true -> x = yapply Pos.eqb_eq. Qed.x, y:BinNums.positive(x =? y) = true -> x = yp, q:BinNums.positive(p ?= q) = Gt <-> p > qreflexivity. Qed.p, q:BinNums.positive(p ?= q) = Gt <-> p > qProof (eq_sym (Pos.add_1_r p)).p:BinNums.positivePos.succ p = p + 1Proof (eq_sym (Pos.add_1_l p)).p:BinNums.positivePos.succ p = 1 + pProof (Pos.compare_cont_refl p Eq).p:BinNums.positivePos.compare_cont Eq p p = EqProof Pos.compare_eq.forall p q : BinNums.positive, Pos.compare_cont Eq p q = Eq -> p = qProof (Pos.compare_antisym q p).p, q:BinNums.positivePos.compare_cont Eq p q = CompOpp (Pos.compare_cont Eq q p)Proof (eq_sym (Pos.sub_1_r p)).p:BinNums.positivePos.pred p = p - 1p, q:BinNums.positivep > q -> exists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))p, q:BinNums.positivep > q -> exists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))p, q:BinNums.positiveH:p > qexists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))p, q:BinNums.positiveH:q < pexists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))p, q:BinNums.positiveH:q < pr:BinNums.positiveU:Pos.sub_mask p q = Pos.IsPos rexists h : BinNums.positive, Pos.sub_mask p q = Pos.IsPos h /\ q + h = p /\ (h = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred h))p, q:BinNums.positiveH:q < pr:BinNums.positiveU:Pos.sub_mask p q = Pos.IsPos rPos.sub_mask p q = Pos.IsPos r /\ q + r = p /\ (r = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred r))p, q:BinNums.positiveH:q < pr:BinNums.positiveU:Pos.sub_mask p q = Pos.IsPos rq + r = pp, q:BinNums.positiveH:q < pr:BinNums.positiveU:Pos.sub_mask p q = Pos.IsPos rr = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred r)p, q:BinNums.positiveH:q < pr:BinNums.positiveU:Pos.sub_mask p q = Pos.IsPos rr = 1 \/ Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred r)p, q:BinNums.positiveH:q < pr:BinNums.positiveU:Pos.sub_mask p q = Pos.IsPos rNE:r <> 1Pos.sub_mask_carry p q = Pos.IsPos (Pos.pred r)p, q:BinNums.positiveH:q < pr:BinNums.positiveU:Pos.sub_mask p q = Pos.IsPos rNE:r <> 1Pos.pred_mask (Pos.IsPos r) = Pos.IsPos (Pos.pred r)now elim NE. Qed.p, q:BinNums.positiveH:q < pU:Pos.sub_mask p q = Pos.IsPos 1NE:1 <> 1Pos.pred_mask (Pos.IsPos 1) = Pos.IsPos (Pos.pred 1)forall p q : BinNums.positive, p > q -> q + (p - q) = pforall p q : BinNums.positive, p > q -> q + (p - q) = pp, q:BinNums.positiveH:p > qq + (p - q) = pnow apply Pos.sub_add, Pos.gt_lt. Qed.p, q:BinNums.positiveH:p > qp - q + 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
forall r : comparison, r = Eq \/ r = Lt \/ r = Gtdestruct r; auto. Qed.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).