interpreting a traceback

Stream: new members

[Julian Berman]

How do I read:

[lean] [I] [eqn_compiler.elim_match] depth [1]
match _match : board m n ι K[_a]
  (0) := s.start_board
  (⁇) := ⁇
  (_x) := s.boards (⁇ - 1)
example: (_a)
[eqn_compiler.elim_match] compilation failed at
match _match : board m n ι K[_a]
  (0) := s.start_board
  (⁇) := ⁇
  (_x) := s.boards (⁇ - 1)
example: (_a)

which is coming out of

def end_board : board m n ι K :=
match o with
| 0 := s.start_board,
| _ := s.boards (o - 1 : fin o)
end

for o a natural number. I'm sure I'm doing multiple things wrong there but yeah can't interpret that error message. _a is some element of the type it's trying to ensure I've covered in the match expression?

[Julian Berman]

(One of the basic things I'm doing wrong I'm sure is I can't figure out how to get n - 1 as an element of fin n, so if that's related yeah let me know.)

[Reid Barton]

I think you will want docs#fin.last

[Julian Berman]

ugh I looked all over https://leanprover-community.github.io/mathlib_docs/core/init/data/fin/basic.html#fin and https://leanprover-community.github.io/mathlib_docs/core/init/data/fin/ops.html and was wondering why there was so little there :/ -- thanks @Reid Barton

[Julian Berman]

Hrm that gives

[lean] [E] invalid type ascription, term has type
  fin (o - 1 + 1)
but is expected to have type
  fin o

though -- there's something that shows those are equivalent I assume?

[Julian Berman]

OK fin.cast maybe...

[Reid Barton]

I don't understand what o is but you should use the n you get out in the n+1 case, never o-1.

[Julian Berman]

o is variables (o : ℕ) and I want the largest element of fin o (as an element of fin o)

[Reid Barton]

In your _ case, you throw away the information you need to do this

[Reid Barton]

So use (o' + 1) or something instead

[Julian Berman]

Sorry, I thought I understood what you were saying, but still getting errors from things not having the right type.

I changed it to:

def end_board : board m n ι K :=
match o with
| 0 := s.start_board
| o' + 1 := s.boards o'
end

but I still get

[lean] [E] type mismatch at application
  s.boards o'
term
  o'
has type
  ℕ
but is expected to have type
  fin o

and neither adding : fin o to the left or right side of o' seems to satisfy the type checker

[Julian Berman]

import data.matrix.notation

variable {o : ℕ}

structure foo :=
(default: ℕ)
(elements: (fin o) → string)

#check {foo . default := 12, elements := !["bla", "bla"]}

namespace foo
variable (f: foo)

def last :=
match o with
| 0 := f.default
| o' + 1 := f.elements o'
end

end foo

I think that's a self-contained example of my confuzzledness.

[Julian Berman]

(no, sorry, that's giving me a different error about actually declaring f... never mind I guess, will keep trying to figure it out.).

[Reid Barton]

You should still use fin.last as well.

[Julian Berman]

I'm still not understanding how you're telling me I should use them together, apologies. I updated the self-contained example, which now does produce a similar error for me -- namely:

[lean] [E] invalid type ascription, term has type
  fin (o' + 1)
but is expected to have type
  fin o

Am I now basically supposed to tell Lean fin o' + 1 and fin o are equivalent or have I completely misunderstood the suggestions?

[Julian Berman]

I guess I figured out how to cheat... I used fin (o + 1) everywhere instead of fin o, and now I don't need fin.last, I can just index with o.

[Mario Carneiro]

You should probably use fin.last anyway. (\u o).val is not defeq to o, but (fin.last o).val = o is

[Julian Berman]

I can't figure out how to use fin.last for this -- I get the error above. Is there something clearly wrong I'm doing there?

[Mario Carneiro]

Ah, yes:

def last :=
match o, f with
| 0, f := f.default
| o' + 1, f := f.elements (fin.last o')
end

f depends on o, so you have to match on them together

[Julian Berman]

aha Thanks! My lack of functional programming knowledge bites me again I'm sure :/ -- very much appreciated.

[Mario Carneiro]

heh, haskell wouldn't save you here, you really need dependent functional programming experience and that's hard to come by unless you're into agda or idris (or lean)

[Julian Berman]

Ah, hm -- well, either way when Lean errors at me I'm having a heck of a time deciphering what it means to tell me, so hopefully I can get some sort of intuition soon. This is like the 4th or 5th thing already that even when I see the solution I wouldn't have guessed was anything to do with the error message if you gave me all week.