I can define finite types in Coq like this:
Inductive fin : nat -> Set :=
| FZ : forall {n}, fin (S n)
| FS : forall {n}, fin n -> fin (S n).
Definition void := fin 0.
Definition unit := fin 1.
Definition vunit : unit := FZ.
Definition bool := fin 2.
Definition true : bool := FZ.
Definition false : bool := FS FZ.
Can I proof the induction principles for void
, unit
and bool
just from the induction principles of nat
and fin
?
I have proven the induction principle for void
already:
Lemma void_ind : forall (P : void -> Prop) (x : void), P x.
Proof.
intros.
inversion x.
Qed.
But I don't know how to proceed with unit
:
Lemma unit_ind : forall (P : unit -> Prop) (x : unit), P vunit -> P x.
I figure I need:
Lemma unit_uniq : forall (x : fin 1), x = FZ.
And in my head this seems obvious, but I don't know how to proceed with the proof.
After that I also like to prove:
Lemma bool_ind : forall (P : bool -> Prop) (x : bool), P true -> P false -> P x.
There are many ways of deriving these induction principles. Since you asked
explicitly about using the induction principles for fin
and nat
, I am going
to use those. Actually, since all the derived types are finite, we can get away
with just using a case analysis principle, which we can define in terms of
induction. Here is how we define case analysis for the natural numbers. (I am
putting the Type
valued recursor here, since we'll need the extra generality.)
Definition nat_case :
forall (P : nat -> Type),
P 0 ->
(forall n, P (S n)) ->
forall n, P n :=
fun P HZ HS => nat_rect P HZ (fun n _ => HS n).
We can define an analogous principle for fin
. But to make it more useful, we
add a little twist. The original recursor for fin
is parameterized over a
predicate P : forall n, fin n -> Prop
that must work for fin
s of an
arbitrary upper bound. We'll use nat_case
so that we can fix the upper bound
we use (cf. the types of P
below).
Inductive fin : nat -> Set :=
| FZ : forall {n}, fin (S n)
| FS : forall {n}, fin n -> fin (S n).
Definition fin_case_result n : fin n -> Type :=
nat_case (fun n => fin n -> Type)
(fun x : fin 0 =>
forall (P : fin 0 -> Type), P x)
(fun m (x : fin (S m)) =>
forall (P : fin (S m) -> Type),
P FZ ->
(forall y, P (FS y)) ->
P x)
n.
Definition fin_case :
forall n (x : fin n), fin_case_result n x :=
fun n x =>
fin_rect fin_case_result
( (* FZ case *)
fun m P HZ HS => HZ)
( (* FS case.
The blank is the result of the recursive call. *)
fun m (y : fin m) _ P HZ HS => HS y)
n x.
Thanks to fin_case
, we can define the induction principles you wanted:
Definition void := fin 0.
Definition unit := fin 1.
Definition vunit : unit := FZ.
Definition bool := fin 2.
Definition true : bool := FZ.
Definition false : bool := FS FZ.
Definition void_ind :
forall (P : void -> Prop)
(x : void),
P x :=
fun P x => fin_case 0 x P.
Definition unit_ind :
forall (P : unit -> Prop)
(HZ : P vunit)
(x : unit),
P x :=
fun P HZ x =>
fin_case 1 x P HZ (void_ind (fun y => P (FS y))).
Definition bool_ind :
forall (P : bool -> Prop)
(HT : P true)
(HF : P false)
(x : bool),
P x :=
fun P HT HF x =>
fin_case 2 x P HT (unit_ind (fun y => P (FS y)) HF).