## Stream: new members

### Topic: why is Lean not able to compute the motive here?

#### Chris M (Aug 05 2020 at 04:19):

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 (Aug 05 2020 at 05:49):

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

#### Kenny Lau (Aug 05 2020 at 06:13):

eo.rec_on eliminates to Prop

#### Kenny Lau (Aug 05 2020 at 06:14):

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 (Aug 05 2020 at 06:14):

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

#### Kenny Lau (Aug 05 2020 at 06:19):

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 (Aug 05 2020 at 06:19):

the trick is to not recurse on eo

#### Chris M (Aug 05 2020 at 15:24):

Yury G. Kudryashov said:

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

sorry my bad, I missed it, edited

Last updated: May 11 2021 at 22:14 UTC