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
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.
