4

我想通过添加一个定理来扩展 Coq'Art 中的练习 6.10，即对于所有非一月的月份，is_January 将等于 false。

我对月份的定义如下：

 Inductive month : Set :=
   | January : month
   | February : month
   | March : month
   | April : month
   | May : month
   | June : month
   | July : month
   | August : month
   | September : month
   | October : month
   | November : month
   | December : month
  .

Check month_rect.

我对 is_January 的定义如下：

Definition is_January (m : month) : Prop :=
  match m with
  | January => True
  | other   => False
  end.

我正在执行以下操作以测试它是否正确。

Eval compute in (is_January January).
Eval compute in (is_January December).

Theorem is_January_eq_January :
  forall m : month, m = January -> is_January m = True.
Proof.
  intros m H.
  rewrite H.
  compute; reflexivity.
Qed.

我对这个定理的证明不是很满意。

Theorem is_January_neq_not_January :
  forall m : month, m <> January -> is_January m = False.
Proof.
  induction m.
  - contradiction.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
  - intro H; simpl; reflexivity.
Qed.

无论如何，Coq 中是否有在- intro H; simpl; reflexivity.非 1 月份重复案例证明（所以我只有两个 - 或类似的东西，所以我不必重复自己）？还是我只是以错误的方式完全解决这个证明？

4

1 回答 1

8

一种方法是

Theorem is_January_neq_not_January :
  forall m : month, m <> January -> is_January m = False.
Proof.
  induction m; try reflexivity.
  contradiction.
Qed.
  • simpl是隐含的reflexivity，因此是不必要的。
  • t1 ; t2将 tactic 应用于t2由 tactic 应用创建的所有分支t1。
  • try t尝试应用策略t（顾名思义），如果t失败则什么也不做。

它的作用是induction像以前一样运行，然后立即reflexivity在所有分支上运行（它适用于并解决除了一月分支之外的所有分支）。在那之后，你只剩下那个单一的分支，可以contradiction像以前一样解决。

对于更复杂的情况，其他可能有用的结构是

  • (t1 ; t2)哪一组战术t1和t2,
  • t1 | t2, t1 || t2，t1 + t2它们是“尝试t1，如果失败/没有做任何有用的事情/……，t2改为做，

  • fail显式失败（如果您想撤消/重置分支中发生的事情，这很有用）

    （作为我的一个证明中的一个复杂示例，考虑try (split; unfold not; intro H'; inversion H'; fail)。这试图创建几个子分支 ( split)，希望它们都是矛盾的并且可以通过 解决inversion H'。如果这不起作用，inversions 只会创建一个大乱七八糟，所以它明确地fail是为了取消战术链的影响。最终结果是许多无聊的案例被自动解决，而有趣的案例保持不变，手动解决。）

  • 还有更多——查看Coq 参考手册（“战术语言”）的第 9 章，以获得对这些和许多其他有用结构的详细描述。

于 2017-05-07T01:32:54.607 回答