Require Import Basics.Overture Basics.Tactics.Require Import Basics.Overture Basics.Tactics.
Require Import Pos.Core.

Local Set Universe Minimization ToSet.

Local Open Scope positive_scope.

(** ** Specification of [succ] in term of [add] *)

Lemma pos_add_1_r p : p + 1 = pos_succ p.
p: Pos
p + 1 = pos_succ p
Proof.
p: Pos
p + 1 = pos_succ p
  by destruct p.
Qed.

Lemma pos_add_1_l p : 1 + p = pos_succ p.
p: Pos
1 + p = pos_succ p
Proof.
p: Pos
1 + p = pos_succ p
  by destruct p.
Qed.

(** ** Specification of [add_carry] *)

Theorem pos_add_carry_spec p q : pos_add_carry p q = pos_succ (p + q).
p, q: Pos
pos_add_carry p q = pos_succ (p + q)
Proof.
p, q: Pos
pos_add_carry p q = pos_succ (p + q)
  revert q.
p: Pos
forall q : Pos, pos_add_carry p q = pos_succ (p + q)
  induction p; destruct q; simpl; by apply ap.
Qed.

(** ** Commutativity of [add] *)

Theorem pos_add_comm p q : p + q = q + p.
p, q: Pos
p + q = q + p
Proof.
p, q: Pos
p + q = q + p
  revert q.
p: Pos
forall q : Pos, p + q = q + p
  induction p; destruct q; simpl; apply ap; trivial.
p: Pos
IHp: forall q0 : Pos, p + q0 = q0 + p
q: Pos
pos_add_carry p q = pos_add_carry q p
  rewrite 2 pos_add_carry_spec; by apply ap.
Qed.

(** ** Permutation of [add] and [succ] *)

Theorem pos_add_succ_r p q : p + pos_succ q = pos_succ (p + q).
p, q: Pos
p + pos_succ q = pos_succ (p + q)
Proof.
p, q: Pos
p + pos_succ q = pos_succ (p + q)
  revert q.
p: Pos
forall q : Pos, p + pos_succ q = pos_succ (p + q)
  induction p; destruct q; simpl; apply ap;
   auto using pos_add_1_r; rewrite pos_add_carry_spec; auto.
Qed.

Theorem pos_add_succ_l p q : pos_succ p + q = pos_succ (p + q).
p, q: Pos
pos_succ p + q = pos_succ (p + q)
Proof.
p, q: Pos
pos_succ p + q = pos_succ (p + q)
  rewrite pos_add_comm, (pos_add_comm p).
p, q: Pos
q + pos_succ p = pos_succ (q + p) apply pos_add_succ_r.
Qed.

Definition pos_add_succ p q : p + pos_succ q = pos_succ p + q.
p, q: Pos
p + pos_succ q = pos_succ p + q
Proof.
p, q: Pos
p + pos_succ q = pos_succ p + q
  by rewrite pos_add_succ_r, pos_add_succ_l.
Defined.

Definition pos_add_carry_spec_l q r
  : pos_add_carry q r = pos_succ q + r.
q, r: Pos
pos_add_carry q r = pos_succ q + r
Proof.
q, r: Pos
pos_add_carry q r = pos_succ q + r
  by rewrite pos_add_carry_spec, pos_add_succ_l.
Qed.

Definition pos_add_carry_spec_r q r
  : pos_add_carry q r = q + pos_succ r.
q, r: Pos
pos_add_carry q r = q + pos_succ r
Proof.
q, r: Pos
pos_add_carry q r = q + pos_succ r
  by rewrite pos_add_carry_spec, pos_add_succ_r.
Defined.

(** ** No neutral elements for addition *)
Lemma pos_add_no_neutral p q : q + p <> p.
p, q: Pos
q + p <> p
Proof.
p, q: Pos
q + p <> p
  revert q.
p: Pos
forall q : Pos, q + p <> p
  induction p as [ |p IHp|p IHp]; intros [ |q|q].
1 + 1 <> 1
q: Pos
q~0 + 1 <> 1
q: Pos
q~1 + 1 <> 1
p: Pos
IHp: forall q : Pos, q + p <> p
1 + p~0 <> p~0
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~0 <> p~0
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~1 + p~0 <> p~0
p: Pos
IHp: forall q : Pos, q + p <> p
1 + p~1 <> p~1
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~1 <> p~1
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~1 + p~1 <> p~1
  1,3: exact x0_neq_xH.
