feat: Rat functionality for ring (#1711)

We implement #1189.
 


Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib/Algebra/Field/Basic.lean

@@ -99,6 +99,8 @@ theorem div_neg (a : K) : a / -b = -(a / b) := by rw [← div_neg_eq_neg_div]
 
 theorem inv_neg : (-a)⁻¹ = -a⁻¹ := by rw [neg_inv]
 
+theorem inv_neg_one : (-1 : K)⁻¹ = -1 := by rw [← neg_inv, inv_one]
+
 end DivisionMonoid
 
 section DivisionRing

Mathlib/Tactic/NormNum/Basic.lean

@@ -163,7 +163,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
       let r1 : Q(Int.add (Int.mul $na $db) (Int.mul $nb $da) = Int.mul $k $nc) :=
         (q(Eq.refl $t1) : Expr)
       let r2 : Q(Nat.mul $da $db = Nat.mul $k $dc) := (q(Eq.refl $t2) : Expr)
-      return (.isRat dα qc nc dc q(isRat_add $pa $pb $r1 $r2) : Result q($a + $b))
+      return (.isRat' dα qc nc dc q(isRat_add $pa $pb $r1 $r2) : Result q($a + $b))
     match ra, rb with
     | .isBool .., _ | _, .isBool .. => failure
     | .isRat dα .., _ | _, .isRat dα .. => ratArm dα
@@ -254,7 +254,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
       let r1 : Q(Int.sub (Int.mul $na $db) (Int.mul $nb $da) = Int.mul $k $nc) :=
         (q(Eq.refl $t1) : Expr)
       let r2 : Q(Nat.mul $da $db = Nat.mul $k $dc) := (q(Eq.refl $t2) : Expr)
-      return (.isRat dα qc nc dc q(isRat_sub $pa $pb $r1 $r2) : Result q($a - $b))
+      return (.isRat' dα qc nc dc q(isRat_sub $pa $pb $r1 $r2) : Result q($a - $b))
     match ra, rb with
     | .isBool .., _ | _, .isBool .. => failure
     | .isRat dα .., _ | _, .isRat dα .. => ratArm dα
@@ -318,7 +318,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
         (q(Eq.refl (Int.mul $na $nb)) : Expr)
       have t2 : Q(ℕ) := mkRawNatLit dd
       let r2 : Q(Nat.mul $da $db = Nat.mul $k $dc) := (q(Eq.refl $t2) : Expr)
-      return (.isRat dα qc nc dc q(isRat_mul $pa $pb $r1 $r2) : Result q($a * $b))
+      return (.isRat' dα qc nc dc q(isRat_mul $pa $pb $r1 $r2) : Result q($a * $b))
     match ra, rb with
     | .isBool .., _ | _, .isBool .. => failure
     | .isRat dα .., _ | _, .isRat dα .. => ratArm dα
@@ -380,7 +380,7 @@ def evalPow : NormNumExt where eval {u α} e := do
       have dc : Q(ℕ) := mkRawNatLit qc.den
       have r1 : Q(Int.pow $na $nb = $nc) := (q(Eq.refl $nc) : Expr)
       have r2 : Q(Nat.pow $da $nb = $dc) := (q(Eq.refl $dc) : Expr)
-      return (.isRat dα qc nc dc (q(isRat_pow $pa $pb $r1 $r2) : Expr) : Result q($a ^ $b))
+      return (.isRat' dα qc nc dc (q(isRat_pow $pa $pb $r1 $r2) : Expr) : Result q($a ^ $b))
   core
 
 theorem isRat_inv_pos {α} [DivisionRing α] [CharZero α] {a : α} {n d : ℕ} :
@@ -389,10 +389,18 @@ theorem isRat_inv_pos {α} [DivisionRing α] [CharZero α] {a : α} {n d : ℕ}
   have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
   refine ⟨this, by simp⟩
 
+theorem isRat_inv_one {α} [DivisionRing α] : {a : α} →
+    IsNat a (nat_lit 1) → IsNat a⁻¹ (nat_lit 1)
+  | _, ⟨rfl⟩ => ⟨by simp⟩
+
 theorem isRat_inv_zero {α} [DivisionRing α] : {a : α} →
     IsNat a (nat_lit 0) → IsNat a⁻¹ (nat_lit 0)
   | _, ⟨rfl⟩ => ⟨by simp⟩
 
+theorem isRat_inv_neg_one {α} [DivisionRing α] : {a : α} →
+    IsInt a (.negOfNat (nat_lit 1)) → IsInt a⁻¹ (.negOfNat (nat_lit 1))
+  | _, ⟨rfl⟩ => ⟨by simp [inv_neg_one]⟩
+
 theorem isRat_inv_neg {α} [DivisionRing α] [CharZero α] {a : α} {n d : ℕ} :
     IsRat a (.negOfNat (Nat.succ n)) d → IsRat a⁻¹ (.negOfNat d) (Nat.succ n) := by
   rintro ⟨_, rfl⟩
@@ -408,27 +416,42 @@ such that `norm_num` successfully recognises `a`. -/
   let .app f (a : Q($α)) ← whnfR e | failure
   let ra ← derive a
   let dα ← inferDivisionRing α
+  let _i ← inferCharZeroOfDivisionRing? dα
   guard <|← withNewMCtxDepth <| isDefEq f q(Inv.inv (α := $α))
-  let ⟨qa, na, da, pa⟩ ← ra.toRat'
-  let qb := qa⁻¹
-  if qa > 0 then
-    let _i ← inferCharZeroOfDivisionRing dα
-    have lit : Q(ℕ) := na.appArg!
-    have lit2 : Q(ℕ) := mkRawNatLit (lit.natLit! - 1)
-    let pa : Q(IsRat «$a» (Int.ofNat (Nat.succ $lit2)) $da) := pa
-    return (.isRat' dα qb q(.ofNat $da) lit
-      (q(isRat_inv_pos (α := $α) $pa) : Expr) : Result q($a⁻¹))
-  else if qa < 0 then
-    let _i ← inferCharZeroOfDivisionRing dα
-    have lit : Q(ℕ) := na.appArg!
-    have lit2 : Q(ℕ) := mkRawNatLit (lit.natLit! - 1)
-    let pa : Q(IsRat «$a» (Int.negOfNat (Nat.succ $lit2)) $da) := pa
-    return (.isRat' dα qb q(.negOfNat $da) lit
-      (q(isRat_inv_neg (α := $α) $pa) : Expr) : Result q($a⁻¹))
-  else
-    let .isNat inst _z (pa : Q(@IsNat _ AddGroupWithOne.toAddMonoidWithOne $a (nat_lit 0))) := ra
-      | failure
-    return (.isNat inst _z (q(isRat_inv_zero $pa) : Expr) : Result q($a⁻¹))
+  let rec
+  /-- Main part of `evalInv`. -/
+  core : Option (Result e) := do
+    let ⟨qa, na, da, pa⟩ ← ra.toRat'
+    let qb := qa⁻¹
+    if qa > 0 then
+      if let .some _i := _i then
+        have lit : Q(ℕ) := na.appArg!
+        have lit2 : Q(ℕ) := mkRawNatLit (lit.natLit! - 1)
+        let pa : Q(IsRat «$a» (Int.ofNat (Nat.succ $lit2)) $da) := pa
+        return (.isRat' dα qb q(.ofNat $da) lit
+          (q(isRat_inv_pos (α := $α) $pa) : Expr) : Result q($a⁻¹))
+      else
+        guard (qa = 1)
+        let .isNat inst _z
+          (pa : Q(@IsNat _ AddGroupWithOne.toAddMonoidWithOne $a (nat_lit 1))) := ra | failure
+        return (.isNat inst _z (q(isRat_inv_one $pa) : Expr) : Result q($a⁻¹))
+    else if qa < 0 then
+      if let .some _i := _i then
+        have lit : Q(ℕ) := na.appArg!
+        have lit2 : Q(ℕ) := mkRawNatLit (lit.natLit! - 1)
+        let pa : Q(IsRat «$a» (Int.negOfNat (Nat.succ $lit2)) $da) := pa
+        return (.isRat' dα qb q(.negOfNat $da) lit
+          (q(isRat_inv_neg (α := $α) $pa) : Expr) : Result q($a⁻¹))
+      else
+        guard (qa = -1)
+        let .isNegNat inst _z
+          (pa : Q(@IsInt _ DivisionRing.toRing $a (.negOfNat 1))) := ra | failure
+        return (.isNegNat inst _z (q(isRat_inv_neg_one $pa) : Expr) : Result q($a⁻¹))
+    else
+      let .isNat inst _z (pa : Q(@IsNat _ AddGroupWithOne.toAddMonoidWithOne $a (nat_lit 0))) := ra
+        | failure
+      return (.isNat inst _z (q(isRat_inv_zero $pa) : Expr) : Result q($a⁻¹))
+  core
 
 theorem isRat_div [DivisionRing α] : {a b : α} → {cn : ℤ} → {cd : ℕ} → IsRat (a * b⁻¹) cn cd →
     IsRat (a / b) cn cd

Mathlib/Tactic/NormNum/Core.lean

@@ -119,7 +119,7 @@ A "raw rat cast" is an expression of the form:
 This representation is used by tactics like `ring` to decrease the number of typeclass arguments
 required in each use of a number literal at type `α`.
 -/
-@[simp] def Rat.rawCast [DivisionRing α] (n : ℤ) (d : ℕ) : α := n / d
+@[simp] def _root_.Rat.rawCast [DivisionRing α] (n : ℤ) (d : ℕ) : α := n / d
 
 theorem IsRat.to_isNat {α} [Ring α] : ∀ {a : α} {n}, IsRat a (.ofNat n) (nat_lit 1) → IsNat a n
   | _, _, ⟨inv, rfl⟩ => have := @invertibleOne α _; ⟨by simp⟩
@@ -144,6 +144,14 @@ theorem IsRat.nonneg_to_eq {α} [DivisionRing α] {n d} :
     {a n' d' : α} → IsRat a (.ofNat n) d → n = n' → d = d' → a = n' / d'
   | _, _, _, ⟨_, rfl⟩, rfl, rfl => by simp [div_eq_mul_inv]
 
+theorem IsRat.of_raw (α) [DivisionRing α] (n : ℤ) (d : ℕ)
+    (h : (d : α) ≠ 0) : IsRat (Rat.rawCast n d : α) n d :=
+  have := invertibleOfNonzero h
+  ⟨this, by simp [div_eq_mul_inv]⟩
+
+theorem IsRat.den_nz {α} [DivisionRing α] {a n d} : IsRat (a : α) n d → (d : α) ≠ 0
+  | ⟨_, _⟩ => nonzero_of_invertible (d : α)
+
 /-- Represent an integer as a typed expression. -/
 def mkRawRatLit (q : ℚ) : Q(ℚ) :=
   let nlit : Q(ℤ) := mkRawIntLit q.num
@@ -227,6 +235,11 @@ def Result.toRat : Result e → Option Rat
 
 end
 
+/-- Convert `undef` to `none` to make an `LOption` into an `Option`. -/
+def _root_.Lean.LOption.toOption {α} : Lean.LOption α → Option α
+  | .some a => some a
+  | _ => none
+
 /-- Helper function to synthesize a typed `AddMonoidWithOne α` expression. -/
 def inferAddMonoidWithOne (α : Q(Type u)) : MetaM Q(AddMonoidWithOne $α) :=
   return ← synthInstanceQ (q(AddMonoidWithOne $α) : Q(Type u)) <|>
@@ -266,8 +279,8 @@ def inferCharZeroOfRing {α : Q(Type u)} (_i : Q(Ring $α) := by with_reducible
 
 /-- Helper function to synthesize a typed `CharZero α` expression given `Ring α`, if it exists. -/
 def inferCharZeroOfRing? {α : Q(Type u)} (_i : Q(Ring $α) := by with_reducible assumption) :
-    MetaM (LOption Q(CharZero $α)) :=
-  trySynthInstanceQ (q(CharZero $α) : Q(Prop))
+    MetaM (Option Q(CharZero $α)) :=
+  return (← trySynthInstanceQ (q(CharZero $α) : Q(Prop))).toOption
 
 /-- Helper function to synthesize a typed `CharZero α` expression given `AddMonoidWithOne α`. -/
 def inferCharZeroOfAddMonoidWithOne {α : Q(Type u)}
@@ -279,8 +292,8 @@ def inferCharZeroOfAddMonoidWithOne {α : Q(Type u)}
 exists. -/
 def inferCharZeroOfAddMonoidWithOne? {α : Q(Type u)}
     (_i : Q(AddMonoidWithOne $α) := by with_reducible assumption) :
-      MetaM (LOption Q(CharZero $α)) :=
-  trySynthInstanceQ (q(CharZero $α) : Q(Prop))
+      MetaM (Option Q(CharZero $α)) :=
+  return (← trySynthInstanceQ (q(CharZero $α) : Q(Prop))).toOption
 
 /-- Helper function to synthesize a typed `CharZero α` expression given `DivisionRing α`. -/
 def inferCharZeroOfDivisionRing {α : Q(Type u)}
@@ -291,8 +304,8 @@ def inferCharZeroOfDivisionRing {α : Q(Type u)}
 /-- Helper function to synthesize a typed `CharZero α` expression given `DivisionRing α`, if it
 exists. -/
 def inferCharZeroOfDivisionRing? {α : Q(Type u)}
-    (_i : Q(DivisionRing $α) := by with_reducible assumption) : MetaM (LOption Q(CharZero $α)) :=
-  trySynthInstanceQ (q(CharZero $α) : Q(Prop))
+    (_i : Q(DivisionRing $α) := by with_reducible assumption) : MetaM (Option Q(CharZero $α)) :=
+  return (← trySynthInstanceQ (q(CharZero $α) : Q(Prop))).toOption
 /--
 Extract from a `Result` the integer value (as both a term and an expression),
 and the proof that the original expression is equal to this integer.
@@ -372,6 +385,17 @@ def Result.ofRawInt {α : Q(Type u)} (n : ℤ) (e : Q($α)) : Result e :=
     let .app (.app _ (rα : Q(Ring $α))) (.app _ (lit : Q(ℕ))) := e | panic! "not a raw int cast"
     .isNegNat rα lit (q(IsInt.of_raw $α (.negOfNat $lit)) : Expr)
 
+/-- Constructs a `Result` out of a raw rat cast.
+Assumes `e` is a raw rat cast expression denoting `n`. -/
+def Result.ofRawRat {α : Q(Type u)} (q : ℚ) (e : Q($α)) (hyp : Option Expr := none) : Result e :=
+  if q.den = 1 then
+    Result.ofRawInt q.num e
+  else Id.run do
+    let .app (.app (.app _ (dα : Q(DivisionRing $α))) (n : Q(ℤ))) (d : Q(ℕ)) := e
+      | panic! "not a raw rat cast"
+    let hyp : Q(($d : $α) ≠ 0) := hyp.get!
+    .isRat dα q n d (q(IsRat.of_raw $α $n $d $hyp) : Expr)
+
 /-- The result depends on whether `q : ℚ` happens to be an integer, in which case the result is
 `.isInt ..` whereas otherwise it's `.isRat ..`. -/
 def Result.isRat' {α : Q(Type u)} {x : Q($α)} (inst : Q(DivisionRing $α) := by assumption)
@@ -382,6 +406,14 @@ def Result.isRat' {α : Q(Type u)} {x : Q($α)} (inst : Q(DivisionRing $α) := b
   else
     .isRat inst q n d proof
 
+/-- Returns the rational number that is the result of `norm_num` evaluation, along with a proof
+that the denominator is nonzero in the `isRat` case. -/
+def Result.toRatNZ : Result e → Option (Rat × Option Expr)
+  | .isBool .. => none
+  | .isNat _ lit _ => some (lit.natLit!, none)
+  | .isNegNat _ lit _ => some (-lit.natLit!, none)
+  | .isRat _ q _ _ p => some (q, q(IsRat.den_nz $p))
+
 /--
 Constructs an `ofNat` application `a'` with the canonical instance, together with a proof that
 the instance is equal to the result of `Nat.cast` on the given `AddMonoidWithOne` instance.

Mathlib/Tactic/Polyrith.lean

@@ -125,7 +125,7 @@ def Poly.toSyntax : Poly → Syntax.Term
 
 /-- Reifies a ring expression of type `α` as a `Poly`. -/
 partial def parse {u} {α : Q(Type u)} (sα : Q(CommSemiring $α))
-    (c : Ring.Cache α) (e : Q($α)) : AtomM Poly := do
+    (c : Ring.Cache sα) (e : Q($α)) : AtomM Poly := do
   let els := do
     try pure <| Poly.const (← (← NormNum.derive e).toRat)
     catch _ => pure <| Poly.var (← addAtom e)
@@ -166,7 +166,7 @@ def parseContext (only : Bool) (hyps : Array Expr) (tgt : Expr) :
   have α : Q(Type u) := α
   have e₁ : Q($α) := e₁; have e₂ : Q($α) := e₂
   let sα ← synthInstanceQ (q(CommSemiring $α) : Q(Type u))
-  let c := { rα := (← trySynthInstanceQ (q(Ring $α) : Q(Type u))).toOption }
+  let c ← mkCache sα
   let tgt := (← parse sα c e₁).sub (← parse sα c e₂)
   let rec
     /-- Parses a hypothesis and adds it to the `out` list. -/