From db583550fd043ec81e05568ef78b58783bbac259 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 14 Sep 2021 19:18:12 -0700
Subject: [PATCH] feat: add `Lean.Rat` for implementing decision procedures

---
 src/Lean/Data.lean                |   1 +
 src/Lean/Data/Rat.lean            | 125 ++++++++++++++++++++++++++++++
 tests/lean/rat1.lean              |  20 +++++
 tests/lean/rat1.lean.expected.out |  16 ++++
 4 files changed, 162 insertions(+)
 create mode 100644 src/Lean/Data/Rat.lean
 create mode 100644 tests/lean/rat1.lean
 create mode 100644 tests/lean/rat1.lean.expected.out

diff --git a/src/Lean/Data.lean b/src/Lean/Data.lean
index de84c8f733..8a12a68ac4 100644
--- a/src/Lean/Data.lean
+++ b/src/Lean/Data.lean
@@ -21,3 +21,4 @@ import Lean.Data.SMap
 import Lean.Data.Trie
 import Lean.Data.PrefixTree
 import Lean.Data.NameTrie
+import Lean.Data.Rat
diff --git a/src/Lean/Data/Rat.lean b/src/Lean/Data/Rat.lean
new file mode 100644
index 0000000000..7404c7469d
--- /dev/null
+++ b/src/Lean/Data/Rat.lean
@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+namespace Lean
+
+/-!
+  Rational numbers for implementing decision procedures.
+  We should not confuse them with the Mathlib rational numbers.
+-/
+
+structure Rat where
+  private mk ::
+    num : Int
+    den : Nat := 1
+  deriving Inhabited, BEq
+
+instance : ToString Rat where
+  toString a := if a.den == 1 then toString a.num else s!"{a.num}/{a.den}"
+
+instance : Repr Rat where
+  reprPrec a _ := if a.den == 1 then repr a.num else s!"({a.num} : Rat)/{a.den}"
+
+@[inline] def Rat.normalize (a : Rat) : Rat :=
+  let n := Nat.gcd a.num.natAbs a.den
+  if n == 1 then a else { num := a.num / n, den := a.den / n }
+
+def mkRat (num : Int) (den : Nat) : Rat :=
+  if den == 0 then { num := 0 } else Rat.normalize { num, den }
+
+namespace Rat
+
+protected def lt (a b : Rat) : Bool :=
+  if a.num < 0 && b.num >= 0 then
+    return true
+  else if a.num == 0 then
+    return b.num > 0
+  else if a.num > 0 && b.num <= 0 then
+    return false
+  else
+    -- `a` and `b` must have the same sign
+   a.num * b.den < b.num * a.den
+
+protected def mul (a b : Rat) : Rat :=
+  let g1 := Nat.gcd a.den b.num.natAbs
+  let g2 := Nat.gcd a.num.natAbs b.den
+  { num := (a.num / g2)*(b.num / g1)
+    den := (b.den / g2)*(a.den / g1) }
+
+protected def inv (a : Rat) : Rat :=
+  if a.num < 0 then
+    { num := - a.den, den := a.num.natAbs }
+  else if a.num == 0 then
+    a
+  else
+    { num := a.den, den := a.num.natAbs }
+
+protected def div (a b : Rat) : Rat :=
+  Rat.mul a b.inv
+
+protected def add (a b : Rat) : Rat :=
+  let g := Nat.gcd a.den b.den
+  if g == 1 then
+    { num := a.num * b.den + b.num * a.den, den := a.den * b.den }
+  else
+    let den := (a.den / g) * b.den
+    let num := (b.den / g) * a.num + (a.den / g) * b.num
+    let g1  := Nat.gcd num.natAbs g
+    if g1 == 1 then
+      { num, den }
+    else
+      { num := num / g1, den := den / g1 }
+
+protected def sub (a b : Rat) : Rat :=
+  let g := Nat.gcd a.den b.den
+  if g == 1 then
+    { num := a.num * b.den - b.num * a.den, den := a.den * b.den }
+  else
+    let den := (a.den / g) * b.den
+    let num := (b.den / g) * a.num - (a.den / g) * b.num
+    let g1  := Nat.gcd num.natAbs g
+    if g1 == 1 then
+      { num, den }
+    else
+      { num := num / g1, den := den / g1 }
+
+protected def neg (a : Rat) : Rat :=
+  { a with num := - a.num }
+
+instance : LT Rat where
+  lt a b := (Rat.lt a b) = true
+
+instance (a b : Rat) : Decidable (a < b) :=
+  inferInstanceAs (Decidable (_ = true))
+
+instance : LE Rat where
+  le a b := ¬(b < a)
+
+instance (a b : Rat) : Decidable (a ≤ b) :=
+  inferInstanceAs (Decidable (¬ _))
+
+instance : Add Rat where
+  add := Rat.add
+
+instance : Sub Rat where
+  sub := Rat.sub
+
+instance : Neg Rat where
+  neg := Rat.neg
+
+instance : Mul Rat where
+  mul := Rat.mul
+
+instance : Div Rat where
+  div a b := a * b.inv
+
+instance : OfNat Rat n where
+  ofNat := { num := n }
+
+instance : Coe Int Rat where
+  coe num := { num }
+
+end Rat
+end Lean
diff --git a/tests/lean/rat1.lean b/tests/lean/rat1.lean
new file mode 100644
index 0000000000..64d2ffd380
--- /dev/null
+++ b/tests/lean/rat1.lean
@@ -0,0 +1,20 @@
+import Lean.Data.Rat
+open Lean
+
+#eval (15 : Rat) / 10
+#eval (15 : Rat) / 10 + 2
+#eval (15 : Rat) / 10 - 2
+#eval (-2 : Rat).inv
+#eval (2 :  Rat).inv == (1 : Rat) / 2
+#eval (-2 :  Rat).inv == (-1 : Rat) / 2
+#eval (4 : Rat)/9 * (3 : Rat)/10
+#eval (4 : Rat)/9 * (-3 : Rat)/10
+#eval (1 : Rat) < (-1 : Rat)
+#eval (-1 : Rat) < (1 : Rat)
+#eval (-1 : Rat)/2 < (1 : Rat)
+#eval (-1 : Rat) < 0
+#eval (-1 : Rat)/2 < 0
+#eval 0 < (-1 : Rat)/2
+#eval (1 : Rat)/3 < (1 : Rat)/2
+#eval (1 : Rat)/2 < (1 : Rat)/3
+-- TODO: add more tests
diff --git a/tests/lean/rat1.lean.expected.out b/tests/lean/rat1.lean.expected.out
new file mode 100644
index 0000000000..12edc8c4b8
--- /dev/null
+++ b/tests/lean/rat1.lean.expected.out
@@ -0,0 +1,16 @@
+(3 : Rat)/2
+(7 : Rat)/2
+(-1 : Rat)/2
+(-1 : Rat)/2
+true
+true
+(2 : Rat)/15
+(-2 : Rat)/15
+false
+true
+true
+true
+true
+false
+true
+false