Failed to synthesize instance for zero index of list

Stream: new members

[Ioannis Konstantoulas]

In the middle of a proof, I have a list L together with an equation : L = x :: y :: ys. Using that, I prove

have positive_length : 0 < L.length := sorry

I then write something like

let l_0 := (0 : Fin L.length)

and get the error message

failed to synthesize instance
  OfNat (Fin (List.length L)) 0

How can I use positive_length to make Lean synthesize that instance for me, so I can use it in the proof?

[Yaël Dillies]

You must wrap it in a Fact.

[Ioannis Konstantoulas]

The conclusion of my theorem is of the form ∃ i : Fin L.length, p L[i] for a predicate p.

[Ioannis Konstantoulas]

Yaël Dillies said:

You must wrap it in a Fact.

Is Fact a type in Core? I am not using Mathlib or Std.

[Yaël Dillies]

docs#Fin.instAddMonoidWithOne tells you what you need. You need docs#NeZero.

[Yaël Dillies]

Tough luck. Core and Std only have a OfNat (Fin n.succ) instance, not a Fact (n != 0) -> OfNat (Fin n) as mathlib does.

[Ioannis Konstantoulas]

I am confused by that statement: previously in the proof, I wrote (0 : Fin 1) with no complaints. Do you mean that I should prove L.length = succ x for some x? That is easy.

[Yaël Dillies]

Yeah because 1 is syntactically of the form Nat.succ n for some n (namely n := 0). The problem in your case is that L.length is not syntactically of the form Nat.succ n for some n.

[Eric Wieser]

(1 is not syntactically succ n, but it does unify with it)

[Ioannis Konstantoulas]

Thank you for your comments, I know how to proceed now!