anonymous instance?

Stream: new members

[Jeremy Teitelbaum]

In TPIL, the example syntax for the instance declaration is given as (for example)

instance Prop_inhabited : inhabited Prop := inhabited.mk true

In reading the source code for the list type, I see something like this:

instance : is_left_id (list α) has_append.append [] :=
⟨ nil_append ⟩

A few questions:

• why is there no name for this instance?
• if I do the command #print instances is_left_id if find that list.nil.is_left_id shows up, which, it seems to me, is the instance declared above. But how did it get associated with list.nil?
• I gather that the \< \> is a default constructor of some kind, so nil_append proves the claim that [] is in fact a left identity element for list.append. But how is this actually being done?

I could add that it appears the reference manual doesn't yet cover the syntax for instances.... unless I'm looking in the wrong place.

[Eric Wieser]

why is there no name for this instance?

instance will attempt to autogenerate a name for you if you do not provide one

But how did it get associated with list.nil?

Presumably it saw [] (which is syntax for list.nil) and named it after that

[Eric Wieser]

But how is this actually being done?

src#list.nil_append is the actual proof

[Jeremy Teitelbaum]

Eric Wieser said:

But how is this actually being done?

src#list.nil_append is the actual proof

I get that, but what is the purpose of the \< \>?

[Arthur Paulino]

(deleted)

[Arthur Paulino]

It's calling the constructor of is_left_id:

instance qq {α : Type} : is_left_id (list α) has_append.append [] :=
is_left_id.mk list.nil_append

[Arthur Paulino]

This is the definition of is_left_id:

@[algebra] class is_left_id (α : Type u) (op : α → α → α) (o : out_param α) : Prop :=
(left_id : ∀ a, op o a = a)

[Arthur Paulino]

I'm going to write it in a strange syntax so maybe it's clearer:

// this is not lean!
instance qq {α' : Type} = is_left_id(
  α = list α',
  op = has_append.append,
  o = []
)

[Yaël Dillies]

(Almost?) every type in Lean is an inductive type. Structures are a special kind of inductive types, with only one constructor. For structure foo, this constructor is (usually) called foo.mk and that's what ⟨ ⟩ does under the hood. ⟨h1, h2, h3⟩ : foo is interpreted as foo.mk h1 h2 h3

[Jeremy Teitelbaum]

Meanwhile list.nil_append says

lemma nil_append (s : list \alpha) : [] ++s = s := rfl

so how does this get disassembled to yield the proper arguments for is_left_id.mk?

[Yaël Dillies]

To take a familiar example, if p : P and q : Q then ⟨p, q⟩ : P ∧ Q.

[Arthur Paulino]

Jeremy Teitelbaum said:

Meanwhile list.nil_append says

lemma nil_append (s : list \alpha) : [] ++s = s := rfl

so how does this get disassembled to yield the proper arguments for is_left_id.mk?

#print list.nil_append
/-
@[_refl_lemma, _simp_cache, simp]
theorem list.nil_append : ∀ {α : Type u} (s : list α), list.nil ++ s = s :=
λ {α : Type u} (s : list α), rfl
-/

[Arthur Paulino]

replace list.nil ++ s for list.append list.nil s and you'd get:

theorem list.nil_append : ∀ {α : Type u} (s : list α), list.append list.nil s = s

[Arthur Paulino]

(deleted)

[Arthur Paulino]

That is, list.nil_append is exactly of the expected type

[Arthur Paulino]

Yes, this is uncomfortable, I get you

[Arthur Paulino]

Compare this:

∀ a, op o a = a

With this:

∀ (s : list α), list.append list.nil s = s

Can you see the pattern here?

[Jeremy Teitelbaum]

This is super helpful, thanks for your patience. I see that pattern. But that is on the right hand side of the function definition for is_left_id,
and somehow I thought we were looking for arguments for the left side (in the definition). SO when you call is_left_id.mk, the effect is
to pull this apart and extract the components?

[Yaël Dillies]

An argument being on the left or right of the : has (the immense majority of the time) no effect.

[Jeremy Teitelbaum]

I'm more concerned about the := then then :.

[Arthur Paulino]

I hope to have understood your doubt. Let's see if I did.
Going back to is_left_id, you can see:
(left_id : ∀ a, op o a = a)

If you had instead:

(foo : some_foo_type)
(bar : some_bar_type)

Calling is_left_id.mk would expect two parameters in the exact order defined above (some_foo_type then some_bar_type)

[Jeremy Teitelbaum]

Well, I just looked at is_left_id.mk and I think some light is dawning:

is_left_id.mk : (∀ (a : ?M_1), ?M_2 ?M_3 a = a) → is_left_id ?M_1 ?M_2 ?M_3