q: Pos
q~0 + 1 <> 1
p: Pos
IHp: forall q : Pos, q + p <> p
1 + p~0 <> p~0
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~0 <> p~0
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~1 + p~0 <> p~0
p: Pos
IHp: forall q : Pos, q + p <> p
1 + p~1 <> p~1
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~1 <> p~1
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~1 + p~1 <> p~1
  1: exact x1_neq_xH.
p: Pos
IHp: forall q : Pos, q + p <> p
1 + p~0 <> p~0
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~0 <> p~0
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~1 + p~0 <> p~0
p: Pos
IHp: forall q : Pos, q + p <> p
1 + p~1 <> p~1
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~1 <> p~1
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~1 + p~1 <> p~1
  1,3: exact x1_neq_x0.
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~0 <> p~0
p: Pos
IHp: forall q : Pos, q + p <> p
1 + p~1 <> p~1
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~1 <> p~1
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~1 + p~1 <> p~1
  2,4: exact x0_neq_x1.
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~0 <> p~0
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
q~0 + p~1 <> p~1
  1,2: intro H; apply (IHp q).
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
H: q~0 + p~0 = p~0
q + p = p
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
H: q~0 + p~1 = p~1
q + p = p
  1: apply x0_inj, H.
p: Pos
IHp: forall q0 : Pos, q0 + p <> p
q: Pos
H: q~0 + p~1 = p~1
q + p = p
  apply x1_inj, H.
Qed.

(** * Injectivity of [pos_succ] *)
Lemma pos_succ_inj n m : pos_succ n = pos_succ m -> n = m.
n, m: Pos
pos_succ n = pos_succ m -> n = m
Proof.
n, m: Pos
pos_succ n = pos_succ m -> n = m
  revert m.
n: Pos
forall m : Pos, pos_succ n = pos_succ m -> n = m
  induction n as [ | n x | n x]; induction m as [ | m y | m y].
pos_succ 1 = pos_succ 1 -> 1 = 1
m: Pos
y: pos_succ 1 = pos_succ m -> 1 = m
pos_succ 1 = pos_succ m~0 -> 1 = m~0
m: Pos
y: pos_succ 1 = pos_succ m -> 1 = m
pos_succ 1 = pos_succ m~1 -> 1 = m~1
n: Pos
x: forall m : Pos, pos_succ n = pos_succ m -> n = m
pos_succ n~0 = pos_succ 1 -> n~0 = 1
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~0 = pos_succ m -> n~0 = m
pos_succ n~0 = pos_succ m~0 -> n~0 = m~0
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~0 = pos_succ m -> n~0 = m
pos_succ n~0 = pos_succ m~1 -> n~0 = m~1
n: Pos
x: forall m : Pos, pos_succ n = pos_succ m -> n = m
pos_succ n~1 = pos_succ 1 -> n~1 = 1
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~1 = pos_succ m -> n~1 = m
pos_succ n~1 = pos_succ m~0 -> n~1 = m~0
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~1 = pos_succ m -> n~1 = m
pos_succ n~1 = pos_succ m~1 -> n~1 = m~1
  +
pos_succ 1 = pos_succ 1 -> 1 = 1 reflexivity.
  +
m: Pos
y: pos_succ 1 = pos_succ m -> 1 = m
pos_succ 1 = pos_succ m~0 -> 1 = m~0 intro p.
m: Pos
y: pos_succ 1 = pos_succ m -> 1 = m
p: pos_succ 1 = pos_succ m~0
1 = m~0
    destruct (x0_neq_x1 p).
  +
m: Pos
y: pos_succ 1 = pos_succ m -> 1 = m
pos_succ 1 = pos_succ m~1 -> 1 = m~1 intro p.
m: Pos
y: pos_succ 1 = pos_succ m -> 1 = m
p: pos_succ 1 = pos_succ m~1
1 = m~1
    simpl in p.
m: Pos
y: pos_succ 1 = pos_succ m -> 1 = m
p: 2 = (pos_succ m)~0
1 = m~1
    apply x0_inj in p.
m: Pos
y: pos_succ 1 = pos_succ m -> 1 = m
p: 1 = pos_succ m
1 = m~1
    destruct m.
