How to get a function from this existence theorem?

Stream: new members

[Juho Pitkänen]

I recently proved the existence and unique of remainder and integer division. I was wondering whether it was possible to get a function for the remainder out of the existence theorem. The current issue is that the existence theorem requires the divisor to be positive, so a naïve approach with Nat.find isn't working. Perhaps the function should take the dividend, the divisor, and a proof that the divisor is positive? However, I have no idea of how to implement this, apart from having a divisor as well as a proof of a property of that divisor reminding me of the BKH interpretation of a proof for existential quantification.

By the way, my code is probably horribly inefficient. I intentionally tried to prove stuff manually, but I was wondering whether Mathlib already had similar stuff, and whether if I my proofs had redundant steps that could have been avoided by alterations to the strategy. Any feedback on the code itself would be appreciated too, even if it doesn't solve my question.

remainder_exists_unique.lean

[Kenny Lau]

you can case on whether the divisor is 0

[Kenny Lau]

the syntax is if h : <condition> then f h else g h

[Kenny Lau]

Juho Pitkänen said:

horribly inefficient

as for efficiency, there's no point trying to optimise, because the Lean Nat secretly uses C (or whatever library) when doing computation

[Juho Pitkänen]

By efficiency, I was thinking about lines of code and effort required to prove something rather than performance

[Kenny Lau]

Juho Pitkänen said:

I was wondering whether Mathlib already had similar stuff

I assure you mathlib has everything you possibly need and want regarding integer division

[Juho Pitkänen]

Kenny Lau wrote:

the syntax is if h : <condition> then f h else g h

Is there a way to use the proof the condition holds? I am unsure how I'd actually use this in the context of the file

[Kenny Lau]

that's the f h part, I used the same letter h to show you that.

[Juho Pitkänen]

I think I maybe understand. I need to review the manuals. Maybe this is covered in _Functional Programming in Lean_?

[Juho Pitkänen]

For clarity, this is the statement of existence I proved in the file provided

∀n m : Nat, m > 0 → ∃q r : Nat, n = q * m + r ∧ r < m

[Robin Arnez]

I guess if you want to know how to do it with existing library stuff:

example : ∀ n m : Nat, m > 0 → ∃ q r : Nat, n = q * m + r ∧ r < m := by
  intro n m hm
  exists n / m, n % m
  rw [Nat.div_add_mod']
  exact ⟨rfl, Nat.mod_lt n hm⟩

[Juho Pitkänen]

Thanks, @Robin Arnez . Is uniqueness similarly quick and provided for by mathlib?

[Robin Arnez]

A bit less quick but still:

example : ∀ n m qa qb ra rb : Nat, n = qa * m + ra ∧ ra < m → n = qb * m + rb ∧ rb < m → qa = qb ∧ ra = rb := by
  intro n m
  have helper (q r : Nat) : n = q * m + r → r < m → r = n % m ∧ q = n / m := by
    rintro rfl hr
    rw [Nat.mul_add_mod_self_right, Nat.mod_eq_of_lt hr, Nat.add_comm,
      Nat.add_mul_div_right _ _ (Nat.zero_lt_of_lt hr), Nat.div_eq_of_lt hr, Nat.zero_add]
    exact ⟨rfl, rfl⟩
  intro qa qb ra rb ⟨h₁, h₂⟩ ⟨h₃, h₄⟩
  simp [helper qa ra h₁ h₂, helper qb rb h₃ h₄]

[Juho Pitkänen]

I see, still quite elegant. Taught me a few useful tricks and developed my mental model

[Kenny Lau]

Nat.div_mod_unique

[Kenny Lau]

(as I said above, I assure you mathlib has everything you possibly need and want regarding integer division)

[Kenny Lau]

also you seem to use "integer" to mean natural numbers? that might be a bit confusing

[Kenny Lau]

in any case both statements are true, mathlib has anything you can ever want about Nat or Int division

[Juho Pitkänen]

Kenny Lau said:

also you seem to use "integer" to mean natural numbers? that might be a bit confusing

If I’ve said integer in this thread, I’ve meant the natural numbers

[Juho Pitkänen]

Kenny Lau said:

the syntax is if h : <condition> then f h else g h

I tried the following, and I think the syntax is okay

   if h : b > 0 then Nat.find (remainder_existence a b h) else a

However, I get the error

failed to synthesize
DecidablePred fun n ↦ ∃ r, a = n * b + r ∧ r < b

I think I know the reason, that being that Lean is unsure of how to decide this proposition. Seems like this is harder than I thought. Perhaps mathlib uses an inductive definition instead and then just proves properties about it?

[Aaron Liu]

can you write down a #mwe

[Aaron Liu]

I was not expecting this error

[Aaron Liu]

and I really don't see where it could be coming from

[Aaron Liu]

oh is it on the Nat.find

[Juho Pitkänen]

Aaron Liu kirjoitti:

oh is it on the Nat.find

Indeed

[Aaron Liu]

then you may have luck swapping the existence statement around, to be ∃ r, r < b ∧ a = n * b + r instead of ∃ r, a = n * b + r ∧ r < b

[Juho Pitkänen]

Aaron Liu kirjoitti:

can you write down a #mwe

There's a link to the file I typed this in at the top. I imported Mathlib and proved the theorem remainder_existence : ∀n m : Nat, m > 0 → ∃q r : Nat, n = q * m + r ∧ r < m

[Kenny Lau]

@Juho Pitkänen indeed, mathlib knows that if the quantifier is bounded then you just need to search finitely many things, but the way to say the quantifier bounded is that it has to go on the front, meaning ∃ r, a = n * b + r ∧ r < b won't work but ∃ r, r < b ∧ a = n * b + r will

[Kenny Lau]

because Lean can't work based on intuition, it works based on very specific rules, and one of those rules is that it only looks at the form of your expression and doesn't try to guess the meaning, so it only knows about the bounded quantifier if you put it at the front

[Juho Pitkänen]

Ah, that makes sense.

[Juho Pitkänen]

theorem remex_alt : ∀n m : Nat, m > 0 → ∃q r : Nat, r < m ∧ n = q * m + r := by{
  intro n m mpos
  have remex := remainder_existence n m mpos
  cases' remex with q qh
  cases' qh with r remex
  use q
  use r
  tauto
}
def natdiv := fun a b : Nat =>
  if h : b > 0 then Nat.find (remex_alt a b h) else a

I got it to work, thanks to y'all's help.

[Kenny Lau]

btw in lean (3/0, 3%0) is (0, 3)

[Juho Pitkänen]

Ah, interesting

[Juho Pitkänen]

Actually, that makes far more sense than how I had defined it.

[Juho Pitkänen]

Looking at the way I proved Liu's alternative version of the theorem, it seems rather verbose, which could be a code smell. I initially assumed tauto would just solve it outright but apparently one has to get rid of the quantifiers first. Am I doing something wrong?

[Kenny Lau]

you mean the one where he swapped the order?

[Aaron Liu]

theorem remex_alt : ∀ n m : Nat, m > 0 → ∃ q r : Nat, r < m ∧ n = q * m + r := by
  simpa only [and_comm] using remainder_existence

[Aaron Liu]

does that work

[Juho Pitkänen]

It does! Magical

[Juho Pitkänen]

Thanks for the help, both of you