Implementing floor division (for ℕ) from scratch

Stream: new members

[Isak Colboubrani]

I'm encountering some issues with the following implementation of (floor) division for natural numbers:

def nat.div (x y : nat) : nat :=
  if 0 < y ∧ y ≤ x then
    nat.div (x - y) (y + 1)
  else
    0
decreasing_by sorry
example : nat.div (100 : nat) (10 : nat) = (10 : nat) := by rfl -- fails

The example fails with a "type mismatch" error that I can't resolve.

Consider the following:

• I'm using my own nat class for learning purposes. See the #mwe below for details. Am I missing something in the setup of nat that prevents rfl from working as expected?
• I'm using decreasing_by sorry to avoid having to prove that nat.div terminates. Although this is a temporary workaround and needs to be addressed, it shouldn't affect the outcome in this case, right?
• The force_decidable (Decidable (0 < y ∧ y ≤ x)) approach is quite hacky. Could this be the cause of the issue? If so, I will need to read up on Decidable since I don't fully understand the exact circumstances under which it is needed.

Here is the #mwe:

inductive nat
  | zero : nat
  | succ (n : nat) : nat
deriving DecidableEq

instance : OfNat nat 0 where ofNat := nat.zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where ofNat := nat.succ (OfNat.ofNat n)

def nat.add (n1 n2 : nat) : nat := match n1, n2 with
  | n1, 0 => n1
  | n1, nat.succ n2 => nat.succ (add n1 n2)
instance : Add nat where add := nat.add

def nat.pred : nat → nat
  | 0 => 0
  | nat.succ a => a
example : nat.pred (2 : nat) = (1 : nat) := by rfl
def nat.sub : nat → nat → nat
  | a, 0 => a
  | a, nat.succ b => nat.pred (nat.sub a b)
instance : Sub nat where sub := nat.sub

inductive nat.le (n : nat) : nat → Prop
  | refl : nat.le n n
  | step {m} : nat.le n m → nat.le n (nat.succ m)
instance : LE nat where le := nat.le
def nat.lt (n m : nat) : Prop :=
  nat.le (nat.succ n) m
instance : LT nat where lt := nat.lt
instance force_decidable (y x : nat) : Decidable (0 < y ∧ y ≤ x) := by sorry
def nat.div (x y : nat) : nat :=
  if 0 < y ∧ y ≤ x then
    nat.div (x - y) (y + 1)
  else
    0
decreasing_by sorry
instance : Div nat where div := nat.div
example : (100 : nat) / (10 : nat) = (10 : nat) := by rfl -- fails

[Andrew Yang]

force_decidable will not work. Decidable is essentially an algorithm that gets used by rfl in if ... then ... else and lean cannot hallucinate one if it is sorried.

[Isak Colboubrani]

Oh, thanks! It looks like I have some reading to do! Do you have any good recommendations?

[Andrew Yang]

Maybe #tpil ?

[Andrew Yang]

In particular this section

[Andrew Yang]

