Zulip Chat Archive

Stream: new members

Topic: support_add


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 18:51):

convert finsupp.support_add, does it

view this post on Zulip 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!!

view this post on Zulip Damiano Testa (Sep 04 2020 at 18:53):

What is convert?

view this post on Zulip Damiano Testa (Sep 04 2020 at 18:53):

#check convert says unknown identifier...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 18:55):

See also tactic#convert

view this post on Zulip Damiano Testa (Sep 04 2020 at 18:55):

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

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 18:56):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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!)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kyle Miller (Sep 04 2020 at 19:09):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)))

view this post on Zulip Damiano Testa (Sep 04 2020 at 19:16):

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

view this post on Zulip Kenny Lau (Sep 04 2020 at 19:16):

just put open_locale classical at the beginning

view this post on Zulip Kenny Lau (Sep 04 2020 at 19:17):

edit: still doesn't work

view this post on Zulip 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).

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Sep 04 2020 at 19:22):

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

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Sep 04 2020 at 19:23):

Ok, this is clearer, thanks!

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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."

view this post on Zulip 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"

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Damiano Testa (Sep 04 2020 at 19:33):

This has been very informative: thanks!

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Sep 04 2020 at 21:50):

I'll try it often, then!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 05 2020 at 17:28):

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

view this post on Zulip Johan Commelin (Sep 05 2020 at 17:28):

They might serve as inspiration.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 06 2020 at 02:17):

Ouch, I see.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 06 2020 at 05:01):

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

view this post on Zulip Chris Wong (Sep 07 2020 at 05:08):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 06:05):

Thanks!

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:38):

This is also the job of exact

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:39):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:41):

It's a brilliant idea

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:41):

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

view this post on Zulip 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 α

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:43):

Just #check subsingleton and jump to definition

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:43):

Or read the docs

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:44):

Right

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:44):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:44):

So lean knows that a bunch of things are subsingletons

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:45):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:45):

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

view this post on Zulip 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

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:46):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:46):

That's not the type of fin 0

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:47):

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

view this post on Zulip 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"

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:47):

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

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:48):

So the first question is "what is the type"

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:48):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:49):

You can try #check @subsingleton

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:50):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:50):

Also look at the docstring for subsingleton

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:51):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:52):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:53):

Right

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:53):

(and all those proofs will be the same!)

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:53):

You can #check what you just posted

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:53):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:53):

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

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:54):

ok, good!

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:54):

So now the question is how to prove it

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:54):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:54):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:55):

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

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:55):

library_search says

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:55):

Oh you cheated!

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:55):

That's not the answer to the question

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:55):

You just proved the theorem yourself

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:57):

And that tactic is called apply_instance

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:57):

And I don't know if it will solve the goal -- let me know!

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:57):

example : subsingleton $ fin 0 := begin
 apply_instance,
end

solves the goal indeed!

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:57):

Great. So here's how that magic worked

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:57):

Because lean does not do magic

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:58):

You found the name of the term already

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:58):

Maybe you used library_search (which might be very slow)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:59):

But now let's #print subsingleton_fin_zero

view this post on Zulip 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

view this post on Zulip Damiano Testa (Sep 07 2020 at 11:59):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:59):

So that definition is tagged with instance

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:01):

That's why the tactic is called apply_instance.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:02):

And then other things like tactics can use the tags

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:05):

(or integers or reals or p-adics)

view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:07):

Choosing the right ones to tag is a complicated research topic

view this post on Zulip Damiano Testa (Sep 07 2020 at 12:07):

Ok

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:08):

Right

view this post on Zulip Damiano Testa (Sep 07 2020 at 12:08):

Ok

view this post on Zulip 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`

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Sep 07 2020 at 12:10):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:10):

Or fin 0, which has type Type

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:10):

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

view this post on Zulip Damiano Testa (Sep 07 2020 at 12:10):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:11):

What do you mean about the valuative criterion?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:11):

Oh you mean subsingleton schemes

view this post on Zulip Damiano Testa (Sep 07 2020 at 12:11):

yes

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:11):

Do you need Noetherian hypotheses here?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:12):

I can't remember the non noeth story

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:12):

I think Hartshorne does it

view this post on Zulip Damiano Testa (Sep 07 2020 at 12:12):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:12):

Is the statement about valuation rings?

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:13):

Wait they have two points

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:18):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:48):

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:49):

The criterion uses doubletons

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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.
    )

view this post on Zulip Johan Commelin (Sep 07 2020 at 12:55):

@Damiano Testa Yup, that makes sense

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 12:57):

That's why compact Hausdorff is such a powerful criterion

view this post on Zulip 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