source: Deliverables/D4.1/Matita/Nat.ma @ 233

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

include "logic/pts.ma".
include "Plogic/equality.ma".
include "Plogic/connectives.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).

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 ≝
  match m with
    [ Z ⇒ True
    | S o ⇒
      match n with
        [ Z ⇒ False
        | S p ⇒ less_than_or_equal_b o p
        ]
    ].
    
notation "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 less_than_p ≝
  λm, n: Nat.
    m ≤ n ∧ ¬(m = n).
    
notation "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).

(*
nlet rec greatest_common_divisor (m: Nat) (n: Nat) on n ≝
  match n with
    [ Z ⇒ m
    | S o ⇒ greatest_common_divisor n (modulus m n)
    ].
*)

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

(*
nlemma less_than_or_equal_injective:
  ∀m, n: Nat.
    S m ≤ S n → m ≤ n.
  #m n.
  nelim m.
  #H.
  napplyS less_than_or_equal_zero.
  #N H H2.
  ndestruct.

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.
  //.
  napplyS H.


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.
  //.
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.
  //.
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.
  //.
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.
*)