injection of a subset

Stream: new members

[Damiano Testa]

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!

[Sebastien Gouezel]

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

[Damiano Testa]

It sounds promising! How can I use it?

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Damiano Testa]

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!

[Kevin Buzzard]

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

[Damiano Testa]

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.

[Kevin Buzzard]

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

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

Kevin Buzzard said:

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

but on the other hand of course you can do something

[Kevin Buzzard]

but first you have to make the sets into types.

[Kevin Buzzard]

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

[Damiano Testa]

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!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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:

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Sebastien Gouezel]

{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)

[Damiano Testa]

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!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

For example π : ℝ and ℝ : Type

[Kevin Buzzard]

Every term has a unique type.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

Kevin Buzzard said:

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

Are proofs terms that are not types?

[Kevin Buzzard]

They're a great example

[Kevin Buzzard]

and $\pi$ is another great example

[Kevin Buzzard]

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)

[Kevin Buzzard]

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

[Damiano Testa]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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?

[Kevin Buzzard]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

What are you doing?

[Damiano Testa]

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

[Damiano Testa]

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!

[Damiano Testa]

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.

[Damiano Testa]

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

[Kevin Buzzard]

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.

[Damiano Testa]

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