Require Import Basics.Overture Basics.Tactics Basics.Decidable
  Spaces.Nat.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Set Universe Minimization ToSet.

(** * Binary Positive Integers *)

(** Most of this file has been adapted from the Coq standard library for positive binary integers. *)

(** Here we define the inductive type of positive binary numbers. *)
Inductive Pos : Type0 :=
  | xH : Pos
  | x0 : Pos -> Pos
  | x1 : Pos -> Pos.

Declare Scope positive_scope.
Delimit Scope positive_scope with pos.

(** Here are some notations that let us write binary positive integers more easily. *)
Notation "1" := xH : positive_scope.
Notation "p ~ 1" := (x1 p) : positive_scope.
Notation "p ~ 0" := (x0 p) : positive_scope.

Local Open Scope positive_scope.

(** ** Successor *)
Fixpoint pos_succ x :=
  match x with
    | p~1 => (pos_succ p)~0
    | p~0 => p~1
    | 1 => 1~0
  end.

(** Peano induction (due to Daniel Schepler) *)
Fixpoint pos_peano_ind (P : Pos -> Type) (a : P 1)
  (f : forall p, P p -> P (pos_succ p)) (p : Pos) : P p
  := let f2 := pos_peano_ind (fun p => P (p~0))
    (f _ a) (fun p (x : P p~0) => f _ (f _ x))
  in match p with
      | q~1 => f _ (f2 q)
      | q~0 => f2 q
      | 1 => a
     end.

(** Computation rules for Peano induction *)
Definition pos_peano_ind_beta_1 (P : Pos -> Type) (a : P 1)
  (f : forall p, P p -> P (pos_succ p))
  : pos_peano_ind P a f 1 = a := idpath.

Definition pos_peano_ind_beta_pos_succ (P : Pos -> Type) (a : P 1)
  (f : forall p, P p -> P (pos_succ p)) (p : Pos)
  : pos_peano_ind P a f (pos_succ p) = f _ (pos_peano_ind P a f p).
P: Pos -> Type
a: P 1
f: forall p : Pos, P p -> P (pos_succ p)
p: Pos
pos_peano_ind P a f (pos_succ p) =
f p (pos_peano_ind P a f p)
Proof.
P: Pos -> Type
a: P 1
f: forall p : Pos, P p -> P (pos_succ p)
p: Pos
pos_peano_ind P a f (pos_succ p) =
f p (pos_peano_ind P a f p)
  revert P a f.
p: Pos
forall (P : Pos -> Type) (a : P 1)
(f : forall p : Pos, P p -> P (pos_succ p)),
pos_peano_ind P a f (pos_succ p) =
f p (pos_peano_ind P a f p)
  induction p; trivial.
p: Pos
IHp: forall (P : Pos -> Type) (a : P 1)
(f : forall p : Pos, P p -> P (pos_succ p)),
pos_peano_ind P a f (pos_succ p) = f p (pos_peano_ind P a f p)
forall (P : Pos -> Type) (a : P 1)
(f : forall p : Pos, P p -> P (pos_succ p)),
pos_peano_ind P a f (pos_succ p~1) =
f p~1 (pos_peano_ind P a f p~1)
  intros P a f.
p: Pos
IHp: forall (P : Pos -> Type) (a : P 1)
(f : forall p : Pos, P p -> P (pos_succ p)),
pos_peano_ind P a f (pos_succ p) = f p (pos_peano_ind P a f p)
P: Pos -> Type
a: P 1
f: forall p : Pos, P p -> P (pos_succ p)
pos_peano_ind P a f (pos_succ p~1) =
f p~1 (pos_peano_ind P a f p~1)
  srapply IHp.
Qed.

Definition pos_peano_rec (P : Type)
  : P -> (Pos -> P -> P) -> Pos -> P
  := pos_peano_ind (fun _ => P).

Definition pos_peano_rec_beta_pos_succ (P : Type)
  (a : P) (f : Pos -> P -> P) (p : Pos)
  : pos_peano_rec P a f (pos_succ p) = f p (pos_peano_rec P a f p)
  := pos_peano_ind_beta_pos_succ (fun _ => P) a f p.

(** ** Properties of constructors *)

