Je pense que Lean est automatiquement essayer de créer les recursors even.rec et odd.rec à travailler avec Type, non Prop. Mais cela ne fonctionne pas parce que Lean sépare le monde logique (Prop) et le monde de calcul (Type). En d'autres termes, nous pouvons détruire un terme logique (preuve) uniquement pour produire un terme logique. Observez, que votre exemple fonctionnerait si vous avez fait even et odd de type ℕ → Type. L'assistant de preuve Coq, qui est un système apparenté, gère automatiquement cette situation en créant deux principes d'induction (plutôt faibles et peu pratiques), mais il ne génère pas les récurrents généraux, bien sûr.
Il existe une solution de contournement, décrite dans cette section Lean wiki article. Il implique d'écrire beaucoup de passe-partout. Permettez-moi de donner un exemple de comment cela pourrait être fait pour ce cas. En premier lieu, nous compilons les types inductifs mutuels dans une famille inductive. Nous ajoutons un index booléen représentant équitabilité:
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)
Ensuite, nous définissons quelques abréviations pour simuler les types mutuellement inductives:
-- 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
Maintenant, nous allons déployer nos propres principes d'induction:
-- 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
Il serait préférable de faire le Ce : ℕ → Prop paramètre de even.induction_on implicite, mais pour une raison quelconque Lean ne peut pas en déduire (voir le lemme à la fin, wher e nous devons passer explicitement Ce, sinon Lean déduit Ce sans rapport avec notre objectif). La situation est symétrique avec odd.induction_on.
Quelle est la syntaxe pour définir les fonctions mutuellement récursives?
Comme expliqué dans ce lean-user thread, le soutien aux fonctions mutuellement récursives est très limité:
il n'y a pas de soutien pour les fonctions mutuellement récursives arbitraires, mais il y a un soutien pour un cas très simple. Après avoir défini un type mutuellement récursif, nous pouvons définir des fonctions mutuellement récursives qui "reflètent" la structure de ces types.
Vous pouvez trouver un exemple dans ce fil de discussion.Mais, encore une fois, nous pouvons simuler des fonctions mutuellement récursives en utilisant la même approche add-a-switching-parameter. Nous allons simuler mutuellement récursives prédicats booléens evenb et 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
Voici un exemple de la façon dont tous les ci-dessus peut être utilisé. Prouvons un simple lemme:
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)