Как определить взаимные индуктивные предложения в Lean?

Question

Я пытаюсь использовать синтаксис для индуктивных типов данных, но получил сообщение об ошибке «взаимно индуктивные типы должны компилироваться в базовый индуктивный тип с зависимым устранением».

Ниже приведен пример моей попытки определить положения 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) 

также связанный с этим вопрос: Что такое синтаксис для определения взаимно рекурсивных функций? Кажется, я не могу найти его документально.

Answer 1

Я думаю, что Lean автоматически пытается создать recursors even.rec и odd.rec работать с Type, не Prop. Но это не работает, потому что Lean разделяет логический мир (Prop) и вычислительный мир (Type). Другими словами, мы можем разрушить логический термин (доказательство) только для создания логического термина. Обратите внимание, что ваш пример будет работать, если вы сделали even и odd типа ℕ → Type.

Помощник Coq proof, который является связанной системой, автоматически обрабатывает эту ситуацию, создавая два (довольно слабых и непрактичных) принципа индукции, но, конечно же, он не генерирует общие рекурсоры.

Существует обходное решение, описанное в этом Lean wiki article. Это связано с написанием довольно много шаблонов. Позвольте мне привести пример, как это можно сделать для этого случая.

Прежде всего, мы собираем взаимные индуктивные типы в индуктивное семейство. Добавим булево индекс, представляющий ровность:

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 

Было бы лучше сделать параметр even.induction_on неявным, но по какой-то причине Lean не может вывести его (см. Лемм в конце, wher e мы должны пройти Ce явно, в противном случае Lean infers Ce не имеет отношения к нашей цели). Ситуация симметрична с odd.induction_on.

Каков синтаксис для определения взаимно-рекурсивных функций?

Как объяснено в этом lean-user thread поддержка взаимно рекурсивные функции очень ограничена:

нет никакой поддержки для любых взаимно рекурсивных функций, но есть поддержка очень простой случай. После определения взаимно-рекурсивных типов мы можем определить взаимно-рекурсивные функции, которые «зеркалируют» структуру этих типов.

Вы можете найти пример в этой теме.Но, опять же, мы можем имитировать взаимно-рекурсивные функции, используя один и тот же подход с добавлением-переключением. Давайте смоделируем взаимно рекурсивных булевых предикатов 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)