Definition x0_inj {z w : Pos} (p : x0 z = x0 w) : z = w
  := transport (fun s => z = (
    match s with xH => w | x0 a => a | x1 a => w end)) p idpath.

Definition x1_inj {z w : Pos} (p : x1 z = x1 w) : z = w
  := transport (fun s => z = (
    match s with xH => w | x0 a => w | x1 a => a end)) p idpath.

Definition x0_neq_xH {z : Pos} : x0 z <> xH
  := fun p => transport (fun s =>
    match s with xH => Empty | x0 a => z = a | x1 a => Empty end) p idpath.

Definition x1_neq_xH {z : Pos} : x1 z <> xH
  := fun p => transport (fun s =>
    match s with xH => Empty | x0 a => Empty | x1 a => z = a end) p idpath.

Definition x0_neq_x1 {z w : Pos} : x0 z <> x1 w
  := fun p => transport (fun s =>
    match s with xH => Empty | x0 a => z = a | x1 _ => Empty end) p idpath.

Definition xH_neq_x0 {z : Pos} : xH <> x0 z
  := x0_neq_xH o symmetry _ _.

Definition xH_neq_x1 {z : Pos} : xH <> x1 z
  := x1_neq_xH o symmetry _ _.

Definition x1_neq_x0 {z w : Pos} : x1 z <> x0 w
  := x0_neq_x1 o symmetry _ _.

(** * Positive binary integers have decidable paths *)

Instance decpaths_pos : DecidablePaths Pos.
DecidablePaths Pos
Proof.
DecidablePaths Pos
  intros n; induction n as [|zn|on];
  intros m; induction m as [|zm|om].
Decidable (1 = 1)
zm: Pos
IHzm: Decidable (1 = zm)
Decidable (1 = zm~0)
om: Pos
IHom: Decidable (1 = om)
Decidable (1 = om~1)
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
Decidable (zn~0 = 1)
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
zm: Pos
IHzm: Decidable (zn~0 = zm)
Decidable (zn~0 = zm~0)
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
om: Pos
IHom: Decidable (zn~0 = om)
Decidable (zn~0 = om~1)
on: Pos
IHon: forall y : Pos, Decidable (on = y)
Decidable (on~1 = 1)
on: Pos
IHon: forall y : Pos, Decidable (on = y)
zm: Pos
IHzm: Decidable (on~1 = zm)
Decidable (on~1 = zm~0)
on: Pos
IHon: forall y : Pos, Decidable (on = y)
om: Pos
IHom: Decidable (on~1 = om)
Decidable (on~1 = om~1)
  +
Decidable (1 = 1) exact (inl idpath).
  +
zm: Pos
IHzm: Decidable (1 = zm)
Decidable (1 = zm~0) exact (inr xH_neq_x0).
  +
om: Pos
IHom: Decidable (1 = om)
Decidable (1 = om~1) exact (inr xH_neq_x1).
  +
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
Decidable (zn~0 = 1) exact (inr x0_neq_xH).
  +
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
zm: Pos
IHzm: Decidable (zn~0 = zm)
Decidable (zn~0 = zm~0) destruct (IHzn zm) as [p|q].
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
zm: Pos
IHzm: Decidable (zn~0 = zm)
p: zn = zm
Decidable (zn~0 = zm~0)
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
zm: Pos
IHzm: Decidable (zn~0 = zm)
q: zn <> zm
Decidable (zn~0 = zm~0)
    -
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
zm: Pos
IHzm: Decidable (zn~0 = zm)
p: zn = zm
Decidable (zn~0 = zm~0) apply inl, ap, p.
    -
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
zm: Pos
IHzm: Decidable (zn~0 = zm)
q: zn <> zm
Decidable (zn~0 = zm~0) apply inr; intro p.
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
zm: Pos
IHzm: Decidable (zn~0 = zm)
q: zn <> zm
p: zn~0 = zm~0
Empty
      by apply q, x0_inj.
  +
zn: Pos
IHzn: forall y : Pos, Decidable (zn = y)
om: Pos
IHom: Decidable (zn~0 = om)
Decidable (zn~0 = om~1) exact (inr x0_neq_x1).
  +
on: Pos
IHon: forall y : Pos, Decidable (on = y)
Decidable (on~1 = 1) exact (inr x1_neq_xH).
  +
