我认为 Lean 会自动尝试创建递归器even.rec
并odd.rec
与之合作Type
,而不是Prop
. 但这不起作用,因为精益将逻辑世界(Prop
)和计算世界(Type
)分开。换句话说,我们可以只为了产生一个逻辑项而破坏一个逻辑项(证明)。请注意,如果您使用even
andodd
类型,您的示例将起作用ℕ → Type
。
Coq 证明助手是一个相关系统,它通过创建两个(相当弱且不切实际的)归纳原则自动处理这种情况,但它当然不会生成通用递归。
有一个解决方法,在这篇Lean wiki 文章中描述。它涉及编写相当多的样板文件。让我举一个例子,在这种情况下如何做到这一点。
首先,我们将互归纳类型编译成一个归纳族。我们添加一个表示均匀度的布尔索引:
inductive even_odd: bool → ℕ → Prop
| ze: even_odd tt 0
| ne: ∀ n, even_odd ff n → even_odd tt (n + 1)
| zo: even_odd ff 1
| no: ∀ n, even_odd tt n → even_odd ff (n + 1)
接下来,我们定义一些缩写来模拟互感类型:
-- types
def even := even_odd tt
def odd := even_odd ff
-- constructors
def even.z : even 0 := even_odd.ze
def even.n (n : ℕ) (o : odd n): even (n + 1) := even_odd.ne n o
def odd.z : odd 1 := even_odd.zo
def odd.n (n : ℕ) (e : even n): odd (n + 1) := even_odd.no n e
现在,让我们推出我们自己的归纳原则:
-- induction principles
def even.induction_on {n : ℕ} (ev : even n) (Ce : ℕ → Prop) (Co : ℕ → Prop)
(ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1))
(co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) : Ce n :=
@even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce)
ce0 (λ n _ co, stepe n co)
co1 (λ n _ ce, stepo n ce)
tt n ev
def odd.induction_on {n : ℕ} (od : odd n) (Co : ℕ → Prop) (Ce : ℕ → Prop)
(ce0 : Ce 0) (stepe : ∀ n : ℕ, Co n → Ce (n + 1))
(co1 : Co 1) (stepo : ∀ n : ℕ, Ce n → Co (n + 1)) :=
@even_odd.rec (λ (switch : bool), bool.rec_on switch Co Ce)
ce0 (λ n _ co, stepe n co)
co1 (λ n _ ce, stepo n ce)
ff n od
最好将Ce : ℕ → Prop
参数设为even.induction_on
隐式,但由于某种原因,Lean 无法推断它(参见最后的引理,我们必须Ce
显式传递,否则 Lean 推断Ce
与我们的目标无关)。情况与 对称odd.induction_on
。
定义相互递归函数的语法是什么?
正如这个精益用户线程中所解释的,对相互递归函数的支持非常有限:
不支持任意相互递归函数,但支持一个非常简单的情况。在我们定义了相互递归的类型之后,我们可以定义相互递归的函数来“镜像”这些类型的结构。
您可以在该线程中找到一个示例。但是,同样,我们可以使用相同的 add-a-switching-parameter 方法来模拟相互递归的函数。让我们模拟相互递归的布尔谓词evenb
和oddb
:
def even_oddb : bool → ℕ → bool
| tt 0 := tt
| tt (n + 1) := even_oddb ff n
| ff 0 := ff
| ff (n + 1) := even_oddb tt n
def evenb := even_oddb tt
def oddb := even_oddb ff
这是如何使用上述所有内容的示例。让我们证明一个简单的引理:
lemma even_implies_evenb (n : ℕ) : even n -> evenb n = tt :=
assume ev : even n,
even.induction_on ev (λ n, evenb n = tt) (λ n, oddb n = tt)
rfl
(λ (n : ℕ) (IH : oddb n = tt), IH)
rfl
(λ (n : ℕ) (IH : evenb n = tt), IH)