Require Import Plus.
Require Import Le.
Require Import Compare.
Open Scope nat_scope.

Fixpoint kth_S (k : nat) (n : nat) {struct k} : nat:=
match k with
| 0 ⇒ S n
| S k' ⇒ S(kth_S k' n)
end.

Fixpoint next_P_k (k : nat) (delta : nat) (P : nat → Prop) {struct k} : Prop:=
match k with
| 0 ⇒ P delta
| S k' ⇒ P (kth_S delta k') ∧ next_P_k k' delta P
end.

Lemma next_P_k_strong : ∀ k delta P,
  next_P_k (S k) delta P → next_P_k k delta P.
induction k.
intros.
unfold next_P_k.
unfold next_P_k in H.
destruct H.
exact H0.

intros.
unfold next_P_k. fold next_P_k.
unfold next_P_k in H. fold next_P_k in H.
destruct H.
destruct H0.
split.
exact H0.
exact H1.
Qed.

Lemma kth_S_comm : ∀ delta gamma n,
  kth_S delta (kth_S gamma n) = kth_S gamma (kth_S delta n).
induction delta.
intros.
induction gamma.
compute. reflexivity.
unfold kth_S. fold kth_S.
unfold kth_S in IHgamma. fold kth_S in IHgamma.
rewrite IHgamma.
reflexivity.

intros.
unfold kth_S. fold kth_S.
rewrite IHdelta.
induction gamma.
compute. reflexivity.
unfold kth_S. fold kth_S.
rewrite IHgamma.
reflexivity.
Qed.

Lemma kth_S_special : ∀ k, kth_S k 0 = S k.
Proof.
induction k.
compute. reflexivity.
unfold kth_S. fold kth_S.
rewrite IHk.
reflexivity.
Qed.

Lemma next_P_k_special: ∀ k delta P,
  next_P_k k delta P → P delta.
Proof.
induction k.
intros. exact H.
intros. apply IHk.
apply next_P_k_strong.
exact H.
Qed.

Lemma kth_S_sym : ∀ k n, kth_S k n = kth_S n k.
Proof.
induction k.
intro.
rewrite kth_S_special.
reflexivity.

intro.
unfold kth_S. fold kth_S.
rewrite IHk.
induction n.
compute. reflexivity.
unfold kth_S. fold kth_S.
rewrite IHn.
reflexivity.
Qed.

Lemma kth_S_plus : ∀ k n, kth_S k n = n + k + 1.
Proof.
induction k.
intro.
unfold kth_S.
rewrite plus_0_r.
rewrite plus_1_r.
reflexivity.
intro.
unfold kth_S. fold kth_S.
rewrite IHk.
assert (n + S k + 1=S k + n +1).
auto with arith.
rewrite H. clear H.
simpl.
auto with arith.
Qed.

Theorem next_P_k_correct : ∀ k delta, ∀ P : nat → Prop,
  P delta → (∀ x, x < k → P (kth_S delta x)) → next_P_k k delta P.
Proof.
induction k.
intros.
simpl.
exact H.
intros.
simpl.
split.
apply H0.
auto with arith.
apply IHk.
exact H.
intros.
apply H0.
auto with arith.
Qed.

Theorem next_P_k_complete : ∀ k delta P,
  next_P_k k delta P → P delta ∧ (∀ x, x < k → P (kth_S delta x)).
Proof.
induction k.
intros.
split.
simpl in H.
auto.
intros.
inversion H0.
intros.
assert (P delta ∧ ∀ x, x<k → P(kth_S delta x)).
apply IHk.
apply next_P_k_strong.
auto.
split.
destruct H0.
auto.
intros.
apply le_le_S_eq in H1.
destruct H1.
apply H0.
auto with arith.
apply eq_add_S in H1.
rewrite H1.
simpl in H.
destruct H.
apply H.
Qed.

Lemma next_P_k_strong2 : ∀ k delta P,
  next_P_k (S k) delta P → next_P_k k (S delta) P.
Proof.
induction k.
intros.
unfold next_P_k. fold next_P_k.
unfold next_P_k in H. rewrite kth_S_special in H.
destruct H. exact H.

intros.
unfold next_P_k. fold next_P_k.
split.
unfold next_P_k in H. fold next_P_k in H.
unfold kth_S. fold kth_S.
destruct H.
rewrite kth_S_sym in H.
unfold kth_S in H. fold kth_S in H.
rewrite kth_S_sym in H.
exact H.
apply IHk.
unfold next_P_k in H. fold next_P_k in H.
destruct H.
exact H0.
Qed.

Theorem nat_k_ind : ∀ k P,
  next_P_k k 0 P → (∀ n, P n → P(kth_S k n)) → ∀ n, P n.
Proof.
intros.
assert (∀ n:nat, next_P_k (S k) n P).
apply nat_ind.
unfold next_P_k. fold next_P_k.
split.
unfold kth_S.
assert (kth_S k 0=S k).
apply kth_S_special.
rewrite <- H1.
apply H0.
apply next_P_k_special with k.
exact H.

exact H.

intros.
unfold next_P_k. fold next_P_k.
split.
rewrite kth_S_sym.
apply H0.
apply next_P_k_strong2 in H1.
apply next_P_k_special with k.
exact H1.
apply next_P_k_strong2.
exact H1.
destruct H1 with n.
fold next_P_k in H3.
apply next_P_k_special with k.
exact H3.
Qed.

Lemma nat_simple_ind : ∀ P : nat → Prop,
   P 0 → (∀ n:nat, P n → P(S n)) → ∀ n, P n.
Proof.
exact (nat_k_ind 0).
Qed.

Lemma nat_double_ind : ∀ P : nat → Prop,
   P 0 → P 1 → (∀ n, P n → P(S(S n))) → ∀ n, P n.
Proof.
intros P H0 H1 Hind.
apply nat_k_ind with 1.
compute.
split.
exact H1. exact H0.
exact Hind.
Qed.

Lemma nat_triple_ind : ∀ P : nat → Prop,
   P 0 → P 1 → P 2-> (∀ n, P n → P(S (S (S n)))) → ∀ n, P n.
Proof.
intros P H0 H1 H2 Hind.
apply nat_k_ind with 2.
compute.
split.
exact H2. split.
exact H1. exact H0.
exact Hind.
Qed.

Lemma nat_strong_ind : ∀ P : nat → Prop,
  P 0 → (∀ n, (∀ k, k≤n → P k) → P(S n)) → ∀ n, P n.
intros.
assert (∀ n, (∀ k, k≤n → P k)).
apply (nat_ind (fun n⇒∀ k, k≤n → P k)).
intros.
apply le_n_O_eq in H1.
rewrite <- H1.
exact H.
intros.
apply le_le_S_eq in H2.
destruct H2.
apply H1.
auto with arith.
rewrite H2.
apply H0.
exact H1.
apply H1 with n.
auto with arith.
Qed.