## Stream: general

### Topic: equation compiler bad term

#### Bhavik Mehta (Sep 26 2020 at 17:24):

namespace list

def thing {ι : Type*} : ℕ → list ι → list (ι → ℕ)
| 0 l := [λ _, 0]
| (n+1) [] := []
| (n+1) (x :: xs) := (range n).bind (λ i, thing i xs)

lemma thing_zero {ι : Type*} (l : list ι) :
thing 0 l = [λ _, 0] :=
begin
refl,
end


Here's my example - the proof refl is accepted (as is by exact rfl) in tactic mode, but the overall definition gives me an error:

type mismatch at definition 'list.thing_zero', has type
∀ {ι : Type u_1} (l : list ι), thing 0 l = thing 0 l
but is expected to have type
∀ {ι : Type u_1} (l : list ι), thing 0 l = [λ (_x : ι), 0]


By looking at #print prefix list.thing, it shows four equations, splitting the first case into two - why does this happen? Also, is it possible for a more helpful error message here: from the definition I gave, I expected those two types to be the same thing

#### Mario Carneiro (Sep 26 2020 at 18:47):

Oh, that is a weird definition. It looks like it's going to be an induction on n but it's not

#### Mario Carneiro (Sep 26 2020 at 18:48):

if you reverse the order of arguments to make it clearer it errors where you would expect

def thing {ι : Type*} : list ι → ℕ → list (ι → ℕ)
| l 0 := [λ _, 0]
| [] (n+1) := []
| (x :: xs) (n+1) := (range n).bind (λ i, thing xs i)

lemma thing_zero {ι : Type*} (l : list ι) :
thing l 0 = [λ _, 0] :=
rfl -- error


#### Mario Carneiro (Sep 26 2020 at 18:51):

I'm not sure how but you have somehow tricked the elaborator into thinking this is rfl when it's not. Looking at the generated definitions it definitely will not be a rfl proof, and the kernel knows what's up

#### Mario Carneiro (Sep 26 2020 at 18:52):

in any case the correct proof is

lemma thing_zero {ι : Type*} (l : list ι) :
thing 0 l = [λ _, 0] :=
by cases l; refl


#### Bhavik Mehta (Sep 26 2020 at 20:04):

Yeah I figured that doing cases would work, but I guess I'm surprised at why the generated definitions are what they are - I would have thought it'd be something like: if the nat is zero then it's this, otherwise case-split on the list

Last updated: May 11 2021 at 14:11 UTC