Add translated LoVe materials and dependencies

lean/.lake/lakefile.olean.trace

@@ -0,0 +1,4 @@
+{"platform": "x86_64-w64-windows-gnu",
+ "options": {},
+ "leanHash": "128a1e6b0a82718382f9c39c79be44ff3284547c",
+ "configHash": "7063407093632191406"}

lean/LoVe copy/LICENSE.txt

@@ -0,0 +1,27 @@
+Copyright 2018–2025 Anne Baanen, Alexander Bentkamp, Jasmin Blanchette,
+Xavier Généreux, Johannes Hölzl, and Jannis Limperg
+
+Redistribution and use in source and binary forms, with or without modification,
+are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+this list of conditions and the following disclaimer in the documentation and/or
+other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its contributors
+may be used to endorse or promote products derived from this software without
+specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

lean/LoVe copy/LoVe01_TypesAndTerms_Demo.lean

@@ -0,0 +1,195 @@
+/- Copyright © 2018–2025 Anne Baanen, Alexander Bentkamp, Jasmin Blanchette,
+Xavier Généreux, Johannes Hölzl, and Jannis Limperg. See `LICENSE.txt`. -/
+
+import LoVe.LoVelib
+
+
+/- # LoVe 前言
+
+## 证明助手
+
+证明助手（也称为交互式定理证明器）
+
+* 检查并帮助开发形式化证明；
+* 可用于证明大型定理，而不仅仅是逻辑谜题；
+* 使用起来可能有些繁琐；
+* 具有高度成瘾性（类似于电子游戏）。
+
+以下是一些按逻辑基础分类的证明助手：
+
+* 集合论：Isabelle/ZF、Metamath、Mizar；
+* 简单类型理论：HOL4、HOL Light、Isabelle/HOL；
+* **依赖类型理论**：Agda、Coq、**Lean**、Matita、PVS。
+
+## 成功案例
+
+数学领域：
+
+* 四色定理（在 Coq 中证明）；
+* 开普勒猜想（在 HOL Light 和 Isabelle/HOL 中证明）；
+* 完美空间的定义（在 Lean 中定义）。
+
+计算机科学领域：
+
+* 硬件；
+* 操作系统；
+* 编程语言理论；
+* 编译器；
+* 安全性。
+
+## Lean
+
+Lean 是一个由 Leonardo de Moura（亚马逊网络服务）自 2012 年起主要开发的证明助手。
+
+其数学库 `mathlib` 由一个庞大的贡献者社区开发。
+
+我们使用 Lean 4 的社区版本。我们使用其基础库、`mathlib4` 和 `LoVelib` 等。Lean 是一个研究项目。
+
+优势：
+
+* 基于一种称为**归纳构造演算**的依赖类型理论，具有高度表达力的逻辑；
+* 扩展了经典公理和商类型；
+* 元编程框架；
+* 现代用户界面；
+* 文档；
+* 开源；
+* 无穷无尽的双关语来源（Lean Forward、Lean Together、Boolean，……）。
+
+## 我们的目标
+
+我们希望您能够：
+
+* 掌握交互式定理证明中的基础理论和技术；
+* 熟悉一些应用领域；
+* 培养一些可以在大型项目中应用的实用技能（作为爱好、硕士或博士研究，或在工业界）；
+* 准备好迁移到另一个证明助手并应用所学知识；
+* 充分理解该领域，能够开始阅读科学论文。
+
+本课程既不是纯粹的逻辑基础课程，也不是 Lean 教程。Lean 是我们的工具，而不是目的本身。
+
+# LoVe 演示 1：类型与项
+
+我们通过研究 Lean 的基础知识开始我们的旅程，首先从项（表达式）及其类型开始。 -/
+
+
+set_option autoImplicit false
+set_option tactic.hygienic false
+
+namespace LoVe
+
+
+/- ## Lean 概述
+
+初步来看：
+
+    Lean = 函数式编程 + 逻辑
+
+在今天的讲座中，我们将介绍类型和项的语法，这些语法与简单类型 λ-演算或类型化函数式编程语言（如 ML、OCaml、Haskell）中的语法相似。
+
+## 类型
+
+类型 `σ`、`τ`、`υ`：
+
+* 类型变量 `α`；
+* 基本类型 `T`；
+* 复杂类型 `T σ1 … σN`。
+
+某些类型构造器 `T` 是中缀形式的，例如 `→`（函数类型）。
+
+函数箭头是右结合的：
+`σ₁ → σ₂ → σ₃ → τ` = `σ₁ → (σ₂ → (σ₃ → τ))`。
+
+多态类型也是可能的。在 Lean 中，类型变量必须使用 `∀` 绑定，例如 `∀α, α → α`。
+
+## 项
+
+项 `t`、`u`：
+
+* 常量 `c`；
+* 变量 `x`；
+* 应用 `t u`；
+* 匿名函数 `fun x ↦ t`（也称为 λ-表达式）。
+
+__柯里化__：函数可以是
+
+* 完全应用的（例如，如果 `f` 最多可以接受 3 个参数，则 `f x y z`）；
+* 部分应用的（例如，`f x y`，`f x`）；
+* 未应用的（例如，`f`）。
+
+应用是左结合的：`f x y z` = `((f x) y) z`。
+
+`#check` 报告其参数的类型。 -/
+
+#check ℕ
+#check ℤ
+
+#check Empty
+#check Unit
+#check Bool
+
+#check ℕ → ℤ
+#check ℤ → ℕ
+#check Bool → ℕ → ℤ
+#check (Bool → ℕ) → ℤ
+#check ℕ → (Bool → ℕ) → ℤ
+
+#check fun x : ℕ ↦ x
+#check fun f : ℕ → ℕ ↦ fun g : ℕ → ℕ ↦ fun h : ℕ → ℕ ↦
+  fun x : ℕ ↦ h (g (f x))
+#check fun (f g h : ℕ → ℕ) (x : ℕ) ↦ h (g (f x))
+
+/- `opaque` 用于定义一个指定类型的任意常量。 -/
+
+opaque a : ℤ
+opaque b : ℤ
+opaque f : ℤ → ℤ
+opaque g : ℤ → ℤ → ℤ
+
+#check fun x : ℤ ↦ g (f (g a x)) (g x b)
+#check fun x ↦ g (f (g a x)) (g x b)
+
+#check fun x ↦ x
+
+
+/- ## 类型检查与类型推断
+
+类型检查和类型推断是可判定的问题（尽管如果添加了诸如重载或子类型等特性，这一性质会迅速丧失）。
+
+类型判断：`C ⊢ t : σ`，表示在局部上下文 `C` 中，`t` 具有类型 `σ`。
+
+类型规则：
+
+    —————————— Cst   如果 c 在全局中声明为类型 σ
+    C ⊢ c : σ
+
+    —————————— Var   如果 x : σ 是 C 中 x 的最右侧出现
+    C ⊢ x : σ
+
+    C ⊢ t : σ → τ    C ⊢ u : σ
+    ——————————————————————————— App
+    C ⊢ t u : τ
+
+    C, x : σ ⊢ t : τ
+    ——————————————————————————— Fun
+    C ⊢ (fun x : σ ↦ t) : σ → τ
+
+如果同一个变量 `x` 在上下文 C 中多次出现，最右侧的出现会遮蔽其他出现。
+
+## 类型可居性
+
+给定一个类型 `σ`，**类型可居性**问题在于找到一个具有该类型的项。类型可居性是不可判定的。
+
+递归过程：
+
+1. 如果 `σ` 的形式为 `τ → υ`，一个候选的可居项是一个匿名函数，形式为 `fun x ↦ _`。
+
+2. 或者，你可以使用任何常量或变量 `x : τ₁ → ⋯ → τN → σ` 来构建项 `x _ … _`。 -/
+
+opaque α : Type
+opaque β : Type
+opaque γ : Type
+
+def someFunOfType : (α → β → γ) → ((β → α) → β) → α → γ :=
+  fun f g a ↦ f a (g (fun b ↦ a))
+
+end LoVe

