unprovable equality?

Stream: general

[Kevin Buzzard]

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]

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

[Floris van Doorn]

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]

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]

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

[Kevin Buzzard]

and vice versa

[Kevin Buzzard]

Ask any mathematician

[Jesse Michael Han]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Yury G. Kudryashov]

In particular, α × β ≠ β × α

[Kevin Buzzard]

Right.

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Andrew Ashworth]

really? why?

[Mario Carneiro]

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]

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]

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]

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

[Andrew Ashworth]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

the transfer stuff won't help you with that proof

[Andrew Ashworth]

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]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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?"

[Johan Commelin]

[/troll]

[Floris van Doorn]

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]

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

[Johan Commelin]

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]

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]

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.