(* File: My_Arith.v  (last edited on 25/10/2000) (c) Klaus Weich  *)

Require Import Le.
Require Import Lt.
Require Import List.
Require Import Plus.

(******* List stuff ***********************************************)


Lemma fold_right_perm :
 forall (A B : Set) (f : B -> A -> A) (o : A) (l0 l1 : list B) (x : B),
 (forall (a b : B) (c : A), f a (f b c) = f b (f a c)) ->
 fold_right f o (l0 ++ x :: l1) = fold_right f o (x :: l0 ++ l1).
(* Goal: forall (A B : Set) (f : forall (_ : B) (_ : A), A) (o : A) (l0 l1 : list B) (x : B) (_ : forall (a b : B) (c : A), @eq A (f a (f b c)) (f b (f a c))), @eq A (@fold_right A B f o (@app B l0 (@cons B x l1))) (@fold_right A B f o (@cons B x (@app B l0 l1))) *)
intros A B f o l0 l1 x f_perm.
(* Goal: @eq A (@fold_right A B f o (@app B l0 (@cons B x l1))) (@fold_right A B f o (@cons B x (@app B l0 l1))) *)
elim l0; clear l0.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
(* Goal: forall (a : B) (l : list B) (_ : @eq A (@fold_right A B f o (@app B l (@cons B x l1))) (@fold_right A B f o (@cons B x (@app B l l1)))), @eq A (@fold_right A B f o (@app B (@cons B a l) (@cons B x l1))) (@fold_right A B f o (@cons B x (@app B (@cons B a l) l1))) *)
intros a0 l0 ih.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
simpl in |- *.
(* Goal: @eq nat (S (max n (S n))) (S (S n)) *)
 rewrite ih. 
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
simpl in |- *.
(* Goal: @eq A (f a0 (f x (@fold_right A B f o (@app B l0 l1)))) (f x (f a0 (@fold_right A B f o (@app B l0 l1)))) *)
apply f_perm.
Qed.




(********************************************************************)


Lemma plus_O : forall n : nat, n + 0 = n.
(* Goal: forall n : nat, @eq nat (Nat.add n O) n *)
intros n.
(* Goal: @eq nat (Nat.add n O) n *)
 rewrite (plus_comm n 0).
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
simpl in |- *.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
Qed.


Lemma n_Sn_false : forall n : nat, n = S n -> False.
(* Goal: forall n : nat, @eq nat (max n O) n *)
intros n; elim n; clear n.
intro u0;  discriminate u0.
(* Goal: forall (n : nat) (_ : forall _ : @eq nat n (S n), False) (_ : @eq nat (S n) (S (S n))), False *)
intros n ih u0.
(* Goal: le n (max m0 n) *)
apply ih.
(* Goal: @eq nat (max (S n) O) (S n) *)
 injection u0; trivial.
Qed.

Lemma le_reg : forall m n : nat, n <= m -> S n <= S m.
(* Goal: forall (m n : nat) (_ : le n m), le (S n) (S m) *)
intros m; elim m; clear m.
(* Goal: forall (n : nat) (_ : le n O), le (S n) (S O) *)
(* Goal: forall (n : nat) (_ : forall (n0 : nat) (_ : le n0 n), le (S n0) (S n)) (n0 : nat) (_ : le n0 (S n)), le (S n0) (S (S n)) *)
intros n; case n; clear n.
(* Goal: forall (l m n : nat) (_ : @eq nat m n), @eq nat (Nat.add l m) (Nat.add l n) *)
intros.
(* Goal: le (S (S m)) (S (S m)) *)
(* Goal: le (S n) (S (S m)) *)
apply le_n.
(* Goal: forall (l m n : nat) (_ : @eq nat m n), @eq nat (Nat.add l m) (Nat.add l n) *)
intros.
(* Goal: le (S n) (S (S m)) *)
inversion_clear H.
(* Goal: forall (n : nat) (_ : forall (n0 : nat) (_ : le n0 n), le (S n0) (S n)) (n0 : nat) (_ : le n0 (S n)), le (S n0) (S (S n)) *)
intros m ih n H.
(* Goal: le (S n) (S (S m)) *)
inversion_clear H.
(* Goal: le (S (S m)) (S (S m)) *)
(* Goal: le (S n) (S (S m)) *)
apply le_n.
(* Goal: le (S n) (S (S m)) *)
apply le_S.
(* Goal: le (S n) (S m) *)
apply ih; assumption.
Qed.


Lemma eq_lt_trans : forall n m p : nat, n = m -> m < p -> n < p.
(* Goal: forall (n m p : nat) (_ : @eq nat n m) (_ : lt m p), lt n p *)
intros n m p eq lt.
(* Goal: Peano.lt n p *)
 rewrite eq; assumption.
Qed.


Lemma S_reg : forall n m : nat, n = m -> S n = S m.
(* Goal: forall (l m n : nat) (_ : @eq nat m n), @eq nat (Nat.add l m) (Nat.add l n) *)
intros.
(* Goal: @eq nat (S n) (S m) *)
 rewrite H.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
Qed.



Lemma plus_reg : forall l m n : nat, m = n -> l + m = l + n.
(* Goal: forall (l m n : nat) (_ : @eq nat m n), @eq nat (Nat.add l m) (Nat.add l n) *)
intros.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
elim l; clear l; simpl in |- *.
(* Goal: @eq nat m n *)
(* Goal: forall (n0 : nat) (_ : @eq nat (Nat.add n0 m) (Nat.add n0 n)), @eq nat (S (Nat.add n0 m)) (S (Nat.add n0 n)) *)
assumption.
(* Goal: forall (n0 : nat) (_ : @eq nat (Nat.add n0 m) (Nat.add n0 n)), @eq nat (S (Nat.add n0 m)) (S (Nat.add n0 n)) *)
intros l' ih.
(* Goal: @eq nat (S (max n (S n))) (S (S n)) *)
 rewrite ih.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