lean/LoVe copy/LoVe01_TypesAndTerms_ExerciseSheet.lean

@@ -0,0 +1,50 @@
+/- Copyright © 2018–2025 Anne Baanen, Alexander Bentkamp, Jasmin Blanchette,
+Xavier Généreux, Johannes Hölzl, and Jannis Limperg. See `LICENSE.txt`. -/
+
+import LoVe.LoVe01_TypesAndTerms_Demo
+
+
+/- # LoVe 练习 1：类型与项
+
+将占位符（例如，`:= sorry`）替换为你的解答。 -/
+
+
+set_option autoImplicit false
+set_option tactic.hygienic false
+
+namespace LoVe
+
+
+/- ## 问题 1：术语
+
+请通过替换 `sorry` 标记为预期类型的术语来完成以下定义。
+
+提示：在《Hitchhiker's Guide》的第 1.4 节中描述了一种系统化的方法来完成此操作。如该节所述，您可以在构造术语时使用 `_` 作为占位符。将鼠标悬停在 `_` 上时，您将看到当前的逻辑上下文。 -/
+
+def I : α → α :=
+  fun a ↦ a
+
+def K : α → β → α :=
+  fun a b ↦ a
+
+def C : (α → β → γ) → β → α → γ :=
+  sorry
+
+def projFst : α → α → α :=
+  sorry
+
+/- 请提供与 `projFst` 不同的答案。 -/
+
+def projSnd : α → α → α :=
+  sorry
+
+def someNonsense : (α → β → γ) → α → (α → γ) → β → γ :=
+  sorry
+
+
+/- ## 问题2：类型推导
+
+展示你在上面定义的 `C` 的类型推导过程，可以使用纸笔或ASCII/Unicode艺术。你可能会发现字符 `–`（用于绘制水平线）和 `⊢` 很有用。 -/
+
+-- 请将您的解决方案写在评论中或纸上。
+end LoVe

