【发布时间】：2016-06-08 21:07:42
【问题描述】：
是否可以在当前证明定理的上下文中创建嵌套定理？
我有一种强烈的感觉，这个功能还没有完全实现。 例如，
1) 我无法破坏证明过程中上下文中的某些类型。
例如有
"Error: my_var is used in conclusion."
当我试图定义定理的类型时。我也有
"Error: ... depends on the variable ... which is not declared in the context."
但谷歌只给了我一个类似错误的链接。此外，我实际上在本节的上下文中有 m。怎么了？
2) 我破坏了自然数 n。 我定义了几个第一步。 我需要定义一个长期的同义词。 我要本地定义
Definition X:=(n.+1;ob).
但我不能。我想用类比让 ... in ... 。
有什么想法吗？
【问题讨论】：
-
第二部分：
remember (<some long term>) as X可能有用。 -
对于第一部分，您可以使用
assert (H: forall n, n+n=2*n).并开始证明它，然后可以在您的证明中使用H。它没有在全局上下文中声明，仅在您正在处理的特定子目标中声明。
标签： coq