on: Pos
IHon: forall y : Pos, Decidable (on = y)
zm: Pos
IHzm: Decidable (on~1 = zm)
Decidable (on~1 = zm~0) exact (inr x1_neq_x0).
  +
on: Pos
IHon: forall y : Pos, Decidable (on = y)
om: Pos
IHom: Decidable (on~1 = om)
Decidable (on~1 = om~1) destruct (IHon om) as [p|q].
on: Pos
IHon: forall y : Pos, Decidable (on = y)
om: Pos
IHom: Decidable (on~1 = om)
p: on = om
Decidable (on~1 = om~1)
on: Pos
IHon: forall y : Pos, Decidable (on = y)
om: Pos
IHom: Decidable (on~1 = om)
q: on <> om
Decidable (on~1 = om~1)
    -
on: Pos
IHon: forall y : Pos, Decidable (on = y)
om: Pos
IHom: Decidable (on~1 = om)
p: on = om
Decidable (on~1 = om~1) apply inl, ap, p.
    -
on: Pos
IHon: forall y : Pos, Decidable (on = y)
om: Pos
IHom: Decidable (on~1 = om)
q: on <> om
Decidable (on~1 = om~1) apply inr; intro p.
on: Pos
IHon: forall y : Pos, Decidable (on = y)
om: Pos
IHom: Decidable (on~1 = om)
q: on <> om
p: on~1 = om~1
Empty
      by apply q, x1_inj.
Defined.

(** Decidable paths imply [Pos] is a hSet *)
Instance ishset_pos : IsHSet Pos := _.

(** * Operations over positive numbers *)

(** ** Addition *)

Fixpoint pos_add x y :=
  match x, y with
    | p~1, q~1 => (pos_add_carry p q)~0
    | p~1, q~0 => (pos_add p q)~1
    | p~1, 1 => (pos_succ p)~0
    | p~0, q~1 => (pos_add p q)~1
    | p~0, q~0 => (pos_add p q)~0
    | p~0, 1 => p~1
    | 1, q~1 => (pos_succ q)~0
    | 1, q~0 => q~1
    | 1, 1 => 1~0
  end

with pos_add_carry x y :=
  match x, y with
    | p~1, q~1 => (pos_add_carry p q)~1
    | p~1, q~0 => (pos_add_carry p q)~0
    | p~1, 1 => (pos_succ p)~1
    | p~0, q~1 => (pos_add_carry p q)~0
    | p~0, q~0 => (pos_add p q)~1
    | p~0, 1 => (pos_succ p)~0
    | 1, q~1 => (pos_succ q)~1
    | 1, q~0 => (pos_succ q)~0
    | 1, 1 => 1~1
  end.

Infix "+" := pos_add : positive_scope.

(** ** Operation [x -> 2*x-1] *)

Fixpoint pos_pred_double x :=
  match x with
    | p~1 => p~0~1
    | p~0 => (pos_pred_double p)~1
    | 1 => 1
  end.

(** ** Predecessor *)

Definition pos_pred x :=
  match x with
    | p~1 => p~0
    | p~0 => pos_pred_double p
    | 1 => 1
  end.

(** ** An auxiliary type for subtraction *)

Inductive Pos_mask : Set :=
  | IsNul : Pos_mask
  | IsPos : Pos -> Pos_mask
  | IsNeg : Pos_mask.

(** ** Operation [x -> 2*x+1] *)

Definition pos_mask_succ_double (x : Pos_mask) : Pos_mask :=
  match x with
    | IsNul => IsPos 1
    | IsNeg => IsNeg
    | IsPos p => IsPos p~1
  end.

(** ** Operation [x -> 2*x] *)

Definition pos_mask_double (x : Pos_mask) : Pos_mask :=
  match x with
    | IsNul => IsNul
    | IsNeg => IsNeg
    | IsPos p => IsPos p~0
  end.

(** ** Operation [x -> 2*x-2] *)

Definition pos_mask_double_pred x : Pos_mask :=
  match x with
    | p~1 => IsPos p~0~0
    | p~0 => IsPos (pos_pred_double p)~0
    | 1 => IsNul
  end.

(** ** Predecessor with mask *)

