$4$ Strong Induction

Let us divide the natural numbers into four classes: those evenly divisible by $4,$ those with remainder $1,$ remainder $2,$ and remainder $3.$ We can write an inductive type for the first and third classes as follows

Inductive div$4$ : nat $->$ Prop :$=$

$|$ div$4\_0$ : div$40$

$|$ div$4\_$S : forall n$,$ rem$2$ n $->$ div$4($S $($S n$))$

with rem$2$ : nat $->$ Prop :$=$

$|$ rem$2\_$S : forall n$,$ div$4$ n $->$ rem$2($S $($S n$)).$

We will prove that these two types are disjoint,

Lemma prob$4$ : forall n$,$ div$4$ n $->$ ~ rem$2$ n$.$

Strong induction is suggested for this problem, and remember that you can use the inversion tactic to unfold inductive definitions.

Use the template:

Require Import Arith.

Inductive acc : nat $->$ Prop :$=$ acc$\_$k : forall k$,($forall y$,$ y $<$ k $->$ acc y$)->$ acc k$.$

Theorem lt$\_$wf : forall n$,$ acc n$.$

Proof.

$($induction n$).$

$($apply acc$\_$k$).$

$($intros y H$).$

$($inversion H$).$

$($induction IHn$).$

clear H$0.$

$($apply acc$\_$k$).$

$($intros y Hlt$).$

$($apply acc$\_$k$).$

$($intros y$0$ Hlt$0).$

$($apply acc$\_$k$).$

$($intros y$1$ Hlt$1).$

$($apply H$).$

Require Import Arith.

$($apply le$\_$trans with $($m :$=$ y$0)).$

exact Hlt$1.$

$($apply le$\_$trans with $($m :$=$ y$)).$

$($apply lt$\_$le$\_$weak$).$

exact Hlt$0.$

$($apply le$\_$S$\_$n$).$

exact Hlt$.$

Qed.

Definition acc$\_$then$\_$Px :

forall $\{$P : nat $->$ Prop$\}($n : nat$),$

$($forall x$,($forall y$,$ y $<$ x $->$ P y$)->$ P x$)$

$->$ acc n

$->$ P n$.$

Proof.

refine $($fun P n f acc $=>$ acc$\_$ind $\_\_\_\_).$

$-$ intros k $\_$ f$\text{'}.$

apply f$.$

exact f$\text{'}.$

$-$ exact acc.

Defined.

Definition strong$\_$nat$\_$ind :

forall P : nat $->$ Prop,

$($forall x$,($forall y$,$ y $<$ x $->$ P y$)->$ P x$)$

$->$ forall x$,$ P x$.$

Proof.

refine $($fun P f x $=>\_).$

refine $($acc$\_$then$\_$Px $\_$ f $\_).$

apply lt$\_$wf$.$

Defined.

Inductive div$4$ : nat $->$ Prop :$=$

$|$ div$4\_0$ : div$40$

$|$ div$4\_$S : forall n$,$ rem$2$ n $->$ div$4($S $($S n$))$

with rem$2$ : nat $->$ Prop :$=$

$|$ rem$2\_$S : forall n$,$ div$4$ n $->$ rem$2($S $($S n$)).$

Lemma prob$4$ : forall n$,$ div$4$ n $->$ ~ rem$2$ n$.$

Proof.

Qed.