Library HoTT.Spaces.BinInt.Spec

Require Import Basics.
Require Import Spaces.Pos.
Require Import Spaces.BinInt.Core.

Local Set Universe Minimization ToSet.

Local Open Scope binint_scope.

Addition is commutative


Lemma binint_add_comm n m : n + m = m + n.
Proof.
  destruct n, m; trivial. all: cbn.
  all: apply ap, pos_add_comm.
Defined.

Zero is the additive identity.


Definition binint_add_0_l n : 0 + n = n
  := 1.

Lemma binint_add_0_r n : n + 0 = n.
Proof.
  by destruct n.
Defined.

Multiplication by zero is zero


Definition binint_mul_0_l n : 0 × n = 0
  := 1.

Lemma binint_mul_0_r n : n × 0 = 0.
Proof.
  by destruct n.
Defined.

One is the multiplicative identity


Lemma binint_mul_1_l n : 1 × n = n.
Proof.
  by destruct n.
Defined.

Lemma binint_mul_1_r n : n × 1 = n.
Proof.
  destruct n; trivial; cbn; apply ap, pos_mul_1_r.
Defined.

Inverse laws


Lemma binint_pos_sub_diag n : binint_pos_sub n n = 0.
Proof.
  induction n; trivial; cbn.
  all: exact (ap binint_double IHn).
Defined.

Lemma binint_add_negation_l n : (-n) + n = 0.
Proof.
  destruct n; trivial; cbn; apply binint_pos_sub_diag.
Defined.

Lemma binint_add_negation_r n : n + (-n) = 0.
Proof.
  destruct n; trivial; cbn; apply binint_pos_sub_diag.
Defined.

Permutation of neg and pos_succ

Lemma binint_neg_pos_succ p : neg (pos_succ p) = binint_pred (neg p).
Proof.
  by destruct p.
Defined.

Permutation of pos and pos_succ

Lemma binint_pos_pos_succ p : pos (pos_succ p) = binint_succ (pos p).
Proof.
  by destruct p.
Defined.

Negation of a doubled positive integer

Lemma binint_negation_double a : - (binint_double a) = binint_double (- a).
Proof.
  by destruct a.
Defined.

Negation of the predecessor of a doubled positive integer.
Lemma binint_negation_pred_double a
  : - (binint_pred_double a) = binint_succ_double (- a).
Proof.
  by destruct a.
Defined.

Negation of the doubling of the sucessor of an positive.
Lemma binint_negation_succ_double a
  : - (binint_succ_double a) = binint_pred_double (- a).
Proof.
  by destruct a.
Defined.

Negation of subtraction of positive integers
Lemma binint_pos_sub_negation a b
  : - (binint_pos_sub a b) = binint_pos_sub b a.
Proof.
  revert a b.
  induction a as [|a ah|a ah];
  destruct b;
  cbn; trivial.
  all: rewrite ?binint_negation_double,
    ?binint_negation_succ_double,
    ?binint_negation_pred_double.
  all: apply ap, ah.
Defined.

binint_succ is a retract of binint_pred

Definition binint_succ_pred : binint_succ o binint_pred == idmap.
Proof.
  intros [n | | n]; [|trivial|].
  all: destruct n; trivial.
  1,2: cbn; apply ap.
  1: apply pos_pred_double_succ.
  rewrite pos_add_1_r.
  apply pos_succ_pred_double.
Defined.

binint_pred is a retract of binint_succ

Definition binint_pred_succ : binint_pred o binint_succ == idmap.
Proof.
  intros [n | | n]; [|trivial|].
  all: destruct n; trivial.
  1,2: cbn; apply ap.
  1: rewrite pos_add_1_r.
  1: apply pos_succ_pred_double.
  apply pos_pred_double_succ.
Defined.

(* ** The successor autoequivalence. *)
Global Instance isequiv_binint_succ : IsEquiv binint_succ | 0
  := isequiv_adjointify binint_succ _ binint_succ_pred binint_pred_succ.

