Zulip Chat Archive

Stream: general

Topic: division on integers

Anas Himmi (Mar 26 2020 at 14:33):

how to show that ∀ a b : ℤ, a / b = 0 ↔ a = 0 ∨ b = 0 ? the converse is trivial because of int.zero_div and int.div_zero in the library but i can't prove the implication.

Mario Carneiro (Mar 26 2020 at 14:35):

it's false

Mario Carneiro (Mar 26 2020 at 14:35):

1 / 2 = 0

Anas Himmi (Mar 26 2020 at 14:36):

i'm dumb sorry for this

Kenny Lau (Mar 26 2020 at 14:51):

import data.int.basic tactic.rcases

example (a b : ℤ) : a / b = 0 ↔ b = 0 ∨ (0 ≤ a ∧ a < abs b) :=
begin
  split,
  { intro H, by_cases hb : b = 0, { left, exact hb },
    right,
    have h1 := int.mod_add_div a b, rw [H, mul_zero, add_zero] at h1,
    rw ← h1,
    exact ⟨int.mod_nonneg a hb, int.mod_lt a hb⟩ },
  { rintro (H | ⟨H1, H2⟩),
    { rw [H, int.div_zero] },
    { exact int.div_eq_zero_of_lt_abs H1 H2 } }
end

Kenny Lau (Mar 26 2020 at 14:51):

that was a fun exercise

Kevin Buzzard (Mar 26 2020 at 14:54):

I think Lean should apologise for having such a silly division. Any kid could tell you 1/2 is not 0

Kevin Buzzard (Mar 26 2020 at 14:55):

That / should just be replaced by the computer scientists' favourite pokemon character emoji or something

Kevin Buzzard (Mar 26 2020 at 14:55):

That'd warn us

Gabriel Ebner (Mar 26 2020 at 14:56):

Python uses // for integer "division".

Andrew Ashworth (Mar 26 2020 at 15:05):

are there any systems that return a [quotient, remainder] tuple for integer division?

Anne Baanen (Mar 26 2020 at 15:07):

Your computer, probably: the div instruction produces both quotient and remainder

Gabriel Ebner (Mar 26 2020 at 15:07):

The truncate function in common lisp also returns multiple values: http://clhs.lisp.se/Body/f_floorc.htm#truncate

Anne Baanen (Mar 26 2020 at 15:09):

Also /MOD in Forth

Anas Himmi (Mar 26 2020 at 15:09):

i didn't know of the by_cases tactic! i love it

Andrew Ashworth (Mar 26 2020 at 15:10):

I wonder if this is an argument for redefining the type signature of division, and what effects that would have

Johan Commelin (Mar 26 2020 at 15:13):

Well, not of has_div.div, please

Johan Commelin (Mar 26 2020 at 15:14):

We could have a has_moddiv class...

Marc Huisinga (Mar 26 2020 at 15:14):

is it not a common lean pattern to have multiple functions instead of one function that returns a conjunction or takes a disjunction?

Anne Baanen (Mar 26 2020 at 15:15):

Apart from design patterns, I expect that in practice users would project out either result often enough to make div a useful abbreviation anyway

Andrew Ashworth (Mar 26 2020 at 15:18):

I am really surprised anyone here knows Forth; FORTH LOVE IF HONK THEN !

Last updated: Dec 20 2023 at 11:08 UTC