Fin without wrapping

Stream: lean4

[Joseph O]

In this photo image.png it wraps the value of 88 mod 5, but I don't really want that . I would prefer it to not typecheck, like in Idris. Is there another version of Fin with that behavior?

[Henrik Böving]

You could implement one, the translation of numerals to types is controlled by the OfNat type class

[Joseph O]

But why is it not default?

[Eric Wieser]

The simple answer is "to match the behavior of lean 3"

[Henrik Böving]

You could also make a mathematical argument if FIn n is supposed to be numbers mod n then 12 mod 10 should be 2

[Joseph O]

But it shouldn't

[Mauricio Collares]

Why? The equivalence class of 12 in the mod 10 relation exists.

[Henrik Böving]

You cant just say it shouldnt, this is how numbers mod n work in mathematics, just because some other language has some other opinion on what Fin represents doesnt mean that we have to follow it

[Joseph O]

I wasn't contradicting how mod worked. So it seems that Fin n represents a mod system of n.

[Damiano Testa]

Also, by analogy with Lean3, an alternative possibility for fin n would probably be absorbing addition. In particular n + n would typecheck and be equal to n.

[Damiano Testa]

I do not think that there is in Lean something that does not typechecks when you are out of bounds. The fact that functions need to be total seems an obstacle to "not typechecking sometimes".

[Mario Carneiro]

It is possible for lean 4 to have a type which only supports some numbers, although you have to do the computation in the typeclass system so that might not be great

[Mario Carneiro]

import Mathlib.Data.Nat.Basic

def Fin' (n : Nat) := Fin n

class IsPos (n : Nat) := pos : 0 < n

instance : IsPos (Nat.succ n) := ⟨Nat.succ_pos _⟩

