ben Yalın düşünmek otomatik even.rec ve odd.recType değil Prop çalışmak recursors oluşturmaya çalışıyor. Ama bu işe yaramaz çünkü Yalın mantıksal dünyayı (Prop) ve hesaplamalı dünyayı (Type) ayırır. Başka bir deyişle, mantıklı bir terimi sadece mantıksal bir terim üretmek için imha edebiliriz. Gözlemleyiniz, örneğiniz, even ve odd türünde ℕ → Type türünü yaptıysanız çalışır.
İlgili bir sistem olan Coq proof asistanı, bu durumu iki (oldukça zayıf ve pratik olmayan) indüksiyon ilkeleri oluşturarak otomatik olarak ele alır, ancak elbette genel tekrarlayıcıları üretmez.
Bu Lean wiki article numaralı belgede açıklanan bir geçici çözüm var. Çok fazla boilerplate yazmayı gerektirir. Bu dava için nasıl yapılabileceğine bir örnek vereyim.
Her şeyden önce, ortak endüktif tiplerini bir endüktif aileye derliyoruz.
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)
Sonra, bazı kısaltmalar karşılıklı endüktif olarak örneklemek için tanımlamak: Biz bir boolean endeksi temsil düzgünlüğü eklemek
-- 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
Şimdi, kendi indüksiyon ilkeleri çevirelim:
-- 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'un Ce : ℕ → Prop parametresinin üstü örtülü olması daha iyi olur, ancak bir nedenden dolayı Lean bunu çıkaramaz (sonunda lemmaya bakın. e Ce'u açıkça belirtmek zorundayız, aksi takdirde hedefimizle ilgili olmayan Ce numaralı telefonlara izin veriniz). Durum odd.induction_on ile simetriktir.
karşılıklı özyinelemeli işlevleri tanımlamak için sözdizimi nedir?
olarak bu lean-user thread açıklandığı karşılıklı özyinelemeli fonksiyonlar için destek çok sınırlıdır:
keyfi karşılıklı özyinelemeli fonksiyonlar için destek yoktur, ancak çok basit bir durum için destek var. Biz karşılıklı özyinelemeli türlerini tanımlamak sonra , bunu “ayna” Bu türlerin yapısı karşılıklı özyinelemeli fonksiyonlar tanımlayabilir.
O dizisindeki bir örnek bulabilirsiniz.Ancak, yine, aynı add-a-switching-parameter yaklaşımını kullanarak karşılıklı özyinelemeli işlevleri simüle edebiliriz. en karşılıklı özyinelemeli boole yüklemleri evenb ve oddb simüle edelim:
İşte
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
ait her şeyden nasıl kullanılabileceği bir örnektir. Basit bir lemma ispatlayalım:
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)