问题标签 [lean]

我正在学习精益教程的第 4 章。

我希望能够证明简单的等式，例如a = b → a + 1 = b + 1 不必使用 calc 环境。换句话说，我想明确地构建以下证明项：

example (a b : nat) (H1 : a = b) : a + 1 = b + 1 := sorry

我最好的猜测是，我需要使用eq.subst标准库中关于自然数相等性的一些相关引理，但我不知所措。我能找到的最接近的精益示例是：

example (A : Type) (a b : A) (P : A → Prop) (H1 : a = b) (H2 : P a) : P b := eq.subst H1 H2

自从我开始阅读交互式精益教程以来，一个问题一直困扰着我：Prop内部分离层次结构的目的是什么Type？

据我现在了解，我们有以下 Universe 层次结构：

1. 边缘是否?真的有标记，或者我只是弥补它们（可能）？
2. 快速查看 Agda 和 Idris 似乎他们没有区分Sort n和Type n。为什么精益区分它们？

令人感到奇怪的Prop是，一方面它就像一个归纳类型（例如，它是封闭的事实意味着p ∧ nat没有意义），但另一方面却像一种类型一样使用（例如，通过构造一个证明值来显示类型 ）。我怀疑这与区别有关，但我无法表达清楚。有一些基本的论文可以阅读吗？p : Propp

我想赋予一个定义reducible。我很确定我的语法是正确的，因为我从教程 (p. 118)中逐字复制了它。

这两个属性的组合都没有通过语法检查：将其直接附加到定义会导致type expected at reducible，而独立声明会导致command expected。

我在 Windows 上，使用 Lean 3.1 二进制发行版和 VS Code 语言工具 fwiw，但它似乎在浏览器中也不起作用。

我试图在精益中证明，如果一个项目小于排序列表的头部，它就不是列表的成员。

在匹配t列表的尾部 as(y::ys)之后，我预计该假设Hs: is_sorted (h::t)会被传播，并添加is_sorted (y::ys)为假设（我发现 Idris 正是这样做的），但在 Lean 中似乎并非如此。此外，没有传播相等性t = (y::ys)，所以我不确定如何证明is_sorted (y::ys).

当模式匹配传播这个假设时，我需要做一些额外的事情吗？

我将 is_sorted 定义为：

_作为占位符的上下文中的假设是：

作为参考，Idris 的定义is_sorted，它在 Idris 中产生所需的行为：

伊德里斯证明：

我还尝试将 Lean 定义为更接近 Idris 定义，:向左移动以允许模式匹配：

但在这种情况下，Lean 抱怨invalid pattern, 'x' already appeared in this pattern（也适用于 h、y 和 ys）。如果我例如重命名h为h1，那么它会抱怨given argument 'h1', expected argument 'h'。我发现实际上似乎可以通过将x,y和ys参数设置为is_sorted_many隐式来解决此问题，因此不必匹配它们，但这似乎有点 hacky。

Lean 带有一个decidable_linear_order类型类，其中包含关于排序及其与相等关系的有用引理，例如：

lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a

这些排序中的等式都用 表示=：

我想知道是否有可能以某种方式扩展这个类（及其超类）以使用任意使用的定义相等关系R: α → α → Prop，该关系是自反的、对称的和传递的，或者这只能通过重写所有相关的引理及其证明来实现使用R而不是eq？

假设我有一个类型：

并且可以确定：

如果我有一个特定的列表：

def l1: list ℕ := [2,3,4,5,16,66]

是否可以证明它是在“编译时”排序的；生产is_sorted l1顶级产品？

我试过def l1_sorted: is_sorted l1 := if H: is_sorted l1 then H else sorry了，但我不知道如何证明后一种情况是不可能的。我也尝试过这种simp策略，但似乎没有帮助。

我可以用 来证明它#reduce，但不可能将它的输出分配给变量。

所以我们可以有明确的参数，用 表示()。
我们也可以有隐式参数，用 表示{}。

到目前为止，一切都很好。

但是，为什么我们还需要[]专门针对类型类的符号呢？

以下两者有什么区别：

我试图证明排序列表的尾部是在 Coq 中排序的，使用模式匹配而不是策略：

然而，这失败了，有：

我怀疑在基础微积分中是可能的，因为以下精益代码类型检查，并且精益也建立在 CIC 之上：

我试图从“精益定理证明”的第 7 章中理解归纳类型。

我为自己设定了一项任务，即证明自然数的后继具有替代等式的属性：

经过一些猜测和相当详尽的搜索后，我能够满足编译器的几种可能性：

我不明白我刚刚给出的任何证明实际上是如何工作的。

1. eq（归纳）类型的完整定义是什么？在 VSCode 中，我可以看到eqas的类型签名eq Π {α : Type} α → α → Prop，但看不到单个（归纳）构造函数（zero和succfrom的类似物natural）。我能在源代码中找到的最好的看起来不太正确。
2. 为什么eq.subst乐于接受一个证明(natural.succ a) = (natural.succ a)提供一个证明(natural.succ a) = (natural.succ b)？
3. 什么是高阶统一，它如何应用于这个特定的例子？
4. 我输入时收到的错误是什么意思#check (eq.rec_on H (eq.refl (natural.succ a)))，即[Lean] invalid 'eq.rec_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but the expected type must be known eq.rec_on : Π {α : Sort u} {a : α} {C : α → Sort l} {a_1 : α}, a = a_1 → C a → C a_1

假设以下定义：

请注意(n + m)在定义中翻转，以免插入add_symm定义。另外，请记住，这add / +是在精益中的 rhs 上定义的。vector是一个手工滚动的 nil / cons 定义的长度索引列表。

所以无论如何，首先我们有一个引理，它从定义中得出：

现在我们有一个不符合定义的引理，因此我用eq.rec它来制定它。

请注意，这eq.rec只是C y → Π {a : X}, y = a → C a.

通过对 的归纳，证明的想法是微不足道的v。基本案例紧随定义，递归案例应紧随归纳假设和定义，但我无法说服 Lean 相信这一点。

我从 Lean 得到的归纳假设是a_1 = eq.rec (a_1 ++ vector.nil) (zero_add n_1).

我如何将它与结论一起使用a :: a_1 = eq.rec (a :: a_1 ++ vector.nil) (zero_add (nat.succ n_1))？我可以unfold app将术语减少a :: a_1 ++ vector.nil到a :: (a_1 ++ vector.nil)，现在我被卡住了。