如何使 coq 简化蕴涵假设内的表达式

Question

我试图证明以下引理：

\n\n

Inductive even : nat \xe2\x86\x92 Prop :=\n| ev_0 : even 0\n| ev_SS (n : nat) (H : even n) : even (S (S n)).\n\nLemma even_Sn_not_even_n : forall n,\n    even (S n) <-> not (even n).\nProof.\n  intros n. split.\n  + intros H. unfold not. intros H1. induction H1 as [|n\' E\' IHn].\n    - inversion H.\n    - inversion_clear H. apply IHn in H0. apply H0.\n  + unfold not. intros H. induction n as [|n\' E\' IHn].\n    -\nQed.\n

\n\n

这是我最后得到的：

\n\n

1 subgoal (ID 173)\n\nH : even 0 -> False\n============================\neven 1\n

\n\n

我希望 coq 将“偶数 0”评估为 true，将“偶数 1”评估为 false。我尝试过simpl，apply ev_0 in H.但他们给出了错误。该怎么办？

\n

Answer 1

回答标题

\n\n

simpl in H.\n

\n\n

真实答案

\n\n

上面的代码将不起作用。

\n\n

even《逻辑基础》一书中对 的定义是：

\n\n

Inductive even : nat \xe2\x86\x92 Prop :=\n| ev_0 : even 0\n| ev_SS (n : nat) (H : even n) : even (S (S n)).\n

\n\n

even 0是一个 Prop，而不是 bool。看起来您正在混淆类型True和False以及布尔值true和false。它们是完全不同的东西，并且在 Coq 的逻辑下不能互换。简而言之，even 0不简化为true或True或任何东西。这只是even 0。如果你想even 0在逻辑上显示 is true，你应该构造一个该类型的值。

\n\n

我不记得 LF 中当时可以使用哪些策略，但这里有一些可能性：

\n\n

(* Since you know `ev_0` is a value of type `even 0`,\n   construct `False` from H and destruct it.\n   This is an example of forward proof. *)\nset (contra := H ev_0). destruct contra.\n\n(* ... or, in one step: *)\ndestruct (H ev_0).\n\n(* We all know `even 1` is logically false,\n   so change the goal to `False` and work from there.\n   This is an example of backward proof. *)\nexfalso. apply H. apply ev_0.\n

\n