Add parametric type to the statement being proven

Stream: lean4

[Leni Aniva]

I'm trying to prove a statement like this:

private theorem list_get_replicate (x: α) (i: Fin n): List.get (List.replicate n x) i = x := ...

However it gives this error even just to state the theorem:

application type mismatch
  List.get (List.replicate n x) i
argument
  i
has type
  Fin n : Type
but is expected to have type
  Fin (List.length (List.replicate n x)) : Type

The equivalence of n and List.length ... is established by List.length_replicate. How can I use this theorem here?

[Adam Topaz]

I would use the length instead of n. Is there a particular reason not to?

[Adam Topaz]

If you want to convert some x : Fin (length …) to Fin n, you could use docs#Fin.cast

[Leni Aniva]

Adam Topaz said:

I would use the length instead of n. Is there a particular reason not to?

How would this be stated? The length of the list comes from n

[Adam Topaz]

Just add n to the context

[Adam Topaz]

e.g.

private theorem list_get_replicate {n : Nat} (x: α) (i: Fin (List.replicate n x).length): List.get (List.replicate n x) i = x := ...

[Leni Aniva]

Adam Topaz said:

e.g.

private theorem list_get_replicate {n : Nat} (x: α) (i: Fin (List.replicate n x).length): List.get (List.replicate n x) i = x := ...

Thanks! Is this a common idiom?

[Adam Topaz]

What idiom are you referring to?

[Adam Topaz]

In this case you could also use your original code, but replace i after the : with an appropriate Fin.cast … i. Either approach works, but it’s up to the author to build the relevant API for the approach they take

[Leni Aniva]

Adam Topaz said:

What idiom are you referring to?

In this case it is necessary to duplicate List.replicate ... twice to ensure that i conforms to Fin condition in the statement of the theorem. Is this commonly seen?

[Leni Aniva]

Adam Topaz said:

In this case you could also use your original code, but replace i after the : with an appropriate Fin.cast … i. Either approach works, but it’s up to the author to build the relevant API for the approach they take

Thanks!

[Leni Aniva]

Adam Topaz said:

In this case you could also use your original code, but replace i after the : with an appropriate Fin.cast … i. Either approach works, but it’s up to the author to build the relevant API for the approach they take

Are you sure its Fin.cast? Lean gives the error

unknown constant 'Fin.cast'

[Adam Topaz]

docs#Fin.cast

[Adam Topaz]

You might be missing the import Std.Data.Fin.Basic

[Adam Topaz]

BTW, it's usually better to provide #mwe 's when asking such questions, which would make it obvious if you have some import missing, for example.