feat: polyrith tactic (leanprover-community#942)

The main functionality of `polyrith` is represented here: it contacts Sagemath to get the coefficients required to pass to linear_combination.

TODO:
* [x] fix docs & lint
* [ ] fix tests
  * There are some auxiliary tactics used to construct test cases for `polyrith` and perform dry-run testing which does not require contacting sage in CI.

Since the mock testing setup is not done yet, you can only test it for real right now, but I don't want to run that in CI for the same reason so currently all the tests are commented out. Most of them are still failing though because of things like a missing instance for `CommSemiring Rat` or the existence of the `Real` type entirely.

Co-authored-by: Scott Morrison <[email protected]>

Mathlib.lean

@@ -435,6 +435,7 @@ import Mathlib.Tactic.NormNum.Basic
 import Mathlib.Tactic.NormNum.Core
 import Mathlib.Tactic.NthRewrite
 import Mathlib.Tactic.PermuteGoals
+import Mathlib.Tactic.Polyrith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Positivity.Basic
 import Mathlib.Tactic.Positivity.Core

Mathlib/Order/Heyting/Basic.lean

@@ -390,8 +390,8 @@ theorem himp_le_himp_himp_himp : b ⇨ c ≤ (a ⇨ b) ⇨ a ⇨ c := by
 #align himp_le_himp_himp_himp himp_le_himp_himp_himp
 
 @[simp]
-theorem himp_inf_himp_inf_le : (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c :=
-  by simpa using @himp_le_himp_himp_himp
+theorem himp_inf_himp_inf_le : (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c := by
+  simpa using @himp_le_himp_himp_himp
 
 -- `p → q → r ↔ q → p → r`
 theorem himp_left_comm (a b c : α) : a ⇨ b ⇨ c = b ⇨ a ⇨ c := by simp_rw [himp_himp, inf_comm]

Mathlib/Tactic/Core.lean

@@ -120,3 +120,18 @@ def allGoals (tac : TacticM Unit) : TacticM Unit := do
   setGoals mvarIdsNew.toList
 
 end Lean.Elab.Tactic
+
+namespace Mathlib
+open Lean
+
+/-- Returns the root directory which contains the package root file, e.g. `Mathlib.lean`. -/
+def getPackageDir (pkg : String) : IO System.FilePath := do
+  let sp ← initSrcSearchPath (← findSysroot)
+  let root? ← sp.findM? fun p =>
+    (p / pkg).isDir <||> ((p / pkg).withExtension "lean").pathExists
+  if let some root := root? then return root
+  throw <| IO.userError s!"Could not find {pkg} directory. {
+    ""}Make sure the LEAN_SRC_PATH environment variable is set correctly."
+
+/-- Returns the mathlib root directory. -/
+def getMathlibDir := getPackageDir "Mathlib"

Mathlib/Tactic/NormNum/Core.lean

@@ -175,6 +175,12 @@ def Result.isInt {α : Q(Type u)} {x : Q($α)} {z : Q(ℤ)}
   else
     .isNegNat inst lit proof
 
+/-- Returns the rational number that is the result of norm_num evaluation. -/
+def Result.toRat : Result e → Rat
+  | .isNat _ lit _ => lit.natLit!
+  | .isNegNat _ lit _ => -lit.natLit!
+  | .isRat _ q .. => q
+
 end
 
 /-- Helper functor to synthesize a typed `AddMonoidWithOne α` expression. -/