y: pos_succ 1 = pos_succ 1 -> 1 = 1
p: 1 = pos_succ 1
1 = 3
m: Pos
y: pos_succ 1 = pos_succ m~0 -> 1 = m~0
p: 1 = pos_succ m~0
1 = m~0~1
m: Pos
y: pos_succ 1 = pos_succ m~1 -> 1 = m~1
p: 1 = pos_succ m~1
1 = m~1~1
    1,3: destruct (xH_neq_x0 p).
m: Pos
y: pos_succ 1 = pos_succ m~0 -> 1 = m~0
p: 1 = pos_succ m~0
1 = m~0~1
    destruct (xH_neq_x1 p).
  +
n: Pos
x: forall m : Pos, pos_succ n = pos_succ m -> n = m
pos_succ n~0 = pos_succ 1 -> n~0 = 1 intro p.
n: Pos
x: forall m : Pos, pos_succ n = pos_succ m -> n = m
p: pos_succ n~0 = pos_succ 1
n~0 = 1
    destruct (x1_neq_x0 p).
  +
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~0 = pos_succ m -> n~0 = m
pos_succ n~0 = pos_succ m~0 -> n~0 = m~0 simpl.
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~0 = pos_succ m -> n~0 = m
n~1 = m~1 -> n~0 = m~0
    intro p.
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~0 = pos_succ m -> n~0 = m
p: n~1 = m~1
n~0 = m~0
    by apply ap, x1_inj.
  +
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~0 = pos_succ m -> n~0 = m
pos_succ n~0 = pos_succ m~1 -> n~0 = m~1 intro p.
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~0 = pos_succ m -> n~0 = m
p: pos_succ n~0 = pos_succ m~1
n~0 = m~1
    destruct (x1_neq_x0 p).
  +
n: Pos
x: forall m : Pos, pos_succ n = pos_succ m -> n = m
pos_succ n~1 = pos_succ 1 -> n~1 = 1 intro p.
n: Pos
x: forall m : Pos, pos_succ n = pos_succ m -> n = m
p: pos_succ n~1 = pos_succ 1
n~1 = 1
    cbn in p.
n: Pos
x: forall m : Pos, pos_succ n = pos_succ m -> n = m
p: (pos_succ n)~0 = 2
n~1 = 1
    apply x0_inj in p.
n: Pos
x: forall m : Pos, pos_succ n = pos_succ m -> n = m
p: pos_succ n = 1
n~1 = 1
    destruct n.
x: forall m : Pos, pos_succ 1 = pos_succ m -> 1 = m
p: pos_succ 1 = 1
3 = 1
n: Pos
x: forall m : Pos, pos_succ n~0 = pos_succ m -> n~0 = m
p: pos_succ n~0 = 1
n~0~1 = 1
n: Pos
x: forall m : Pos, pos_succ n~1 = pos_succ m -> n~1 = m
p: pos_succ n~1 = 1
n~1~1 = 1
    1,3: destruct (x0_neq_xH p).
n: Pos
x: forall m : Pos, pos_succ n~0 = pos_succ m -> n~0 = m
p: pos_succ n~0 = 1
n~0~1 = 1
    destruct (x1_neq_xH p).
  +
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~1 = pos_succ m -> n~1 = m
pos_succ n~1 = pos_succ m~0 -> n~1 = m~0 intro p.
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~1 = pos_succ m -> n~1 = m
p: pos_succ n~1 = pos_succ m~0
n~1 = m~0
    cbn in p.
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~1 = pos_succ m -> n~1 = m
p: (pos_succ n)~0 = m~1
n~1 = m~0
    destruct (x0_neq_x1 p).
  +
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~1 = pos_succ m -> n~1 = m
pos_succ n~1 = pos_succ m~1 -> n~1 = m~1 intro p.
n: Pos
x: forall m0 : Pos, pos_succ n = pos_succ m0 -> n = m0
m: Pos
y: pos_succ n~1 = pos_succ m -> n~1 = m
p: pos_succ n~1 = pos_succ m~1
n~1 = m~1
    apply ap, x, x0_inj, p.
Defined.

(** ** Addition is associative *)

Theorem pos_add_assoc p q r : p + (q + r) = p + q + r.
p, q, r: Pos
p + (q + r) = p + q + r
Proof.
p, q, r: Pos
p + (q + r) = p + q + r
  revert q r.
p: Pos
forall q r : Pos, p + (q + r) = p + q + r
  induction p.