SO this is exactly what we want.

[Arthur Paulino]

Yeah, it's a function that, if you provide a term of type (∀ (a : ?M_1), ?M_2 ?M_3 a = a), it returns a term of type is_left_id ?M_1 ?M_2 ?M_3

[Arthur Paulino]

And list.nil_append is of type ∀ (s : list α), list.append list.nil s = s. So if you feed it to is_left_id.mk it will return a term of type is_left_id (list α) list.append list.nil

[Arthur Paulino]

There's extra stuff going on with this instance involving type classes. It's not a good minimal example of anonymous instance

[Jeremy Teitelbaum]

Just to beat this into the ground, suppose i do

is_left_id.mk list.nil_append

Then #check tells me that I have a term of type is_left_id (list ?M_1) list.append list.nil:

{left_id := list.nil_append ?M_1} : is_left_id (list ?M_1) append list.nil

This term has a field left_id which is list.nil_append ?M_1.

How would I fill in the placeholder ?M_1?

[Kevin Buzzard]

I'm not entirely sure of the context, but presumably ?M_1 is coming from an input in {} brackets. If you use @foo instead of foo then Lean will let you fill in the {} inputs instead of getting the unifier to do it.

[Kevin Buzzard]

e.g. #check is_left_id.mk (@list.nil_append ℕ)

[Jeremy Teitelbaum]

Yes after your comment I tried that and it cleared things up:

#check (is_left_id.mk (@list.nil_append \N ) ).left_id

is a term:

is_left_id.left_id : ∀ (a : list ℕ), list.nil ++ a = a

[Kevin Buzzard]

Alternatively tell Lean the type you expect:

#check (is_left_id.mk list.nil_append : is_left_id (list bool) append list.nil)

[Jeremy Teitelbaum]

Is it fair to say that is_left_id (list bool) append list.nil is a proposition that asserts that list.nil is a left identity for list.append, and
is_left_id.mk constructs a proof of that proposition? I need to keep types and terms of a given type straight in my head.

[Kevin Buzzard]

Yes -- is_left_id (list bool) append list.nil is the theorem statement and is_left_id.mk list.nil_append is the proof.

#check is_left_id (list bool) append list.nil -- Prop

[Kevin Buzzard]

Hovering over is_left_id you can see the ultimate output is a term of type Prop (i.e. a theorem statement, which is a kind of type), and hovering over is_left_id.mk you can see that the ultimate output is a term of type is_left_id α op o which isn't a universe so must be a type of some kind (indeed it's a proposition) so this must be a term (i.e., in this case, a proof)

[Jeremy Teitelbaum]

To return to the original question, how would one use this anonymous instance in practice? My informal interpretation is that we have
proven the general fact that list.append has a left identity element list.nil and so the list class belongs to has_append and also its append method has this property. Is there a way to see where this might be invoked?

[Henrik Böving]

In practice the instance should be automatically resolved by type class resolution whenever required.

[Arthur Paulino]

I think he's asking for an example of such "whenever required" context, but it's not clear to me either :sweat_smile:

[Jeremy Teitelbaum]

Here's a trivial example.

example : [] ++ [0,1,2] = [0,1,2] :=sorry,

It seems like this result should be relevant here.

[Kevin Buzzard]

example : [] ++ [0,1,2] = [0,1,2] := rfl ;-)

[Jeremy Teitelbaum]

Which brings me back to the question of what we needed the instance for in the first place.

[Kevin Buzzard]

example : [] ++ [0,1,2] = [0,1,2] := is_left_id.left_id _

[Arthur Paulino]

I think the instance is what allows you to prove [] ++ [0,1,2] = [0,1,2] with rfl

[Kevin Buzzard]

no, this just follows from definition of ++

[Kevin Buzzard]

Oh I take that back!

[Kevin Buzzard]

++ is not list.append, it's has_append.append

[Yaël Dillies]

Still, the is_left_id instance has nothing to do with it being refl

[Kevin Buzzard]

Yes, we're just using the fact that this works:

example (α) : has_append (list α) := infer_instance

[Yakov Pechersky]

The presence or absence of an instance is never the reason a proof is rfl, unless the instance itself _defines_ the statement you're trying to prove.

[Arthur Paulino]

How would this instance be invoked then? :thinking:

[Yaël Dillies]

What makes it refl is that it's a concrete list.

[Yakov Pechersky]

Here, ((++) : list T -> list T) = list.append := rfl because of the has_append instance. Then list.append [] s = s := rfl by the definition of list.append (as long as I got the order of args right).

[Yaël Dillies]

