如何在 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 中是否有在非 1 月份重复 - intro H; simpl; reflexivity. 案例证明（所以我只有两个 - 或类似的东西，所以我不必重复自己）？还是我只是完全以错误的方式处理这个证明？

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 是“尝试t1 和如果 失败/没有做任何有用的事情/……，改为t2，

• fail 显式失败（如果您想撤消/重置，这很有用 分支发生了什么）

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

• 还有更多 - 查看Chapter 9 of the Coq Reference Manual ("The tactic language") 以获得对这些和许多其他有用结构的详细描述。