why is Lean not able to compute the motive here?

Stream: new members

[Chris M]

I'm just playing around with Toy examples for inductive families. For the following code I'm getting the error: "eliminator" elaborator failed to compute the motive

inductive eo : eo_index → ℕ → Prop
| even_zero : eo even 0
| even_succ : ∀ n, eo odd n → eo even (n + 1)
| odd_succ : ∀ n, eo even n → eo odd (n + 1)

inductive X:Type
| const : X
| succ : X → X

def test (i: eo_index) (n:nat) (e:eo i n) : X :=
eo.rec_on e (X.const) (fun n k, X.succ X.const ) (fun n k, X.succ X.const)

Why is this? It seems to me like it should be able to find the motive very easily by just looking at the type signature of test: C:\Pi (i: eo_index) (n:nat) (e:eo i n) ,X

[Yury G. Kudryashov]

This is not an #mwe because it has no definition of eo_index

[Kenny Lau]

eo.rec_on eliminates to Prop

[Kenny Lau]

mwe:

inductive eo_index : Type
| even | odd

open eo_index

inductive eo : eo_index → ℕ → Prop
| even_zero : eo even 0
| even_succ : ∀ n, eo odd n → eo even (n + 1)
| odd_succ : ∀ n, eo even n → eo odd (n + 1)

inductive X : Type
| const : X
| succ : X → X

def test (i : eo_index) (n : nat) (e : eo i n) : X :=
eo.rec_on e _ _ _

[Kenny Lau]

eo is Prop, so it cannot "eliminate into data"

[Kenny Lau]

and here's the fix:

inductive eo_index : Type
| even | odd

open eo_index

inductive eo : eo_index → ℕ → Prop
| even_zero : eo even 0
| even_succ : ∀ n, eo odd n → eo even (n + 1)
| odd_succ : ∀ n, eo even n → eo odd (n + 1)

inductive X : Type
| const : X
| succ : X → X

theorem eo.odd_of_even_succ {n : ℕ} (h : eo even (n+1)) : eo odd n :=
by { cases h, assumption }

theorem eo.even_of_odd_succ {n : ℕ} (h : eo odd (n+1)) : eo even n :=
by { cases h, assumption }

theorem eo.not_odd_zero (h : eo odd 0) : false :=
by cases h

def test : Π (i : eo_index) (n : nat) (e : eo i n), X
| even 0     H := X.const
| even (n+1) H := X.succ $ test odd n $ eo.odd_of_even_succ H
| odd  0     H := absurd H eo.not_odd_zero
| odd  (n+1) H := X.succ $ test even n $ eo.even_of_odd_succ H

[Kenny Lau]

the trick is to not recurse on eo

[Chris M]

Yury G. Kudryashov said:

This is not an #mwe because it has no definition of eo_index

sorry my bad, I missed it, edited