coq-tactic
-
如何在coq中证明关于ListMap递归函数的定理？
-
如何在 Coq 中将 "Zneq_bool a b = true" 转换为 "a <> b" 的见证？
-
Coq XML 协议：可能是 PrintAST 故障
-
Coq 的 XML 协议文档中的 "editId" 是什么？
-
破坏固定点时，添加假设而不简化
-
在 Coq 中重写假设，保持蕴涵
-
在归纳的递归步骤中使用 Fixpoint 的 'unfold'
-
等同于 `remember (f x) as y eqn:H;清除 H；清除 x`？
-
战术自动化：简单的决策程序
-
"Ring" 不接受 CoqIde 中的策略
-
如何将 Coq 中的 `forall i: nat i < S k -> H` 分解为 `i < k and i=k`？
-
证明从递归定义的函数返回的列表在 Coq 中是固定长度的
-
绑定器下的泛化表达式
-
Coq：如何证明涉及字符串的 if 语句？
-
Coq：如何证明 max a b <= a+b？
-
elim 在 Coq 中如何在 /\ 和 \/ 上工作？
-
为什么策略 'exact' 对于 Coq 证明是完整的？
-
为什么 Coq 不能自己找出等式的对称性？
-
Eta转换策略？
-
在 Coq 中简化子公式