如何使 coq 简化蕴涵假设中的表达式答案

【问题标题】：How to make coq simplify expressions inside an implication hypothesis如何使 coq 简化蕴涵假设中的表达式
【发布时间】：2019-05-28 21:59:43
【问题描述】：

我试图证明以下引理：

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 将“偶数 0”评估为真，将“偶数 1”评估为假。我试过simpl，apply ev_0 in H.，但他们给出了一个错误。怎么办？

【问题讨论】：

你还没有向我们展示even的定义。
@Perry 添加了定义。

标签： coq logical-foundations

【解决方案1】：

回答题目

simpl in H.

真实答案

上面的代码不起作用。

Logical Foundations 书中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.

【讨论】：