proper subtraction

Stream: general

[Kevin Buzzard]

In thinking about experimental extensions to the natural number game, I wondered where I could add "proper subtraction", where you only allow x - y to typecheck if the system can find a proof that y<=x. What would be some nice Lean 4 ways of doing this? I want to be secretly powered by linarith or something. Oh -- I don't even know if linarith works in NNG4 for their bespoke nats.

[Henrik Böving]

First thing that comes to mind: Some code that takes a proof as an argument where the argument has a default value of := by linarith because Lean evaluates these default values in the context of the caller so it can use information from the call site to derive the property.

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

Is there a proper tutorial on how to work with subtypes? Wouldn't/Couldn't proper subtraction be implemented with subtypes?

[Siddhartha Gadgil]

A first sketch (essentially from my course):

/-- Subtract `m` and `n` in the presence of a proof that `n ≤ m`. -/
def minus (m n : ℕ)(hyp : n ≤ m) : ℕ :=
  match m, n, hyp with
  | m, 0, _ => m
  | 0, _ +1, pf => nomatch pf
  | m + 1, n + 1 , pf =>
    minus m n (le_of_succ_le_succ pf)

#eval minus 5 3 (by decide) -- 2

macro n:term "-₀" m:term : term => do
  `(minus $n $m (by decide))

#eval 5 -₀ 3 -- 2

[Siddhartha Gadgil]

Here is a variant using the - symbol and falling back to the usual subtraction in cases other than natural numbers. There is an error for natural numbers if the proof fails.

elab(priority:=high) n:term "-" m:term : term =>
  Term.withoutErrToSorry do
  try
    Term.elabTermEnsuringType (← `(minus $n $m (by decide))) (mkConst ``Nat)
  catch _ =>
    let n ← Term.elabTerm n none
    let m ← Term.elabTerm m none
    mkAppM ``HSub.hSub #[n, m]

#eval (5 : ℤ) - (6 : ℤ)
#eval 6 - 5 -- 1
-- #eval 5 - 6 -- error