Coq 中的“intro ->”在上下文中是如何工作的？

Question

我对依赖类型定理证明者如何在上下文中进行替换感兴趣。我在 Coq 中找到了一个名为“intro ->”的东西，如下所述：

https://coq.inria.fr/refman/proof-engine/tactics.html#intropattern-rarrow-ex

在示例中，它表示目标：

x，y，z：自然

H : x = y

​​>

y = z -> x = z

会变成

x, z : 自然

H : x = z

---

x = z

在应用“intros ->”之后。

不知道将H:x = y 代入H:x = z 的步骤是怎么做的，这一步Coq 的逻辑规则是什么？这似乎是重写的一个步骤，根据我目前的知识，大多数重写都是根据等式，所以从 H:x = y 到 H:x = z 的替换应该来自像 (H:x = y ) = (H:x= z) ($\diamond$)，但是这样的等式是非良构的，因为原则上，我们要求等式的 LHS 和 RHS 具有相同的类型，所以这种相等（$\diamond$）取决于 y = z 的假设。

有人可以帮忙解释一下“intro ->”是如何工作的吗？我们是否需要参与像 ($\diamond$) 这样的“等式”？

Answer 1

在 Coq 中，重写上下文是一个派生的概念。本例中intros ->的策略大致等价于以下策略：

intros H'. rewrite H' in H. clear y H'.

策略rewrite H' in H.，反过来，大致相当于

revert H. rewrite H'. intros H.

换句话说，为了重写上下文，Coq 首先将所有相关假设转移到目标，重写目标，然后将假设带回上下文。

重写目标对相等类型使用以下消除原则：

forall [A : Type] [a : A] (P : A -> Prop), P a -> forall b : A, b = a -> P b

为了重写上面的H'，我们会：

A := T
a := z
P := fun c => x = c -> x = z
b := y

所以，

P b == x = y -> x = z
P a == x = z -> x = z

确实，在执行重写时，Coq 忽略了进出上下文的移动步骤，从 P b 变为 P a。