Jak definiować wzajemne propozycje indukcyjne w Lean?

Question

Próbuję użyć składni indukcyjnych typów danych, ale otrzymałem komunikat o błędzie "typy wzajemnie indukcyjne muszą się kompilować z podstawowym typem indukcyjnym z zależną eliminacją".

Poniżej jest przykład mój próba zdefiniowania propozycji even i odd na liczbach naturalnych

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) 

także powiązany pytanie: Co to jest składnia do definiowania funkcji wzajemnie rekurencyjne? Nie wydaje mi się, żeby to było udokumentowane w dowolnym miejscu.

Answer 1

myślę Lean jest automatycznie próbuje stworzyć recursors even.rec i odd.rec do pracy z Type, nie Prop. Ale to nie działa, ponieważ Lean oddziela świat logiczny (Prop) i świat obliczeniowy (Type). Innymi słowy, możemy zniszczyć logiczny termin (dowód) tylko po to, by wytworzyć logiczny termin. Zauważ, że Twój przykład zadziała, jeśli wykonasz even i odd typu ℕ → Type.

Pomocniczy asystent Coq, który jest pokrewnym systemem, automatycznie obsługuje tę sytuację, tworząc dwie (raczej słabe i niepraktyczne) zasady indukcji, ale nie generuje oczywiście ogólnych rekursorów.

Istnieje obejście opisane w tej publikacji: Lean wiki article. Polega na napisaniu całkiem niezłego zestawu znaków. Podam przykład, jak można to zrobić w tej sprawie.

Po pierwsze, kompilujemy wzajemne typy indukcyjne do rodziny indukcyjnej. Dodamy logiczną indeksu równość reprezentujący:

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) 

Następnie definiujemy pewne skróty do symulacji rodzajów wzajemnie indukcyjne:

-- 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 

Teraz niech toczą się nasze własne zasady indukcji:

-- 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 

Lepiej byłoby wprowadzić domyślny parametr Ce : ℕ → Prop, ale z jakiegoś powodu Lean nie może go wywnioskować (patrz lemat na końcu, wer. e musimy wyraźnie przekazać Ce, w przeciwnym razie Lean infers Ce nie jest powiązany z naszym celem). Sytuacja jest symetryczna z odd.induction_on.

Jaka jest składnia do definiowania wzajemnie rekursywnych funkcji?

Jak wyjaśniono w tym lean-user thread, wsparcie dla funkcji wzajemnie rekurencyjnych jest bardzo ograniczony:

nie ma wsparcia dla dowolnych funkcji rekurencyjnych wzajemnie, ale nie ma wsparcia dla bardzo prostej sprawy. Po zdefiniowaniu typów rekursywnych, możemy zdefiniować funkcje rekursywne, które "odzwierciedlają" strukturę tych typów.

Możesz znaleźć przykład w tym wątku.Ale znowu możemy symulować wzajemnie rekursywne funkcje przy użyciu tego samego podejścia do przełączania parametrów. Załóżmy symulować wzajemnie rekurencyjnych Boolean orzeczników evenb i 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 

Oto przykład, jak wszystkie powyższe mogą być użyte. Udowodnijmy prosty lemat:

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)