How to convert function of `\nat` to function of `fin n`

Stream: new members

[Jeffrey Li]

Any function of \nat can be resolved to a function of fin n because fin n \subset \nat, but when i try to pass a function \nat \to A as an argument that is typed as fin n \to A, it gives me a type mismatch error. Can I do the conversion implicitly or do i have to explicitly make a new function to satisfy the fin n \to A type constraint? Thanks

[Yakov Pechersky]

If you have a function f : fin 3 -> A, what do you want f 5 to be?

[Jeffrey Li]

Sorry I think you misunderstand, I have a function f : \nat \to A, and I want to pass it as an argument of type fin n \to A

[Jeffrey Li]

Also how I produce the proof that allows me to compare (fin n) with ℕ? Right now if I have the variable i : fin n, I can't do the comparison i == 1, because I believe I need the following proof

instance eq_decidable_fin_n(i : fin n)(k : ℕ) : decidable (i == k) := sorry

But I'm not sure how to produce that proof. Thanks

[Reid Barton]

Jeffrey Li said:

fin n \subset \nat

This isn't how it works in Lean--fin n and nat are two different types, and a type can't be a subset of another one. Rather, there is a coercion from fin n to nat. This means that if you have x : fin n and you write x : ℕ then Lean will notice that it doesn't type check and replace x by a coercion ↑x, which elsewhere was defined to mean x.val or whatever.

[Reid Barton]

Jeffrey Li said:

Can I do the conversion implicitly or do i have to explicitly make a new function to satisfy the fin n \to A type constraint?

You will have to write something like λ x, f x (which really means λ x, f (↑x)) instead of just f.

[Reid Barton]

Jeffrey Li said:

Also how I produce the proof that allows me to compare (fin n) with ℕ? Right now if I have the variable i : fin n, I can't do the comparison i == 1, because I believe I need the following proof

instance eq_decidable_fin_n(i : fin n)(k : ℕ) : decidable (i == k) := sorry

But I'm not sure how to produce that proof. Thanks

This is not possible. Basically, don't use ==.

[Reid Barton]

Oh sorry, it actually is possible but i == k doesn't mean what you want anyways.

[Jeffrey Li]

Reid Barton said:

Jeffrey Li said:

fin n \subset \nat

This isn't how it works in Lean--fin n and nat are two different types, and a type can't be a subset of another one. Rather, there is a coercion from fin n to nat. This means that if you have x : fin n and you write x : ℕ then Lean will notice that it doesn't type check and replace x by a coercion ↑x, which elsewhere was defined to mean x.val or whatever.

Oh thank you so much, using x.val makes everything work. Still new to lean so trying to figure out how the type / subtype system works.