Qed.


Lemma lt_plus_assoc_l :
 forall n m k l : nat, n + m + k < l -> n + (m + k) < l.
(* Goal: forall (n m k l : nat) (_ : lt (Nat.add (Nat.add n m) k) l), lt (Nat.add n (Nat.add m k)) l *)
intros n m k l lt.
(* Goal: @eq nat m n *)
(* Goal: forall (n0 : nat) (_ : @eq nat (Nat.add n0 m) (Nat.add n0 n)), @eq nat (S (Nat.add n0 m)) (S (Nat.add n0 n)) *)
 rewrite (plus_assoc n m k); assumption.
Qed.


Lemma my_lt_weak : forall n m : nat, S n < m -> n < m.
(* Goal: forall (n m : nat) (_ : lt (S n) m), lt n m *)
intros n m H.
(* Goal: lt n m *)
apply lt_S_n.
(* Goal: @eq nat m n *)
(* Goal: forall (n0 : nat) (_ : @eq nat (Nat.add n0 m) (Nat.add n0 n)), @eq nat (S (Nat.add n0 m)) (S (Nat.add n0 n)) *)
apply lt_trans with m; try assumption.
(* Goal: lt m (S m) *)
apply lt_n_Sn.
Qed.






(********************************************************************)
(*      max                                                         *)


Fixpoint max (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => match m with
           | O => S p
           | S q => S (max p q)
           end
  end.

Lemma le_n_max1 : forall n m : nat, n <= max n m.
(* Goal: forall n : nat, @eq nat (max n O) n *)
intros n; elim n; clear n.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
simpl in |- *.
(* Goal: forall m : nat, le O (max m O) *)
(* Goal: forall (n : nat) (_ : forall m : nat, le n (max m n)) (m : nat), le (S n) (max m (S n)) *)
intros m.
(* Goal: le O (max m O) *)
(* Goal: forall (n : nat) (_ : forall m : nat, le n (max m n)) (m : nat), le (S n) (max m (S n)) *)
apply le_O_n.
(* Goal: forall (n : nat) (_ : forall m : nat, le n (max m n)) (m : nat), le (S n) (max m (S n)) *)
intros n ih m.
(* Goal: le (S n) (max m (S n)) *)
case m; clear m.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
simpl in |- *.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
intros m0; simpl in |- *.
(* Goal: le (S n) (S (max m0 n)) *)
apply le_n_S.
(* Goal: le n (max m0 n) *)
apply ih.
Qed.


Lemma le_n_max2 : forall n m : nat, n <= max m n.
(* Goal: forall n : nat, @eq nat (max n O) n *)
intros n; elim n; clear n.
(* Goal: forall m : nat, le O (max m O) *)
(* Goal: forall (n : nat) (_ : forall m : nat, le n (max m n)) (m : nat), le (S n) (max m (S n)) *)
intros m.
(* Goal: le O (max m O) *)
(* Goal: forall (n : nat) (_ : forall m : nat, le n (max m n)) (m : nat), le (S n) (max m (S n)) *)
apply le_O_n.
(* Goal: forall (n : nat) (_ : forall m : nat, le n (max m n)) (m : nat), le (S n) (max m (S n)) *)
intros n ih m.
(* Goal: le (S n) (max m (S n)) *)
case m; clear m.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
simpl in |- *.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
intros m0; simpl in |- *.
(* Goal: le (S n) (S (max m0 n)) *)
apply le_n_S.
(* Goal: le n (max m0 n) *)
apply ih.
Qed.


Lemma max_n_n : forall n : nat, max n n = n.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
simple induction n; clear n; simpl in |- *. 
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
(* Goal: forall (n : nat) (_ : @eq nat (max n O) n), @eq nat (max (S n) O) (S n) *)
intros n ih.
(* Goal: @eq nat (S (max n (S n))) (S (S n)) *)
 rewrite ih.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
Qed.

Lemma max_Sn_n : forall n : nat, max (S n) n = S n.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
simple induction n; clear n; simpl in |- *. 
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
(* Goal: forall (n : nat) (_ : @eq nat (max n O) n), @eq nat (max (S n) O) (S n) *)
intros n ih.
(* Goal: @eq nat (S (max n (S n))) (S (S n)) *)
 rewrite ih.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
Qed.

Lemma max_n_Sn : forall n : nat, max n (S n) = S n.
(* Goal: le (S n) (max O (S n)) *)
(* Goal: forall n0 : nat, le (S n) (max (S n0) (S n)) *)
simple induction n; clear n; simpl in |- *.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
(* Goal: forall (n : nat) (_ : @eq nat (max n O) n), @eq nat (max (S n) O) (S n) *)
intros n ih.
(* Goal: @eq nat (S (max n (S n))) (S (S n)) *)
 rewrite ih.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
Qed.


Lemma max_n_O : forall n : nat, max n 0 = n.
(* Goal: forall n : nat, @eq nat (max n O) n *)
intros n; elim n; clear n.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
(* Goal: forall (n : nat) (_ : @eq nat (max n O) n), @eq nat (max (S n) O) (S n) *)
intros n ih.
(* Goal: @eq nat (max (S n) O) (S n) *)
trivial.
Qed.

