问题标签 [coq-tactic]

考虑以下发展：

如果我有一个假设stream_le (scons h1 t1) (scons h2 t2)，那么将destruct其转化为一对假设R h1 h2和的策略是合理的eqA h1 h2 -> stream_le t1 t2。但这不是发生的事情，因为destruct每当做任何不平凡的事情时都会丢失信息。相反，新术语h0, h3, t0,t3被引入上下文中，但不记得它们分别等于h1, h2, t1, t2。

我想知道是否有一种快速简便的方法可以做到这种“智能destruct”。这是我现在拥有的：

我想在保留旧版本的同时重写一个假设，并将重写的结果保存在一个新名称下。我该怎么做？

我正在尝试为我编写的矩阵库创建一个提示重写数据库。但是当我写

Hint Rewrite kron_1_r : M_db

我收到以下错误：

Cannot infer the implicit parameter m of kron_1_r whose type is "nat".

kron_1_r具有 type forall {m n : nat} (A : Matrix m n), A ⊗ Id 1 = A，因此 m 和 n 应在调用 autorewrite 时根据上下文推断。我不确定为什么它需要一个参数，或者如何告诉它推迟。

如何rewrite在 ltac 中调用以仅重写一次出现？我认为 coq 的文档中提到了一些内容，rewrite at但我无法在实践中实际使用它，也没有示例。

这是我正在尝试做的一个例子：

假设我有以下设置：

我尝试使用自定义策略来证明一个简单的定理：

这失败了，因为目标不是形式adt (CE ?N)而是形式adt (nat_to_exp ?N)（这在使用时明确显示Set Printing Coercions）。

试图证明一个稍微不同的定理是可行的：

我知道的可能的解决方法：

• 不使用强制。
• 在策略中展开强制（带有unfold nat_to_exp）。这稍微缓解了问题，但是一旦引入了该策略不知道的新强制，就会失败。

理想情况下，如果在展开所有定义后模式匹配，我希望模式匹配成功（当然，定义不应保持展开）。

这可能吗？如果不是，有什么理由不可以吗？

我试图在 Coq 中定义不同类型的等式。在大学课程中，我的教授给了我们四种不同类型的规则，如下（我只提供规则的链接）：

• 根岑：https ://ibb.co/imQOCF
• 莱布尼茨：https ://ibb.co/n0uBzv
• 马丁-洛夫：https ://ibb.co/fALZKv
• 路径归纳：https ://ibb.co/esZuKv

这四种类型的区别在于C型。

我试图证明它们之间的同构。不幸的是，我在将第一个和第二个声明为归纳类型时遇到了一些麻烦，因为我找不到指定类型 C 的方法。我有第三个和第四个的定义，并且我已经证明了它们之间的同构。

提前致谢。

我在这里和 Coq 一起研究我定义的两种类型之间的关系。第一个类似于 的有限子集nat，只有三个元素：

第二种是 sigma 类型，其元素满足命题{x: nat | x < 3}。这是它的定义：

我想证明这两种类型是同构的。我以以下方式定义了涉及的两个函数：

其中l_0_3, l_1_3, 和l_2_3只是公理：

我成功定义了同构的第一部分

但我无法定义另一面。这是我到目前为止所做的：

我完全不确定定义的其余部分。我也尝试在 onx和 on 上进行模式匹配(N3_to_lt3 (lt3_to_N3 x))，但我不确定要返回什么。

谢谢您的帮助。

我根据不相交和的定义定义了一个布尔归纳类型：

给定两种类型A，B我试图证明之间的同构

和

我设法证明了同构的一方面

但是我在证明另一方时遇到了麻烦，主要是因为我没有设法在不同之间建立平等，x并且p涉及以下证明：

有谁知道我如何证明后一个引理？

谢谢您的帮助。

我正在尝试编写一个返回值的策略，并且在这样做的过程中它需要检查某些东西是否是一个 evar。

不幸的是，我不能使用is_evar，因为那时该策略不被视为返回值（而是另一种策略）。下面是一个例子。

有什么建议么？

I am trying to proof that the application of an empty Substitution on a term is equal to the given term. Here is the code:

I am trying to proof some properties of this function.

I am stuck after the reflexivity. I wanted to do induction on the list build in a term but if i do so i'ĺl get stuck in a loop. i will appreciate any help.