Definition pos_mask_pred (p : Pos_mask) : Pos_mask :=
  match p with
    | IsPos 1 => IsNul
    | IsPos q => IsPos (pos_pred q)
    | IsNul => IsNeg
    | IsNeg => IsNeg
  end.

(** ** Subtraction, result as a mask *)

Fixpoint pos_mask_sub (x y : Pos) {struct y} : Pos_mask :=
  match x, y with
    | p~1, q~1 => pos_mask_double (pos_mask_sub p q)
    | p~1, q~0 => pos_mask_succ_double (pos_mask_sub p q)
    | p~1, 1 => IsPos p~0
    | p~0, q~1 => pos_mask_succ_double (pos_mask_sub_carry p q)
    | p~0, q~0 => pos_mask_double (pos_mask_sub p q)
    | p~0, 1 => IsPos (pos_pred_double p)
    | 1, 1 => IsNul
    | 1, _ => IsNeg
  end

with pos_mask_sub_carry (x y : Pos) {struct y} : Pos_mask :=
  match x, y with
    | p~1, q~1 => pos_mask_succ_double (pos_mask_sub_carry p q)
    | p~1, q~0 => pos_mask_double (pos_mask_sub p q)
    | p~1, 1 => IsPos (pos_pred_double p)
    | p~0, q~1 => pos_mask_double (pos_mask_sub_carry p q)
    | p~0, q~0 => pos_mask_succ_double (pos_mask_sub_carry p q)
    | p~0, 1 => pos_mask_double_pred p
    | 1, _ => IsNeg
  end.

(** ** Subtraction, result as a positive, returning 1 if [x<=y] *)

Definition pos_sub x y :=
  match pos_mask_sub x y with
    | IsPos z => z
    | _ => 1
  end.

Infix "-" := pos_sub : positive_scope.

(** ** Multiplication *)

Fixpoint pos_mul x y :=
  match x with
    | p~1 => y + (pos_mul p y)~0
    | p~0 => (pos_mul p y)~0
    | 1 => y
  end.

Infix "*" := pos_mul : positive_scope.

(** ** Iteration over a positive number *)

Definition pos_iter {A : Type} (f : A -> A)
  : Pos -> A -> A.
A: Type
f: A -> A
Pos -> A -> A
Proof.
A: Type
f: A -> A
Pos -> A -> A
  apply (pos_peano_rec (A -> A) f).
A: Type
f: A -> A
Pos -> (A -> A) -> A -> A
  intros n g.
A: Type
f: A -> A
n: Pos
g: A -> A
A -> A
  exact (f o g).
Defined.

(** ** Iteration of a two-variable function, with nesting reflecting the bits *)

Definition pos_iter_op {A} (op : A -> A -> A)
  := fix p_iter (p : Pos) (a : A) : A
    := match p with
        | 1 => a
        | p~0 => p_iter p (op a a)
        | p~1 => op a (p_iter p (op a a))
       end.

(** ** Power *)

Definition pos_pow (x : Pos) := pos_iter (pos_mul x) 1.

(** ** Square *)

Fixpoint pos_square p :=
  match p with
    | p~1 => (pos_square p + p)~0~1
    | p~0 => (pos_square p)~0~0
    | 1 => 1
  end.

(** ** Division by 2 rounded below but for 1 *)

Definition pos_div2 p :=
  match p with
    | 1 => 1
    | p~0 => p
    | p~1 => p
  end.

(** Division by 2 rounded up *)

Definition pos_div2_up p :=
 match p with
   | 1 => 1
   | p~0 => p
   | p~1 => pos_succ p
 end.

(** ** Number of digits in a positive number *)

Fixpoint nat_pos_size p : nat :=
  match p with
    | 1 => S O
    | p~1 => S (nat_pos_size p)
    | p~0 => S (nat_pos_size p)
  end.

(** Same, with positive output *)

Fixpoint pos_size p :=
  match p with
    | 1 => 1
    | p~1 => pos_succ (pos_size p)
    | p~0 => pos_succ (pos_size p)
  end.

(** ** From binary positive numbers to Peano natural numbers *)

(** Sends [n] to [n], missing [0]. *)
Definition nat_of_pos (p : Pos) : nat
  := pos_iter S p 0%nat.

(** ** From Peano natural numbers to binary positive numbers *)

(** A version preserving positive numbers, and sending 0 to 1. *)