forall q r : Pos, 1 + (q + r) = 1 + q + r
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
forall q r : Pos, p~0 + (q + r) = p~0 + q + r
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
forall q r : Pos, p~1 + (q + r) = p~1 + q + r
  +
forall q r : Pos, 1 + (q + r) = 1 + q + r intros [|q|q] [|r|r].
1 + (1 + 1) = 1 + 1 + 1
r: Pos
1 + (1 + r~0) = 1 + 1 + r~0
r: Pos
1 + (1 + r~1) = 1 + 1 + r~1
q: Pos
1 + (q~0 + 1) = 1 + q~0 + 1
q, r: Pos
1 + (q~0 + r~0) = 1 + q~0 + r~0
q, r: Pos
1 + (q~0 + r~1) = 1 + q~0 + r~1
q: Pos
1 + (q~1 + 1) = 1 + q~1 + 1
q, r: Pos
1 + (q~1 + r~0) = 1 + q~1 + r~0
q, r: Pos
1 + (q~1 + r~1) = 1 + q~1 + r~1
    all: try reflexivity.
r: Pos
1 + (1 + r~0) = 1 + 1 + r~0
r: Pos
1 + (1 + r~1) = 1 + 1 + r~1
q, r: Pos
1 + (q~0 + r~1) = 1 + q~0 + r~1
q, r: Pos
1 + (q~1 + r~0) = 1 + q~1 + r~0
q, r: Pos
1 + (q~1 + r~1) = 1 + q~1 + r~1
    all: simpl.
r: Pos
(pos_succ r)~0 =
match r with
| 1 => 2
| q~0 => q~1
| q~1 => (pos_succ q)~0
end~0
r: Pos
(pos_succ r)~1 =
match r with
| 1 => 2
| q~0 => q~1
| q~1 => (pos_succ q)~0
end~1
q, r: Pos
(pos_succ (q + r))~0 = (pos_add_carry q r)~0
q, r: Pos
(pos_succ (q + r))~0 = (pos_succ q + r)~0
q, r: Pos
(pos_add_carry q r)~1 = (pos_succ q + r)~1
    1,2: by destruct r.
q, r: Pos
(pos_succ (q + r))~0 = (pos_add_carry q r)~0
q, r: Pos
(pos_succ (q + r))~0 = (pos_succ q + r)~0
q, r: Pos
(pos_add_carry q r)~1 = (pos_succ q + r)~1
    1,2: apply ap; symmetry.
q, r: Pos
pos_add_carry q r = pos_succ (q + r)
q, r: Pos
pos_succ q + r = pos_succ (q + r)
q, r: Pos
(pos_add_carry q r)~1 = (pos_succ q + r)~1
    1: apply pos_add_carry_spec.
q, r: Pos
pos_succ q + r = pos_succ (q + r)
q, r: Pos
(pos_add_carry q r)~1 = (pos_succ q + r)~1
    1: apply pos_add_succ_l.
q, r: Pos
(pos_add_carry q r)~1 = (pos_succ q + r)~1
    apply ap.
q, r: Pos
pos_add_carry q r = pos_succ q + r
    rewrite pos_add_succ_l.
