标签: lean

在 Haskell 中，我可以使用括号将中缀运算符 like 转换+为前缀函数，因此(+) 2 3与 相同2 + 3。Lean中有类似的功能吗？

当对cases归纳数据类型使用 - 策略时，精益会生成多个案例，但不会创建说明当前案例假设的假设。例如：

inductive color | blue | red\n\ntheorem exmpl (c : color) : true :=\nbegin\n    cases c,\nend\n

导致以下战术状态

case color.blue\n\xe2\x8a\xa2 true\ncase color.red\n\xe2\x8a\xa2 true\n

但没有创建一个单独的假设（如c = color.red）来使用。你如何得到这样的假设？

如何在 Lean 4 中创建 TCP 套接字并接受传入连接或连接到远程地址？换句话说，如何在 Lean 4 中实现 TCP 服务器或客户端？

section\nopen classical\nexample : \xc2\xac (A \xe2\x86\x94 \xc2\xac A) :=\nhave hn : (A \xe2\x88\xa8 \xc2\xac A), from sorry,\n  assume h : (A \xe2\x86\x94 \xc2\xac A),\n  show false, from or.elim hn\n    (assume h1 : A, h.mp h1 h1)\n    (assume h2 : \xc2\xac A, h2 (h.mpr h2))\nend\n

我正在阅读 Jeremy Avigad 的《逻辑与证明》一书来学习精益。问题是我只能用by_contradiction战术来应对排中法则。有人可以帮我吗？

我是一个初学者，我遇到了以下问题：

import tactic.linarith\nimport tactic.suggest\n\nnoncomputable theory\nopen_locale classical\n\nlemma two_ne_four_mul_any (n:\xe2\x84\x95) : 2 \xe2\x89\xa0 2 * 2 * n := begin\n  cases n,\n  linarith,\n  rw mul_assoc,\n  ???\nend\n

现在的状态是：

n : \xe2\x84\x95\n\xe2\x8a\xa2 2 \xe2\x89\xa0 2 * (2 * n.succ)\n

它看起来如此微不足道，以至于我认为必须有一种策略来解决它。但 linarith、ring、simpl、trivial 不起作用。

那么，我是否错过了一些重要的内容？

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

n : \xe2\x84\x95\n\xe2\x8a\xa2 1 \xe2\x89\xa0 2 * n.succ\n

希望某些更高级别的策略现在能够看到这是真的。但是，我不知道如何对方程两边进行一些操作。两边都除以2不是应该有可能吗？

我的计划是继续将 rhs 更改为 2*(n+1) 和 2n+2，也许目标是

\xe2\x8a\xa2 0 \xe2\x89\xa0 2 * n + 1\n

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

我正在尝试学习精益，并且试图弄清楚如何I*M = {i*m | i in I, m in M}从理想的I和R模块M 创建新的R模块。

因此，我的尝试是首先定义一个映射ideal_mult，该映射将创建一个新的R模块，然后弄清楚如何为其分配一个好的符号。

import ring_theory.ideals
import algebra.module

universes u v
variables {R : Type u} {M : Type v}
variables [comm_ring R] [add_comm_group M] [module R M]
variables (I: ideal R)

def ideal_mult (I: ideal R) (M: Type v)
        [add_comm_group M] [module R M]: Type v
        :=
    sorry

#check ideal_mult I M

我该如何定义它，以便例如举例说明一个假设(h: I*M = M)？

感谢您的帮助！

我开始学习Lean编程语言https://leanprover.github.io

我发现有函数、结构、if/else 和其他常见的编程命令。

然而，我还没有找到任何可以处理的事情loops。有没有一种方法可以在精益中迭代或重复代码块？类似于其他语言for或while其他语言的东西。如果是这样，请添加语法或示例。

先感谢您。

我想在精益定理证明器中证明这个定理。首先，我需要定义部分有序集合之类的东西，以便我可以定义 infimum/supremum。这在精益中是如何完成的？本教程提到了 setoids，它们是具有关联等价关系的类型。但我不清楚这有什么帮助。