include "basics/types.ma".
include "arithmetics/nat.ma".

inductive nat_compared : nat → nat → Type[0] ≝
| nat_lt : ∀n,m:nat. nat_compared n (n+S m)
| nat_eq : ∀n:nat.   nat_compared n n
| nat_gt : ∀n,m:nat. nat_compared (m+S n) m.

let rec nat_compare (n:nat) (m:nat) : nat_compared n m ≝
match n return λx. nat_compared x m with
[ O ⇒ match m return λy. nat_compared O y with [ O ⇒ nat_eq ? | S m' ⇒ nat_lt ?? ]
| S n' ⇒
    match m return λy. nat_compared (S n') y with
    [ O ⇒ nat_gt n' O
    | S m' ⇒ match nat_compare n' m' return λx,y.λ_. nat_compared (S x) (S y) with
             [ nat_lt x y ⇒ nat_lt ??
             | nat_eq x ⇒ nat_eq ?
             | nat_gt x y ⇒ nat_gt ? (S y)
             ]
    ]
].

lemma nat_compare_eq : ∀n. nat_compare n n = nat_eq n.
#n elim n
[ @refl
| #m #IH whd in ⊢ (??%?); >IH @refl
] qed.

lemma nat_compare_lt : ∀n,m. nat_compare n (n+S m) = nat_lt n m.
#n #m elim n
[ //
| #n' #IH whd in ⊢ (??%?); >IH @refl
] qed.

lemma nat_compare_gt : ∀n,m. nat_compare (m+S n) m = nat_gt n m.
#n #m elim m
[ //
| #m' #IH whd in ⊢ (??%?); >IH @refl
] qed.


let rec eq_nat_dec (n:nat) (m:nat) : Sum (n=m) (n≠m) ≝
match n return λn.Sum (n=m) (n≠m) with
[ O ⇒ match m return λm.Sum (O=m) (O≠m) with [O ⇒ inl ?? (refl ??) | S m' ⇒ inr ??? ]
| S n' ⇒ match m return λm.Sum (S n'=m) (S n'≠m) with [O ⇒ inr ??? | S m' ⇒ 
           match eq_nat_dec n' m' with [ inl E ⇒ inl ??? | inr NE ⇒ inr ??? ] ]
].
[ 1,2: % #E destruct
| >E @refl
| % #E destruct cases NE /2/
] qed.

lemma max_l : ∀m,n,o:nat. o ≤ m → o ≤ max m n.
#m #n #o #H whd in ⊢ (??%); @leb_elim #H'
[ @(transitive_le ? m ? H H')
| @H
] qed.

lemma max_r : ∀m,n,o:nat. o ≤ n → o ≤ max m n.
#m #n #o #H whd in ⊢ (??%); @leb_elim #H'
[ @H
| @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) //
] qed.

lemma le_S_to_le: ∀n,m:ℕ.S n ≤ m → n ≤ m.
 /2/ qed.

lemma le_plus_k:
  ∀n,m:ℕ.n ≤ m → ∃k:ℕ.m = n + k.
 #n #m elim m -m;
 [ #Hn % [ @O | <(le_n_O_to_eq n Hn) // ]
 | #m #Hind #Hn cases (le_to_or_lt_eq … Hn) -Hn; #Hn
   [ elim (Hind (le_S_S_to_le … Hn)) #k #Hk % [ @(S k) | >Hk // ]
   | % [ @O | <Hn // ]
   ]
 ]
qed.

lemma eq_plus_S_to_lt:
  ∀n,m,p:ℕ.n = m + (S p) → m < n.
 #n #m #p /2 by lt_plus_to_lt_l/
qed.

(* "Fast" proofs:  some proofs get reduced during normalization (in particular,
   some functions which use a proof for rewriting are applied to constants and
   get reduced during a proof or while matita is searching for a term;
   they may also be normalized during testing), and so here are some more
   efficient versions.  Perhaps they could be replaced using some kind of proof
   irrelevance? *)

let rec plus_n_Sm_fast (n:nat) on n : ∀m:nat. S (n+m) = n+S m ≝
match n return λn'.∀m.S(n'+m) = n'+S m with
[ O ⇒ λm.refl ??
| S n' ⇒ λm. ?
]. normalize @(match plus_n_Sm_fast n' m with [ refl ⇒ ? ]) @refl qed.

let rec plus_n_O_faster (n:nat) : n = n + O ≝
match n return λn.n=n+O with
[ O ⇒ refl ??
| S n' ⇒ match plus_n_O_faster n' return λx.λ_.S n'=S x with [ refl ⇒ refl ?? ]
].

let rec commutative_plus_faster (n,m:nat) : n+m = m+n ≝
match n return λn.n+m = m+n with
[ O ⇒ plus_n_O_faster ?
| S n' ⇒ ?
]. @(match plus_n_Sm_fast m n' return λx.λ_. ? = x with [ refl ⇒ ? ])
@(match commutative_plus_faster n' m return λx.λ_.? = S x with [refl ⇒ ?]) @refl qed.

lemma distributive_times_plus_fast : distributive ? times plus.
#n elim n [ #m #p % ]
#n' #IH #m #p normalize
>IH
>associative_plus in ⊢ (???%);
<(associative_plus ? p) in ⊢ (???%);
>(commutative_plus_faster ? p) in ⊢ (???%);
>(associative_plus p)
@associative_plus
qed.

lemma times_n_Sm_fast : ∀n,m.n + n * m = n * S m.
#n elim n -n
[ #m % ]
#n #IH #m normalize <IH
<associative_plus >(commutative_plus_faster n)
>associative_plus >IH %
qed.

lemma commutative_times_fast : commutative ? times.
#n elim n -n
[ #m <times_n_O % ]
#n #IH #m normalize <times_n_Sm_fast >IH %
qed.