(not sure why the link to the section doesn't work. I mean the "decidable propositions" section in the 10. type class chapter)

[Andrew Yang]

Also I believe the definition should be nat.div (x - y) y + 1?

[Isak Colboubrani]

Thanks Andrew!

I believe I have resolved this issue. The missing components were:

instance nat.decLe (n m : nat) : Decidable (LE.le n m) :=
  dite (Eq (nat.ble n m) true) (fun h => isTrue (nat.le_of_ble_eq_true h)) (fun h => isFalse (nat.not_le_of_not_ble_eq_true h))
instance nat.decLt (n m : nat) : Decidable (LT.lt n m) :=
  nat.decLe (nat.succ n) m

… along with def nat.ble : nat → nat → Bool, and the six theorems directly or indirectly referenced: not_le_of_not_ble_eq_true, ble_eq_true_of_le, ble_succ_eq_true, ble_self_eq_true, le_of_ble_eq_true, zero_le and succ_le_succ.

Decidability indeed seems somewhat... cumbersome!

Below is the updated #mwe. Can it be improved or simplified? Are there any shortcuts, or is this level of complexity necessary for decidability? :cold_sweat:

inductive nat
  | zero : nat
  | succ (n : nat) : nat
deriving DecidableEq

instance : OfNat nat 0 where ofNat := nat.zero
instance {n : Nat} [OfNat nat n] : OfNat nat (n + 1) where ofNat := nat.succ (OfNat.ofNat n)

def nat.add (n1 n2 : nat) : nat := match n1, n2 with
  | n1, 0 => n1
  | n1, nat.succ n2 => nat.succ (add n1 n2)
instance : Add nat where add := nat.add

def nat.pred : nat → nat
  | 0 => 0
  | nat.succ a => a
def nat.sub : nat → nat → nat
  | a, 0 => a
  | a, nat.succ b => nat.pred (nat.sub a b)
instance : Sub nat where sub := nat.sub

inductive nat.le (n : nat) : nat → Prop
  | refl : nat.le n n
  | step {m} : nat.le n m → nat.le n (nat.succ m)
instance : LE nat where le := nat.le
def nat.lt (n m : nat) : Prop :=
  nat.le (nat.succ n) m
instance : LT nat where lt := nat.lt

def nat.ble : nat → nat → Bool
  | nat.zero, nat.zero => true
  | nat.zero, nat.succ _ => true
  | nat.succ _, nat.zero => false
  | nat.succ n, nat.succ m => nat.ble n m

theorem nat.succ_le_succ {n m : nat} : LE.le n m → LE.le (nat.succ n) (nat.succ m)
  | nat.le.refl => nat.le.refl
  | nat.le.step h => nat.le.step (nat.succ_le_succ h)
theorem nat.zero_le : (n : nat) → LE.le 0 n
  | zero   => nat.le.refl
  | succ n => nat.le.step (nat.zero_le n)
theorem nat.le_of_ble_eq_true {n m : nat} (h : Eq (nat.ble n m) true) : LE.le n m :=
  match n, m with
  | 0, _ => nat.zero_le _
  | succ _, succ _ => nat.succ_le_succ (nat.le_of_ble_eq_true h)
theorem nat.ble_self_eq_true : (n : nat) → Eq (nat.ble n n) true
  | 0 => rfl
  | nat.succ n => nat.ble_self_eq_true n
theorem nat.ble_succ_eq_true : {n m : nat} → Eq (nat.ble n m) true → Eq (nat.ble n (nat.succ m)) true
  | 0, _, _ => rfl
  | succ n, succ _, h => nat.ble_succ_eq_true (n := n) h
theorem nat.ble_eq_true_of_le {n m : nat} (h : LE.le n m) : Eq (nat.ble n m) true :=
  match h with
  | nat.le.refl => nat.ble_self_eq_true n
  | nat.le.step h => nat.ble_succ_eq_true (nat.ble_eq_true_of_le h)
theorem nat.not_le_of_not_ble_eq_true {n m : nat} (h : Not (Eq (nat.ble n m) true)) : Not (LE.le n m) :=
  fun h' => absurd (nat.ble_eq_true_of_le h') h

instance nat.decLe (n m : nat) : Decidable (LE.le n m) :=
  dite (Eq (nat.ble n m) true) (fun h => isTrue (nat.le_of_ble_eq_true h)) (fun h => isFalse (nat.not_le_of_not_ble_eq_true h))
instance nat.decLt (n m : nat) : Decidable (LT.lt n m) :=
  nat.decLe (nat.succ n) m

def nat.div (x y : nat) : nat :=
  if 0 < y ∧ y ≤ x then
    nat.div (x - y) y + 1
  else
    0
decreasing_by sorry
example : nat.div (100 : nat) (10 : nat) = (10 : nat) := by rfl
instance : Div nat where div := nat.div
example : (100 : Nat) / (10 : Nat) = (10 : Nat) := by rfl