sum of variables of different types

Stream: new members

[Mikhail Makarov]

Hello,

I am having trouble with the sum of variables of different types in Lean. Specifically, I have the code that boils down to this (in fact, it is more complex, but I simplified it to demonstrate the essense of the issue that I am having):

def pfin (n : pnat) : Type := { x : pnat // x ≤ n }

def f (x : pnat) : pnat := x

def tricky_definition_1 (m : nat) (l : pnat) (x : pfin l) : pnat := f (m + x)  --does not compile; how to make "m + x" work here?

Again, in reality, the function f is much more complex than just returning x, but it's not relevant to the current issue, so I simplified it to that. What is important is that it accepts the argument of type "pnat". So, I need the sum "m + x" to be casted to the type "pnat".

Regarding the type "pfin", I would prefer to use a type for the numbers { 1, ..., n } instead of for the numbers { 0, ..., n-1 }, that's why I use this custom type "pfin" instead of the existing type "fin". But I am also considering reverting to using "fin", in which case my definition would look like this:

def tricky_definition_2 (m : nat) (l : pnat) (x : fin l) : pnat := f (m + x + 1)  --does not compile; how to make "m + x + 1" work here?

So, I would appreciate if you would help me how to make these sums "m + x" and "m + x + 1" to work in the definitions above.

[Alex J. Best]

In lean addition is only between two terms of the same type, so we cannot expect that the add symbol will work out of the box.
Here you are relying on the fact that a positive natural added to any natural is again positive, so you can take f of it, this is fairly obvious to us but it does need to be proved somewhere for lean!
Here is one way to do this, we add m to x.1 which is notation for the underlying natural of x, then use simp to prove that this is positive and make a new pnat we can apply f to

def tricky_definition_1 (m : nat) (l : pnat) (x : pfin l) : pnat := f (⟨m + x.1, by simp⟩)

[Mikhail Makarov]

Ok, thank you, it works.
But is this notation .1 documented anywhere?
Before posting the question here, I tried m + (x:nat) and m+↑x, neither of which worked. I am confused by how casting works in Lean.

[Alex J. Best]

x.val is another name for the same thing, which is maybe more intuitive (meaning val).

[Alex J. Best]

Casting is managed using the typeclass system, so if you make a new type like pfin then generally you have to tell lean what casts you want it to have to other types

[Alex J. Best]

For examples you could add:

instance {n : ℕ+} : has_coe (pfin n) pnat := ⟨λ x : pfin n, x.val⟩

variables x : pfin 3
#check (↑x : nat)
#check (↑x : pnat)