For an arbitrary list (by which I mean we don't know how it was built), the lemma won't be refl

[Jeremy Teitelbaum]

How about this then:

example : \forall (x: \N), [] ++ [0,1,x] = [0,1,x]:=sorry,

[Kevin Buzzard]

Lean is using the existence of list.has_append to make sense of the question, but then the question becomes list.append [] [0,1,2] = [0,1,2] which is definitionally true.

[Yaël Dillies]

We still know how [0, 1, x] was built.

[Kevin Buzzard]

What's the question?

example : ∀ (x: ℕ), [] ++ [0,1,x] = [0,1,x]:= λ x, is_left_id.left_id _

example : ∀ (x: ℕ), [] ++ [0,1,x] = [0,1,x]:= λ x, rfl

[Kevin Buzzard]

Here's an example where rfl doesn't work:

example : 0 + 37 = 37 := rfl
example (x : ℕ) : 0 + x = x := rfl -- fails

[Alex J. Best]

I think one of the issues here is that is_left_id is maybe a bit of a niche typeclass

[Alex J. Best]

So seeing where its used isn't so easy

[Kevin Buzzard]

But list.append is defined by recursion on the left variable so rfl will always work here

[Henrik Böving]

The most "practical" use case would probably be to construct more complex algebraic type classses based on it?

[Yaël Dillies]

Yes. Just the same way as when you declare a 0 on a concrete type. When you're dealing with your concrete_type you can always use the spelling concrete_type.zero instead 0. But without the has_zero concrete_type instance you can't use general machinery

[Arthur Paulino]

Feels like I'm gonna be learning the basics of Lean for the next 5 years :rofl:

[Alex J. Best]

Here's a different example:

def head [inhabited α] : list α → α
| []       := default α
| (a :: l) := a

here head is a function that takes a list and produces the first element of the list.

But what if the list was empty? We want a function from list of alphas to alphas, rather than "alpha or nothing", so one way to do this is to pick once and for all a default element of alpha for each alpha.
Of course this isn't always possible, some types are empty and have no elements after all! But when it is we can define an instance of the inhabited typeclass, which is then inferred automatically whenever head is called.
inhabited has type

class inhabited (α : Sort u) :=
(default [] : α)

so we can make an instance using

instance inst1 : inhabited ℕ := {default := 1}

but this is a bit verbose, when we just want to say a number, so this is where anonymous constructors, which are just a shorthand come in:

instance inst2: inhabited ℕ := ⟨2⟩

after defining one of these instances we can check it was inferred automatically by

lemma a : list.head [] = 2 := rfl

This example also highlights one of the main stumbling blocks with typeclasses, what if we declare more than one of the same type? In this case this is a bad thing, as then the default value of nat will depend on whichever instance lean happens to choose. So in general we have to pay attention to ensure than all instances with the same type are equal.

[Alex J. Best]

If we want to give the typeclass argument manually by hand we can do that too, by using @ to signal that we want to provide all implicit arguments for example

lemma b : @list.head ℕ inst1 [] = 1 := rfl

[Alex J. Best]

This is the only time when the name of an instance should really matter, as it is a somewhat rare situation that we need to tell lean the instance by hand

[Jeremy Teitelbaum]

In LISP (which I admit I haven't used in 30 years) if you take the car of an empty list you get a nil symbol, but I guess in lean you can't even define the head of a list unless you have some kind of default value of the same type as the list entries, is that right?

[Kevin Buzzard]

Right -- else you could take [] : list empty and make an element of the empty type which would let you prove anything

[Alex J. Best]

Yeah there are other functions like docs#list.nth that you can use instead if you want that behaviour

[Jeremy Teitelbaum]

Maybe this is too vague, but suppose you want to write a Lean function that takes a string that represents a computation in postfix notation, and return the value of the expression. You'd typically use a stack. I'm trying visualize what this might look like in lean. Is there something like this out there to look at?

[Jeremy Teitelbaum]

On the earlier point:
Alex J. Best said:

Yeah there are other functions like docs#list.nth that you can use instead if you want that behaviour

So in that case you are extending the type of elements of the list to allow for a none symbol or whatever option \alpha has.

[Kevin Buzzard]

You're only extending the type of the output to allow none but yes.

[Alex J. Best]

Jeremy Teitelbaum said:

Maybe this is too vague, but suppose you want to write a Lean function that takes a string that represents a computation in postfix notation, and return the value of the expression. You'd typically use a stack. I'm trying visualize what this might look like in lean. Is there something like this out there to look at?

Fun exercise! Here is how I would code it, note that this looks a bit different to the process of proving mathematical results in lean, but there is a lot of overlap still such as in using the equation compiler to make definitions specifying outputs corresponding to matching inputs, hope it helps!

import data.list.basic
import data.int.basic

-- following this outline from: https://www.geeksforgeeks.org/stack-set-4-evaluation-postfix-expression/
-- 1) Create a stack to store operands (or values).
-- 2) Scan the given expression and do the following for every scanned element.
-- …..a) If the element is a number, push it into the stack
-- …..b) If the element is an operator, pop operands for the operator from the stack. Evaluate the operator and push the result back to the stack
-- 3) When the expression is ended, the number in the stack is the final answer