q, r: Pos
pos_add_carry q r = pos_succ (q + r)
    apply pos_add_carry_spec.
  +
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
forall q r : Pos, p~0 + (q + r) = p~0 + q + r intros [|q|q] [|r|r].
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
p~0 + (1 + 1) = p~0 + 1 + 1
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p~0 + (1 + r~0) = p~0 + 1 + r~0
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p~0 + (1 + r~1) = p~0 + 1 + r~1
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p~0 + (q~0 + 1) = p~0 + q~0 + 1
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~0 + (q~0 + r~0) = p~0 + q~0 + r~0
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~0 + (q~0 + r~1) = p~0 + q~0 + r~1
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p~0 + (q~1 + 1) = p~0 + q~1 + 1
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~0 + (q~1 + r~0) = p~0 + q~1 + r~0
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~0 + (q~1 + r~1) = p~0 + q~1 + r~1
    all: try reflexivity.
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
p~0 + (1 + 1) = p~0 + 1 + 1
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p~0 + (1 + r~1) = p~0 + 1 + r~1
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~0 + (q~0 + r~0) = p~0 + q~0 + r~0
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~0 + (q~0 + r~1) = p~0 + q~0 + r~1
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p~0 + (q~1 + 1) = p~0 + q~1 + 1
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~0 + (q~1 + r~0) = p~0 + q~1 + r~0
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~0 + (q~1 + r~1) = p~0 + q~1 + r~1
    all: cbn; apply ap.
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
p + 1 = pos_succ p
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p + pos_succ r = pos_add_carry p r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (q + r) = p + q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (q + r) = p + q + r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_succ (p + q)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (q + r) = p + q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry (p + q) r
    3,4,6: apply IHp.
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
p + 1 = pos_succ p
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p + pos_succ r = pos_add_carry p r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_succ (p + q)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry (p + q) r
    1: apply pos_add_1_r.
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p + pos_succ r = pos_add_carry p r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_succ (p + q)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry (p + q) r
    1: symmetry; apply pos_add_carry_spec_r.
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_succ (p + q)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry (p + q) r
    1: apply pos_add_succ_r.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry (p + q) r
    rewrite 2 pos_add_carry_spec_l.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (pos_succ q + r) = pos_succ (p + q) + r
    rewrite <- pos_add_succ_r.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (pos_succ q + r) = p + pos_succ q + r
    apply IHp.
  +
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
forall q r : Pos, p~1 + (q + r) = p~1 + q + r intros [|q|q] [|r|r].
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
p~1 + (1 + 1) = p~1 + 1 + 1
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p~1 + (1 + r~0) = p~1 + 1 + r~0
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p~1 + (1 + r~1) = p~1 + 1 + r~1
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p~1 + (q~0 + 1) = p~1 + q~0 + 1
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~1 + (q~0 + r~0) = p~1 + q~0 + r~0
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~1 + (q~0 + r~1) = p~1 + q~0 + r~1
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p~1 + (q~1 + 1) = p~1 + q~1 + 1
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~1 + (q~1 + r~0) = p~1 + q~1 + r~0
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p~1 + (q~1 + r~1) = p~1 + q~1 + r~1
    all: cbn; apply ap.
p: Pos
IHp: forall q r : Pos, p + (q + r) = p + q + r
p + 1 = pos_succ p
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
pos_add_carry p r = pos_succ p + r
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p + pos_succ r = pos_succ p + r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
pos_add_carry p q = pos_succ (p + q)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (q + r) = p + q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry (p + q) r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_add_carry p q
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry p q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry p q + r
    1: apply pos_add_1_r.
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
pos_add_carry p r = pos_succ p + r
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p + pos_succ r = pos_succ p + r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
pos_add_carry p q = pos_succ (p + q)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (q + r) = p + q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry (p + q) r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_add_carry p q
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry p q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry p q + r
    1: apply pos_add_carry_spec_l.
p: Pos
IHp: forall q r0 : Pos, p + (q + r0) = p + q + r0
r: Pos
p + pos_succ r = pos_succ p + r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
pos_add_carry p q = pos_succ (p + q)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (q + r) = p + q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry (p + q) r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_add_carry p q
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry p q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry p q + r
    1: apply pos_add_succ.
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
pos_add_carry p q = pos_succ (p + q)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (q + r) = p + q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry (p + q) r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_add_carry p q
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry p q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry p q + r
    1: apply pos_add_carry_spec.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (q + r) = p + q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry (p + q) r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_add_carry p q
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry p q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry p q + r
    1: apply IHp.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry (p + q) r
p: Pos
IHp: forall q0 r : Pos, p + (q0 + r) = p + q0 + r
q: Pos
p + pos_succ q = pos_add_carry p q
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry p q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry p q + r
    2: symmetry; apply pos_add_carry_spec_r.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry (p + q) r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_add_carry p (q + r) = pos_add_carry p q + r
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry p q + r
    1,2: rewrite 2 pos_add_carry_spec, ?pos_add_succ_l.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_succ (p + (q + r)) = pos_succ (p + q + r)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
pos_succ (p + (q + r)) = pos_succ (p + q + r)
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry p q + r
    1,2: apply ap, IHp.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + pos_add_carry q r = pos_add_carry p q + r
    rewrite ?pos_add_carry_spec_r.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (q + pos_succ r) = p + pos_succ q + r
    rewrite pos_add_succ.
p: Pos
IHp: forall q0 r0 : Pos, p + (q0 + r0) = p + q0 + r0
q, r: Pos
p + (pos_succ q + r) = p + pos_succ q + r
    apply IHp.
