如何使coq简化隐含假设中的表达式

标题的答复

simpl in H.

真实答案

定义 even

Inductive even : nat → Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

even 0 是个道具,不是傻瓜。看起来你把类型弄混了 True 和 False true 和 false . 它们是完全不同的东西,按照Coq的逻辑是不可互换的。简言之 不简化为 或 或者别的什么。只是 偶数0 . 如果你想展示 偶数0 如果逻辑上为true,则应构造该类型的值。

我不记得在LF中有哪些战术可用,但这里有一些可能性:

(* Since you know `ev_0` is a value of type `even 0`,
   construct `False` from H and destruct it.
   This is an example of forward proof. *)
set (contra := H ev_0). destruct contra.

(* ... or, in one step: *)
destruct (H ev_0).

(* We all know `even 1` is logically false,
   so change the goal to `False` and work from there.
   This is an example of backward proof. *)
exfalso. apply H. apply ev_0.