在 Coq 定理中使用局部符号

Question

假设我想证明一个关于一个对象的定理，这个定理拼写起来很冗长，比如说 ABCDEFGHIJKLMNOPQRSTUVWXYZ，这样未缩写的定理是

Theorem verbose :
prop_1 ABCDEFGHIJKLMNOPQRSTUVWXYZ
-> prop_2 ABCDEFGHIJKLMNOPQRSTUVWXYZ
-> prop_3 ABCDEFGHIJKLMNOPQRSTUVWXYZ
-> prop_4 ABCDEFGHIJKLMNOPQRSTUVWXYZ
-> prop_5 ABCDEFGHIJKLMNOPQRSTUVWXYZ.

有没有办法在定理中使用局部符号，这样我就可以将它压缩成类似下面的形式？

Theorem succinct :
prop_1 X -> prop_2 X -> prop_3 X -> prop_4 X -> prop_5 X
where "X" := ABCDEFGHIJKLMNOPQRSTUVWXYZ.

如果我重复使用冗长的术语，我会使用常规符号，但对于一次性情况，如果定理有类似 where 的东西会很好，这样我就可以重用好的名字。

Answer 1

您可以使用Definition myobj := ABCDEFGHIJKLMNOPQRSTUVWXYZ. 为对象定义名称。稍后，您可以使用 unfold myobj. 将名称扩展为其值。

要将其引入本地证明环境，请使用remember。

Theorem foo:
    forall x y z : Z, x + y - z = x + (y - z).
    intros.
    remember (x+y) as bar.

现在的环境是

...
Heqbar : bar = x + y
============================
bar - z = x + (y - z)

Answer 2

您可以使用 Section 和 Let 进行本地定义。

Section thm.

Let X := ABCDEFGHIJKLMNOPQRSTUVWXYZ.

Theorem succinct : prop_1 X -> prop_2 X.

....

End thm.

在 Coq 定理中使用局部符号

Using local notation inside a Coq theorem

coq