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

Question

我想通过添加一个定理来扩展Coq'Art中的练习6.10，该定理是：对于不是1月的所有月份，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月份的月份重复案例证明（所以我只有两个-或类似的东西，所以我不必重复自己）？还是我只是以错误的方式完全使用了这种证明？

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会创建一个大分支一团糟，所以它显式地fail是s，以便撤消战术链的影响。最终结果是，许多无聊的情况会自动得到解决，而有趣的情况对于手动解决仍保持不变。）

• 以及更多–请参阅Coq参考手册的第9章（“战术语言”），以获取对这些以及许多其他有用构造的详细说明。