Definition equiv_binint_succ : BinInt <~> BinInt
  := Build_Equiv _ _ _ isequiv_binint_succ.

Negation distributes over addition

Lemma binint_negation_add_distr n m : - (n + m) = - n + - m.
Proof.
 destruct n, m; simpl; trivial using binint_pos_sub_negation.
Defined.

Negation is injective

Lemma binint_negation_inj n m : -n = -m → n = m.
Proof.
  destruct n, m; simpl; intro H.
  1: apply pos_inj in H.
  2: apply pos_neq_zero in H.
  3: apply pos_neq_neg in H.
  4: apply zero_neq_pos in H.
  6: apply zero_neq_neg in H.
  7: apply neg_neq_pos in H.
  8: apply neg_neq_zero in H.
  9: apply neg_inj in H.
  all: by destruct H.
Defined.

Subtracting 1 from a sucessor gives the positive integer.

Lemma binint_pos_sub_succ_l a
  : binint_pos_sub (pos_succ a) 1%pos = pos a.
Proof.
  destruct a; trivial.
  cbn; apply ap, pos_pred_double_succ.
Defined.

Subtracting a sucessor from 1 gives minus the integer.

Lemma binint_pos_sub_succ_r a
  : binint_pos_sub 1%pos (pos_succ a) = neg a.
Proof.
  destruct a; trivial.
  cbn; apply ap, pos_pred_double_succ.
Defined.

Interaction of doubling functions and subtraction


Lemma binint_succ_double_binint_pos_sub a b
  : binint_succ_double (binint_pos_sub a (pos_succ b))
    = binint_pred_double (binint_pos_sub a b).
Proof.
  revert a b.
  induction a; induction b; trivial.
  + cbn; apply ap.
    by rewrite pos_pred_double_succ.
  + destruct a; trivial.
  + cbn; destruct (binint_pos_sub a b); trivial.
  + cbn.
    rewrite <- IHa.
    destruct (binint_pos_sub a (pos_succ b)); trivial.
  + destruct a; trivial.
  + cbn; destruct (binint_pos_sub a b); trivial.
  + cbn.
    rewrite IHa.
    cbn; destruct (binint_pos_sub a b); trivial.
Defined.

Lemma binint_pred_double_binint_pos_sub a b
  : binint_pred_double (binint_pos_sub (pos_succ a) b)
    = binint_succ_double (binint_pos_sub a b).
Proof.
  revert a b.
  induction a; induction b; trivial.
  + by destruct b.
  + by destruct b.
  + cbn; by destruct (binint_pos_sub a b).
  + cbn; by destruct (binint_pos_sub a b).
  + cbn; apply ap.
    by rewrite pos_pred_double_succ.
  + cbn.
    rewrite <- IHa.
    by destruct (binint_pos_sub (pos_succ a) b).
  + cbn.
    rewrite IHa.
    by destruct (binint_pos_sub a b).
Defined.

Subtractions cancel sucessors.

Lemma binint_pos_sub_succ_succ a b
  : binint_pos_sub (pos_succ a) (pos_succ b) = binint_pos_sub a b.
Proof.
  rewrite <- 2 pos_add_1_r.
  revert a b.
  induction a; induction b; trivial.
  1: destruct b; trivial.
  { destruct b; trivial.
    cbn; apply ap.
    by rewrite pos_pred_double_succ. }
  1: destruct a; trivial.
  1: apply binint_succ_double_binint_pos_sub.
  { destruct a; trivial.
    cbn; apply ap, ap, pos_pred_double_succ. }
  1: apply binint_pred_double_binint_pos_sub.
  cbn; apply ap.
  rewrite <- 2 pos_add_1_r.
  apply IHa.
Defined.

Predecessor of a subtraction is the subtraction of a sucessor.

Lemma binint_pred_pos_sub_r a b
  : binint_pred (binint_pos_sub a b) = binint_pos_sub a (pos_succ b).
