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

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