辅酶Q：归因于纳特和鳍的空，单位和布尔的归纳原理

问题描述

我可以像这样在Coq中定义有限类型：

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.

我可以仅从void和unit的归纳原理来证明bool，nat和fin的归纳原理吗？

我已经证明了void的归纳原理：

Lemma void_ind : forall (P : void -> Prop) (x : void),P x.
Proof.
  intros.
  inversion x.
Qed.

但是我不知道如何进行unit：

Lemma unit_ind : forall (P : unit -> Prop) (x : unit),P vunit -> P x.

我认为我需要：

Lemma unit_uniq : forall (x : fin 1),x = FZ.

在我看来，这似乎很明显，但是我不知道如何进行证明。

此后，我还想证明：

Lemma bool_ind : forall (P : bool -> Prop) (x : bool),P true -> P false -> P x.

解决方法

有许多方法可以得出这些归纳原理。既然你问 明确地关于为fin和nat使用归纳原理，我要 使用那些。实际上，由于所有派生类型都是有限的，我们可以逃脱 只需使用案例分析原理，我们就可以定义 感应。这是我们为自然数定义案例分析的方式。 （我是 将Type值的递归放在这里，因为我们需要额外的通用性。）

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).

我们可以为fin定义一个类似的原理。但是为了使其更有用，我们 加一点扭曲。 fin的原始递归通过 谓词P : forall n,fin n -> Prop必须对fin个 任意上限。我们将使用nat_case，以便我们可以确定上限 我们使用（请参见下面的P的类型）。

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.

感谢fin_case，我们可以定义您想要的归纳原理：

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).