Proof.
  revert a.
  induction b as [|b bH] using pos_peano_ind.
  1: destruct a; trivial; destruct a; trivial.
  intro a.
  revert b bH.
  induction a as [|a aH] using pos_peano_ind.
  { intros b bH.
    rewrite <- bH.
    destruct b; trivial.
    cbn; apply ap.
    rewrite 2 pos_add_1_r.
    rewrite pos_succ_pred_double.
    rewrite pos_pred_double_succ.
    trivial. }
  intros b bH.
  rewrite 2 binint_pos_sub_succ_succ.
  apply bH.
Defined.

Negation of the predecessor is an involution.

Lemma binint_negation_pred_negation_red x
  : - binint_pred (- binint_pred x) = x.
Proof.
  destruct x as [x| |x]; trivial;
  destruct x; trivial; cbn; apply ap.
  1: apply pos_pred_double_succ.
  rewrite pos_add_1_r.
  apply pos_succ_pred_double.
Defined.

Predecessor of a sum is the sum with a predecessor

Lemma binint_pred_add_r a b
  : binint_pred (a + b) = a + binint_pred b.
Proof.
  revert a b.
  intros [a| |a] [b| |b]; trivial.
  + cbn; apply ap.
    by rewrite pos_add_assoc.
  + revert a.
    induction b as [|b bH] using pos_peano_ind.
    - intro a; exact (binint_pred_succ (neg a)).
    - intro a.
      rewrite <- pos_add_1_r.
      rewrite (binint_pred_succ (pos b)).
      rewrite binint_add_comm.
      cbn.
      rewrite pos_add_1_r.
      rewrite <- binint_pos_sub_negation.
      rewrite <- binint_pred_pos_sub_r.
      apply binint_negation_inj.
      rewrite binint_pos_sub_negation.
      apply binint_negation_pred_negation_red.
  + cbn.
    rewrite pos_add_1_r.
    apply binint_pred_pos_sub_r.
  + revert a.
    induction b as [|b bH] using pos_peano_ind.
    - intro a; exact (binint_pred_succ (pos a)).
    - intro a.
      rewrite <- pos_add_1_r.
      rewrite (binint_pred_succ (pos b)).
      cbn; rewrite pos_add_assoc.
      change (binint_pred (binint_succ (pos (a + b)%pos)) = pos a + pos b).
      apply binint_pred_succ.
Defined.

Subtraction from a sum is the sum of a subtraction

Lemma binint_pos_sub_add (a b c : Pos)
  : binint_pos_sub (a + b)%pos c = pos a + binint_pos_sub b c.
Proof.
  revert c b a.
  induction c as [|c ch] using pos_peano_ind.
  { intros b a.
    change (binint_pred (pos a + pos b) = pos a + (binint_pred (pos b))).
    apply binint_pred_add_r. }
  intros b a.
  rewrite <- binint_pred_pos_sub_r.
  rewrite ch.
  rewrite <- binint_pred_pos_sub_r.
  apply binint_pred_add_r.
Defined.

An auxillary lemma used to prove associativity.
Lemma binint_add_assoc_pos p n m : pos p + (n + m) = pos p + n + m.
Proof.
  destruct n as [n| |n], m as [m| |m]; trivial.
  - cbn; apply binint_negation_inj.
    rewrite !binint_negation_add_distr, !binint_pos_sub_negation.
    rewrite binint_add_comm, pos_add_comm.
    apply binint_pos_sub_add.
  - symmetry.
    apply binint_add_0_r.
  - by rewrite <- binint_pos_sub_add, binint_add_comm,
      <- binint_pos_sub_add, pos_add_comm.
  - symmetry.
    apply binint_pos_sub_add.
  - cbn; apply ap, pos_add_assoc.
Defined.

Associativity of addition

Lemma binint_add_assoc n m p : n + (m + p) = n + m + p.
Proof.
  destruct n.
  - apply binint_negation_inj.
    rewrite !binint_negation_add_distr.
    apply binint_add_assoc_pos.
  - trivial.
  - apply binint_add_assoc_pos.
