Subtraction types?

Stream: new members

[Sandy Maguire]

I'm working on a theorem that postulates x \in \R - \Z. Does lean have a notion of subtraction types? Or do I need to kludge this together with x \in R and by showing \not \exists (k : \N), coe k = x?

[Kevin Buzzard]

What is \R - \Z? Is it a subtype or a subset? There are I guess different ways you can formalise this. If x : \R then you could just say

import data.real.basic

open set

example (x : ℝ) : x ∉ range (coe : ℤ → ℝ) := sorry

[Yakov Pechersky]

Is ℝ a floor_ring? You could use things that aren't equal to their own floor.

[Kevin Buzzard]

It is a floor_ring but this is kind of clunky

[Yakov Pechersky]

Aww the thumbs up went away.

[Kevin Buzzard]

I wanted to indicate "yes it's a floor ring" but then I decided I didn't want to promote the idea of using this fact ;-)

[Yakov Pechersky]

Right, because it'd be equiv to the "not in range of coe", and one would have to show anyway that the things that _are_ equal to their own floor are exactly those that are in the range of coe.

[Kevin Buzzard]

It might all depend on how one is going to use this in the proof.

[Sandy Maguire]

Sorry --- forgot about this thread. The example is:

Suppose x∈R − Z and m∈Z such that x < m < x+ 1. Show that m is unique.

[Kevin Buzzard]

By "m is unique" you mean x < m < x + 1 -> x < n < x + 1 -> m = n right? In which case you don't need to assume that x is not an integer, this is true even in that case (for trivial reasons).

[Sandy Maguire]

Yes, that's what i mean by unique! But is this true for non-integers with lt rather than le?

[Kevin Buzzard]

import data.real.basic

example (x : ℝ) (m n : ℤ) : x < m → (m : ℝ) < x + 1 →
  x < n → (n : ℝ) < x + 1 → m = n := sorry

should be provable.

[Kevin Buzzard]

It's also true if you change x < m to x <= m and x < n to x <= n yes.

[Kevin Buzzard]

You don't ever need to assume something is a non-integer.

[Kevin Buzzard]

Where you need a non-integer is when you prove "exists m : Z, x < m < x + 1`. You don't need it for uniqueness.

[Sandy Maguire]

maybe i'm slow this morning (before coffee), but if x is an integer, then there are no integers for m, n to be between x and x + 1, right?

[Kevin Buzzard]

That's right, and that's why you can prove it, because you have a false assumption so you can prove anything.

[Sandy Maguire]

oh i see, thanks

[Kevin Buzzard]

I'm never saying "there exists an m for which this works", I'm only saying "if we have an m for which this works, then ..."

[Sandy Maguire]

that's more trivial than i was expecting :)

[Damiano Testa]

In Lean, trivial is the new hard...

[Kevin Buzzard]

And there will be a very elegant proof using le_floor or floor_le or floor_lt or whatever there is.

[Sandy Maguire]

out of personal curiosity (i'm a type guy first and foremost), is there some way to show x \in \R - \Z?

[Kevin Buzzard]

The floor function is a great example of an adjoint functor, I found to my surprise a while ago.

[Kevin Buzzard]

Sandy Maguire said:

out of personal curiosity (i'm a type guy first and foremost), is there some way to show x \in \R - \Z?

Under what assumptions? Of course this is false in general (take x = 37)

[Sandy Maguire]

sorry, show is the wrong word. subtract Z from the R type

[Kevin Buzzard]

(m : \R) <= x iff m <= floor(x)

[Kevin Buzzard]

You have to decide what the type of x is going to be. x can only have one type.

[Kevin Buzzard]

If x is going to have type real then you can just say that x is not an element of the subset of real consisting of integers.

[Sandy Maguire]

i think what you're saying is "just show it with a witness" rather than construct a new type which excludes the values

[Kevin Buzzard]

If however you want to make a completely new type R - Z, then you can make this type, and then if x is a term of that type then x will represent a real which isn't an integer, but x itself will not be a real number, which might have some annoying consequences down the line.

[Kevin Buzzard]

You can put a predicate on real saying "I am not in the range of the map from the integers" and then you can make a subtype corresponding to that predicate.

[Sandy Maguire]

i haven't yet wrapped my mind around lean's type system, and this question is just me trying to suss out where the edges are

[Sandy Maguire]

that's helpful, thanks

[Kevin Buzzard]

But then you will have a map from that subtype to the reals, and that map will not be "the identity map".

[Sandy Maguire]

while i have you, i'm trying to write a function biggest : \forall {alpha : Type}, (alpha -> \nat) -> \alpha

[Kevin Buzzard]

It will of course morally be the inclusion, but do you really want to make a new definition and then constantly apply that inclusion, prove lemmas about the definition? It is typically easier in a system like Lean to just use the definitions which are already there.

[Sandy Maguire]

which is not computable in general but probably lean can handle this?

[Kevin Buzzard]

computability isn't an issue, that's right

[Sandy Maguire]

i'm happy to restrict alpha to finite, enumerable types

[Kevin Buzzard]

Then it's nat.find on the image.

[Sandy Maguire]

i'll dig in. i really appreciate how helpful you are, kevin!

[Kevin Buzzard]

import data.real.basic

def RminusZ : Type := {x : ℝ // ¬ ∃ n : ℤ, x = n}

example (x : RminusZ) : ℝ := x -- fails because x is not a real

example (x : RminusZ) : ℝ := x.val -- works because val : RminusZ -> R

[Kevin Buzzard]

Wait, it's a bit trickier than nat.find because what happens if the map from alpha to nat isn't injective? Then you have to choose a random element whose image is the max.

[Kevin Buzzard]

i.e. you have "joint biggest" elements.

[Yakov Pechersky]

What's annoying about the new type is that it's not closed under addition.

[Yakov Pechersky]

Can one even define addition on it?

[Kevin Buzzard]

Every definition you make is annoying until you have made the API for that definition.

[Kevin Buzzard]

You can define an action of the integers on it, Z -> RminusZ -> RminusZ using addition.

[Kevin Buzzard]

But every new definition comes with a certain amount of pain, and this is why it's easier to just add in assumptions to your theorems like (hx : ¬ ∃ n : ℤ, x = n).

[Sandy Maguire]

this is an extremely fruitful discussion. i'm coming from haskell where the answer is ALWAYS "define a new type"

[Kevin Buzzard]

Because what are you going to do with x : RminusZ anyway? You'll try and compare it with other real numbers or integers, so you will never be talking about x, you'll always be talking about x.val. And then eventually you'll need the proof that x isn't an integer, which is x.property I think (I just call it x.2), and then you realise that actually all you ever needed was x.val and x.2 and you could have just started with these anyway.

[Kevin Buzzard]

I don't know anything about Haskell I'm afraid, I'm a mathematician with very little programming experience.

[Kevin Buzzard]

I've just learnt the hard way how to say things in Lean in the way which makes them easiest to prove.

[Sandy Maguire]

@Kevin Buzzard mind pushing me a bit further on the "nat.find on the image" thread? is the predicate i want that x | \forall (y : \alpha), f x > f y ?

[Kevin Buzzard]

That predicate will never hold because y can be x

[Sandy Maguire]

fair. if i restrict that part away? :)

[Kevin Buzzard]

If f isn't injective you still have problems.

[Sandy Maguire]

okay, i'll think about what i actually want

[Sandy Maguire]

thanks again