## Stream: new members

#### Damiano Testa (Sep 04 2020 at 18:49):

Dear All,

I am trying to get Lean to check that the support of the sum of two polynomials is contained in the union of the supports. I found the command finsupp.support_add, claiming to do exactly this. Unfortunately, with the #mwe below, I get an error. I imagine that Lean has coerced something in the wrong type, but I have been unable to figure out what...

Thank you!

import tactic
import data.polynomial.degree.basic

lemma supps {R : Type*} [field R] {p q : polynomial R} : (p+q).support ⊆ p.support ∪ q.support :=
begin
end


Error (with finsupp underlined in red in the code):

invalid type ascription, term has type
(?m_4 + ?m_5).support ⊆ ?m_4.support ∪ ?m_5.support
but is expected to have type
(p + q).support ⊆ p.support ∪ q.support
state:
R : Type u_1,
_inst_1 : field R,
p q : polynomial R
⊢ (p + q).support ⊆ p.support ∪ q.support


#### Kevin Buzzard (Sep 04 2020 at 18:51):

convert finsupp.support_add, does it

#### Damiano Testa (Sep 04 2020 at 18:52):

@Kevin Buzzard Thank you so much!! I wasted so much time trying to figure out what types Lean was inferring!!

#### Damiano Testa (Sep 04 2020 at 18:53):

What is convert?

#### Damiano Testa (Sep 04 2020 at 18:53):

#check convert says unknown identifier...

#### Kevin Buzzard (Sep 04 2020 at 18:54):

exact @finsupp.support_add _ _ _ p q, gives the following error:

invalid type ascription, term has type
(p + q).support ⊆
@finsupp.support ℕ R
(@ring.to_add_comm_group R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
p ∪
@finsupp.support ℕ R
(@ring.to_add_comm_group R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
q
but is expected to have type
@finsupp.support ℕ R
(@mul_zero_class.to_has_zero R
(@monoid_with_zero.to_mul_zero_class R
(@semiring.to_monoid_with_zero R
(@ring.to_semiring R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
(p + q) ⊆
@finsupp.support ℕ R
(@mul_zero_class.to_has_zero R
(@monoid_with_zero.to_mul_zero_class R
(@semiring.to_monoid_with_zero R
(@ring.to_semiring R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
p ∪
@finsupp.support ℕ R
(@mul_zero_class.to_has_zero R
(@monoid_with_zero.to_mul_zero_class R
(@semiring.to_monoid_with_zero R
(@ring.to_semiring R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
q


and we can see if we can debug this.

#### Kevin Buzzard (Sep 04 2020 at 18:54):

convert is a tactic, so #check doesn't work. You can hover over it to see the docstring.

#### Damiano Testa (Sep 04 2020 at 18:55):

They do look different, but I do not know why...

#### Kevin Buzzard (Sep 04 2020 at 18:56):

Me neither -- this is what type class inference is doing under the hood.

#### Damiano Testa (Sep 04 2020 at 18:57):

Ok, anyway, I am glad that I learned how to see what Lean is doing and I will now learn convert!

#### Kevin Buzzard (Sep 04 2020 at 18:59):

def X := @finsupp.support ℕ R
(@ring.to_add_comm_group R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))

def Y := @finsupp.support ℕ R
(@mul_zero_class.to_has_zero R
(@monoid_with_zero.to_mul_zero_class R
(@semiring.to_monoid_with_zero R
(@ring.to_semiring R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))

example : @X = @Y := rfl


So those outputs were more similar than we thought.

#### Damiano Testa (Sep 04 2020 at 19:01):

I interpret this as Lean having found 2 separate ways of loosing information to obtain a semi-quasi-almost-monoid and then being confused about why they are the same... is this more or less correct?

#### Kevin Buzzard (Sep 04 2020 at 19:03):

Well, exact is failing so there are some things which really are not equal by definition. We have to dig deeper:

import tactic
import data.polynomial.degree.basic

variables {R : Type*} [field R] {p q : polynomial R}

set_option pp.all true -- NEW

lemma supps  : (p+q).support ⊆ p.support ∪ q.support :=
begin
exact @finsupp.support_add _ _ _ p q,
end


#### Damiano Testa (Sep 04 2020 at 19:06):

Btw, also assuming semiring things do not work with exact: that might have less overhead of conversion...

#### Damiano Testa (Sep 04 2020 at 19:07):

(I'm feeding my cats, so I can only type with my phone for a couple minutes!)

#### Kevin Buzzard (Sep 04 2020 at 19:08):

import tactic
import data.polynomial.degree.basic

variables {R : Type*} [semiring R] {p q : polynomial R}

set_option pp.all true

lemma supps  : (p+q).support ⊆ p.support ∪ q.support :=
begin
exact @finsupp.support_add _ _ _ p q,
end

def X :=  @has_subset.subset.{0} (finset.{0} nat) (@finset.has_subset.{0} nat)
(@finsupp.support.{0 u_1} nat R
(@finsupp.{0 u_1} nat R
p
q))
(@has_union.union.{0} (finset.{0} nat)
(@finset.has_union.{0} nat (λ (a b : nat), classical.prop_decidable (@eq.{1} nat a b)))
(@finsupp.support.{0 u_1} nat R
p)
(@finsupp.support.{0 u_1} nat R
q))

def Y :=  @has_subset.subset.{0} (finset.{0} nat) (@finset.has_subset.{0} nat)
(@finsupp.support.{0 u_1} nat R
(@mul_zero_class.to_has_zero.{u_1} R
(@monoid_with_zero.to_mul_zero_class.{u_1} R (@semiring.to_monoid_with_zero.{u_1} R _inst_1)))
(@semiring.to_distrib.{u_1} (@polynomial.{u_1} R _inst_1) (@polynomial.semiring.{u_1} R _inst_1)))
p
q))
(@has_union.union.{0} (finset.{0} nat) (@finset.has_union.{0} nat (λ (a b : nat), nat.decidable_eq a b))
(@finsupp.support.{0 u_1} nat R
(@mul_zero_class.to_has_zero.{u_1} R
(@monoid_with_zero.to_mul_zero_class.{u_1} R (@semiring.to_monoid_with_zero.{u_1} R _inst_1)))
p)
(@finsupp.support.{0 u_1} nat R
(@mul_zero_class.to_has_zero.{u_1} R
(@monoid_with_zero.to_mul_zero_class.{u_1} R (@semiring.to_monoid_with_zero.{u_1} R _inst_1)))
q))

example : @X = @Y := rfl -- fails


#### Kyle Miller (Sep 04 2020 at 19:08):

In case it's helpful, I've expanded out convert as tactics:

lemma supps {R : Type*} [field R] {p q : polynomial R} : (p + q).support ⊆ p.support ∪ q.support :=
begin
have h := @finsupp.support_add _ _ _ p q,
apply eq.mpr _ h,
congr,
end


#### Kyle Miller (Sep 04 2020 at 19:09):

Now it's congr that's doing the heavy lifting, somehow.

#### Kevin Buzzard (Sep 04 2020 at 19:13):

example : @X R _inst_1 p q = @Y R _inst_1 p q :=
begin
unfold X,
unfold Y,
-- refl, -- fails
congr' -- works
end


Right, so you've got to the same stage as me but without the ugly staring at types. Nice!

#### Kyle Miller (Sep 04 2020 at 19:14):

I've gotten down to finset.has_union not equaling finset.has_union by refl:

lemma supps {R : Type*} [field R] {p q : polynomial R} : (p + q).support ⊆ p.support ∪ q.support :=
begin
have h := @finsupp.support_add _ _ _ p q,
apply eq.mpr _ h,
congr_core',
-- finset ℕ = finset ℕ
refl,
-- finset.has_subset = finset.has_subset
refl,
-- (p + q).support = (p + q).support
refl,
-- p.support ∪ q.support = p.support ∪ q.support
-- refl doesn't work!
congr_core',
-- finset ℕ = finset ℕ
refl,
swap,
-- p.support = p.support
refl,
swap,
-- q.support = q.support
refl,
-- finset.has_union = finset.has_union
-- refl doesn't work!

end


#### Kevin Buzzard (Sep 04 2020 at 19:15):

Here's another way:

lemma supps {R : Type*} [field R] {p q : polynomial R} : (p + q).support ⊆ p.support ∪ q.support :=
begin
have h := @finsupp.support_add _ _ _ p q,
apply eq.mpr _ h,
congr' 2,
refl, -- fails
end


Note congr' 3 solves the goal.

#### Kyle Miller (Sep 04 2020 at 19:15):

It looks like it's the decidability proof for finset's union:

⊢ @eq.{1} (has_union.{0} (finset.{0} nat)) (@finset.has_union.{0} nat (λ (a b : nat), nat.decidable_eq a b))
(@finset.has_union.{0} nat (λ (a b : nat), classical.prop_decidable (@eq.{1} nat a b)))


#### Damiano Testa (Sep 04 2020 at 19:16):

Can I say that finsets are evil? They always cause problems for me...

#### Kenny Lau (Sep 04 2020 at 19:16):

just put open_locale classical at the beginning

#### Kenny Lau (Sep 04 2020 at 19:17):

edit: still doesn't work

#### Kevin Buzzard (Sep 04 2020 at 19:17):

So @Damiano Testa the solution is that nat.decidable_eq a b is not equal by definition to classical.prop_decidable (@eq.{1} nat a b).

#### Damiano Testa (Sep 04 2020 at 19:18):

Ok, I am not sure that I understand, but at least I am getting a sense of what is happening...

#### Kevin Buzzard (Sep 04 2020 at 19:20):

variables (a b : ℕ)

example : nat.decidable_eq a b = classical.prop_decidable (@eq.{1} nat a b) := rfl -- fails

example : subsingleton (decidable (a = b)) := by apply_instance -- works


This is why exact fails but convert works.

#### Damiano Testa (Sep 04 2020 at 19:22):

@Kevin Buzzard are your two examples equivalent mathematically? I do not really understand what they say...

#### Kevin Buzzard (Sep 04 2020 at 19:22):

It turns out that the two terms were not exactly the same. Lean's type class inference system fills in a lot of missing information for you -- that's its job. When you have (a b : nat) and write a + b this literally means has_add.add a b. Lean now has to figure out exactly the addition you mean, and it asks the type class inference system for an addition on the naturals, and the type class inference system returns one.

When you were trying to use the finsupp lemma to prove a result about polynomials, Lean twice had to ask the type class inference system for a proof that it is possible to decide whether two naturals are equal -- first when you stated the theorem, and secondly when you used the term that you hoped would prove it. However it got two different answers.

#### Damiano Testa (Sep 04 2020 at 19:23):

Ok, this is clearer, thanks!

#### Kevin Buzzard (Sep 04 2020 at 19:24):

By the way, the reason it's asking for this is that for finitely supported functions, the way they are implemented, the support is part of the data, and for Lean to figure out exactly which naturals are in the support it needs an algorithm to work out if two naturals are equal. It found two algorithms.

#### Damiano Testa (Sep 04 2020 at 19:25):

I had thought that the issue was with identifying the supports of the sum and the individual supports as being sets in the same ambient space... If I understand correctly, the issue was at a deeper level

#### Kevin Buzzard (Sep 04 2020 at 19:25):

The first one is nat.decidable_eq:

instance : decidable_eq ℕ
| zero     zero     := is_true rfl
| (succ x) zero     := is_false (λ h, nat.no_confusion h)
| zero     (succ y) := is_false (λ h, nat.no_confusion h)
| (succ x) (succ y) :=
match decidable_eq x y with
| is_true xeqy := is_true (xeqy ▸ eq.refl (succ x))
| is_false xney := is_false (λ h, nat.no_confusion h (λ xeqy, absurd xeqy xney))
end


This is the algorithm which uses induction: zero = zero, and succ m = succ n iff m = n.

#### Kevin Buzzard (Sep 04 2020 at 19:27):

But classical.prop_decidable just says "oh come on, x=y is a true-false statement, and mathematicians believe in the law of the excluded middle, which means that an algorithm exists for figuring out whether this is true or false, and let's use that algorithm."

#### Kevin Buzzard (Sep 04 2020 at 19:28):

These are definitely two different algorithms, not least because one of them isn't really an algorithm, it's just switching on a switch which says "forget the algorithm stuff, we are mathematicians and do not care about decidable equality"

#### Kevin Buzzard (Sep 04 2020 at 19:29):

However, Lean also knows that both these algorithms are correct, and hence must produce the same answer. Hence the algorithms must be equal, if we define equal algorithms in a highly mathematical way as "must produce the same answer".

#### Damiano Testa (Sep 04 2020 at 19:30):

This is making more sense. This is now off a tangent and is completely irrelevant for the purpose of my original question: why did Lean once use nat.decidable and once classical.prop_decidable?

#### Kevin Buzzard (Sep 04 2020 at 19:30):

For example, there is only one "sort" function, which takes a finite list of natural numbers and returns the same list but sorted. Two functions are equal if and only if they output the same output given the same input, right?

#### Kevin Buzzard (Sep 04 2020 at 19:30):

But computer scientists would argue that there were many sorting algorithms, because they care about the implementation and not just the output.

#### Damiano Testa (Sep 04 2020 at 19:31):

Kevin Buzzard said:

For example, there is only one "sort" function, which takes a finite list of natural numbers and returns the same list but sorted. Two functions are equal if and only if they output the same output given the same input, right?

It is similar to using or not using the bound given by GRH to compute class groups...

#### Kevin Buzzard (Sep 04 2020 at 19:31):

convert is clever. It looks for subsingleton instances, and if it finds them then it uses them. So convert can find a proof that a = b if it knows that a : T and b : T and subsingleton T.

#### Kevin Buzzard (Sep 04 2020 at 19:32):

well the problem with the GRH algorithm is that we haven't yet proved that it works :-)

#### Kevin Buzzard (Sep 04 2020 at 19:33):

The reason Lean found both is because they are both in the system, and Lean used different methods to look for them and found them both.

#### Damiano Testa (Sep 04 2020 at 19:33):

Kevin Buzzard said:

well the problem with the GRH algorithm is that we haven't yet proved that it works :-)

Right, but should GRH be true, the two algorithms are the same!

Anyway, I understand the difference, thanks!

#### Damiano Testa (Sep 04 2020 at 19:33):

This has been very informative: thanks!

#### Kevin Buzzard (Sep 04 2020 at 19:33):

One could fiddle with instance priorities to try and make this not happen, but this is beyond my pay grade. I have no idea why Lean finds them both.

#### Damiano Testa (Sep 04 2020 at 19:34):

Kevin Buzzard said:

One could fiddle with instance priorities to try and make this not happen, but this is beyond my pay grade. I have no idea why Lean finds them both.

Sure and, for me, already just knowing that I could use convert was a pretty good answer!

#### Kevin Buzzard (Sep 04 2020 at 21:47):

convert is a great tactic when something which should work, doesn't. It's also a cool way of reasoning -- I use it a lot. You kind of know what the last line of the proof is, approximately, early on, and convert lets you apply it it immediately.

#### Damiano Testa (Sep 04 2020 at 21:50):

I'll try it often, then!

#### Adam Topaz (Sep 04 2020 at 21:54):

I also think convert is great, but one thing to keep in mind: sometimes it spits out incomprehensible nonsense. When this has happened to me, it was always my fault, and just meant that I needed to do a bit more work before using it.

#### Kevin Buzzard (Sep 05 2020 at 15:08):

@Damiano Testa I looked into this a bit more. The file data.finsupp.basic in mathlib has the following warning at the beginning:

A general piece of advice is to not use α →₀ β directly, as the type class setup might not be a
good fit. Defining a copy and selecting the instances that are best suited for the application works
better.

## Implementation notes

This file is a noncomputable theory and uses classical logic throughout.

## Notation

This file defines α →₀ β as notation for finsupp α β.


So what's happening is that when you use finsupp.support_add it uses classical logic to deal with the decidable equality issues, but when you use polynomial it uses constructive logic.

I can't find polynomial.support_add in mathlib -- you should make a PR adding it, and proving it using convert.

#### Damiano Testa (Sep 05 2020 at 17:26):

Kevin Buzzard said:

I can't find polynomial.support_add in mathlib -- you should make a PR adding it, and proving it using convert.

I will try it!

#### Johan Commelin (Sep 05 2020 at 17:27):

Kevin Buzzard said:

So what's happening is that when you use finsupp.support_add it uses classical logic to deal with the decidable equality issues, but when you use polynomial it uses constructive logic.

Whut? polynomial is quite classical I would think.

#### Johan Commelin (Sep 05 2020 at 17:28):

@Damiano Testa There are lemmas called support_add. But maybe about multivariate polynomials.

#### Johan Commelin (Sep 05 2020 at 17:28):

They might serve as inspiration.

#### Kevin Buzzard (Sep 05 2020 at 19:35):

@Johan Commelin

import tactic
import data.polynomial.degree.basic

set_option pp.all true

lemma supps {R : Type*} [semiring R] {p q : polynomial R} :
(p+q).support ⊆ p.support ∪ q.support :=
begin
have h := @finsupp.support_add _ _ _ p q,
-- h uses classical.prop_decidable
-- polynomials (the goal) use nat.decidable
sorry
end


Ouch, I see.

#### Chris Wong (Sep 06 2020 at 02:59):

convert is clever. It looks for subsingleton instances, and if it finds them then it uses them. So convert can find a proof that a = b if it knows that a : T and b : T and subsingleton T.

Should this be mentioned in the docs somewhere? That's the first time I've heard that.

#### Scott Morrison (Sep 06 2020 at 04:42):

Yes, it should be! Interested in making a documentation-only PR, that adds a sentence to the doc-string for convert?

#### Mario Carneiro (Sep 06 2020 at 05:01):

It's actually a feature of congr, which is inherited by congr' and convert

Thanks!

#### Damiano Testa (Sep 07 2020 at 07:35):

I am glad that @Chris Wong took care of this, since, even after looking at the suggestion, I am still unsure about what all this means!

Thanks!

#### Kevin Buzzard (Sep 07 2020 at 11:38):

@Damiano Testa The job of tactics like convert and congr is to try and prove that two terms are equal.

#### Kevin Buzzard (Sep 07 2020 at 11:38):

This is also the job of exact

#### Kevin Buzzard (Sep 07 2020 at 11:39):

exact is quick because it works with definitional equality which is exactly what lean is good at

#### Kevin Buzzard (Sep 07 2020 at 11:39):

But convert is more powerful because it has a second trick up its sleeve

#### Kevin Buzzard (Sep 07 2020 at 11:41):

If it has a : X and b : X and it can't prove that they are definitionally equal, it asks the type class inference system if perchance it knows a proof that X is a subsingleton

#### Kevin Buzzard (Sep 07 2020 at 11:41):

It's a brilliant idea

#### Kevin Buzzard (Sep 07 2020 at 11:41):

Subsingleton is a class so the type class system is very happy to manage this job

#### Damiano Testa (Sep 07 2020 at 11:42):

What is a subsingleton? I am reading #print subsingleton, but I cannot say that I understand the output.

@[class]
inductive subsingleton : Sort u → Prop
constructors:
subsingleton.intro : ∀ {α : Sort u}, (∀ (a b : α), a = b) → subsingleton α


#### Kevin Buzzard (Sep 07 2020 at 11:42):

Which means that occasionally convert gets lucky, finds an instance of subsingleton X, unwraps it to get a proof of "for all a and b : X, a=b" (the definition of subsingleton) and then applies this and moves on

#### Kevin Buzzard (Sep 07 2020 at 11:44):

Use #print just to get technical information such as whether a certain lemma is tagged with [simp]. You almost always don't want #print.

#### Damiano Testa (Sep 07 2020 at 11:44):

Ok, so subsingleton is a singleton where you do not assume that it has one element, right? it is a type with at most one term, correct?

Right

#### Damiano Testa (Sep 07 2020 at 11:44):

Ok, indeed looking at the definition was much easier to understand than print!

#### Kevin Buzzard (Sep 07 2020 at 11:44):

So lean knows that a bunch of things are subsingletons

#### Damiano Testa (Sep 07 2020 at 11:45):

(I did not realize that #print and jumping to the definition were different)

#### Kevin Buzzard (Sep 07 2020 at 11:45):

Like presumably fin 0 and fin 1 (do you know how to check?)

#### Kevin Buzzard (Sep 07 2020 at 11:46):

#print gives you a description which doesn't use any variables and which doesn't display the docstring

#### Damiano Testa (Sep 07 2020 at 11:46):

#check (fin 0) : subsingleton  did not work...

#### Kevin Buzzard (Sep 07 2020 at 11:46):

That's not the type of fin 0

#### Kevin Buzzard (Sep 07 2020 at 11:47):

fin 0 has type Type  because it's what I'd call a set

#### Kevin Buzzard (Sep 07 2020 at 11:47):

So I asked "can you see if the type class system knows that fin 0 is a subsingleton"

#### Damiano Testa (Sep 07 2020 at 11:47):

Ok, so I do not know how to check whether fin 0 is a subsingleton

#### Kevin Buzzard (Sep 07 2020 at 11:48):

And the thing we have to do is to turn this into a question of the form "make a term of a type"

#### Kevin Buzzard (Sep 07 2020 at 11:48):

So the first question is "what is the type"

#### Kevin Buzzard (Sep 07 2020 at 11:48):

And the second question is what to use to make the term

#### Kevin Buzzard (Sep 07 2020 at 11:49):

You can try #check @subsingleton

#### Kevin Buzzard (Sep 07 2020 at 11:50):

That's the sort of output I'd find useful for making the type

#### Kevin Buzzard (Sep 07 2020 at 11:50):

Also look at the docstring for subsingleton

#### Damiano Testa (Sep 07 2020 at 11:51):

Lean says: subsingleton : Sort u_1 → Prop, so I understand that subsingleton takes a term of type u_1 and produces a proposition, likely saying whether or not what I feed to subsingleton is a subsingleton!

#### Kevin Buzzard (Sep 07 2020 at 11:51):

So what is the type that we want to construct a term of?

#### Kevin Buzzard (Sep 07 2020 at 11:52):

The translation into Lean of the statement of the theorem that fin 0 is a subsingleton?

#### Damiano Testa (Sep 07 2020 at 11:53):

we would like subsingleton (fin 0) is the type whose terms will be proofs of what we want, right?

Right

#### Damiano Testa (Sep 07 2020 at 11:53):

(and all those proofs will be the same!)

#### Kevin Buzzard (Sep 07 2020 at 11:53):

You can #check what you just posted

#### Damiano Testa (Sep 07 2020 at 11:53):

I get
subsingleton (fin 0) : Prop, which I confirms that this is a proposition!

#### Kevin Buzzard (Sep 07 2020 at 11:53):

And observe that it has type Prop which means it's a theorem statement

ok, good!

#### Kevin Buzzard (Sep 07 2020 at 11:54):

So now the question is how to prove it

#### Damiano Testa (Sep 07 2020 at 11:54):

so now I would like to know that there are terms in this type

#### Damiano Testa (Sep 07 2020 at 11:55):

library_search says

lemma ss : subsingleton (fin 0) :=
begin
exact subsingleton_fin_zero,
end


Oh you cheated!

#### Kevin Buzzard (Sep 07 2020 at 11:55):

That's not the answer to the question

#### Kevin Buzzard (Sep 07 2020 at 11:55):

You just proved the theorem yourself

#### Kevin Buzzard (Sep 07 2020 at 11:56):

You don't want convert saying "ok they're equal as long as you can prove that the following things are subsingletons"

#### Damiano Testa (Sep 07 2020 at 11:56):

Kevin Buzzard said:

You can put example : subsingleton $fin 0 := begin This compiles, I added end after and Lean interprets it as looking for a term of the correct type #### Kevin Buzzard (Sep 07 2020 at 11:56): We need to use a tactic which doesn't involve knowing the name of the term beforehand #### Kevin Buzzard (Sep 07 2020 at 11:57): And that tactic is called apply_instance #### Kevin Buzzard (Sep 07 2020 at 11:57): And I don't know if it will solve the goal -- let me know! #### Damiano Testa (Sep 07 2020 at 11:57): example : subsingleton$ fin 0 := begin
apply_instance,
end


solves the goal indeed!

#### Kevin Buzzard (Sep 07 2020 at 11:57):

Great. So here's how that magic worked

#### Kevin Buzzard (Sep 07 2020 at 11:57):

Because lean does not do magic

#### Kevin Buzzard (Sep 07 2020 at 11:58):

You found the name of the term already

#### Kevin Buzzard (Sep 07 2020 at 11:58):

Maybe you used library_search (which might be very slow)

#### Damiano Testa (Sep 07 2020 at 11:58):

Kevin Buzzard said:

Maybe you used library_search (which might be very slow)

Yes, I do not like using it

#### Kevin Buzzard (Sep 07 2020 at 11:59):

But now let's #print subsingleton_fin_zero

#### Kevin Buzzard (Sep 07 2020 at 11:59):

To see what's going on under the hood. Can you post the output? I'm on mobile

#### Damiano Testa (Sep 07 2020 at 11:59):

@[instance]
protected def subsingleton_fin_zero : subsingleton (fin 0) :=
fin_zero_equiv.subsingleton


#### Kevin Buzzard (Sep 07 2020 at 11:59):

So that definition is tagged with instance

#### Kevin Buzzard (Sep 07 2020 at 12:00):

And all the type class inference system does is that it's a fast program written in C or C++ or something which looks through everything tagged with instance and sees if anything helps

#### Kevin Buzzard (Sep 07 2020 at 12:01):

That's why the tactic is called apply_instance.

#### Damiano Testa (Sep 07 2020 at 12:01):

Ah, so apply_instance is similar to library_search, except that it only searches for statements tagged instance?

#### Kevin Buzzard (Sep 07 2020 at 12:02):

All of those @[derive decibable_equality, ext, simp] things you see lying around in mathlib are just literally doing nothing more than tagging words onto the names of theorems and definitions

#### Kevin Buzzard (Sep 07 2020 at 12:02):

And then other things like tactics can use the tags

#### Kevin Buzzard (Sep 07 2020 at 12:03):

Right, apply_instance is similar but it's only looking at instances. But there's also another thing

#### Kevin Buzzard (Sep 07 2020 at 12:04):

This tactic is running behind the scenes all of the time because the elaborator is calling it every time you write 2+2

#### Kevin Buzzard (Sep 07 2020 at 12:04):

The elaborator sees this and says to the type class inference system "do you happen to know an addition on the naturals"

#### Kevin Buzzard (Sep 07 2020 at 12:05):

(or integers or reals or p-adics)

#### Damiano Testa (Sep 07 2020 at 12:05):

This probably explains why sometimes, when I type 1 : something, Lean then asks me for a has_one instance, right?

#### Kevin Buzzard (Sep 07 2020 at 12:05):

And the type class inference system says "sure, they're a semiring, let me just look up the addition for you"

#### Kevin Buzzard (Sep 07 2020 at 12:06):

Because there are functions defined in lean saying things like "if you are a semiring then you have an addition" and a carefully chosen collection are tagged with instance

#### Kevin Buzzard (Sep 07 2020 at 12:07):

Choosing the right ones to tag is a complicated research topic

Ok

#### Kevin Buzzard (Sep 07 2020 at 12:07):

In Lean 4 the algorithm will be replaced by a completely different one so we will have to learn how to use it from scratch

#### Damiano Testa (Sep 07 2020 at 12:08):

so, all terms in Prop are subsingletons, right? (this is just to make sure that I understand the definitions)

#### Kevin Buzzard (Sep 07 2020 at 12:08):

But if you just want to do mathematics then we basically have worked out what works best in lean 3

Right

Ok

#### Kevin Buzzard (Sep 07 2020 at 12:09):

So that means lean will be able to make a term of type subsingleton P if P : Prop

#### Johan Commelin (Sep 07 2020 at 12:09):

But some things are subsingleton even though they don't have type Prop. Like prime_spectrum K.

#### Damiano Testa (Sep 07 2020 at 12:10):

yes, ok, I only meant it as an example, not an exhaustive one!

#### Kevin Buzzard (Sep 07 2020 at 12:10):

Or fin 0, which has type Type

#### Kevin Buzzard (Sep 07 2020 at 12:10):

It's all the propositions and all the sets with at most one element

#### Damiano Testa (Sep 07 2020 at 12:10):

for instance, I guess that you could formulate the valuative criterion of separatedness using subsingletons

#### Kevin Buzzard (Sep 07 2020 at 12:11):

You can model a false proposition as a set with no elements and a true one as a set with one element

#### Kevin Buzzard (Sep 07 2020 at 12:11):

What do you mean about the valuative criterion?

#### Kevin Buzzard (Sep 07 2020 at 12:11):

Oh you mean subsingleton schemes

yes

#### Kevin Buzzard (Sep 07 2020 at 12:11):

Do you need Noetherian hypotheses here?

#### Kevin Buzzard (Sep 07 2020 at 12:12):

I can't remember the non noeth story

#### Kevin Buzzard (Sep 07 2020 at 12:12):

I think Hartshorne does it

#### Damiano Testa (Sep 07 2020 at 12:12):

in the proof, you reduce to something being noetherian, but the statement may not require it

#### Kevin Buzzard (Sep 07 2020 at 12:12):

Is the statement about valuation rings?

#### Kevin Buzzard (Sep 07 2020 at 12:13):

Wait they have two points

#### Damiano Testa (Sep 07 2020 at 12:14):

yes, so i think that you can formulate the valuative criterion without noetherian hypotheses, but then they crop up somewhere...

#### Kevin Buzzard (Sep 07 2020 at 12:18):

General valuation rings can have more than two primes. Subsingleton is less than two

#### Damiano Testa (Sep 07 2020 at 12:24):

Ok, I had in mind the statement of the valuative criterion for "reasonable" schemes: I think that if X is of finite type, then you only need to check dvrs in the valuative criteria

#### Kevin Buzzard (Sep 07 2020 at 12:48):

Yes and this doesn't change the fact that fin 2 is not a subsingleton :-)

#### Kevin Buzzard (Sep 07 2020 at 12:49):

The criterion uses doubletons

#### Damiano Testa (Sep 07 2020 at 12:50):

Ok, I see what you are saying! I was thinking that once you fix the generic morphism, then there is at most one way of filling it in...

#### Damiano Testa (Sep 07 2020 at 12:51):

so, one of the elements of the doubleton is fixed and the other one is... a subsingleton! Ahahaha

#### Damiano Testa (Sep 07 2020 at 12:52):

(at least, this is how i view the valuative criteria: you are given the generic map and all you want to do is know if

1. you can extend it;
2. if so, can you extend it uniquely.
)

#### Johan Commelin (Sep 07 2020 at 12:55):

@Damiano Testa Yup, that makes sense

#### Kevin Buzzard (Sep 07 2020 at 12:55):

Oh I see! Yes you should have formalised what you meant. Yes, separated is at most one, there's some adjective which is at least one and then proper is singleton

#### Damiano Testa (Sep 07 2020 at 12:56):

Great! I realize that explaining subsingleton via the valuative criteria is maybe not the most direct route...

#### Kevin Buzzard (Sep 07 2020 at 12:57):

There's a way of formalising the definition of compact to mean some statement involving filters has at least one answer, and a way of formalising Hausdorff so that it says the same statement has at most one answer

#### Kevin Buzzard (Sep 07 2020 at 12:57):

Basically certain filters have at least one limit in a compact space and at most one limit in a Hausdorff space

#### Kevin Buzzard (Sep 07 2020 at 12:57):

That's why compact Hausdorff is such a powerful criterion

#### Damiano Testa (Sep 07 2020 at 12:59):

I think that what you described is very close to my intuition for proper

Last updated: May 14 2021 at 00:42 UTC