Defined.

Relationship between int_succ, int_pred and addition.

Lemma binint_add_succ_l a b : binint_succ a + b = binint_succ (a + b).
Proof.
  rewrite <- binint_add_assoc, (binint_add_comm 1 b).
  apply binint_add_assoc.
Defined.

Lemma binint_add_succ_r a b : a + binint_succ b = binint_succ (a + b).
Proof.
  apply binint_add_assoc.
Defined.

Lemma binint_add_pred_l a b : binint_pred a + b = binint_pred (a + b).
Proof.
  rewrite <- binint_add_assoc, (binint_add_comm (-1) b).
  apply binint_add_assoc.
Defined.

Lemma binint_add_pred_r a b : a + binint_pred b = binint_pred (a + b).
Proof.
  apply binint_add_assoc.
Defined.

Commutativity of multiplication

Lemma binint_mul_comm n m : n × m = m × n.
Proof.
  destruct n, m; cbn; try reflexivity;
  apply ap; apply pos_mul_comm.
Defined.

Distributivity of multiplication over addition

Lemma binint_pos_sub_mul_pos n m p
  : binint_pos_sub n m × pos p = binint_pos_sub (n × p)%pos (m × p)%pos.
Proof.
  rewrite binint_mul_comm.
  rewrite 2 (pos_mul_comm _ p).
  induction p.
  { rewrite 2 pos_mul_1_l.
    apply binint_mul_1_l. }
  { cbn.
    rewrite <- IHp.
    set (binint_pos_sub n m) as k.
    by destruct k. }
  cbn.
  rewrite binint_pos_sub_add.
  rewrite <- (binint_pos_sub_negation _ (x0 _)).
  rewrite binint_pos_sub_add.
  rewrite binint_negation_add_distr.
  rewrite binint_pos_sub_negation.
  rewrite binint_add_assoc.
  cbn.
  rewrite <- IHp.
  set (binint_pos_sub n m) as k.
  by destruct k.
Defined.

Lemma binint_pos_sub_mul_neg n m p
  : binint_pos_sub m n × neg p = binint_pos_sub (n × p)%pos (m × p)%pos.
Proof.
  rewrite binint_mul_comm.
  rewrite 2 (pos_mul_comm _ p).
  induction p.
  { rewrite 2 pos_mul_1_l.
    rewrite <- binint_pos_sub_negation.
    by destruct (binint_pos_sub n m). }
  { cbn.
    rewrite <- IHp.
    rewrite <- binint_pos_sub_negation.
    set (binint_pos_sub n m) as k.
    by destruct k. }
  cbn.
  rewrite binint_pos_sub_add.
  rewrite <- (binint_pos_sub_negation _ (x0 _)).
  rewrite binint_pos_sub_add.
  rewrite binint_negation_add_distr.
  rewrite binint_pos_sub_negation.
  rewrite binint_add_assoc.
  cbn.
  rewrite <- IHp.
  rewrite <- (binint_pos_sub_negation m).
  set (binint_pos_sub m n) as k.
  by destruct k.
Defined.

Lemma binint_mul_add_distr_r n m p : (n + m) × p = n × p + m × p.
Proof.
  induction p; destruct n, m; cbn; trivial; try f_ap;
  try apply pos_mul_add_distr_r;
  try apply binint_pos_sub_mul_neg;
  try apply binint_pos_sub_mul_pos;
  apply binint_mul_0_r.
Defined.

Lemma binint_mul_add_distr_l n m p : n × (m + p) = n × m + n × p.
Proof.
  rewrite 3 (binint_mul_comm n); apply binint_mul_add_distr_r.
Defined.

Lemma binint_mul_assoc n m p : n × (m × p) = n × m × p.
Proof.
  destruct n, m, p; cbn; trivial; f_ap; apply pos_mul_assoc.
Defined.