From 89e0de9fbb1c11b5b124b233ccbf300cff90fd48 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Mar 2022 13:08:59 -0800
Subject: [PATCH] chore: use WF compiler to define `Nat.mod` and `Nat.div`

---
 src/Init/Data/Nat/Div.lean | 55 +++++++++++++++++++-------------------
 1 file changed, 27 insertions(+), 28 deletions(-)

diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index a44253bd25..76082e6808 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -5,33 +5,27 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.WF
+import Init.WFTactics
 import Init.Data.Nat.Basic
 namespace Nat
 
 private def div_rec_lemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=
   fun ⟨ypos, ylex⟩ => sub_lt (Nat.lt_of_lt_of_le ypos ylex) ypos
 
-private def div.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) : Nat :=
-  if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y + 1 else zero
-
 @[extern "lean_nat_div"]
-protected def div (a b : @& Nat) : Nat :=
-  WellFounded.fix (measure id).wf div.F a b
+protected def div (x y : @& Nat) : Nat :=
+  if h : 0 < y ∧ y ≤ x then
+    Nat.div (x - y) y + 1
+  else
+    0
+termination_by div x y => x
+decreasing_by apply div_rec_lemma; assumption
 
 instance : Div Nat := ⟨Nat.div⟩
 
-private theorem div_eq_aux (x y : Nat) : x / y = if h : 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
-  congrFun (WellFounded.fix_eq (measure id).wf div.F x) y
-
-theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 :=
-  dif_eq_if (0 < y ∧ y ≤ x) ((x - y) / y + 1) 0 ▸ div_eq_aux x y
-
-private theorem div.induction.F.{u}
-        (C : Nat → Nat → Sort u)
-        (ind  : ∀ x y, 0 < y ∧ y ≤ x → C (x - y) y → C x y)
-        (base : ∀ x y, ¬(0 < y ∧ y ≤ x) → C x y)
-        (x : Nat) (f : ∀ (x₁ : Nat), x₁ < x → ∀ (y : Nat), C x₁ y) (y : Nat) : C x y :=
-  if h : 0 < y ∧ y ≤ x then ind x y h (f (x - y) (div_rec_lemma h) y) else base x y h
+theorem div_eq (x y : Nat) : x / y = if 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := by
+  simp [Nat.div] -- hack to force eq theorem to be generated. We don't have `conv` yet.
+  apply Nat.div._eq_1
 
 theorem div.inductionOn.{u}
       {motive : Nat → Nat → Sort u}
@@ -39,22 +33,27 @@ theorem div.inductionOn.{u}
       (ind  : ∀ x y, 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
       (base : ∀ x y, ¬(0 < y ∧ y ≤ x) → motive x y)
       : motive x y :=
-  WellFounded.fix (measure id).wf (div.induction.F motive ind base) x y
-
-private def mod.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) : Nat :=
-  if h : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma h) y else x
+  if h : 0 < y ∧ y ≤ x then
+    ind x y h (inductionOn (x - y) y ind base)
+  else
+    base x y h
+termination_by inductionOn x y _ _ => x
+decreasing_by apply div_rec_lemma; assumption
 
 @[extern "lean_nat_mod"]
-protected def mod (a b : @& Nat) : Nat :=
-  WellFounded.fix (measure id).wf mod.F a b
+protected def mod (x y : @& Nat) : Nat :=
+  if h : 0 < y ∧ y ≤ x then
+    Nat.mod (x - y) y
+  else
+    x
+termination_by mod x y => x
+decreasing_by apply div_rec_lemma; assumption
 
 instance : Mod Nat := ⟨Nat.mod⟩
 
-private theorem mod_eq_aux (x y : Nat) : x % y = if h : 0 < y ∧ y ≤ x then (x - y) % y else x :=
-  congrFun (WellFounded.fix_eq (measure id).wf mod.F x) y
-
-theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x :=
-  dif_eq_if (0 < y ∧ y ≤ x) ((x - y) % y) x ▸ mod_eq_aux x y
+theorem mod_eq (x y : Nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x := by
+  simp [Nat.mod] -- hack to force eq theorem to be generated. We don't have `conv` yet.
+  apply Nat.mod._eq_1
 
 theorem mod.inductionOn.{u}
       {motive : Nat → Nat → Sort u}