instance [IsPos (n - i)] : OfNat (Fin' n) i :=
  ⟨i, Nat.lt_of_not_le fun h => ne_of_gt IsPos.pos (Nat.sub_eq_zero_iff_le.2 h)⟩

#check (3 : Fin' 5) -- ok
#check (4 : Fin' 5) -- ok
#check (5 : Fin' 5) -- fail
#check (6 : Fin' 5) -- fail

[Damiano Testa]

I look forward to having ℕ subtraction being undefined when it should be negative! :upside_down:

[Mario Carneiro]

This doesn't work as well when the numbers aren't concrete, though. For nat subtraction that would be bad because you wouldn't be able to write a - b where a and b are variables

[Damiano Testa]

Sure, anyway, after the initial shock of being able to compute 3-4 to

• obtain a natural number,
• and moreover the natural number 0

i have grown used to it and would probably prefer the garbage values to pain involving typeclasses!

[Damiano Testa]

At the beginning it seemed a little a joke: "I am formalizing mathematics to not make mistakes. For instance, I can prove that 2-4=0 and that 7/0=0".

[James Gallicchio]

Is there an implicit coercion from Nat to Fin n in Lean 3? I think this really only is an issue with numeric literals, since I don't think a coercion exists

[Mario Carneiro]

In the case of Fin' it's probably fine since as you say you would only care if you want to write a literal, and 1 : Fin n doesn't make sense anyway (although I can imagine that being annoying if, say, n is a prime number)

[Mario Carneiro]

for nat subtraction it wouldn't really work though because the Sub typeclass is accessed whenever you have a - in the expression

[Joseph O]

Why are the bodies of the instances product types? @Mario Carneiro ?

[Joseph O]

Also, what does OfNat (Fin' n) i do

[Joseph O]

as well as the body of the instance. Im not really sure what any of those instances do

[Mario Carneiro]

An instance is a proof/construction of an element of a class, which is a special kind of structure, which is essentially a generalized tuple type

[Mario Carneiro]

In this case we are creating an inhabitant of docs4#OfNat

[Mario Carneiro]

Actually, now that you mention it, I'm surprised that what I wrote typechecks. Normally I would have needed to write

instance [IsPos (n - i)] : OfNat (Fin' n) i :=
  ⟨⟨i, Nat.lt_of_not_le fun h => ne_of_gt IsPos.pos (Nat.sub_eq_zero_iff_le.2 h)⟩⟩

which is probably easier to explain

[Mario Carneiro]

@Gabriel Ebner Did you know about this behavior?

example : Inhabited (Nat × Nat) := ⟨1, 2⟩

[Mario Carneiro]

But to get back to your question @Joseph O: The instance has the form ⟨⟨i, h⟩⟩ where the first set of brackets is destructuring the OfNat class to produce a goal of Fin' n, and the second set is unpacking Fin' n which is defined to be Fin n (docs4#Fin) which is a tuple of an element, here i, and a proof that i < n

[Joseph O]

class IsPos (n : Nat) := pos : 0 < n

here, pos just returns a proof that n is greater than 0?

[Joseph O]

Mario Carneiro said:

But to get back to your question Joseph O: The instance has the form ⟨⟨i, h⟩⟩ where the first set of brackets is destructuring the OfNat class to produce a goal of Fin' n, and the second set is unpacking Fin' n which is defined to be Fin n (docs4#Fin) which is a tuple of an element, here i, and a proof that i < n

Would i understand this all better if i read TPIL4?

[Mario Carneiro]

The purpose of the instance OfNat (Fin' n) i is a signal to lean's parser. When you write 3 : Fin 5, it expands the 3 to something like OfNat.ofNat (nat_lit 3) where nat_lit 3 is a "raw" nat literal (these are primitive in the syntax) and ofNat has an additional hidden argument of type OfNat (Fin' 5) (nat_lit 3) that is inferred by typeclass inference. Since we have declared this instance, typeclass inference will try to apply it, resulting in the subgoal IsPos (5 - 3). It will then try to unify this with IsPos (Nat.succ ?n), and lean's unifier can solve the equation 5 - 3 = Nat.succ ?n to ?n := 1, so the numeral typechecks

[Mario Carneiro]

IsPos n is a class which is equivalent to 0 < n (hence the name), but it is a class which means it can be used in typeclass inference. You can't have an argument like instance [0 < n] : MyClass (foo n) directly

[Mario Carneiro]

Joseph O said:

Would i understand this all better if i read TPIL4?

The answer is usually "yes" to this kind of question

[Joseph O]

Mario Carneiro said:

But to get back to your question Joseph O: The instance has the form ⟨⟨i, h⟩⟩ where the first set of brackets is destructuring the OfNat class to produce a goal of Fin' n, and the second set is unpacking Fin' n which is defined to be Fin n (docs4#Fin) which is a tuple of an element, here i, and a proof that i < n

But why are you nesting tuples?

[Mario Carneiro]

Because OfNat A i is a tuple containing A, so OfNat (Fin n) i is a tuple containing Fin n which is itself a tuple containing a natural number and a proof that it is less than n

[Joseph O]

Why [IsPos (n - i)] in the last instance?

[Mario Carneiro]

We want the typeclass problem to be solvable iff i < n, so one way to do that without too many steps is to compute n - i and if it is nonzero then i < n

[Mario Carneiro]

The set of things we can compute this way is somewhat limited, but natural number inequalities happen to be provable this way

[Mario Carneiro]

we probably won't be able to have a type which only admits numerals which are prime numbers

[Mario Carneiro]

But also, to be clear: this is totally an abuse of the typeclass and unification algorithms and I don't recommend it. There are better ways to do this with fewer downsides

[Mario Carneiro]

notation "♯" n => (⟨n, by decide⟩ : Fin _)
#check (♯3 : Fin 5) -- ok
#check (♯4 : Fin 5) -- ok
#check (♯5 : Fin 5) -- fail
#check (♯6 : Fin 5) -- fail

[Joseph O]

That is clean

[Joseph O]

But Im not sure how I would utilize it with functions

[Mario Carneiro]

This one works on primes too:

def isPrime (p : Nat) : Bool := Id.run do
  for i in [2:p] do
    if p % i == 0 then return false
  return p ≠ 1

def Prime := {n // isPrime n}
notation "♯" n => (⟨n, by decide⟩ : Prime)
#check ♯3 -- ok
#check ♯4 -- fail
#check ♯5 -- ok
#check ♯6 -- fail
#check ♯12 -- fail
#check ♯37 -- ok

[Joseph O]

Mario Carneiro said:

But also, to be clear: this is totally an abuse of the typeclass and unification algorithms and I don't recommend it. There are better ways to do this with fewer downsides

I mean, I still wish I understood it. I will probably have to come back to this thread later on

[Joseph O]

Mario Carneiro said:

This one works on primes too:

def isPrime (p : Nat) : Bool := Id.run do
  for i in [2:p] do
    if p % i == 0 then return false
  return p ≠ 1

def Prime := {n // isPrime n}
notation "♯" n => (⟨n, by decide⟩ : Prime)
#check ♯3 -- ok
#check ♯4 -- fail
#check ♯5 -- ok
#check ♯6 -- fail
#check ♯12 -- fail
#check ♯37 -- ok

Why do you need to use the do dsl?

[Mario Carneiro]

Here is an approach using only functions instead of notation:

def Fin.mk' (i : Nat) (h : i < n := by decide) : Fin n := ⟨i, h⟩
#check (Fin.mk' 3 : Fin 5) -- ok
#check (Fin.mk' 4 : Fin 5) -- ok
#check (Fin.mk' 5 : Fin 5) -- fail
#check (Fin.mk' 6 : Fin 5) -- fail

[Joseph O]

Interesting

[Joseph O]

what does by decide tactic do?

[Mario Carneiro]

I don't need the do DSL, I use it because it is nice but you can write the same loop in other ways

[Mario Carneiro]

The by decide tactic proves any decidable proposition that evaluates to true

[Mario Carneiro]

In this case the purpose of the isPrime function was to give an implementation that can be executed to determine primality of a number suitable for by decide

[Mario Carneiro]

decidable propositions are also marked by a typeclass docs4#Decidable

[Mario Carneiro]

basically, a decidable proposition is one equivalent to a (computable) Bool value

[Mario Carneiro]

and all the basic stuff like a < b on natural numbers is decidable so lean knows how to evaluate it even though syntactically it has type Prop not Bool

[Joseph O]

Mario Carneiro said:

notation "♯" n => (⟨n, by decide⟩ : Fin _)
#check (♯3 : Fin 5) -- ok
#check (♯4 : Fin 5) -- ok
#check (♯5 : Fin 5) -- fail
#check (♯6 : Fin 5) -- fail

So fin has an instance of Decidable?

[Mario Carneiro]

Props in general can be undecidable, for example

def isTwinPrime (p : Nat) := isPrime p && isPrime (p + 2)

#check ∀ n, ∃ p, n < p ∧ isTwinPrime p

If you find a way to decide this proposition you will win fame and fortune

[Mario Carneiro]

Not Fin, the thing being decided there are propositions like 3 < 5 and 5 < 5

[Mario Carneiro]

If you replace by decide with by {}, lean will give an error showing the proposition it is trying to solve

[Joseph O]

image.png

[Joseph O]

I would like to start from the beginning. What is this typeclass instance doing, and also what really is the purpose of IsPos,

instance : IsPos (Nat.succ n) := ⟨Nat.succ_pos _⟩

[Joseph O]

I feel like this would be useful for me in the future

[Joseph O]

No need to explain the second instance a second time.

[Joseph O]

But I will try to utilize the simpler solutions

[Mario Carneiro]

The typeclass instance makes it so that when lean wants to solve a problem of the form IsPos (Nat.succ ?n), it will find that proof. For example:

def foo [IsPos (Nat.succ 2)] : Nat := 0
#check foo

Writing foo here elaborates to @foo _ where the _ is a proof of IsPos (Nat.succ 2), and we are asking the typeclass inference system to go find a proof using the declared instances. It will come back with myInst 2, assuming that the name of that instance was myInst (it has an automatically generated name, but you can name it with instance myInst : IsPos (Nat.succ n) := ⟨Nat.succ_pos _⟩).

[Mario Carneiro]

The purpose of the IsPos typeclass is to make it so that typeclass inference can solve problems of the form "is this a nonzero natural number?"

[Mario Carneiro]

The second instance makes use of this class to ask "is n - i a nonzero natural number?", which is equivalent to "Is i < n?"

[Mario Carneiro]

The point is that we are trying to get typeclass inference to answer this "Is i < n?" question because this is the necessary component to make fin numerals work the way you expect: we want 3 : Fin 5 to work but not 5 : Fin 3, and in general i : Fin n for numerals i and n should work exactly when i < n

[Joseph O]

Ah thanks

[Joseph O]

how would I go about fixing this error?

failed to synthesize instance
  OfNat (Fin' (length (a :: as))) 0

[Kevin Buzzard]

Make the instance :-) We have it in Lean 3:

instance : has_zero (fin (succ n)) := ⟨⟨0, succ_pos n⟩⟩

[Joseph O]

Thanks. I will just translate that to Lean 4.

[Joseph O]

instance : HasZero (Fin' (Nat.succ n)) :=
  ⟨⟨0, Nat.succ_pos n⟩⟩

it has a different name in lean 4?

[Kevin Buzzard]

I don't know whether the Lean 4 type class inference system will be smart enough to know that length(a::as)=succ(something) either

[Kevin Buzzard]

Yeah, in Lean 4 you use this OfNat thing instead. I don't know the details of that either.

[Joseph O]

well that didnt exactly work

instance : OfNat (Fin' (length (a :: as))) 0 :=
  ⟨⟨0, Nat.succ_pos (length (a :: as))⟩⟩

[Joseph O]

How would I go about making this instance?

[Kevin Buzzard]

I'm late to this thread and not a Lean 4 expert; can you post a mwe? I don't even know what Fin' is.

[Joseph O]

Here you go

import Mathlib.Data.Nat.Basic

def Fin' (n : Nat) := Fin n

class IsPos (n : Nat) := pos : 0 < n

instance : IsPos (Nat.succ n) := ⟨Nat.succ_pos _⟩

instance [IsPos (n - i)] : OfNat (Fin' n) i :=
  ⟨i, Nat.lt_of_not_le fun h => ne_of_gt IsPos.pos (Nat.sub_eq_zero_iff_le.2 h)⟩

instance : OfNat (Fin' (List.length (a :: as))) 0 :=
  ⟨⟨0, Nat.lt 0 (List.length (a :: as))⟩⟩

[Kevin Buzzard]

That doesn't work because you never told Lean the type of as.

[Kevin Buzzard]

and when you do, it doesn't work for the reason that the error explains: right you the second component of ⟨0, _⟩ is the statement 0 < length..., as opposed to its proof.

[Kevin Buzzard]

variable (a : α) (as : List α)

instance : OfNat (Fin' (List.length (a :: as))) 0 :=
  ⟨⟨0, (Nat.succ_pos _ : Nat.lt 0 (List.length (a :: as)))⟩⟩

[Joseph O]

Ah thank you

[Joseph O]

Now that the instance is made, the error should go away in this function, but it isn't

def List.get'' [OfNat i 0] {α : Type u} : (as : List α) → (i : Fin' as.length) → α
  | nil, i => False.elim $ Nat.not_lt_zero _ _
  | cons a as, 0 => a

[Joseph O]

failed to synthesize instance
  OfNat (Fin' (length (a :: as))) 0

[Kevin Buzzard]

Rotten luck -- type class inference can't find it, by the looks of things. I know nothing about how Lean 4 type class inference works I'm afraid

[Gabriel Ebner]

Hint: you need to write instance : OfNat (Fin' (List.length (a :: as))) (nat_lit 0)

[Kevin Buzzard]

[OfNat i 0] looks like nonsense -- maybe remove it?

[Joseph O]

Ah yeah. That was part of my previous attempts.

[Joseph O]

Gabriel Ebner said:

Hint: you need to write instance : OfNat (Fin' (List.length (a :: as))) (nat_lit 0)

Why did that fix it though?

[Joseph O]

Also, now the function

def List.get'' {α : Type u} : (as : List α) → (i : Fin' as.length) → α
  | nil, i => False.elim $ Nat.not_lt_zero _ _
  | a::as, 0 => a
  | a::as, i+1 => as.get'' i

has the error

failed to synthesize instance
  HAdd (Fin' (length (a :: as))) (Fin' (length (a :: as))) ?m.1019

[Kevin Buzzard]

You know what to do then :-)

[Kevin Buzzard]

You understand the error, right? You defined Fin' so it's now your problem. If i : Fin' n then what does i + 1 mean? No idea -- you didn't tell me what + meant, or what 1 meant.

[Joseph O]

I see. I think i have a fix

[Joseph O]

image.png Well thats strange. How do people match on Nat.succ i then.

[Joseph O]

Also, for a MWE,

def Fin'.succ (n : Fin' k) := Fin.succ n

[Henrik Böving]

Fin.succ is not a constructor of the Fin datatype (whcih you could see by looking at its definition) thus it and any further definition cannot just be matched upon like this.

[Joseph O]

then, what alternative solutions lie?

[Leonardo de Moura]

@Joseph O Note that in other systems (e.g, Agda and Idris), Fin n is an inductive datatype with two constructors. In Lean, it is essentially a subtype of Nat, i.e, a pair containing: a Nat, and a proof that it is smaller than n. You can use match to "access" this structure.

def get : (as : List α) → (i : Fin as.length) → α
  | a::as, ⟨0, _⟩   => a
  | a::as, ⟨i+1, h⟩ => get as ⟨i, Nat.lt_of_succ_lt_succ h⟩

Here is the same definition without the anonymous constructor notation.

def get : (as : List α) → (i : Fin as.length) → α
  | a::as, Fin.mk 0 _     => a
  | a::as, Fin.mk (i+1) h => get as (Fin.mk i (Nat.lt_of_succ_lt_succ h))

We can also define Fin n as it is defined in other systems and then match on Fin.succ. Example:

namespace Ex -- Using namespace `Ex` to avoid name collision with the Lean `Fin`

inductive Fin : Nat → Type
  | zero : Fin (Nat.succ n)
  | succ : Fin n → Fin (Nat.succ n)
  deriving Repr

def get : (as : List α) → (i : Fin as.length) → α
  | a::as, Fin.zero   => a
  | a::as, Fin.succ i => get as i

end Ex

[Joseph O]

Ah i see. Tho, it would still be the wrapping version I think

[Joseph O]

Also, why did you decide not to consider the | nil, i case anymore?

[Leonardo de Moura]

Joseph O said:

Ah i see. Tho, it would still be the wrapping version I think

You can still use the wrapping if you want

def Fin' (n : Nat) := Fin n

def get : (as : List α) → (i : Fin' as.length) → α
  | a::as, ⟨0, _⟩   => a
  | a::as, ⟨i+1, h⟩ => get as ⟨i, Nat.lt_of_succ_lt_succ h⟩

[Leonardo de Moura]

Joseph O said:

Also, why did you decide not to consider the | nil, i case anymore?

Lean 4 can prove it is unreachable.

[Joseph O]

But it is reachable? Like what if someone gives List.get [] 8

[Joseph O]

Also, I have this error again, failed to synthesize instance OfNat (Fin' (List.length [1, 5, 4])) 7

[Leonardo de Moura]

Joseph O said:

But it is reachable? Like what if someone gives List.get [] 8

It is not. You will not be able to do that. The type Fin [].length is not inhabited.

[Henrik Böving]

That would mean they are passing an element of type Fin 0 and that is equivalent to the emtpy type and thus impossible to do

[Joseph O]

Empty type. Ok i see.

[Henrik Böving]

Leonardo de Moura said:

Joseph O said:

Also, why did you decide not to consider the | nil, i case anymore?

Lean 4 can prove it is unreachable.

This is also a thing that I've been wondering about for a bit, how does it actually automagically construct this proof? Can you explain it/point me to the implementation?

[Leonardo de Moura]

Joseph O said:

Also, I have this error again, failed to synthesize instance OfNat (Fin' (List.length [1, 5, 4])) 7

I did not add OfNat instances in my example. I just showed you how to define the get function.

[Joseph O]

Right but I already have the OfNat instance

[Joseph O]

instance : OfNat (Fin' (List.length (a :: as))) (nat_lit 0) :=
  ⟨⟨0, (Nat.succ_pos _ : Nat.lt 0 (List.length (a :: as)))⟩⟩

[Leonardo de Moura]

Henrik Böving said:

Leonardo de Moura said:

Joseph O said:

Also, why did you decide not to consider the | nil, i case anymore?

Lean 4 can prove it is unreachable.

This is also a thing that I've been wondering about for a bit, how does it actually automagically construct this proof? Can you explain it/point me to the implementation?

https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Match/Match.lean#L148-L152

[Leonardo de Moura]

Joseph O said:

instance : OfNat (Fin' (List.length (a :: as))) (nat_lit 0) :=
  ⟨⟨0, (Nat.succ_pos _ : Nat.lt 0 (List.length (a :: as)))⟩⟩

This instance is for 0 only.

[Henrik Böving]

That looks quite a lot easier than I imagined :octopus:

[Joseph O]

Leonardo de Moura said:

Joseph O said:

instance : OfNat (Fin' (List.length (a :: as))) (nat_lit 0) :=
  ⟨⟨0, (Nat.succ_pos _ : Nat.lt 0 (List.length (a :: as)))⟩⟩

This instance is for 0 only.

Well, does that mean I have to do it manually for every literal?

[Leonardo de Moura]

@Joseph O I did not read the whole thread. I think this kind of instance is not the way to go. You could add another instance for the Nat.succ case, but I see it as an abuse of the typeclass mechanism. Moreover, you will have to do it for many other functions. These two are for List.length. Fin is like a subtype. So we often have to synthesize proofs. We can use tactics to synthesize the proofs. Example:

#eval get [1, 2, 3] ⟨0, by decide⟩

We can also create helper notation if we have to do it a lot.

notation "#(" a ")" => (Fin.mk a (by decide))

#eval get [1, 2, 3] #(0)
#eval get [1, 2, 3] #(1)
#eval get [1, 2, 3] #(2)
#eval get [1, 2, 3] #(3) -- Error

[Joseph O]

Ah cool, thanks

[Joseph O]

So i rewrote my nth function with this new Fin',

def nth {αs : List Type} : HList αs → (n : Fin' αs.length) → αs.get' n
  | cons x xs, ⟨0, _⟩ => x
  | cons x xs, ⟨n+1, h⟩ => xs.nth ⟨n, Nat.lt_of_succ_lt_succ h⟩

but,
when i try to run

#eval ⟪1,"2",3.0⟫.nth #(1)

, it gives this error

expression
  nth (1!!"2"!!3.0!!unit) { val := 1, isLt := (_ : 1 < List.length [ℕ, String, Float]) }
has type
  List.get' [ℕ, String, Float] { val := 1, isLt := (_ : 1 < List.length [ℕ, String, Float]) }
but instance
  Lean.MetaEval (List.get' [ℕ, String, Float] { val := 1, isLt := (_ : 1 < List.length [ℕ, String, Float]) })
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

[Mauricio Collares]

What's the definition of List.get'? #mwe

[Mauricio Collares]

(deleted)

[Joseph O]

def List.get' {α : Type u} : (as : List α) → (i : Fin' as.length) → α
  | a::as, ⟨0, _⟩ => a
  | a::as, ⟨i+1, h⟩ => as.get' ⟨i, Nat.lt_of_succ_lt_succ h⟩
```

[Chris B]

The error message says you need to tell Lean how to display/print the result.

[Leonardo de Moura]

@Joseph O During typeclass resolution, Lean only unfolds definitions tagged as [reducible]. The motivation is to control the cost of this procedure. The result type of your example depends on List.get'. Thus, Lean fails to build the Repr instance for the type. Here is a working example:

inductive HList : List (Type u) → Type (u+1)
  | nil  : HList []
  | cons : α → HList αs → HList (α::αs)

@[reducible] def List.get' : (as : List α) → (i : Fin as.length) → α
  | a::as, ⟨0, _⟩   => a
  | a::as, ⟨i+1, h⟩ => get' as ⟨i, Nat.lt_of_succ_lt_succ h⟩

def HList.nth : HList αs → (n : Fin αs.length) → αs.get' n
  | cons x xs, ⟨0, _⟩   => x
  | cons x xs, ⟨n+1, h⟩ => xs.nth ⟨n, Nat.lt_of_succ_lt_succ h⟩

notation "#(" a ")" => (Fin.mk a (by decide))

syntax "⟪" term,* "⟫"  : term

macro_rules
  | `(⟪ ⟫) => `(HList.nil)
  | `(⟪ $a ⟫) => `(HList.cons $a HList.nil)
  | `(⟪ $a, $as,* ⟫) => `(HList.cons $a ⟪$as,*⟫)

#eval ⟪10, true, 20.1⟫.nth #(0)
#eval ⟪10, true, 20.1⟫.nth #(1)
#eval ⟪10, true, 20.1⟫.nth #(2)

[Leonardo de Moura]

Another trick you can use is to tell Lean what type containing the List.get' reduces too. The type checker will make sure you provided the correct type.

#eval id (α := String) (⟪1,"2",3.0⟫.nth #(1))

You can also define your own identity function where all arguments are explicit.

def the (α : Type u) (a : α) := a

#eval the String (⟪1,"2",3.0⟫.nth #(1))

[Leonardo de Moura]

I pushed a small improvement to the #eval command. Now, when it fails to construct the MetaEval instance, it reduces the result type and tries again. The next nighly build should have this improvement, and your example will work without any tricks.

[Leonardo de Moura]

I also added this example to the test suite: https://github.com/leanprover/lean4/blob/master/tests/lean/run/hlistOverload.lean

[Joseph O]

Leonardo de Moura said:

I also added this example to the test suite: https://github.com/leanprover/lean4/blob/master/tests/lean/run/hlistOverload.lean

Im honored, though how were you still able to use the brackets? I remember when I was creating the macro, it would give me an error saying that [] was already taken

[Joseph O]

ah, you gave it a name. Got it. Ive always wanted to use the brackets

[Joseph O]

Ah, its actually the kind tag.

[Joseph O]

I will keep that in mind for my future macros, thanks

[Joseph O]

Do you mind explaining why this error? image.png
it has to do with using HList

[Horatiu Cheval]

Does the notation work outside of match? For instance, in #check [1, "2"]?

[Horatiu Cheval]

Might it be because there is some ToString instance for Nat? (just guessing)

[Joseph O]

image.png

[Horatiu Cheval]

And the same if you don't explicitely annotate the type in check?

[Joseph O]

It can't decide whether Im refering to list or hlist image.png

[Horatiu Cheval]

Or maybe a better experiment to test the ToString speculation, would #check ([1, "2"] : List String) also work? (I'm not really sure that what I'm saying makes sense)

[Horatiu Cheval]

Oh, so it seems that's it then

[Horatiu Cheval]

1 can be implicitely converted to the String "1"

[Joseph O]

Same error image.png

[Horatiu Cheval]

Maybe if you write (1 : Nat) inside the list notation? Though I'm skeptical, it is probably the same thing

[Horatiu Cheval]

Sorry, I don't know how to fix this, we'll have to wait for someone who knows better. At least it seems that we've figured out the root cause

[Leonardo de Moura]

@Joseph O You have to get the most recent nightly build. The support for overloaded notations in patterns has been implemented a few days ago.

[Joseph O]

Ah I see. Let me update.

[Joseph O]

Huh, seems like im on the latest.

[Joseph O]

leanprover/lean4:nightly-2022-03-09

[Joseph O]

I also have to use the same version as mathlib, or else I get errors.

[Joseph O]

`c:\Users\vatis\.elan\toolchains\leanprover--lean4---nightly\bin\lake.exe print-paths Init Mathlib.Data.Nat.Basic` failed:

stderr:
info: mathlib: trying to update .\lean_packages\mathlib to revision master
info: > LEAN_PATH=.\lean_packages\mathlib\.\build\lib;.\build\lib c:\Users\vatis\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe .\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean -R .\lean_packages\mathlib\.\. -o .\lean_packages\mathlib\.\build\lib\Mathlib\Init\Logic.olean -i .\lean_packages\mathlib\.\build\lib\Mathlib\Init\Logic.ilean -c .\lean_packages\mathlib\.\build\ir\Mathlib\Init\Logic.c
info: .\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:371:16: error: unknown identifier 'decidable_of_decidable_of_iff'
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:377:7: error: unknown identifier 'decidable_of_decidable_of_iff'
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:455:34: error: function expected at
  decidable_of_decidable_of_iff
term has type
  ?m.10918
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:456:38: error: function expected at
  decidable_of_decidable_of_iff
term has type
  ?m.10918
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:453:6: error: (kernel) declaration has metavariables 'if_ctx_simp_congr_prop'
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:460:34: error: function expected at
  decidable_of_decidable_of_iff
term has type
  ?m.11110
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:461:1: error: unknown identifier 'if_ctx_simp_congr_prop'
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:458:6: error: (kernel) declaration has metavariables 'if_simp_congr_prop'
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:480:44: error: function expected at
  decidable_of_decidable_of_iff
term has type
  ?m.11607
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:481:28: error: function expected at
  decidable_of_decidable_of_iff
term has type
  ?m.11607
.\lean_packages\mathlib\.\.\Mathlib\Init\Logic.lean:475:6: error: (kernel) declaration has metavariables 'dif_ctx_simp_congr'

error: external command c:\Users\vatis\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe exited with status 1
error: build failed

its honestly really annoying tbh

[Leonardo de Moura]

This is the latest https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2022-03-13
I just added your example to the test suite: https://github.com/leanprover/lean4/commit/672a889c83cfc00a07a78a28a9d9d99ae1a41162

[Joseph O]

It works now, thanks!

[Leonardo de Moura]

Joseph O said:

I also have to use the same version as mathlib, or else I get errors.

Recent changes in Lean seem to have broken Mathlib 4. It will be fixed soon.

[Mario Carneiro]

Mathlib4 has been updated to today's nightly now

[Joseph O]

Small questions:

1. What does Nat.lt_of_succ_lt_succ do, and why was it used here | a::as, ⟨i+1, h⟩ => get as ⟨i, Nat.lt_of_succ_lt_succ h⟩?
2. What does Nat.succ_pos do?
3. Why did lean need this instance,

instance : OfNat (Fin' (List.length (a :: as))) (nat_lit 0) :=
  ⟨⟨0, (Nat.succ_pos _ : Nat.lt 0 (List.length (a :: as)))⟩⟩

and how exactly in the second argument of the Fin' working in this instance?
4

[Joseph O]

Sorry for all the questions, but Im quite new to this way of programming

[Joseph O]

If only the functions had docstrings. But that's ok.

[Joseph O]

The core team is doing so much work already :clap:

[Henrik Böving]

Joseph O said:

If only the functions had docstrings. But that's ok.

Awaiting your diff :stuck_out_tongue_wink:

[Joseph O]

I would if I knew what they did lol

[James Gallicchio]

Joseph O said:

What does Nat.lt_of_succ_lt_succ do, and why was it used here | a::as, ⟨i+1, h⟩ => get as ⟨i, Nat.lt_of_succ_lt_succ h⟩?

The type of Nat.lt_of_succ_lt_succ should tell you everything about it; it just says that n + 1 < m + 1 implies n < m.
Similar for Nat.succ_pos, the type gives you all the information.

get expects something of type Fin as.length, which is a structure that contains a Nat and a proof that this nat is < as.length

[Kevin Buzzard]

In mathlib we give docstrings to all our definitions but to very few of our proofs for precisely this reason: the type of the proof tells you what it's a proof of.

[Joseph O]

Ok, but the question unanswered: Why did lean need this instance?

[Mario Carneiro]

Refer back to here. The OfNat (Fin' (List.length (a :: as))) (nat_lit 0) instance means that when interpreting 0 as an element of Fin' (List.length (a :: as)) it will use this instance to supply the value

[Mario Carneiro]

without it, 0 : Fin' (List.length (a :: as)) will not typecheck

[Mario Carneiro]

and with it, this expands to ⟨0, (Nat.succ_pos _ : Nat.lt 0 (List.length (a :: as)))⟩ : Fin' (List.length (a :: as))

[Joseph O]

Ah I see. But what about any other literal?

[Joseph O]

I remember that they are handled.

[Mario Carneiro]

No other literal will work in the type Fin' (List.length (a :: as)), as you can observe

[Mario Carneiro]

Like Leo said, this instance only works for 0

[Mario Carneiro]

And indeed it wouldn't be reasonable for any other literal to work because 1 might not actually be in the type if as is the empty list

[Mario Carneiro]

if as = [] then this type is Fin' 1 which only has a 0

[Mario Carneiro]

So maybe you want an instance for 1 : Fin' (List.length (a :: b :: as)) as well, and this just gets back to why this is a terrible idea

[Joseph O]

So then why did my code work?

[Joseph O]

I remember I made a function with a generic type that needed to be added, and it need an [OfNat a 0] instance as well. Why does it only need to know 0? Is this all the information it needs? What does the OfNat instance tell about a type?

[Joseph O]

Mario Carneiro said:

No other literal will work in the type Fin' (List.length (a :: as)), as you can observe

Besides 0?

[Joseph O]

Ok so i was trying to decipher this part of one of the instances:

Nat.lt_of_not_le fun h => ne_of_gt IsPos.pos (Nat.sub_eq_zero_iff_le.2 h)

So far I have:
Nat.lt_of_not_le takes in two nats and a proof of ~ a <= b, and returns a proof that b < a. I don't know where you are giving in the two nats, but fun h => ne_of_gt IsPos.pos (Nat.sub_eq_zero_iff_le.2 h) is the proof of ~ a <= b, which is evident from the type signature n ≤ i → False (I have no idea how the n and i get in the signature. In the body, you then prove that a /= b by giving in a proof of b < a to Nat.ne_of_gt (where are you giving in the two nats). I don't know what the IsPos.pos arg is doing there, as it is only proving that 0 < n, and after that you are taking the second element of Nat.sub_eq_zero_iff_le which is Nat.sub_eq_zero_of_le and giving in h which I have which has a signature of n <= i, which we are trying to prove false. in short, i have no idea how this is working

[Ruben Van de Velde]

First thing you need to know is that lean has implicit arguments, so if you give ~ a <= b to Nat.lt_of_not_le, it can figure out the a and b itself

[Ruben Van de Velde]

If h is a term of type n <= i, then Nat.sub_eq_zero_iff_le.2 h is a term of type n - i = 0.
ne_of_gt takes a term of type x > y (not sure what they are here) and gives a term of type x /= y or x = y → false; if you then apply that to an equality (n - i = 0), you get false.
So I'm guessing x = n - i, y = 0, so IsPos.pos must be x - i > 0?

[Joseph O]

yeah

[Ruben Van de Velde]

Does that connect a few dots? :)

[Joseph O]

I have to read it again but yeah

[Joseph O]

:)

[Arthur Paulino]

offtopic: I remember being mind blown by these crazy types when I only knew simple types like int, float, string etc

[Notification Bot]

Joseph O has marked this topic as unresolved.

[Joseph O]

Wait, so this whole time

notation:max "#" a:max => (Fin.mk a (by decide))

what the equivalent of

def Fin' (n : Nat) := Fin n

variable (a : α) (as : List α)

instance : OfNat (Fin' (List.length (a :: as))) (nat_lit 0) :=
  ⟨⟨0, (Nat.succ_pos _ : Nat.lt 0 (List.length (a :: as)))⟩⟩

class IsPos (n : Nat) := pos : 0 < n

instance : IsPos (Nat.succ n) := ⟨Nat.succ_pos _⟩

instance [IsPos (n - i)] : OfNat (Fin' n) i :=
  ⟨i, Nat.lt_of_not_le fun h => ne_of_gt IsPos.pos (Nat.sub_eq_zero_iff_le.2 h)⟩

:rofl:

[Joseph O]

Ruben Van de Velde said:

If h is a term of type n <= i, then Nat.sub_eq_zero_iff_le.2 h is a term of type n - i = 0.
ne_of_gt takes a term of type x > y (not sure what they are here) and gives a term of type x /= y or x = y → false; if you then apply that to an equality (n - i = 0), you get false.
So I'm guessing x = n - i, y = 0, so IsPos.pos must be x - i > 0?

yeah so now the only thing i don't understand is

ne_of_gt IsPos.pos (Nat.sub_eq_zero_iff_le.2 h)

[James Gallicchio]

What is your question about it?

[Ruben Van de Velde]

Do you know that f a b is actually (f a) b, where f is a function that takes a and returns another function that takes b?
Also, that x ≠ yis really a function that takes a proof of x = yto false?