Zulip Chat Archive

Stream: new members

Topic: injection of a subset


view this post on Zulip Damiano Testa (Aug 13 2020 at 12:04):

Given natural number r,s \in \N, I would like to define the inclusion {n : \N | n \leq r} \to {n : \N | n \leq r+s}, but I am having a hard time convincing Lean that the first set is a subset of the other.

Can someone suggest a quick way of defining the inclusion above?

More generally, is there a similar fix in the case in which S is a subset of T and I want to have the inclusion of S in T?

Thank you very much!

view this post on Zulip Sebastien Gouezel (Aug 13 2020 at 12:08):

There is inclusion in data.set.basic. Does it help you?

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:09):

It sounds promising! How can I use it?

view this post on Zulip Sebastien Gouezel (Aug 13 2020 at 12:11):

If you have h a proof that s : set alpha is included in t : set alpha, then inclusion h is the canonical inclusion from s (seen as a Type) to t (seen as a Type).

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

@Damiano Testa what do you mean by "the inclusion"? What kind of object is an inclusion?

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:12):

Ok, so then my question is how to prove that {n : ℕ | n ≤ r } is a subset of {n : ℕ | n ≤ r+s }?

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:13):

Kevin Buzzard said:

Damiano Testa what do you mean by "the inclusion"? What kind of object is an inclusion?

I have the two initial intervals of the natural numbers, from 0 to r and from 0 to r+s and I would like to view an element of the first interval as an element of the second one as well. I hope that this is clear!

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:14):

What do you mean by an element of the first interval?

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:15):

the first set is {0,1,2,...,r}, the second one is {0,1,2,...,r,r+1,...,r+s}. The first r+1 elements are in common and I would like to assign to 0 in the first interval 0 in the second and so on.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:15):

What is the type of an element of the first set?

view this post on Zulip Sebastien Gouezel (Aug 13 2020 at 12:15):

I think Kevin wants you to insist on the difference between sets and types. Are you familiar with these notions?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:16):

I know Damiano, I am just trolling him :-)

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:16):

Damiano -- it seems to me that your question is actually this: if n is a natural number then prove n<=r implies n<=r+s

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:16):

Kevin Buzzard said:

I know Damiano, I am just trolling him :-)

Glad to hear this, since I was completely lost by your question!

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:17):

But you see, as mathematicians we have 100 equivalent ways of thinking about something.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:17):

and in Lean you have to write down an explicit term, which says very precisely what you mean

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:17):

and there are ten ways to write down a term corresponding to your original vague (as far as Lean is concerned) question

view this post on Zulip Sebastien Gouezel (Aug 13 2020 at 12:18):

For the record, here is a solution to your question, but to understand it properly you should pay attention to every little detail, notably // vs. |

def my_beautiful_inclusion {r s : } : {n // n  r}  {n // n  r + s} :=
begin
  have : {n | n  r}  {n | n  r + s},
  { assume n hn,
    simp at hn,
    apply le_trans hn,
    exact nat.le.intro rfl },
  exact inclusion this
end

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:18):

Kevin Buzzard said:

Damiano -- it seems to me that your question is actually this: if n is a natural number then prove n<=r implies n<=r+s

I have been able to get Lean to accept this, but it took many lines of code and I am not sure that the result is what I want, since when I try to use it, Lean then produces lots of symbols that I do not understand...

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:18):

If you think that an inclusion is a function, then there is an issue here, because functions in Lean are functions between types, and sets in Lean are not types, they are terms

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:19):

so in some literal sense it is not even possible to write down a function between two sets

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:19):

but on the other hand of course you can do something

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:19):

but first you have to make the sets into types.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:19):

On the other hand, if all you are trying to express is that something in the first set is in the second set

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:20):

Ok, first of all, thank you @Sebastien Gouezel for the code: I will try to use it!!

Second, @Kevin Buzzard I am still trying to get my head around how to write mathematics in Lean and the distinction between sets types and terms is still hazy for me!