lean/LoVe copy/LoVe01_TypesAndTerms_HomeworkSheet.lean

@@ -0,0 +1,61 @@
+/- Copyright © 2018–2025 Anne Baanen, Alexander Bentkamp, Jasmin Blanchette,
+Xavier Généreux, Johannes Hölzl, and Jannis Limperg. See `LICENSE.txt`. -/
+
+import LoVe.LoVelib
+
+
+/- # LoVe 作业 1（10 分）：类型与项
+
+将占位符（例如，`:= sorry`）替换为你的解答。 -/
+
+
+set_option autoImplicit false
+set_option tactic.hygienic false
+
+namespace LoVe
+
+
+/- ## 问题 1（6 分）：术语
+
+我们首先声明四个新的不透明类型。 -/
+
+opaque α : Type
+opaque β : Type
+opaque γ : Type
+opaque δ : Type
+
+/- 1.1 (4 分). 请通过提供具有预期类型的术语来完成以下定义。
+
+请为绑定变量使用合理的名称，例如 `a : α`、`b : β`、`c : γ`。
+
+提示：在《Hitchhiker's Guide》的第 1.4 节中描述了一种系统化的方法。如该节所述，您可以在构造术语时使用 `_` 作为占位符。将鼠标悬停在 `_` 上时，您将看到当前的逻辑上下文。 -/
+
+def B : (α → β) → (γ → α) → γ → β :=
+  sorry
+
+def S : (α → β → γ) → (α → β) → α → γ :=
+  sorry
+
+def moreNonsense : ((α → β) → γ → δ) → γ → β → δ :=
+  sorry
+
+def evenMoreNonsense : (α → β) → (α → γ) → α → β → γ :=
+  sorry
+
+/- 1.2 （2分）。完成以下定义。
+
+这个看起来更难一些，但如果你按照《Hitchhiker's Guide》中描述的程序操作，应该会相当直接。
+
+注意：Peirce的发音类似于英语单词“purse”。 -/
+
+def weakPeirce : ((((α → β) → α) → α) → β) → β :=
+  sorry
+
+/- ## 问题 2（4 分）：类型推导
+
+请使用 ASCII 或 Unicode 艺术展示你上面定义的 `B` 的类型推导过程。你可能会发现字符 `–`（用于绘制水平线）和 `⊢` 很有用。
+
+可以自由引入缩写，以避免重复较大的上下文 `C`。 -/
+
+-- 请将您的解决方案写在这里。
+end LoVe