问题标签 [lean]

让我们看一些引理的例子（它的陈述以及它是否正确与这个讨论无关）：

我想在这里强调的一点是，当用该策略破坏我的假设时，cases除了多次使用该策略（可以说每个“层”一次）之外，我不知道任何其他方法。

如果我在 Coq 中查看相同的引理：

我可以用一个嵌套的模式匹配来破坏我的假设。

我猜我可以在精益中做同样的事情，但我不知道怎么做。我会很感激被告知，因为我发现嵌套模式匹配在实践中非常方便。

我有兴趣做一个依赖自动证明的项目，作为一种学习练习。到目前为止，我的在线搜索表明，理论上精益是要走的路。

然而，我读到的所有关于它的内容都是关于在 VS 代码或 Emacs 中将其用作证明助手。但这不是我需要的，我需要一个可以完全以编程方式与之通信的系统。IE 假设字符串进入 -> 指定可扣除性的字符串出现或类似的东西。

更准确地说，我需要能够在字符串上调用解析函数，这些函数完成了确定一组结果是否可以从输入假设中推导出来的繁重工作。

我找不到有关 Lean 能够做到这一点的文档。

通过证明可调查性，我理解人类用户可以“追踪”证明的所有细节这一事实。有些事情不容易追踪。例如，SMT 证明基于特定的启发式，然后将其转换为证明者。在这种情况下，拥有简单的机制（无需专家即可让您使用）来扫描证明失败的原因或检查证明过程的内部结构可能很有用。

我想知道与 Coq 或 Isabelle 相比，Lean 是否增强了这种证明可测量性。我通过A Metaprogramming Framework for Formal Verification得到的印象可能是这种情况。

当留下一个ite ("a"="b") x y涉及两个不同字符串文字之间可判定相等的形式的表达式时，似乎simp它本身不允许我将此表达式简化为y. ite ("a"="a") x y这与简化为xwith的情况相反simp。所以我发现自己在做一个案例分析cases decidable.em ("a"="b") with H H，然后使用exfalsoand处理一个案例dec_trivial，另一个使用simp [H]. 所以我能够继续前进，但我想知道是否有更惯用和更短的方法来实现相同的结果。

我试图用精益定理证明者证明 ¬ (A ∧ B) → (A → ¬ B)。我已经这样设置了。

我已经尝试对 h1 使用 and.left 和 and.right ，但是当连词被否定时，这些都不起作用。我找不到任何从否定开始证明这种暗示的例子。任何帮助将非常感激。

我试图解决这个问题，但不能，有什么帮助吗？到目前为止我的解决方案：

下面是我的错误尝试。关于如何进行的任何建议？

我是一个初学者，我坚持以下几点：

现在的状态是：

它看起来如此微不足道，以至于我认为必须有解决它的策略。但是 linarith, ring, simp, trivial 不起作用。

那么，我错过了一些重要的进口吗？

我还尝试使用现有的引理来解决这个问题。第一步，我想达到：

希望现在一些更高级别的策略会看到这是真的。但是，我不知道如何在等式的两边进行一些操作。难道不应该以某种方式将两边除以2吗？

我的计划是通过将 rhs 更改为 2*(n+1) 和 2n+2 来进行，也许目标是

希望在图书馆中找到适用的引理。

我证明了一些相当琐碎的引理

显然，同样适用于非负整数、有理数、实数等：

一般来说，如果我们有p n一些n:nat，我们应该能够得出结论0 ≤ z → p' zp' 与 p “相同”。但是，我什至不知道如何在精益中制定这一点，更不用说如何证明它了。

所以，问题是，这可以在精益中得到证明吗？如何去做呢？

一项发现 Setoids 广泛用于 Agda、Coq 等语言……事实上，Lean 等语言认为它们可以帮助避免“Setoid Hell”。首先使用 Setoids 的原因是什么？转向基于HoTT（例如立方体Agda）的扩展类型理论是否会减少对Setoids的需求？