Anyway, thank you very much for your help!

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:20):

then you can imagine that the first set is defined by a predicate P : nat -> Prop and the second set is defined by a predicate Q : nat -> Prop, and all you have to do is to prove forall x, P x -> Q x

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:21):

As a mathematician these two ways of thinking about the problem are trivially equivalent, but as you can see they are different ways of packaging up the same information in Lean

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:21):

Sebastien posted code which constructs a function between two subtypes. Do you see he used // and not |?

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:22):

Kevin Buzzard said:

Sebastien posted code which constructs a function between two subtypes. Do you see he used // and not |?

I see it, but I suspect that I am not understanding what I am seeing! :smile:

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:23):

Here is some code which also answers your question:

import tactic

example (r s x : ) : x  r  x  r + s :=
begin
  intro h,
  linarith
end

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:23):

Sebastian has written down a function, and functions go between types, and sets are not types.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:23):

However given a set {x : X | P x} there is a corresponding type {x : X // P x} which packages up the same information in a different way

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:24):

It's like how Cauchy sequences modulo equivalence package up the same information as Dedekind cuts

view this post on Zulip Sebastien Gouezel (Aug 13 2020 at 12:24):

{n // n ≤ r} is not a subset of the integers, it's a type, so something of a different nature, in a way carved out of the integers. For instance, the integer 0 does not belong to it (and asking if it does is a question that does not even make sense)

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:25):

Kevin Buzzard said:

Sebastian has written down a function, and functions go between types, and sets are not types.

Indeed, what you wrote is more concise than what I have been using, but it is in this spirit. Yet, I feel that this approach that I was following was heavy and I think that I prefer the other... provided I understand how it works!

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:25):

So you have some mental model of how things work, and it's in some instances different to how Lean's model works.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:25):

Did you read https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/ ?

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:26):

Kevin Buzzard said:

Did you read https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/ ?

I did not: my introduction to Lean so far has been playing your natural numbers game, watching a couple of your online lectures and then using the reference manuals for lean that I found online.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:27):

So the way type theory works is that instead of this one fundamental thing \in there is one fundamental thing :

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:27):

and x : X means that the term x has the type X

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:27):

and every type is a term, but not every term is a type

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:28):

For example π : ℝ and ℝ : Type

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:28):

Every term has a unique type.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:28):

Uniqueness is quite shocking to mathematicians, because it is not our mental model for how things work

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:29):

In Lean a = b only makes sense if a and b have the same type.

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:30):

Kevin Buzzard said:

and every type is a term, but not every term is a type

Are proofs terms that are not types?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:30):

They're a great example

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:30):

and π\pi is another great example

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:30):

In set theory, π\pi is a set whose elements you don't care about (maybe they're Cauchy sequences, maybe they're Dedekind cuts, who cares)

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:31):

in type theory, π\pi is a term but not a type, so a : π makes no sense

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:31):

Kevin Buzzard said:

and π\pi is another great example

Is it correct/reasonable/fruitful to think of \pi as a proof that \R is not empty?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:31):

You can think of it like that, but the issue there is that 37 : ℝ so 37 would be a different proof because 37 \ne \pi

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:32):

and the big difference between the Type universe and the Prop universe is that if X : Type and a : X and b : X then a = b makes sense but it might not be true

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:32):

whereas if P : Prop and a : P and b : P then a = b is true by definition

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:33):

Types in the Prop universe (theorem statements) can only have one term (and if they're false then they have no terms)

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:33):

The thing which mathematicians find weird is that in type theory every term has a unique type

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:33):

Ok, this is clearing up several doubts and confusions that I had!

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:33):

so 0 : \N and 0 : \R cannot be equal

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:33):

because it does not even make sense to ask that they are equal

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:34):

Instead, there is this invisible function from nat to real and the theorem is that the image of nat's 0 is real's 0

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:34):

