# Library Coqtail.Arith.Nk_ind

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.

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.

commutativity of nested kth_S

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.

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.

special case of kth_S

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.

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.

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.

symmetry of kth_S

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.

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.

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.

introduction of next_P_k

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.

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.

elimination of next_P_k

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.

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.

next_P_k lower weakening

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.

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.

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.

Simple nat induction is a special case

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.

P 0 → (∀ n:nat, P n → P(S n)) → ∀ n, P n.

Proof.

exact (nat_k_ind 0).

Qed.

Double-step nat induction is a special case

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.

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.

Triple-step nat induction is a special case

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.

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.

Strong induction on nat

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.

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.