如何定义精益中的互归纳命题?

问题描述 投票:0回答:2

我尝试使用归纳数据类型的语法,但收到错误消息“互归纳类型必须编译为具有依赖性消除的基本归纳类型”

下面是我尝试在自然数上定义命题

even
odd
的示例

mutual inductive even, odd
with even: ℕ → Prop
| z: even 0
| n: ∀ n, odd n → even (n + 1)
with odd: ℕ → Prop
| z: odd 1
| n: ∀ n, even n → odd (n + 1)

还有一个相关问题:定义相互递归函数的语法是什么?我似乎在任何地方都找不到它的记录。

dependent-type theorem-proving mutual-recursion lean
2个回答
5
投票

我认为精益会自动尝试创建递归器

even.rec
odd.rec
来使用
Type
,而不是
Prop
。但这是行不通的,因为精益将逻辑世界 (
Prop
) 和计算世界 (
Type
) 分开。换句话说,我们只能破坏一个逻辑项(证明)来产生一个逻辑项。请注意,如果您制作了
even
odd
类型为
ℕ → Type
,那么您的示例将会起作用。

Coq 证明助手是一个相关系统,它通过创建两个(相当弱且不切实际的)归纳原理来自动处理这种情况,但当然它不会生成通用递归。

有一个解决方法,在这篇精益维基文章中描述。它涉及编写大量的样板文件。让我举一个例子,如何针对这种情况进行操作。

首先,我们将互归纳类型编入归纳族。我们添加一个代表均匀度的布尔索引:

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
对称。

定义相互递归函数的语法是什么?

正如这个精益用户线程中所解释的,对相互递归函数的支持非常有限:

不支持任意相互递归函数,但支持非常简单的情况。 在定义了相互递归类型之后,我们可以定义“镜像”这些类型的结构的相互递归函数。

您可以在该线程中找到一个示例。但是,我们可以使用相同的添加切换参数方法来模拟相互递归函数。让我们模拟一下相互递归的布尔谓词

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)

0
投票

问题和现有答案是关于旧版本的精益。在精益 4 中,互归纳命题的问题为零 – 以下效果很好:

mutual
inductive Even: Nat → Prop
| zero: Even 0
| succOdd: Odd n → Even n.succ

inductive Odd: Nat → Prop
| succEven: Even n → Odd n.succ
end

这里有一个简单的方法来使用它们来证明两个是偶数:

def twoIsEven: Even 2 := Even.succOdd (Odd.succEven Even.zero)
© www.soinside.com 2019 - 2024. All rights reserved.