Zulip Chat Archive

Stream: general

Topic: equation compiler bad term


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

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

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

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

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

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