-- this is a language of tokenised terms we will use, we do this because pattern matching on strings
-- isn't so nice in lean (roughly because strings are list of characters, which are given by nats
-- representing their ascii numeral)
inductive postfix_lang
| add : postfix_lang
| sub : postfix_lang
| mul : postfix_lang
| nat (n : ℤ) : postfix_lang

open postfix_lang

-- now we can make elements of this type like so
#check postfix_lang.add
#check postfix_lang.sub
#check postfix_lang.nat 2
-- every element is either one of these symbols or a natural number

-- converts a string token, either + - or * into the postfix lang
def of_string : string → postfix_lang
| "+" := add
| "-" := sub
| "*" := mul
| s   := nat (string.to_nat s) -- anything that doesn't match the above gets converted to a nat

-- the core of the algorithm, a recursive function that takes a list of tokens and stack of integers
-- so far and returns the new stack
def eval_postfix_aux : list postfix_lang → list ℤ → list ℤ
-- the next token is an add so we take the first two elements of the stack, add them and put it
-- back on the rest of the stack, and recurse with the remaining tokens and that stack
| (add :: r) (a :: b :: s) := eval_postfix_aux r ((b + a) :: s)
| (sub :: r) (a :: b :: s) := eval_postfix_aux r ((b - a) :: s)
| (mul :: r) (a :: b :: s) := eval_postfix_aux r ((b * a) :: s)
-- the next token is the natural number `n` so we put `n` on the stack (it is implicitly converted
-- to an integer)
| (nat n :: r) s := eval_postfix_aux r (n :: s)
| [] s := s -- if there are no operations left stop recursing and return the stack as is
| _ _ := [] -- if we see anything else there is probably a mistake

-- we can call this directly on a list of postfix_langs like so
#eval eval_postfix_aux [nat 2, nat 3, nat 1, mul, add, nat 9, sub] []
#eval eval_postfix_aux [nat 2, nat 3, nat 1, mul, add, nat 9, sub] [1] -- starting with a nonempty stack
#eval eval_postfix_aux [nat 2, nat 3, nat 1, mul, add, nat 9, sub, sub] [] -- nonsense case

-- but you asked for a function from strings to evaluations, we can do this like so:
-- call the above algorithm on a string by tokenising, running eval_postfix_aux and then taking the
-- head of the resulting list
def eval_postfix (s : string) : ℤ := (eval_postfix_aux ((s.split_on ' ').map of_string) []).head

#eval eval_postfix "2 3 1 * + 9 -"
#eval eval_postfix "2 3 1 * + 9 - 7 +"

-- we get zero if we do nonesense
#eval eval_postfix "2 3 1 * + 9 - - - -"

[Jeremy Teitelbaum]

This is fantastic, thanks!!!! :tada: :+1: :octopus:

[Eric Wieser]

Regarding docs#is_left_id (and the entire file it resides in), it's part of a major refactor of the algebraic typeclasses that was abandoned long ago. See the github link at the top of the page.

[Eric Wieser]

So the answer to "what's the instance useful for" is "not much because those typeclasses never replaced things like monoid"

[Jeremy Teitelbaum]

So much for reading the middle of source code files.

[Jeremy Teitelbaum]

@Alex J. Best following up on your parser, what about the following?
In general terms, we have the type of list postfix_lang that you've described. Then some of these are "well-formed" in the sense
that they evaluate to a number. This gives a predicate on list postfix_lang which is decidable (via your algorithm). Would such an approach make sense?

I'm not trying to give you homework, so if you think it's reasonable I can try to do it for my homework.

[Alex J. Best]

You could definitely define that predicate, either by counting number of operations vs number of nats in the list, or just asserting that eval_postfix_aux doesn't return [] I guess, hopefully one can prove they are equivalent. And it should be provable that it is a docs#decidable_pred.

[Jeremy Teitelbaum]

OK, this gives me something concrete to think about, thanks for the help!

[Alex J. Best]

Hmm I guess "counting" was a bit over-simple, and the condition is something like there are always at least 1 more number than operation in every prefix of the list?