问题描述
我可以像这样在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.
解决方法
暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！
如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@）