Coq: induction principles for void, unit and bool from nat and fin

user_515276 0
Viewed 141

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.
coq
1 Answers

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 fins 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).
user_16337700
Related