Qed.

(** ** One is neutral for multiplication *)

Lemma pos_mul_1_l p : 1 * p = p.
p: Pos
1 * p = p
Proof.
p: Pos
1 * p = p
  reflexivity.
Qed.

Lemma pos_mul_1_r p : p * 1 = p.
p: Pos
p * 1 = p
Proof.
p: Pos
p * 1 = p
  induction p; cbn; trivial; by apply ap.
Qed.

(** [pos_succ] and doubling functions *)

Lemma pos_pred_double_succ n
  : pos_pred_double (pos_succ n) = n~1.
n: Pos
pos_pred_double (pos_succ n) = n~1
Proof.
n: Pos
pos_pred_double (pos_succ n) = n~1
  induction n as [|n|n nH].
pos_pred_double (pos_succ 1) = 3
n: Pos
IHn: pos_pred_double (pos_succ n) = n~1
pos_pred_double (pos_succ n~0) = n~0~1
n: Pos
nH: pos_pred_double (pos_succ n) = n~1
pos_pred_double (pos_succ n~1) = n~1~1
  all: trivial.
n: Pos
nH: pos_pred_double (pos_succ n) = n~1
pos_pred_double (pos_succ n~1) = n~1~1
  cbn; apply ap, nH.
Qed.

Lemma pos_succ_pred_double n
  : pos_succ (pos_pred_double n) = n~0.
n: Pos
pos_succ (pos_pred_double n) = n~0
Proof.
n: Pos
pos_succ (pos_pred_double n) = n~0
  induction n as [|n nH|n].
pos_succ (pos_pred_double 1) = 2
n: Pos
nH: pos_succ (pos_pred_double n) = n~0
pos_succ (pos_pred_double n~0) = n~0~0
n: Pos
IHn: pos_succ (pos_pred_double n) = n~0
pos_succ (pos_pred_double n~1) = n~1~0
  all: trivial.
n: Pos
nH: pos_succ (pos_pred_double n) = n~0
pos_succ (pos_pred_double n~0) = n~0~0
  cbn; apply ap, nH.
Qed.

(** ** Iteration and [pos_succ] *)
Lemma pos_iter_succ_l {A} (f : A -> A) p a
  : pos_iter f (pos_succ p) a = f (pos_iter f p a).
A: Type
f: A -> A
p: Pos
a: A
pos_iter f (pos_succ p) a = f (pos_iter f p a)
Proof.
A: Type
f: A -> A
p: Pos
a: A
pos_iter f (pos_succ p) a = f (pos_iter f p a)
  unfold pos_iter.
A: Type
f: A -> A
p: Pos
a: A
pos_peano_rec (A -> A) f (fun (_ : Pos) (g : A -> A) (x : A) => f (g x))
  (pos_succ p) a =
f
  (pos_peano_rec (A -> A) f (fun (_ : Pos) (g : A -> A) (x : A) => f (g x)) p
     a)
  by rewrite pos_peano_rec_beta_pos_succ.
Qed.

Lemma pos_iter_succ_r {A} (f : A -> A) p a
  : pos_iter f (pos_succ p) a = pos_iter f p (f a).
A: Type
f: A -> A
p: Pos
a: A
pos_iter f (pos_succ p) a = pos_iter f p (f a)
Proof.
A: Type
f: A -> A
p: Pos
a: A
pos_iter f (pos_succ p) a = pos_iter f p (f a)
  revert p f a.
A: Type
forall (p : Pos) (f : A -> A) (a : A),
pos_iter f (pos_succ p) a = pos_iter f p (f a)
  srapply pos_peano_ind.
A: Type
(fun p : Pos =>
 forall (f : A -> A) (a : A), pos_iter f (pos_succ p) a = pos_iter f p (f a))
  1
