Addition on ℝ

[lowasser]

As requested, a big, self-contained larger review.

[fredrik-bakke]

The fact that you have to do so many long proofs just to be able to define addition tells us that we are in need of additional infrastructure. I believe a good starting point would be to do the following (but you're the expert on real numbers here):

• Factor out a file on lower Dedekind real numbers/lower Dedekind cuts
• Factor out a file on upper Dedekind real numbers/upper Dedekind cuts
• Factor out a file on located cuts
• Factor out a file about addition on lower Dedekind real numbers
• Factor out a file about addition on upper Dedekind real numbers

[fredrik-bakke]

You could also even start by writing a file on Minkowski sums of subsets of a monoid (that is what you're doing on the lower and upper cuts of the sum of two real numbers).

[lowasser]

You could also even start by writing a file on Minkowski sums of subsets of a monoid (that is what you're doing on the lower and upper cuts of the sum of two real numbers).

Before I get too deep into this: I don't see what the advantage is of making this about monoids, as opposed to semigroups.

[fredrik-bakke]

You could also even start by writing a file on Minkowski sums of subsets of a monoid (that is what you're doing on the lower and upper cuts of the sum of two real numbers).

Before I get too deep into this: I don't see what the advantage is of making this about monoids, as opposed to semigroups.

Oh, yeah, sure. The agda-unimath way would be to have a file for each, who build on each other. But you don't have to go that far. Something like the following should be true though:

• The Minkowski sum operation on a semigroup defines a semigroup
• The Minkowski sum operation on a monoid defines a monoid
• The Minkowski sum operation on a commutative monoid defines a commutative monoid

[lowasser]

I'm going that far. But I think I will break Minkowski sums out into a separate review, just because that seems like a good self-contained unit. (Also, I'm calling it a Minkowski product, since semigroups and monoids both use mul terminology?)

[fredrik-bakke]

Great! Yes, that sounds like a good unit for a PR. Thank you for doing that. Actually, aren't the results I listed useful to you to show that addition of reals is associative, unital, and commutative respectively?

[fredrik-bakke]

Perhaps call it Monkowski multiplication. The term product is used a lot to denote cartesian products, and since Minkowski operations are about operations on subtypes, it sounds like it would be easy to confuse the two.

[EgbertRijke]

Perhaps call it Monkowski multiplication. The term product is used a lot to denote cartesian products, and since Minkowski operations are about operations on subtypes, it sounds like it would be easy to confuse the two.

This would be very neat! But I'd say the most decisive factor for what to name something is what it is commonly known as in the literature. Probably it is best to refer to a standard text on monoids, and see what they call the pointwise product of two subsets of a monoid, use that name in the library, and cite that text.

[lowasser]

Minkowski stuff is now in #1309.

[fredrik-bakke]

I'll convert this PR to a draft. The approach seems to be that you will implement this in steps somewhat according to the discussion here. Is that correct?

[fredrik-bakke]

By the way, the typechecker has been stuck on addition-real-numbers for over 5 hours now. Clearly, performance needs to be considered for this implementation.

[lowasser]

Yes. My bad.

[VojtechStep]

Did you close the PR because you're not working on addition of real numbers, or because there are some blockers? For WIP PRs and interdependent PRs we use Drafts, to make it clear that you have the intention of eventually having it merged. Closing a PR is more of a "I ran out of steam, someone else can pick this formalization target up"

[lowasser]

I expect to rewrite it almost completely at this point, is what's going on, in terms of lower and upper Dedekind cuts. That can be a draft if that's more conventional.

[lowasser]

(The other reason I closed it was because, as stated, CI was stuck on it, and I didn't want it to consume resources. Actually, in retrospect, that convinced me to leave it closed unless you explicitly say so.)