## Stream: general

### Topic: unprovable equality?

#### Kevin Buzzard (Jul 10 2019 at 22:11):

Is it correct to say that if I define  posreal := {r : ℝ // 0 < r} then, remembering nnreal := {r : ℝ // 0 ≤ r}, am I right in thinking that it is impossible to prove nnreal = with_zero posreal in Lean?

#### Kevin Buzzard (Jul 10 2019 at 22:12):

@Floris van Doorn ? BTW -- nice to meet you today!

#### Floris van Doorn (Jul 10 2019 at 22:14):

That is correct. You can prove that your types are equivalent, but you can (almost) never prove that two types are equal. Therefore, it is "evil" to work with equality between types (unless you're doing homotopy type theory, where this equality is an easy consequence of univalence).

#### Kevin Buzzard (Jul 10 2019 at 22:17):

Well, the non-negative reals are equal to the disjoint union of zero and the positive reals, so how am I supposed to say this in Lean?

#### Kevin Buzzard (Jul 10 2019 at 22:18):

Every theorem about the non-negative reals is also true for the disjoint union of zero and the positive reals.

and vice versa

#### Jesse Michael Han (Jul 10 2019 at 22:53):

you would have a better shot proving that with_zero posreal is equal to the positive ennreals since both with_zero and ennreal reduce to option _

but then you're basically trying to prove

example {α : Type*} {P : α → Prop} : (option {a : α // P a}) = {a : option α // option.cases_on a true (λ x, P x)} := sorry


and i'm not sure if that's provable in Lean

#### Jesse Michael Han (Jul 10 2019 at 23:10):

with_zero seems like a construction for adjoining a generic element (by option) and guiding typeclass inference to ensure that none behaves like a zero; if i take the reals, chop off zero, and then adjoin a generic point and say it must behave like zero, i shouldn't expect the new generic point to be literally equal to the old one, only that i end up at an isomorphic copy of the reals

but if we don't discard the information of the original zero, then of course, if we have two provably equivalent predicates (0 ≤ x vs 0 < x ∨ 0 = x) their subtypes are equal

#### Kevin Buzzard (Jul 10 2019 at 23:13):

If you want to use the word "isomorphic" instead of "equal" that's fine.

#### Kevin Buzzard (Jul 10 2019 at 23:16):

Q1) True or false: the non-negative reals are equal to (or equivalent in some precise way to) the disjoint union of zero and the positive reals.

Q2) True or false: every true mathematical theorem about the non-negative reals is also true for the disjoint union of zero and the positive reals.

#### Yury G. Kudryashov (Jul 10 2019 at 23:27):

E.g., you can prove ring equivalence (see data/equiv/algebra). Unfortunately, there is no simple way to rewrite over such equivalences in Lean.

#### Yury G. Kudryashov (Jul 10 2019 at 23:34):

Types in Lean care about internal representation of its members in the memory, not about mathematical properties.

#### Yury G. Kudryashov (Jul 10 2019 at 23:36):

In particular, α × β ≠ β × α

Right.

#### Kevin Buzzard (Jul 10 2019 at 23:44):

This issue is costing me a lot of time right now.

#### Mario Carneiro (Jul 11 2019 at 01:26):

This is just the transfer problem yet again. The answer to Q1 is yes and Q2 is no, although if I show you the counterexample you will complain it's not mathematical enough

#### Andrew Ashworth (Jul 11 2019 at 01:46):

Q2: define the universal axioms of a mathematical theorem. For example, let me define a proposition that reads: "forall types, return true if types = cauchy sequence and false if types = dedekind cut". Then even though the two types of real numbers are isomorphic, we clearly have a proposition here that returns a different value for each one. In order to prove things that hold for both objects we have to restrict our propositions to the language of fields, then we can write a tactic to prove things about both of them just as the ring tactic does, which is what transfer does using relators.

#### Andrew Ashworth (Jul 11 2019 at 01:48):

I feel like there's an infinite number of dumb propositions that can distinguish between two isomorphic objects, and how is a computer supposed to infer what axioms must hold for each object? It's also true that there are an infinite number of dumb propositions that hold for two isomorphic objects. It's a human problem to decide which ones are relevant, only humans can decide what makes a property "interesting", because math is done for the sake of human curiosity.

#### Andrew Ashworth (Jul 11 2019 at 02:05):

So I guess that I'm of the opinion that Q2 is false; and all you can say easily is that all theorems in the language of semirings hold for the non negative reals and the disjoint union of zero and the positive reals, and everything else must be proven.

#### Mario Carneiro (Jul 11 2019 at 02:09):

One thing you can say is that any "property of rings" is preserved by ring isomorphism; but of course this leaves open the question of what a property of rings is, and I would define it as a property preserved by ring isomorphism

#### Mario Carneiro (Jul 11 2019 at 02:11):

By the way, you can't prove that the proposition "forall types, return true if types = cauchy sequence and false if types = dedekind cut" exists

really? why?

#### Mario Carneiro (Jul 11 2019 at 02:12):

You can define the proposition "X = cauchy reals" but you can't prove that this is false when X = dedekind reals because that's equivalent to cauchy reals != dedekind reals, and "cauchy reals = dedekind reals" is consistent with lean

#### Andrew Ashworth (Jul 11 2019 at 02:18):

One thing you can say is that any "property of rings" is preserved by ring isomorphism; but of course this leaves open the question of what a property of rings is, and I would define it as a property preserved by ring isomorphism

I can't even imagine what the algorithm would be to work backwards and figure out what additional properties of rings you would need to preserve in order to transfer a proposition between the cauchy and dedekind reals

#### Andrew Ashworth (Jul 11 2019 at 02:26):

I guess what you could do is write a hole tactic, for which you provide two isomorphic types, a list of properties, and the proposition you want to transfer. Then the tactic will recursively parse the proposition and check that each term preserves the property axioms, maybe with some sort of automatic prover. Anything left over is spit out for the human to prove.

#### Andrew Ashworth (Jul 11 2019 at 02:27):

I can already feel like there might be some problems with this but I spent about 30 seconds thinking about it.

#### Andrew Ashworth (Jul 11 2019 at 02:34):

Also suddenly your tactic is actually as complicated as an optimizing compiler

#### Mario Carneiro (Jul 11 2019 at 02:40):

I can't even imagine what the algorithm would be to work backwards and figure out what additional properties of rings you would need to preserve in order to transfer a proposition between the cauchy and dedekind reals

You don't need any additional properties - they are isomorphic as rings so any ring proposition will transfer

#### Mario Carneiro (Jul 11 2019 at 02:41):

I guess what you could do is write a hole tactic, for which you provide two isomorphic types, a list of properties, and the proposition you want to transfer. Then the tactic will recursively parse the proposition and check that each term preserves the property axioms, maybe with some sort of automatic prover. Anything left over is spit out for the human to prove.

This is basically what transfer does

#### Andrew Ashworth (Jul 11 2019 at 02:44):

Yes, but I think Kevin was interested in transferring an arbitrary proposition; so we then have the task of deciding whether or not that proposition is in the set of properties that are shared by both cauchy reals and dekekind reals

#### Andrew Ashworth (Jul 11 2019 at 02:47):

or (union of zero and the positive reals) intersect (non negative reals), as he mentioned in q2

#### Mario Carneiro (Jul 11 2019 at 02:50):

I am presuming that the isomorphism of rings is determined manually in advance

#### Andrew Ashworth (Jul 11 2019 at 02:52):

yeah, but that's what he wants, because that's what you need to make q2 = true (I think). Automatic classification of an arbitrary proposition as "mathematical" or not, where mathematical is undefined but every mathematician knows it when they see it

#### Mario Carneiro (Jul 11 2019 at 04:17):

The proof that two very different definitions of the reals are equivalent is not obvious in any sense under discussion

#### Mario Carneiro (Jul 11 2019 at 04:17):

What is obvious is all the consequences of this fact, like if the cauchy reals are noetherian then so are the dedekind reals

#### Johan Commelin (Jul 11 2019 at 04:35):

Of course cauchy vs dedekind is a red herring wrt Kevin's example. with_zero preal = nnreal is in fact obvious.

#### Johan Commelin (Jul 11 2019 at 04:37):

I think every mathematician agrees that you need to do some work to prove cauchy_reals = dedekind_reals. But for the other one they certainly won't understand what the question even means, like: "What is there to prove? Aren't they defeq?"

[/troll]

#### Floris van Doorn (Jul 11 2019 at 07:51):

Well, the non-negative reals are equal to the disjoint union of zero and the positive reals, so how am I supposed to say this in Lean?

Equality between types is evil, but equality between sets on a type is fine. You can prove in Lean that

{ x : ℝ | x > 0 } ∪ {0} = { x : ℝ | x ≥ 0 }


#### Johan Commelin (Jul 11 2019 at 07:55):

Lean even knows that this implies that the corresponding subtypes are equiv.

#### Johan Commelin (Jul 11 2019 at 07:56):

But of course the LHS of Floris's equation is not with_zero preal. You can prove that it is the image of the obvious, canonical map with_zero preal → ℝ. But then... you might as well show that the RHS is the image, which is also obvious.

#### Kevin Buzzard (Jul 11 2019 at 10:08):

So I guess that I'm of the opinion that Q2 is false;

So I think that mathematicians are very much of the opinion that Q2 is true.

#### Kevin Buzzard (Jul 11 2019 at 10:09):

yeah, but that's what he wants, because that's what you need to make q2 = true (I think). Automatic classification of an arbitrary proposition as "mathematical" or not, where mathematical is undefined but every mathematician knows it when they see it

Yes Andrew, this is exactly the issue. We know it when we see it, but it seems hard to formalise. In some sense, I don't know why this is.

Last updated: May 15 2021 at 23:13 UTC