如何使Coq在一个蕴含假设中简化表达式

Question

我试图证明以下引理：

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

Lemma even_Sn_not_even_n : forall n,
    even (S n) <-> not (even n).
Proof.
  intros n. split.
  + intros H. unfold not. intros H1. induction H1 as [|n' E' IHn].
    - inversion H.
    - inversion_clear H. apply IHn in H0. apply H0.
  + unfold not. intros H. induction n as [|n' E' IHn].
    -
Qed.

以下是我最终得到的内容：

1 subgoal (ID 173)

H : even 0 -> False
============================
even 1

我希望coq能够将"even 0"计算为true，"even 1"计算为false。我尝试了"simpl"、"apply ev_0 in H."，但它们都出错了。该怎么办？

- user4035

---

你还没有展示给我们“even”的定义。 - Perry

@Perry 已添加了定义。 - user4035

Answer 1

标题回答

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是Prop，而不是bool。看起来您混淆了类型True和False以及布尔值true和false。它们是完全不同的东西，在Coq的逻辑下不能互换。简而言之，even 0不会简化为true, True或其他任何东西。它就是even 0。如果您想展示even 0在逻辑上是正确的，您应该构建一个该类型的值。

我不记得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.

- Bubbler