include "Cartesian.ma".
include "Maybe.ma".
include "Bool.ma".

include "logic/pts.ma".
include "Plogic/equality.ma".

ninductive Nat: Type[0] ≝
  Z: Nat
| S: Nat → Nat.

nlet rec plus (n: Nat) (o: Nat) on n ≝
  match n with
    [ Z ⇒ o
    | S p ⇒ S (plus p o)
    ].
    
notation "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 "n break - m"
  right associative with precedence 47
  for @{ 'minus $n $m }.
  
interpretation "Nat minus" 'minus n m = (minus n m).
    
nlet rec multiplication (n: Nat) (o: Nat) on n ≝
  match n with
    [ Z ⇒ Z
    | S p ⇒ o + (multiplication p o)
    ].
    
notation "n break * m"
  right associative with precedence 47
  for @{ 'multiplication $n $m }.
  
interpretation "Nat multiplication" 'times n m = (multiplication n m).

nlet rec less_than_or_equal (n: Nat) (m: Nat) ≝
  match n with
    [ Z ⇒ True
    | S o ⇒
      match m with
        [ Z ⇒ False
        | S p ⇒ less_than_or_equal o p
        ]
    ].
    
notation "n break ≤ m"
  non associative with precedence 47
  for @{ 'less_than_or_equal $n $m }.
  
interpretation "Nat less than or equal" 'less_than_or_equal n m = (less_than_or_equal n m).

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 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.
  napplyS plus_symmetrical.
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.
  napplyS multiplication_succ.
nqed.

nlemma multiplication_succ_zero_left_neutral:
  ∀m: Nat.
    (S Z) * m = m.
  #m.
  nelim m.
  nnormalize.
  @.
  #N H.
  nnormalize.
  napplyS succ_plus.
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.
  napplyS plus_associative.
nqed.

nlemma multiplication_distributes_left_plus:
  ∀m, n, o: Nat.
    o * (m + n) = o * m + o * n.
  #m n o.
  napplyS multiplication_symmetrical.
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.
  napplyS 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.
*)