如何在 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 显式失败（如果你想 un-do/reset 分支中发生的事情）

（作为我的一个证明中的一个复杂示例，请考虑 try (split; unfold not; intro H'; inversion H'; fail)。这会尝试创建几个子分支 (split)，希望它们都是矛盾的并且可以通过inversion H'。如果这不起作用，inversions 只会造成一个大混乱，所以它明确地 fails 以取消策略链的效果。结束结果是很多无聊的案例自动解决，有趣的案例保持手动解决。）
以及更多——查看 Chapter 9 of the Coq Reference Manual ("The tactic language") 以获得对这些和许多其他有用结构的更详细描述。

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

How to repeat proof tactics in case in Coq?

coq

coq-tactic