markusdeEverybody gangsta about being correct by construction until they hear about grade school arithmetic
Max S. New ⚜️@markusde I think this post is designed in a lab to piss me off and yet I am too zen to take the bait
bhakti@bhaktishh @markusde do your worst
bhakti (@[email protected])
dumb category theory question that might not even make sense. I am incapable of thinking about arrows without thinking about them as functions on sets so that’s probably where is coming from So the identity arrow is the identity on composition, but can you ever construct an arrow that obeys the compositional identity but isn’t “truly” the identity? Or is there no notion of “true” identity for an abstract object as there is for a set (ie mapping each thing to itself)
@maxsnew maybe it won’t piss you off but will certainly make you wonder if I really know any category theory at all
@bhaktishh I almost dropped out of being a math major because I couldn't understand wtf was going on in my abstract algebra class so I have personal experience with these kind of questions.
@maxsnew unrelated but I *did* drop out of being a math major because I couldn’t understand why we cared about any part of real analysis. Maybe if I had the chance to take algebra before analysis I would have made it through … or not … we’ll never know
@bhaktishh @maxsnew Physics, reality, etc?
@bhaktishh @maxsnew I did do math but I didn't really start caring about analysis until I started working with verified probability stuff, where describing even exact programs that only involve integers can still need real numbers
Cody
Koz Ross
Morgan Arnold@bhaktishh @markusde @maxsnew you can do a whole lot of real analysis without believing in the real numbers! i say this as someone who does analysis and also doesn't tend to believe in the real numbers. errett bishop wrote an excellent book on real analysis from the constructivist point of a view.
a lot of classical theorems from analysis don't hold anymore (i.e. the intermediate value theorem), but it turns out that you can recover fairly similar constructive analogues of a lot of these theorems! and a lot of classical theorems should still work just fine constructively! off the top of my head, the picard-lindelhöf theorem and the weierstrass approximation theorems should still hold
@bhaktishh @markusde @maxsnew i also know that within my discipline of differential geometry there have been some really cool ideas which could be used to put the whole field on constructive footing, like locales as constructive analogues of topological spaces, or the synthetic differential geometry of lawvere. unfortunately, these ideas were discovered by category theorists, who don't seem to write down their ideas in a manner which is accessible to non-category theorists
@mra @bhaktishh @maxsnew OK I can never really tell if you're joking on here but people who unironically use the phrase "belief" when it comes to mathematical foundations then you belong in viXra prison with NJ Wildberger.
Do you really do purely synthetic differential geometry in your research? Love that for you if true but consider me skeptical.
zwarich@markusde @mra @bhaktishh @maxsnew I first got interested in topos theory long ago because of this promise of synthetic mathematics. In practice, it seems to be the sort of thing you consider after proving both results rather than using one to derive the other. And even in theory, composing distinct synthetic perspectives seems very difficult. I had hoped that proof assistants might lead to more uses of these techniques, but it hasn’t yet to come to pass.
Another sort of alternative mathematics with a transfer principle is Robinson-style nonstandard analysis, and despite many of the analogous problems being more subdued in that setting (it is much easier to include things built from the reals in a nonstandard superstructure), it alo has essentially no real usage.
Frang 
josh g.
Weekend EditorSomewhere in Mecklenburg-Schwerin, the ghost of Gottlob Frege is trembling with anger and excitement.
Lindsey Kuper
Lars Hupel 
ShadSterling
jcreed@markusde @maxsnew
A+++ great work
but wait ok I am worried I'm not seeing all the foot-rakes present here. I know about Fin literal wrapping, and saturating subtraction, but
((3 : Nat) * n) / n
is fine... isn't it?
theorem markusde_cant_fool_me (x n : ℕ) (h : n ≠ 0): (x * n) / n = x :=
Eq.symm (Nat.eq_div_of_mul_eq_left h rfl)
or are you just deliberately sowing some reasonable examples among the surprising to keep us all on our toes
@jcreed @maxsnew
> (n : ℕ) (h : n ≠ 0)
Good! I didn't tell you the type of N, but you inferred that it should probably be a natural number, and you probably need a side condition about it being nonzero.
You correctly did _not_ infer that N was some nonzero-by-construction type which would avoid that side condition at the expense of becoming completely bizarre.
chris martens@markusde @jcreed @maxsnew fwiw i think the “by construction” datasort refinement version of this is fine:
pos refines nat
* : nat -> pos -> nat
/ : nat -> pos -> nat
(n.b. for * that’s an admissible but not the most general sort, which would be an intersection)
m = (x : nat) * (n : pos) : nat
(m : nat) / (n : pos) : nat
@chrisamaphone @jcreed @maxsnew I agree that refinements like this are generally fine, datasort refinements are not that different from using a nat + positivity hypothesis anyhow.
In my eyes the best version will just set N/0=0 and require positivity hypotheses where needed. I've encountered a handful of cases where not having to prove that extra hypothesis has saved me some work or cleaned up my theorem. Admittedly, the examples I can think of involve stranger number systems than Pos (the extended and/or nonnegative reals) but even for little things like (forall N D : Nat, N / D <= N) not having to prove positivity can still be a great time saver when D is horrible.
Here are things I really do not like (from the perspective of doing verified math, mostly):
- The idiom of making some lemmas "correct by construction" by restricting their syntactic forms: forall N D, (N * S D) / S D = N
- Same goes if Pos is replaced by an inductive type & coercions
inductive Pos (n : Nat) where | isPos n : Pos (S n)
This one I find totally bizarre.
- Proof-relevant refinements, because it makes for footguns like stating forall (N : Nat) (D : Pos), (N * D) / D = N. In fairness I doubt anyone would do that for Nat.
@markusde @chrisamaphone @maxsnew the general approach of "make undefined behavior defined to some arbitrary thing, and require hypotheses" seemed REALLY bizarre to me at first encounter, but I think I'm slowly warming up to itAAAA
@jcreed @chrisamaphone @maxsnew I think it's nice in general! I think this also works really well whenever classical is appropriate, when you have access to choice [1] the property that you case on can be arbitrarily complex, and not having to prove them all the time can save a _ton_ of work.
Nuclear Oatmeal