# Zulip Chat Archive

## Stream: new members

### Topic: Failed to synthesize instance for zero index of list

#### Ioannis Konstantoulas (Sep 11 2023 at 10:23):

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 (Sep 11 2023 at 10:25):

You must wrap it in a `Fact`

.

#### Ioannis Konstantoulas (Sep 11 2023 at 10:26):

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

for a predicate `p`

.

#### Ioannis Konstantoulas (Sep 11 2023 at 10:26):

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 (Sep 11 2023 at 10:27):

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

#### Yaël Dillies (Sep 11 2023 at 10:28):

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 (Sep 11 2023 at 10:32):

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 (Sep 11 2023 at 10:34):

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 (Sep 11 2023 at 11:19):

(1 is *not* syntactically `succ n`

, but it does unify with it)

#### Ioannis Konstantoulas (Sep 11 2023 at 12:39):

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

Last updated: Dec 20 2023 at 11:08 UTC