coq - 如何在 Coq 中重复证明策略？

Question

我想通过添加一个定理来扩展 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 中是否有重复 - 介绍 H;简单；非一月份的反身性。 案例证明(所以我只有两个 - 或类似的东西，所以我不必重复自己)？或者我只是完全以错误的方式进行了这个证明？

Answer 1

实现此目的的一种方法是

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应用策略t2到应用程序创建的所有分支 战术t1 .
• try t尝试运用策略t (顾名思义)或者什么都不做 如果t失败。

它的作用是运行 induction像以前一样，然后立即运行 reflexivity在所有分支上(适用于并解决除一月分支之外的所有分支)。之后，你就剩下那个单一的分支，这可以通过 contradiction 来解决。和以前一样。

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

• (t1 ; t2)哪组战术t1和t2 ,
• t1 | t2 , t1 || t2 , t1 + t2这是“try t1 和 if 失败/没有做任何有用的事情/…，做 t2相反，

• fail明确失败(如果您想撤消/重置，这很有用 分支中发生了什么)

  (作为我的一个证明中的一个复杂示例，请考虑 try (split; unfold not; intro H'; inversion H'; fail) 。这尝试创建几个子分支( split )，希望它们都是矛盾的并且可以通过 inversion H' 来解决。如果那样不起作用， inversion 只会造成大困惑，因此它明确地 fail 是为了消除策略链的影响。最终结果是许多无聊的情况会自动解决，而有趣的情况会被自动解决。对于手动求解，保持不变。)

• 还有更多 - 查看 Chapter 9 of the Coq Reference Manual ("The tactic language")有关这些和许多其他有用结构的详细说明。