Nat to Fin conversion

Stream: new members

[jsodd]

Is there a way to convert j \leq n of type Nat to an element of Fin n?

[jsodd]

Example: I have a vector x : Fin i \to R, where i \leq n, and I want to extend it by zero by y : Fin n \to R := fun j \map if j \leq i then x j else 0. This doesn't work because x doesn't accept j of type Nat.

[Eric Wieser]

What if j = n? The maximum value of Fin n is n - 1

[jsodd]

Okay, I see. The question 1 easily changes to "is there a way to convert j \leq n-1 of type Nat to an element of type Fin n.

[jsodd]

But I'm actually more interested in the question from the example

[jsodd]

Maybe I'm doing something wrong and there is a more natural way to extend a vector by zeros?

[Eric Wieser]

Can you write your question as a #mwe ?

[jsodd]

Eric Wieser said:

Can you write your question as a #mwe ?

Of course, I'm sorry. Here it is:

import Mathlib

variable {n i : Nat} {R : Type} {x : Fin n → R} [Zero R]

def y {_ : i ≤ n} : Fin i → R := λ j ↦ if j ≤ i then x j else 0

[Eric Wieser]

This works, but might not be what you want:

import Mathlib

variable {n i : Nat} {R : Type} {x : Fin n → R} [Zero R]

def y {hi : i ≤ n} : Fin i → R := λ j ↦ if j < i then x (Fin.castLE hi j) else 0

[Eric Wieser]

This isn't extending by zero though, this is truncating

[jsodd]

Forgive me, I made a stupid mistake in my example... I'll send a new one if you don't mind

[jsodd]

import Mathlib

variable {n i : Nat} {R : Type} {x : Fin i → R}[Zero R]

def y {_ : i ≤ n} : Fin n → R := λ j ↦ if j ≤ i then x j else 0

[jsodd]

Eric Wieser said:

This works, but might not be what you want:

import Mathlib

variable {n i : Nat} {R : Type} {x : Fin n → R} [Zero R]

def y {hi : i ≤ n} : Fin i → R := λ j ↦ if j < i then x (Fin.castLE hi j) else 0

I guess in this case it should be possible to use Fin.castLE directly on x, and if ... then isn't necessary

[Eric Wieser]

Are you looking for

def y : Fin n → R := λ j ↦ if h : j < i then x ⟨j, h⟩ else 0

[jsodd]

Eric Wieser said:

Are you looking for

def y : Fin n → R := λ j ↦ if h : j < i then x ⟨j, h⟩ else 0

I think yes, but how do I check if it works? I've tried

import Mathlib

variable {R : Type} [Zero R] [One R]

def x : Fin 2 → R := λ _ ↦ 1
def z : Fin 3 → R := λ j ↦ if h : j < 2 then x ⟨j, h⟩ else 0

#eval z 2

but it gives a mistake...

[Eric Wieser]

It's much easier to help if you provide the error message :)

[Eric Wieser]

In this case

#eval z (R := ℕ)

works

[Eric Wieser]

Lean is unhappy because it doesn't know what type of coefficients you wanted

[jsodd]

Thank you very much!