A: Type
forall p : Pos,
(fun p0 : Pos =>
 forall (f : A -> A) (a : A),
 pos_iter f (pos_succ p0) a = pos_iter f p0 (f a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (a : A),
 pos_iter f (pos_succ p0) a = pos_iter f p0 (f a)) 
  (pos_succ p)
  1: hnf; intros; trivial.
A: Type
forall p : Pos,
(fun p0 : Pos =>
 forall (f : A -> A) (a : A),
 pos_iter f (pos_succ p0) a = pos_iter f p0 (f a)) p ->
(fun p0 : Pos =>
 forall (f : A -> A) (a : A),
 pos_iter f (pos_succ p0) a = pos_iter f p0 (f a)) 
  (pos_succ p)
  hnf; intros p q f a.
A: Type
p: Pos
q: forall (f0 : A -> A) (a0 : A),
pos_iter f0 (pos_succ p) a0 = pos_iter f0 p (f0 a0)
f: A -> A
a: A
pos_iter f (pos_succ (pos_succ p)) a = pos_iter f (pos_succ p) (f a)
  refine (_ @ _ @ _^).
A: Type
p: Pos
q: forall (f0 : A -> A) (a0 : A),
pos_iter f0 (pos_succ p) a0 = pos_iter f0 p (f0 a0)
f: A -> A
a: A
pos_iter f (pos_succ (pos_succ p)) a = ?Goal0
A: Type
p: Pos
q: forall (f0 : A -> A) (a0 : A),
pos_iter f0 (pos_succ p) a0 = pos_iter f0 p (f0 a0)
f: A -> A
a: A
?Goal0 = ?Goal
A: Type
p: Pos
q: forall (f0 : A -> A) (a0 : A),
pos_iter f0 (pos_succ p) a0 = pos_iter f0 p (f0 a0)
f: A -> A
a: A
pos_iter f (pos_succ p) (f a) = ?Goal
  1,3: unfold pos_iter;
    by rewrite pos_peano_rec_beta_pos_succ.
A: Type
p: Pos
q: forall (f0 : A -> A) (a0 : A),
pos_iter f0 (pos_succ p) a0 = pos_iter f0 p (f0 a0)
f: A -> A
a: A
f
  (pos_peano_rec (A -> A) f (fun (_ : Pos) (g : A -> A) (x : A) => f (g x))
     (pos_succ p) a) =
f
  (pos_peano_rec (A -> A) f (fun (_ : Pos) (g : A -> A) (x : A) => f (g x)) p
     (f a))
  apply ap.
A: Type
p: Pos
q: forall (f0 : A -> A) (a0 : A),
pos_iter f0 (pos_succ p) a0 = pos_iter f0 p (f0 a0)
f: A -> A
a: A
pos_peano_rec (A -> A) f (fun (_ : Pos) (g : A -> A) (x : A) => f (g x))
  (pos_succ p) a =
pos_peano_rec (A -> A) f (fun (_ : Pos) (g : A -> A) (x : A) => f (g x)) p
  (f a)
  apply q.
Qed.

(** ** Right reduction properties for multiplication *)
Lemma mul_xO_r p q : p * q~0 = (p * q)~0.
p, q: Pos
p * q~0 = (p * q)~0
Proof.
p, q: Pos
p * q~0 = (p * q)~0
  induction p; simpl; f_ap; f_ap; trivial.
Qed.

Lemma mul_xI_r p q : p * q~1 = p + (p * q)~0.
p, q: Pos
p * q~1 = p + (p * q)~0
Proof.
p, q: Pos
p * q~1 = p + (p * q)~0
  induction p; simpl; trivial; f_ap.
p, q: Pos
IHp: p * q~1 = p + (p * q)~0
q + p * q~1 = p + (q + (p * q)~0)
  rewrite IHp.
p, q: Pos
IHp: p * q~1 = p + (p * q)~0
q + (p + (p * q)~0) = p + (q + (p * q)~0)
  rewrite pos_add_assoc.
p, q: Pos
IHp: p * q~1 = p + (p * q)~0
q + p + (p * q)~0 = p + (q + (p * q)~0)
  rewrite (pos_add_comm q p).
p, q: Pos
IHp: p * q~1 = p + (p * q)~0
p + q + (p * q)~0 = p + (q + (p * q)~0)
  symmetry.
p, q: Pos
IHp: p * q~1 = p + (p * q)~0
p + (q + (p * q)~0) = p + q + (p * q)~0
  apply pos_add_assoc.
Qed.

(** ** Commutativity of multiplication *)
Lemma pos_mul_comm p q : p * q = q * p.
p, q: Pos
p * q = q * p
Proof.
p, q: Pos
p * q = q * p
  induction q; simpl.
p: Pos
p * 1 = p
p, q: Pos
IHq: p * q = q * p
p * q~0 = (q * p)~0
p, q: Pos
IHq: p * q = q * p
p * q~1 = p + (q * p)~0
  1: apply pos_mul_1_r.
p, q: Pos
IHq: p * q = q * p
p * q~0 = (q * p)~0
p, q: Pos
IHq: p * q = q * p
p * q~1 = p + (q * p)~0
  +
p, q: Pos
IHq: p * q = q * p
p * q~0 = (q * p)~0 rewrite mul_xO_r.
p, q: Pos
IHq: p * q = q * p
(p * q)~0 = (q * p)~0
    f_ap.
  +
p, q: Pos
IHq: p * q = q * p
p * q~1 = p + (q * p)~0 rewrite mul_xI_r.
p, q: Pos
IHq: p * q = q * p
p + (p * q)~0 = p + (q * p)~0
    f_ap; f_ap.
Qed.

(** ** Distributivity of addition over multiplication *)
Theorem pos_mul_add_distr_l p q r :
  p * (q + r) = p * q + p * r.
p, q, r: Pos
p * (q + r) = p * q + p * r
Proof.
p, q, r: Pos
p * (q + r) = p * q + p * r
  induction p; cbn; [reflexivity | f_ap | ].
p, q, r: Pos
IHp: p * (q + r) = p * q + p * r
q + r + (p * (q + r))~0 = q + (p * q)~0 + (r + (p * r)~0)
  rewrite IHp.
p, q, r: Pos
IHp: p * (q + r) = p * q + p * r
q + r + (p * q + p * r)~0 = q + (p * q)~0 + (r + (p * r)~0)
  set (m:=(p*q)~0).
p, q, r: Pos
IHp: p * (q + r) = p * q + p * r
m:= (p * q)~0: Pos
q + r + (p * q + p * r)~0 = q + m + (r + (p * r)~0)
  set (n:=(p*r)~0).
p, q, r: Pos
IHp: p * (q + r) = p * q + p * r
m:= (p * q)~0: Pos
n:= (p * r)~0: Pos
q + r + (p * q + p * r)~0 = q + m + (r + n)
  change ((p*q+p*r)~0) with (m+n).
p, q, r: Pos
IHp: p * (q + r) = p * q + p * r
m:= (p * q)~0: Pos
n:= (p * r)~0: Pos
q + r + (m + n) = q + m + (r + n)
  rewrite 2 pos_add_assoc; f_ap.
p, q, r: Pos
IHp: p * (q + r) = p * q + p * r
m:= (p * q)~0: Pos
n:= (p * r)~0: Pos
q + r + m = q + m + r
  rewrite <- 2 pos_add_assoc; f_ap.
p, q, r: Pos
IHp: p * (q + r) = p * q + p * r
m:= (p * q)~0: Pos
n:= (p * r)~0: Pos
r + m = m + r
  apply pos_add_comm.
Qed.

Theorem pos_mul_add_distr_r p q r :
  (p + q) * r = p * r + q * r.
p, q, r: Pos
(p + q) * r = p * r + q * r
Proof.
p, q, r: Pos
(p + q) * r = p * r + q * r
  rewrite 3 (pos_mul_comm _ r); apply pos_mul_add_distr_l.
Qed.

(** ** Associativity of multiplication *)
Theorem pos_mul_assoc p q r : p * (q * r) = p * q * r.
p, q, r: Pos
p * (q * r) = p * q * r
Proof.
p, q, r: Pos
p * (q * r) = p * q * r
  induction p; simpl; rewrite ?IHp; trivial.
p, q, r: Pos
IHp: p * (q * r) = p * q * r
q * r + (p * q * r)~0 = (q + (p * q)~0) * r
  by rewrite pos_mul_add_distr_r.
Qed.

(** ** [pos_succ] and [pos_mul] *)

Lemma pos_mul_succ_l p q
  : (pos_succ p) * q = p * q + q.
p, q: Pos
pos_succ p * q = p * q + q
Proof.
p, q: Pos
pos_succ p * q = p * q + q
  by rewrite <- pos_add_1_r, pos_mul_add_distr_r, pos_mul_1_l.
Qed.

Lemma pos_mul_succ_r p q
  : p * (pos_succ q) = p + p * q.
p, q: Pos
p * pos_succ q = p + p * q
Proof.
p, q: Pos
p * pos_succ q = p + p * q
  by rewrite <- pos_add_1_l, pos_mul_add_distr_l, pos_mul_1_r.
Qed.