我如何简化形式为Coq的True-> P的假设？

Question

如果我在证明上下文中有一个看起来像H: True -> P的假设，并且想要将其转换为H: P，那么最简单的方法是什么？我尝试了simpl in H，但是它什么也没有做，而我发现的唯一方法是极其不令人满意的pose proof (H Coq.Init.Logic.I) as H。有没有更简单的方法？

Answer 1

除了使用pose proof以外，还有两种方法可以使用。

使用specialize。

此策略允许您为假设提供论据。您可以的话

specialize (H I).

甚至

specialize H with (1 := I).

并且如果要创建副本而不是直接实例化as，则可以使用H。

使用forward。

我认为这就是您想要的。 forward H.将要求您证明H的第一个假设。因此，您将执行以下操作：

forward H.
- auto.
- (* Then resume with H : P *)

但是您也可以为它提供（目标关闭）策略：

forward H by auto.
(* Now you have one goal, and H has type P *)

到目前为止，

forward尚未成为标准库的一部分。但是，可以很容易地定义它（这是MetaCoq库的定义）。

Ltac forward_gen H tac :=
  match type of H with
  | ?X -> _ => let H' := fresh in assert (H':X) ; [tac|specialize (H H'); clear H']
  end.

Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.

---

请注意，simpl在这里不起作用，因为按照通常的意义简化假设实际上并不是一种策略，实际上只是应用一些计算规则的策略，它基本上是评估目标或对其应用假设的方法。 True -> P不会减少为P，因为这样会减少一个参数。