如何在精益中定义相互归纳命题？

我尝试使用归纳数据类型的语法,但它得到一条错误消息"互感类型必须编译为具有依赖消除的基本归纳类型".

下面是我尝试定义命题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)

还有一个相关的问题:定义相互递归函数的语法是什么？我似乎无法在任何地方找到它.

我认为Lean会自动尝试创建递归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,但由于某种原因,精益无法推断它(最后看到引理,我们必须Ce明确传递,否则精益推断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)