trans in index bound proof

Stream: lean4

[Jun Yoshida]

When I index-access to List/Array, it is frustrating the following causes errors:

example (x : List Nat) (i : Nat) (hi : i < x.length) : Nat :=
  -- Both arguments of `trans` cause errors.
  x[i-1]'(trans i.pred_le hi)

I want to know why trans doesn't work here.

From the error message above, it seems that trans cannot infer its implicit arguments correctly.
So I next tried the following:

example (x : List Nat) (i : Nat) (hi : i < x.length) : Nat :=
  -- Only `i.pred_le` causes an error.
  x[i-1]'(trans (r:=LE.le) i.pred_le hi)
/-
The error message says
> application type mismatch
>   trans (Nat.pred_le i)
> argument
>   Nat.pred_le i
> has type
>   Nat.pred i ≤ i : Prop
> but is expected to have type
>   x ≤ ?m.2258 : Prop
-/

example (x : List Nat) (i : Nat) (hi : i < x.length) : Nat :=
  -- The same errors as in the case without `s` specified.
  x[i-1]'(trans (s:=LT.lt) i.pred_le hi)

example (x : List Nat) (i : Nat) (hi : i < x.length) : Nat :=
  -- No error
  x[i-1]'(trans (t:=LT.lt) i.pred_le hi)

Seeing the result, I completely got lost.
Why on earth does the elaborator think r:=LE.le (List Nat) is the appropriate choice when r:=LE.le is given?
I am not sure either why the last one compiles while it doesn't without t specified; isn't the target binary relation t of trans determined by GetElem instance of List?
I am glad if you could give me a hint.

[Eric Rodriguez]

Note that hi is not a le statement, but a lt statement. I think there is other issues in here, but this is one issue

[Eric Rodriguez]

Here's a way you could do it with mathlib:

import Mathlib.Init.Data.Nat.Lemmas
import Mathlib.Order.Basic

example (x : List Nat) (i : Nat) (hi : i < x.length) : Nat := x[i-1]'((i.pred_le).trans_lt hi)

but it does seem quite annoying to do in basic Lean

[Jun Yoshida]

Eric Rodriguez said:

Note that hi is not a le statement, but a lt statement. I think there is other issues in here, but this is one issue

Thank you for commenting, but I can't see what you mean. Note that Trans is a heterogeneous transitivity, and actually it can use docs#Nat.instTransNatLeInstLENatLtInstLTNat .
In fact, trans uses it in my example if (t:=LT.lt) is supplied. One of my questions is why we need to specify it.

[Jun Yoshida]

I mean, the following works:

example (x : List Nat) (i : Nat) (hi : i < x.length) : Nat :=
  have : i-1 < x.length := trans i.pred_le hi
  x[i-1]'this -- or just `x[i-1]`

[Jun Yoshida]

Oh, I was a bit surprised knowing the code just above works without type specification in have-clause.

[Jun Yoshida]

Hmm, this even works:

example (x : List Nat) (i : Nat) (hi : i < x.length) : Nat :=
  x[i-1]'(trans i.pred_le hi : _)

[Eric Rodriguez]

Oh I see! Apologies, this was based on old Lean3 knowledge, I didn't know that this worked automatically. It seems to be an expected type issue, I now agree this is bizarre!