Fixpoint pos_of_nat (n : nat) : Pos :=
 match n with
   | O => 1
   | S O => 1
   | S x => pos_succ (pos_of_nat x)
 end.

(* Another version that converts [n] into [n+1] *)

Fixpoint pos_of_succ_nat (n : nat) : Pos :=
  match n with
    | O => 1
    | S x => pos_succ (pos_of_succ_nat x)
  end.

(** ** Conversion with a decimal representation for printing/parsing *)

Local Notation ten := 1~0~1~0.

Fixpoint pos_of_uint_acc (d : Decimal.uint) (acc : Pos) :=
  match d with
  | Decimal.Nil => acc
  | Decimal.D0 l => pos_of_uint_acc l (pos_mul ten acc)
  | Decimal.D1 l => pos_of_uint_acc l (pos_add 1 (pos_mul ten acc))
  | Decimal.D2 l => pos_of_uint_acc l (pos_add 1~0 (pos_mul ten acc))
  | Decimal.D3 l => pos_of_uint_acc l (pos_add 1~1 (pos_mul ten acc))
  | Decimal.D4 l => pos_of_uint_acc l (pos_add 1~0~0 (pos_mul ten acc))
  | Decimal.D5 l => pos_of_uint_acc l (pos_add 1~0~1 (pos_mul ten acc))
  | Decimal.D6 l => pos_of_uint_acc l (pos_add 1~1~0 (pos_mul ten acc))
  | Decimal.D7 l => pos_of_uint_acc l (pos_add 1~1~1 (pos_mul ten acc))
  | Decimal.D8 l => pos_of_uint_acc l (pos_add 1~0~0~0 (pos_mul ten acc))
  | Decimal.D9 l => pos_of_uint_acc l (pos_add 1~0~0~1 (pos_mul ten acc))
  end.

Fixpoint pos_of_uint (d : Decimal.uint) : option Pos :=
  match d with
    | Decimal.Nil => None
    | Decimal.D0 l => pos_of_uint l
    | Decimal.D1 l => Some (pos_of_uint_acc l 1)
    | Decimal.D2 l => Some (pos_of_uint_acc l 1~0)
    | Decimal.D3 l => Some (pos_of_uint_acc l 1~1)
    | Decimal.D4 l => Some (pos_of_uint_acc l 1~0~0)
    | Decimal.D5 l => Some (pos_of_uint_acc l 1~0~1)
    | Decimal.D6 l => Some (pos_of_uint_acc l 1~1~0)
    | Decimal.D7 l => Some (pos_of_uint_acc l 1~1~1)
    | Decimal.D8 l => Some (pos_of_uint_acc l 1~0~0~0)
    | Decimal.D9 l => Some (pos_of_uint_acc l 1~0~0~1)
  end.

Definition pos_of_decimal_int (d:Decimal.int) : option Pos :=
  match d with
  | Decimal.Pos d => pos_of_uint d
  | Decimal.Neg _ => None
  end.

Definition pos_of_number_uint (d:Numeral.int) : option Pos :=
  match d with
  | Numeral.IntDec d => pos_of_decimal_int d
  | Numeral.IntHex _ => None
  end.

Fixpoint pos_to_little_uint p :=
  match p with
  | 1 => Decimal.D1 Decimal.Nil
  | p~1 => Decimal.Little.succ_double (pos_to_little_uint p)
  | p~0 => Decimal.Little.double (pos_to_little_uint p)
  end.

Definition pos_to_uint p := Decimal.rev (pos_to_little_uint p).

Definition pos_to_decimal_int n := Decimal.Pos (pos_to_uint n).

Definition pos_to_number_uint p := Numeral.UIntDec (pos_to_uint p).

Definition pos_to_nat : Pos -> nat.
Pos -> nat
Proof.
Pos -> nat
  intro p.
p: Pos
nat induction p.
nat
p: Pos
IHp: nat
nat
p: Pos
IHp: nat
nat
  +
nat exact (S O).
  +
p: Pos
IHp: nat
nat exact (nat_add IHp IHp).
  +
p: Pos
IHp: nat
nat exact (S (nat_add IHp IHp)).
Defined.

Number Notation Pos pos_of_number_uint pos_to_number_uint : positive_scope.