Zulip Chat Archive

Stream: new members

Topic: member of cartesian product of sets


view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 18:44):

I'm struggling to understand why this (contrived example) doesn't compile, I don't understand how sets work really:

import analysis.normed_space.basic

variables (S R : Type*) [normed_ring R]

lemma x (f : S  R) (r : set S × S) : true :=
begin
  have :  x  r, f x.1 = f x.2 := sorry
end

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 18:47):

I think this is just the Lean 3 parser giving up on you rather than any misunderstanding on your part.

view this post on Zulip Johan Commelin (Feb 17 2021 at 18:48):

lemma x (f : S  R) (r : set (S × S)) : true :=
begin
  have :  (x : S × S) (hx : x  r), f x.1 = f x.2 := sorry
end

view this post on Zulip Johan Commelin (Feb 17 2021 at 18:48):

Note that you had another problem. Lean parses the type of r as (set S) × S

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 18:50):

Oh I see, so the point is that membership is a proposition?

view this post on Zulip Johan Commelin (Feb 17 2021 at 18:50):

yes

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 18:50):

Cool thanks

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 18:50):

#print notation × -- _ `×`:35 _:34 := prod #1 #0 -- \times has a meagre binding power of 35, and set is a function so has a binding power of something like 1000.

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 19:03):

Hm okay does this nonarchimedean_normed_ring.ultrametric look like a reasonable statement then? It compiles but I'm not sure I'm using everything correctly.

import analysis.normed_space.basic
import ring_theory.power_series.basic

open filter

noncomputable theory
open_locale big_operators

class nonarchimedean_normed_ring (R : Type*) extends normed_ring R :=
(ultrametric_inequality :  x y : R, x + y  (max x y))

variables {R : Type*} [normed_ring R]

lemma nonarchimedean_normed_ring.ultrametric {S : set R} {t : finset S} {n : nonempty S} (m: S  R) :
   x : S, ∥∑ p in t, m p  m x   y : S, m y  m x :=
begin
  sorry
end

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:04):

Functions seem to have binding power 1024 by the way:

variables (f :   ) (a b : )

def moo :      := λ a b, 0

notation a `★`:1025 b := moo a b -- will fail if you lower this to 1024

#check f a  b -- works

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:06):

For exactly this reason of binding powers, you shouldn't need () around max here:

(ultrametric_inequality :  x y : R, x + y  (max x y))

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:07):

The lemma statement looks a bit non-idiomatic too me...

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:09):

I would replace {S : set R} by {S : Type*}

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:09):

And use [nonempty S]

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:09):

I'm not sure it's true as it stands. What about if S is infinite, m is unbounded, and t is empty?

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:10):

And also what Johan says -- S doesn't need to be anything to do with R. I think you want that t is nonempty.

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 19:10):

Sorry I'm confused, basically there should only be S, I wanted t to be a proof that S is finite, but I think I'm misinterpreting what a finset is

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:11):

t : finset S means t is a finite subset of S. Maybe you want hS : S.finite then

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:11):

except that because you don't even need S to be a set, you maybe want a random nonempty finite type S.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:12):

lemma nonarchimedean_normed_ring.ultrametric {ι : Type*} [fintype ι]
[nonempty ι] (m: ι  R) :
   x : ι, ∥∑ p, m p  m x   y : ι, m y  m x :=
begin
  sorry
end

hopefully that's true.

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:13):

But actually, the version with s : finset \iota will probably be more useful in practice.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:14):

set S is the type of subsets of S, finset S is the type of finite subsets of S, set.finite is a predicate on set S saying "I am finite", fintype is a predicate on Type saying "I am finite".

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:14):

So the I would drop the [fintype \iota], replace [nonempty \iota] by (hs : s.nonempty) and \ex x : \iota by \ex x \in s.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:14):

with s : finset iota

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:17):

I totally agree that this is confusing and that there is no obvious reference to point to.

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 19:18):

Thanks that clarifies things! Then this gives an error still

lemma nonarchimedean_normed_ring.ultrametric {ι : Type*} {S : finset ι} (hS : S.nonempty) (m : S  R) :
   x  S, ∥∑ p, m p  m x   y  S, m y  m x :=
begin
  sorry
end

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 19:18):

Apparently I can't make a map out of a finset... I guess it's not a type

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:18):

