From c06c62c03efddb631472b388e4619cd6446465e2 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 22 Jun 2017 19:49:02 -0400
Subject: [PATCH] refactor(init/data/nat/gcd): define gcd using eqn compiler

---
 library/init/data/nat/gcd.lean    | 39 ++++++++++++++-----------------
 library/init/data/nat/lemmas.lean |  6 ++---
 2 files changed, 20 insertions(+), 25 deletions(-)

diff --git a/library/init/data/nat/gcd.lean b/library/init/data/nat/gcd.lean
index 211f1f2322..b6950b7abb 100644
--- a/library/init/data/nat/gcd.lean
+++ b/library/init/data/nat/gcd.lean
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 Definitions and properties of gcd, lcm, and coprime.
 -/
 prelude
-import init.data.nat.lemmas init.wf
+import init.data.nat.lemmas init.meta.well_founded_tactics
 
 open well_founded
 
@@ -14,35 +14,30 @@ namespace nat
 
 /- gcd -/
 
-def gcd.F : Π (y : ℕ), (Π (y' : ℕ), y' < y → nat → nat) → nat → nat
-| 0        f x := x
-| (succ y) f x := f (x % succ y) (mod_lt _ $ succ_pos _) (succ y)
+def gcd : nat → nat → nat
+| 0        y := y
+| (succ x) y := have y % succ x < succ x, from mod_lt _ $ succ_pos _,
+                gcd (y % succ x) (succ x)
 
-def gcd (x y : nat) := fix lt_wf gcd.F y x
 
-@[simp] theorem gcd_zero_right (x : nat) : gcd x 0 = x := congr_fun (fix_eq lt_wf gcd.F 0) x
+@[simp] theorem gcd_zero_left (x : nat) : gcd 0 x = x := by simp [gcd]
 
-@[simp] theorem gcd_succ (x y : nat) : gcd x (succ y) = gcd (succ y) (x % succ y) :=
-congr_fun (fix_eq lt_wf gcd.F (succ y)) x
+@[simp] theorem gcd_succ (x y : nat) : gcd (succ x) y = gcd (y % succ x) (succ x) :=
+by simp [gcd]
 
-theorem gcd_one_right (n : ℕ) : gcd n 1 = 1 :=
-eq.trans (gcd_succ n 0) (by rw [mod_one, gcd_zero_right])
+@[simp] theorem gcd_one_left (n : ℕ) : gcd 1 n = 1 := by simp [gcd]
 
-theorem gcd_def (x : ℕ) : Π (y : ℕ), gcd x y = if y = 0 then x else gcd y (x % y)
-| 0        := gcd_zero_right _
-| (succ y) := (gcd_succ x y).trans (if_neg (succ_ne_zero y)).symm
+theorem gcd_def (x y : ℕ) : gcd x y = if x = 0 then y else gcd (y % x) x :=
+by cases x; simp [gcd, succ_ne_zero]
 
-theorem gcd_self : Π (n : ℕ), gcd n n = n
-| 0         := gcd_zero_right _
-| (succ n₁) := (gcd_succ (succ n₁) n₁).trans (by rw [mod_self, gcd_zero_right])
+@[simp] theorem gcd_self (n : ℕ) : gcd n n = n :=
+by cases n; simp [gcd, mod_self]
 
-theorem gcd_zero_left : Π (n : ℕ), gcd 0 n = n
-| 0         := gcd_zero_right _
-| (succ n₁) := (gcd_succ 0 n₁).trans (by rw [zero_mod, gcd_zero_right])
+@[simp] theorem gcd_zero_right (n : ℕ) : gcd n 0 = n :=
+by cases n; simp [gcd]
 
-theorem gcd_rec (m : ℕ) : Π (n : ℕ), gcd m n = gcd n (m % n)
-| 0         := by rw [mod_zero, gcd_zero_left, gcd_zero_right]
-| (succ n₁) := gcd_succ _ _
+theorem gcd_rec (m n : ℕ) : gcd m n = gcd (n % m) m :=
+by cases m; simp [gcd]
 
 @[elab_as_eliminator]
 theorem gcd.induction {P : ℕ → ℕ → Prop}
diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean
index a01c50aed6..dcf1124608 100644
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@@ -884,7 +884,7 @@ nat.strong_induction_on a $ λ n,
 lemma mod_def (x y : nat) : x % y = if 0 < y ∧ y ≤ x then (x - y) % y else x :=
 by have h := mod_def_aux x y; rwa [dif_eq_if] at h
 
-lemma mod_zero (a : nat) : a % 0 = a :=
+@[simp] lemma mod_zero (a : nat) : a % 0 = a :=
 begin
   rw mod_def,
   have h : ¬ (0 < 0 ∧ 0 ≤ a),
@@ -951,10 +951,10 @@ by rw [-(zero_add (m*n)), add_mul_mod_self_left, zero_mod]
 @[simp] theorem mul_mod_left (m n : ℕ) : (m * n) % n = 0 :=
 by rw [mul_comm, mul_mod_right]
 
-theorem mod_self (n : nat) : n % n = 0 :=
+@[simp] theorem mod_self (n : nat) : n % n = 0 :=
 by rw [mod_eq_sub_mod (le_refl _), nat.sub_self, zero_mod]
 
-lemma mod_one (n : ℕ) : n % 1 = 0 :=
+@[simp] lemma mod_one (n : ℕ) : n % 1 = 0 :=
 have n % 1 < 1, from (mod_lt n) (succ_pos 0),
 eq_zero_of_le_zero (le_of_lt_succ this)