# Zulip Chat Archive

## Stream: new members

### Topic: support_add

#### 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...

Can someone help me, please?

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
exact finsupp.support_add,
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
(@add_monoid.to_has_zero R
(@add_group.to_add_monoid R
(@add_comm_group.to_add_group R
(@ring.to_add_comm_group R (@division_ring.to_ring R (@field.to_division_ring R _inst_1))))))
p ∪
@finsupp.support ℕ R
(@add_monoid.to_has_zero R
(@add_group.to_add_monoid R
(@add_comm_group.to_add_group 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.

#### Bryan Gin-ge Chen (Sep 04 2020 at 18:55):

See also tactic#convert

#### 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
(@add_monoid.to_has_zero R
(@add_group.to_add_monoid R
(@add_comm_group.to_add_group 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
(@add_monoid.to_has_zero.{u_1} R
(@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1)))
(@has_add.add.{u_1}
(@finsupp.{0 u_1} nat R
(@add_monoid.to_has_zero.{u_1} R
(@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1))))
(@finsupp.has_add.{0 u_1} nat R
(@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1)))
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
(@add_monoid.to_has_zero.{u_1} R
(@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1)))
p)
(@finsupp.support.{0 u_1} nat R
(@add_monoid.to_has_zero.{u_1} R
(@add_comm_monoid.to_add_monoid.{u_1} R (@semiring.to_add_comm_monoid.{u_1} R _inst_1)))
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)))
(@has_add.add.{u_1} (@polynomial.{u_1} R _inst_1)
(@distrib.to_has_add.{u_1} (@polynomial.{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 `finset`

s 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
```

#### Johan Commelin (Sep 06 2020 at 02:17):

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`

#### Chris Wong (Sep 07 2020 at 05:08):

https://github.com/leanprover-community/mathlib/pull/4060 :smile:

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

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:43):

Just #check subsingleton and jump to definition

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

Or read the docs

#### 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?

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

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?

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

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

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

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

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

You can put `example : subsingleton $ fin 0 := begin`

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

Does the $ work there instead of the bracket? I'm on mobile

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

library_search says

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

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

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

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

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

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

Right

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

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

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

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

- you can extend it;
- 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