时间戳

首页 > 解决方案 > 如何简化 Coq 中 True -> P 形式的假设？

coq - 如何简化 Coq 中 True -> P 形式的假设？

问题描述

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

标签： coqcoq-tactic

解决方案

除了使用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因为它会少一个参数。

推荐阅读