问题标签 [lean]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
lean - 定理中命题的大括号和圆括号之间的区别
我对在定理中使用大括号表示命题感到非常困惑。请参阅以下四个片段：
我想，它们都是一样的，但显然它们不是，因为当我想使用contraprositive_1并contraprositive_2在另一个定理的证明中，lean显示类型不匹配的错误：
术语 h1 具有类型 P → Q : Prop 但预计具有类型 Prop : Type
另一方面，contraprositive_3工作contraprositive_4正常。
大括号和圆括号有什么区别？
theorem-proving - 如何通过精益中的归纳简化证明？
我想通过精益中的归纳来简化证明。
我在 Lean 中定义了一个具有 3 个构造函数的归纳类型，并在此类型上定义了一个二元关系。我已经包含了这些公理，因为 Lean 不允许我将它们作为 rel 的构造函数。
一个目标是证明以下定理：
我已经通过对 x、y 和 z 的归纳证明了这一点；“z”来自上面 pw_o_2 的定义。但是证明很长（约 136 行）。还有另一种方法可以得到更短的证明吗？
functional-programming - 将函数定义为 codomain 的子集
我正在尝试将函数
f : A → B 的图像限制定义为 f': A → f[A]，其中 f'(a) = f(a) 。但是，我不确定如何在精益中定义它。
在我看来，最直观的定义方式是：
但是，这会被拒绝，因为 (fa) 不是 B 类型（图像 f set.univ）。
我什至尝试证明 f(a) ∈ (image f univ) 。它没有帮助：
错误信息是：
set.univ 和 image 在 data.set 中定义如下
知道如何做到这一点吗？
lean - 如何在 Emacs 中为 Lean 2 切换到 HoTT 模式
我从 github 存储库编译了 Lean 2。然后，按照 scr/emacs/README.md 中的说明，我修改了我的 .emacs 文件，打开一个文件，单击“创建新项目”，单击“打开”，输入“hott”并按 Enter。
然后我输入
我收到了一条消息
我也尝试lean-hott-mode了相同结果的命令。
我究竟做错了什么？
lean - 例如： (p ∨ q) ∧ (p ∨ r) → p ∨ (q ∧ r)
精益定理证明的第 3.6 节显示以下内容：
由于这涉及到iff，我们先演示一个方向，从左到右：
要走向另一个方向，我们必须展示：
鉴于本书到目前为止显示的示例，这个不同之处在于左侧涉及两个 or表达式......所以似乎我必须使用or.elim两次......
我搞砸了一些方法。这是一个嵌套or.elim在另一个内部的一个：
这里让我感到奇怪的一件事是以下表达式出现了两次：
有没有不涉及这种重复的方法？
有没有更惯用的方法？
theorem-proving - 精益：证明 \not p \to (p \ to q) 或类似的 false \to p
我是精益证明的新手，我正在尝试解决在线教程中的示例。
我被这个例子困住了，我需要证明“假暗示q”或类似的东西。我的代码是：
我不认为定义 hnpq 会有所帮助，因为这个证明是 (¬ p ∨ q) → (p → q) 的一部分。在集合论中，我认为 false 意味着一切。
有什么建议或想法吗？
agda - Agda 如何推断 `Vec.foldl` 的隐含参数？
当把上面的函数翻译成精益时，我震惊地发现它的真实形式实际上就像......
我发现 Agda 能够f正确推断出隐含的论点确实令人印象深刻。它是如何做到的？