But when you talk about "the set {0,1,2,...,r}" you have to decide whether this set is a type or a term

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:34):

Kevin Buzzard said:

so 0 : \N and 0 : \R cannot be equal

Ok, I have struggled with this concept while playing with Magma and realizing that sometimes you need to specify such things

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:35):

and if you want it to be a type, then you write {n // n ≤ r} and now you are going to have to think very carefully about what it means to be a term of this type

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:35):

Yes, it's just the same in magma and I learnt it in just the same way

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:35):

But if x : {n // n ≤ r} then, for the same reason, x can't be a natural number

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:36):

It turns out that x is actually a pair, consisting of a natural number and a proof that it is <= r.

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:36):

Kevin Buzzard said:

and if you want it to be a type, then you write {n // n ≤ r} and now you are going to have to think very carefully about what it means to be a term of this type

So, is it not the case that a term of type {n // n ≤ r} is any natural number up to r?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:36):

A term of that type is not equal to a natural number

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:36):

Ah, you answered my question, while I was formulating it!

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:36):

Type theory enables us to think of proofs as mathematical objects, they can have names like h

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:37):

This explains why there were all these langles and rangles appearing in the Lean output!! Ahahaha

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:38):

import tactic

example (r : ) (x : {n :  // n  r}) : false :=
begin
  /-
  r: ℕ
  x: {n // n ≤ r}
  ⊢ false
  -/
  cases x with n hn,
  /-
  r n: ℕ
  hn: n ≤ r
  ⊢ false
  -/
  sorry
end

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:38):

You can extract the pair from x with the cases tactic.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:39):

And conversely given n and hn you can reconstruct x with langle and rangle

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:39):

I think that I am going to convert all my sets into types!

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:40):

import tactic

example (r : ) (x : {n :  // n  r}) : false :=
begin
  let x2 := x, -- make a copy of x before destroying it
  cases x with m hm,
  -- hm : m ≤ r
  let y : { n // n  r} := m, hm,
  have h : x2 = y,
    refl,
  sorry
end

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 12:41):

What are you doing?

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:41):

So, when I input a set into Lean, then Lean "tries" to convert it into a type and stuff becomes awkward? (I realize that this is more of a philosophical question, but I am trying to get some vague intuition for how things work.)

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:42):

Kevin Buzzard said:

What are you doing?

At the moment, I am trying to prove the statement that if a forest has at least one edge, then it has a leaf. The underlying reason is that I would like to understand how Lean works and maybe use it for some less well-known maths!

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:43):

But I am really trying to build the statement from scratch: defining graphs, defining trees/forests, and seeing which lemmas I need along the way.

view this post on Zulip Damiano Testa (Aug 13 2020 at 12:48):

Anyway, this discussion was really helpful: thank you very much! I will read the post that you sent earlier!

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 13:25):

Lean can handle sets, but it treats them as terms not types. But given a set {x | P x} you can make the corresponding subtype {x // P x}. Mathematically there is nothing happening here, it is just two ways of modelling the concept. A third way is just the function P : X -> Prop, i.e. the characteristic function of the set (P is also a term, but it's a function too; It's not a type, it has type X -> Prop which is Lean's way of saying Hom(X,{T,F}) basically). There are of course ways of moving between these three concepts, and one can prove that all the diagrams commute, but deciding what you want to use is a design implementation decision and mathematicians are often not equipped to make such decisions without some help. The natural number game involves filling in proofs in begin/end blocks -- all definitions are hidden from the user. Definitions are the hard part for mathematicians, in some sense, because we have to go from our fluid concept of what an idea is to a formal representation, i.e. literally a way to store the idea as a sequence of 0's and 1's which we are going to commit to.

view this post on Zulip Damiano Testa (Aug 13 2020 at 13:59):

Thank you so much: this is very helpful! Especially knowing what is difficult!


Last updated: May 07 2021 at 00:30 UTC