Maybe you want m : iota -> R

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 19:19):

But then presumably m has to be defined on all of \iota, when I would just want it to be defined on S

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:19):

S : finset iota is a term not a type, it has type finset iota. Types have type Type. But clearly you sometimes want to think of S as a type in itself, the type of elements of S, so there is a way to coerce it into a type, but it involves up-arrows because nobody fixed it yet.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:21):

If you only want m to be defined on S then you could go with my [fintype iota] suggestion. But Johan's point is that actually if you think you have a map defined only on S, you might well find that Lean will happily let it be defined on all of iota, even if it involves things like division by 0, because this is some type theory philosophy that maps should be defined on all of a type and return junk values away from the domain of interest.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:21):

If you really only want m defined on S then there's no point having iota.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:22):

1/0=0, sup of the naturals in the reals is 0, as is sup of the empty set etc.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:22):

if you're foolish enough to give a set to the real.sup function which isn't non-empty and bounded, you'll get a junk answer rather than an error.

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:23):

Ashwin Iyengar said:

Apparently I can't make a map out of a finset... I guess it's not a type

S : finset \iota means that S has type finset \iota. S : Type means that S has type Type. The latter means "S is a type". So indeed, finsets aren't types.
It takes a bit of time to get used to, but really everything only has 1 type.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:23):

so similarly here you might think that m is only defined on S but probably it will make sense on all of iota.

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:24):

@Ashwin Iyengar for proofs it will be extremely convenient to have m defined on all of \iota, but also have s around as finset.

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:24):

It means that you can restrict the sum to a smaller finset, or do induction on the size of the finset, and all the while m : \iota \to R doesn't change.

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:25):

Thousands of lines of code about \sum x in s, m s have shown that this model is extremely convenient to work with in practice.

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 19:25):

Okay thanks. Final question, do you imagine that

lemma nonarchimedean_normed_ring.ultrametric {S : finset R} (hS : S.nonempty):
   x  S, ∥∑ p in S, p  x   y  S, y  x

would be less useful than

lemma nonarchimedean_normed_ring.ultrametric {ι : Type*} {S : finset ι} (hS : S.nonempty) (m : ι  R) :
   x  S, ∥∑ p in S, m p  m x   y  S, m y  m x

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:26):

sure

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:27):

the first is a trivial special case of the second, where two random types are being randomly decreed to be equal despite having nothing to do with each other.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:27):

Even if you have a type which you are convinced is equal to R (e.g. a type canonically isomorphic to R), Lean might not let you prove that it's equal to R.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:28):

Oh I see, you removed m too.

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:28):

I would certainly go for the second version

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:28):

I would still prove the second.

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:29):

The proof will be just as long as that of the first, but it will be much easier to apply the second version

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 19:29):

Okay thanks, maybe to convince myself I'll compare how hard it is to apply the first one vs the second one in my proof that you can multiply restricted power series

view this post on Zulip Johan Commelin (Feb 17 2021 at 19:29):

(Note that when you apply the second version, usually lean will figure out automatically what \iota and m are. But with the first version you will hit situations quickly where you want to apply it, but lean will say "nope")

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:41):

Ashwin, if you think that R[1/fg]=R[1/f][1/g]R[1/fg]=R[1/f][1/g] then your notion of what equality is is not the same as Lean's. If you think you have elements of RR and they're actually elements of a ring canonically isomorphic to RR then you need the map. Experience has shown us that having an index type is a powerful level of abstraction which covers essentially all use cases.

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 19:42):

If you really are in the situation where your map is not defined on all of iota, which does occasionally happen, then you just promote S to a type and continue anyway.

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 21:20):

Johan Commelin said:

For exactly this reason of binding powers, you shouldn't need () around max here:

(ultrametric_inequality :  x y : R, x + y  (max x y))

Oh btw it doesn't work without the () for some reason

view this post on Zulip Ashwin Iyengar (Feb 17 2021 at 21:21):

≤ seems to take priority over the application of max or something

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 23:46):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/parsing.20question.20about.20.60.E2.88.A5x.E2.88.A5.60/near/226744899

view this post on Zulip Johan Commelin (Feb 18 2021 at 04:34):

@Ashwin Iyengar ypu, you are right. sorry for making a false claim


Last updated: May 09 2021 at 19:11 UTC