Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Aug 05 2020 at 05:49):

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

view this post on Zulip Kenny Lau (Aug 05 2020 at 06:13):

eo.rec_on eliminates to Prop

view this post on Zulip 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 _ _ _

view this post on Zulip Kenny Lau (Aug 05 2020 at 06:14):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 05 2020 at 06:19):

the trick is to not recurse on eo

view this post on Zulip 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