(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Nat.ma: Natural numbers and common arithmetical functions.                 *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
include "Cartesian.ma".
include "Bool.ma".

include "Connectives.ma".

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* The datatype.                                                              *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
ninductive Nat: Type[0] ≝
  Z: Nat
| S: Nat → Nat.

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Orderings.                                                                 *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝
  ltoe_refl: less_than_or_equal_p n n
| ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m).

nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝
  match m with
    [ Z ⇒ true
    | S o ⇒
      match n with
        [ Z ⇒ false
        | S p ⇒ less_than_or_equal_b o p
        ]
    ].
    
notation "hvbox(n break ≤ m)"
  non associative with precedence 47
  for @{ 'less_than_or_equal $n $m }.
  
interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m).
interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m).

ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝
  λm, n: Nat.
    n ≤ m.

ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝
  λm, n: Nat.
    n ≤ m.
    
notation "hvbox(n break ≥ m)"
  non associative with precedence 47
  for @{ 'greater_than_or_equal $n $m }.
  

interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m).
interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m).

(* Add Boolean versions.                                                      *)
ndefinition less_than_p ≝
  λm: Nat.
  λn: Nat.
    less_than_or_equal_p (S m) n.
    
notation "hvbox(n break < m)"
  non associative with precedence 47
  for @{ 'less_than $n $m }.
  
interpretation "Nat less than prop" 'less_than n m = (less_than_p n m).

ndefinition greater_than_p ≝
  λm, n: Nat.
    n < m.
    
notation "hvbox(n break > m)"
  non associative with precedence 47
  for @{ 'greater_than $n $m }.
  
interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Addition and subtraction.                                                  *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
nlet rec plus (n: Nat) (o: Nat) on n ≝
  match n with
    [ Z ⇒ o
    | S p ⇒ S (plus p o)
    ].
    
notation "hvbox(n break + m)"
  right associative with precedence 52
  for @{ 'plus $n $m }.
  
interpretation "Nat plus" 'plus n m = (plus n m).
    
nlet rec minus (n: Nat) (o: Nat) on n ≝
  match n with
    [ Z ⇒ Z
    | S p ⇒
      match o with
        [ Z ⇒ S p
        | S q ⇒ minus p q
        ]
    ].
    
notation "hvbox(n break - m)"
  right associative with precedence 47
  for @{ 'minus $n $m }.
  
interpretation "Nat minus" 'minus n m = (minus n m).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Multiplication, modulus and division.                                      *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    
nlet rec multiplication (n: Nat) (o: Nat) on n ≝
  match n with
    [ Z ⇒ Z
    | S p ⇒ o + (multiplication p o)
    ].
    
notation "hvbox(n break * m)"
  right associative with precedence 47
  for @{ 'multiplication $n $m }.
  
interpretation "Nat multiplication" 'times n m = (multiplication n m).

nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝
  match n ≤ p with
    [ true ⇒ Z
    | false ⇒
      match m with
        [ Z ⇒ Z
        | (S q) ⇒ S (division_aux q (n - (S p)) p)
        ]
    ].
    
ndefinition division ≝
  λm, n: Nat.
    match n with
      [ Z ⇒ S m
      | S o ⇒ division_aux m m o
      ].
      
notation "hvbox(n break ÷ m)"
  right associative with precedence 47
  for @{ 'division $n $m }.
  
interpretation "Nat division" 'division n m = (division n m).
      
nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝
  match n ≤ p with
    [ true ⇒ n
    | false ⇒
      match m with
        [ Z ⇒ n
        | S o ⇒ modulus_aux o (n - (S p)) p
        ]
    ].
    
ndefinition modulus ≝
  λm, n: Nat.
    match n with
      [ Z ⇒ m
      | S o ⇒ modulus_aux m m o
      ].
    
notation "hvbox(n break 'mod' m)"
  right associative with precedence 47
  for @{ 'modulus $n $m }.
  
interpretation "Nat modulus" 'modulus m n = (modulus m n).

ndefinition divide_with_remainder ≝
  λm, n: Nat.
    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Exponentials, and square roots.                                            *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlet rec exponential (m: Nat) (n: Nat) on n ≝
  match n with
    [ Z ⇒ S (Z)
    | S o ⇒ m * exponential m o
    ].
    
notation "hvbox(n ^ m)"
  left associative with precedence 52
  for @{ 'exponential $n $m }.
  
interpretation "Nat exponential" 'exponential n m = (exponential n m).

nlet rec decidable_equality (m: Nat) (n: Nat) on m: Bool ≝
  match m with
    [ Z ⇒
      match n with
        [ Z ⇒ true
        | _ ⇒ false
        ]
    | S o ⇒
      match n with
        [ S p ⇒ decidable_equality o p
        | _ ⇒ false
        ]
    ].

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Greatest common divisor and least common multiple.                         *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
(* Lemmas.                                                                    *)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)

nlemma less_than_or_equal_zero:
  ∀n: Nat.
    Z ≤ n.
  #n.
  nelim n.
  //.
  #N.
  napply ltoe_step.
nqed.

naxiom less_than_or_equal_injective:
  ∀m, n: Nat.
    S m ≤ S n → m ≤ n.

(*
nlemma less_than_or_equal_zero_equal_zero:
  ∀m: Nat.
    m ≤ Z → m = Z.
  #m.
  nelim m.
  //.
  #N H H2.
  nnormalize.
*)

nlemma less_than_or_equal_reflexive:
  ∀n: Nat.
    n ≤ n.
  #n.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  //.
nqed.

(*
nlemma less_than_or_equal_succ:
  ∀m, n: Nat.
    S m ≤ n → m ≤ n.
  #m n.
  nelim m.
  #H.
  napplyS less_than_or_equal_zero.
  #N H H2.
  nrewrite > H.
  nnormalize.

nlemma less_than_or_equal_transitive:
  ∀m, n, o: Nat.
    m ≤ n ∧ n ≤ o → m ≤ o.
  #m n o.
  nelim m.
  #H.
  napply less_than_or_equal_zero.
  #N H H2.
  nnormalize.
*)

nlemma plus_zero:
  ∀n: Nat.
    n + Z = n.
  #n.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma plus_associative:
  ∀m, n, o: Nat.
    (m + n) + o = m + (n + o).
  #m n o.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma succ_plus:
  ∀m, n: Nat.
    S(m + n) = m + S(n).
  #m n.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma succ_plus_succ_zero:
  ∀n: Nat.
    S n = plus n (S Z).
  #n.
  nelim n.
  //.
  #N H.
  nnormalize.
  nrewrite < H.
  @.
nqed.

nlemma plus_symmetrical:
  ∀m, n: Nat.
    m + n = n + m.
  #m n.
  nelim m.
  nnormalize.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite < H.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  napplyS succ_plus.
nqed.

nlemma multiplication_zero_right_neutral:
  ∀m: Nat.
    m * Z = Z.
  #m.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma multiplication_succ:
  ∀m, n: Nat.
    m * S(n) = m + (m * n).
  #m n.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite < (plus_associative n N ?).
  nrewrite > (plus_symmetrical n N).
  nrewrite > (plus_associative N n ?).
  @.
nqed.

nlemma multiplication_symmetrical:
  ∀m, n: Nat.
    m * n = n * m.
  #m n.
  nelim m.
  nnormalize.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite < H.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite > (multiplication_succ ? ?).
  @.
nqed.

nlemma multiplication_succ_zero_left_neutral:
  ∀m: Nat.
    (S Z) * m = m.
  #m.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > (succ_plus ? ?).
  nrewrite < (succ_plus_succ_zero ?).
  @.
nqed.

nlemma multiplication_succ_zero_right_neutral:
  ∀m: Nat.
    m * (S Z) = m.
  #m.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

nlemma multiplication_distributes_right_plus:
  ∀m, n, o: Nat.
    (m + n) * o = m * o + n * o.
  #m n o.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite < (plus_associative ? ? ?).
  @.
nqed.

nlemma multiplication_distributes_left_plus:
  ∀m, n, o: Nat.
    o * (m + n) = o * m + o * n.
  #m n o.
  nelim o.
  //.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite < (plus_associative ? n (N * n)).
  nrewrite > (plus_symmetrical (m + N * m) n).
  nrewrite < (plus_associative n m (N * m)).
  nrewrite < (plus_symmetrical n m).
  nrewrite > (plus_associative (n + m) (N * m) (N * n)).
  @.
nqed.

nlemma mutliplication_associative:
  ∀m, n, o: Nat.
    m * (n * o) = (m * n) * o.
  #m n o.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  nrewrite > (multiplication_distributes_right_plus ? ? ?).
  @.
nqed.

nlemma minus_minus:
  ∀n: Nat.
    n - n = Z.
  #n.
  nelim n.
  nnormalize.
  @.
  #N H.
  nnormalize.
  nrewrite > H.
  @.
nqed.

(*
nlemma succ_injective:
  ∀m, n: Nat.
    S m = S n → m = n.
  #m n.
  nelim m.
  #H.
  ninversion H.
  #H.
  ndestruct 

nlemma plus_minus_associate:
  ∀m, n, o: Nat.
    (m + n) - o = m + (n - o).
  #m n o.
  nelim m.
  nnormalize.
  @.
  #N H.
  

nlemma plus_minus_inverses:
  ∀m, n: Nat.
    (m + n) - n = m.
  #m n.
  nelim m.
  nnormalize.
  napply minus_minus.
  #N H.
*)