feat: allow several tactics on types that are slightly less obviously Types (#3682)

Many tactics attempt to get the universe of the sort of the terms involved by matching on the level being a succ of something.
Unfortunately this fails on some nontrivial examples like mvpolynomial which can have type `Sort (max (u+1) (v+1))` 
Instead we decrement the level manually after matching it.

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60ring.60.20tactic.20cannot.20prove.20equality.20about.20.60MvPolynomial.60/near/352549549

This PR modifies ring, ring_nf, nontriviality, polyrith, linarith, and some norm_num handlers to appropriately handle this.
Test cases showing examples that failed before (inspired by the case of mvpolynomial, but in principle there could be other interesting types that have multiple universe parameters in this way, some of which may even have a linear order who knows).

In doing so we factor out `inferTypeQ'` into its own file `Mathlib.Tactic.Qq` for mathlib-relevant extensions of Qq

Author: alexjbest

Mathlib.lean

@@ -2050,6 +2050,7 @@ import Mathlib.Util.IncludeStr
 import Mathlib.Util.LongNames
 import Mathlib.Util.MemoFix
 import Mathlib.Util.Pickle
+import Mathlib.Util.Qq
 import Mathlib.Util.Syntax
 import Mathlib.Util.SynthesizeUsing
 import Mathlib.Util.Tactic

Mathlib/Tactic/Linarith/Verification.lean

@@ -7,6 +7,7 @@ Ported by: Scott Morrison
 
 import Mathlib.Tactic.Linarith.Elimination
 import Mathlib.Tactic.Linarith.Parsing
+import Mathlib.Util.Qq
 
 /-!
 # Deriving a proof of false
@@ -36,14 +37,6 @@ def ofNatQ (α : Q(Type $u)) (_ : Q(Semiring $α)) (n : ℕ) : Q($α) :=
       (q(instAtLeastTwoHAddNatInstHAddInstAddNatOfNat (n := $k)) : Expr)
     q(OfNat.ofNat $lit)
 
-/-- Analogue of `inferTypeQ`, but that gets universe levels right for our application. -/
--- See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Using.20.60QQ.60.20when.20you.20only.20have.20an.20.60Expr.60/near/303349037
-def inferTypeQ' (e : Expr) : MetaM ((u : Level) × (α : Q(Type $u)) × Q($α)) := do
-  let α ← inferType e
-  let .sort (.succ u) ← instantiateMVars (← whnf (← inferType α))
-    | throwError "not a type{indentExpr α}"
-  pure ⟨u, α, e⟩
-
 end Qq
 
 namespace Linarith

Mathlib/Tactic/Nontriviality/Core.lean

@@ -113,8 +113,9 @@ syntax (name := nontriviality) "nontriviality" (ppSpace (colGt term))?
       if let some (α, _) := tgt.app4? ``LT.lt then return α
       throwError "The goal is not an (in)equality, so you'll need to specify the desired {""
         }`Nontrivial α` instance by invoking `nontriviality α`.")
-    let .sort (.succ u) ← whnf (← inferType α) | throwError "not a type{indentExpr α}"
-    let α : Q(Type u) := α
+    let .sort u ← whnf (← inferType α) | unreachable!
+    let some v := u.dec | throwError "not a type{indentExpr α}"
+    let α : Q(Type v) := α
     let tac := do
       let ty := q(Nontrivial $α)
       let m ← mkFreshExprMVar (some ty)

Mathlib/Tactic/NormNum/Basic.lean

@@ -6,7 +6,7 @@ Authors: Mario Carneiro, Thomas Murrills
 import Mathlib.Tactic.NormNum.Core
 import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Algebra.Order.Invertible
-import Qq
+import Mathlib.Util.Qq
 
 /-!
 ## `norm_num` basic plugins
@@ -723,7 +723,7 @@ theorem eq_of_false (ha : ¬a) (hb : ¬b) : a = b := propext (iff_of_false ha hb
 such that `norm_num` successfully recognises both `a` and `b`. -/
 @[norm_num _ = _, Eq _ _] def evalEq : NormNumExt where eval {u α} e := do
   let .app (.app f a) b ← whnfR e | failure
-  let ⟨.succ u, α, a⟩ ← inferTypeQ a | failure
+  let ⟨u, α, a⟩ ← inferTypeQ' a
   have b : Q($α) := b
   guard <|← withNewMCtxDepth <| isDefEq f q(Eq (α := $α))
   let ra ← derive a; let rb ← derive b
@@ -778,7 +778,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
 such that `norm_num` successfully recognises both `a` and `b`. -/
 @[norm_num _ ≤ _] def evalLE : NormNumExt where eval (e : Q(Prop)) := do
   let .app (.app f a) b ← whnfR e | failure
-  let ⟨.succ u, α, a⟩ ← inferTypeQ a | failure
+  let ⟨u, α, a⟩ ← inferTypeQ' a
   have b : Q($α) := b
   let ra ← derive a; let rb ← derive b
     let intArm (_ : Unit) : MetaM (@Result _ (q(Prop) : Q(Type)) e) := do
@@ -834,7 +834,7 @@ such that `norm_num` successfully recognises both `a` and `b`. -/
 such that `norm_num` successfully recognises both `a` and `b`. -/
 @[norm_num _ < _] def evalLT : NormNumExt where eval (e : Q(Prop)) := do
   let .app (.app f a) b ← whnfR e | failure
-  let ⟨.succ u, α, a⟩ ← inferTypeQ a | failure
+  let ⟨u, α, a⟩ ← inferTypeQ' a
   have b : Q($α) := b
   let ra ← derive a; let rb ← derive b
   let intArm (_ : Unit) : MetaM (@Result _ (q(Prop) : Q(Type)) e) := do

Mathlib/Tactic/NormNum/Core.lean

@@ -10,8 +10,7 @@ import Mathlib.Data.Rat.Cast
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Int.Basic
 import Mathlib.Tactic.Conv
-import Qq.MetaM
-import Qq.Delab
+import Mathlib.Util.Qq
 
 /-!
 ## `norm_num` core functionality
@@ -619,7 +618,7 @@ def isNormalForm : Expr → Bool
 returning a `Simp.Result`. -/
 def eval (e : Expr) (post := false) : MetaM Simp.Result := do
   if isNormalForm e then return { expr := e }
-  let ⟨.succ _, _, e⟩ ← inferTypeQ e | failure
+  let ⟨_, _, e⟩ ← inferTypeQ' e
   (← derive e post).toSimpResult
 
 /-- Erases a name marked `norm_num` by adding it to the state's `erased` field and

Mathlib/Tactic/Polyrith.lean

@@ -164,10 +164,11 @@ def parseContext (only : Bool) (hyps : Array Expr) (tgt : Expr) :
     AtomM (Expr × Array (Source × Poly) × Poly) := do
   let fail {α} : AtomM α := throwError "polyrith failed: target is not an equality in semirings"
   let some (α, e₁, e₂) := (← whnfR <|← instantiateMVars tgt).eq? | fail
-  let .sort (.succ u) ← whnf (← inferType α) | fail
-  have α : Q(Type u) := α
+  let .sort u ← instantiateMVars (← whnf (← inferType α)) | unreachable!
+  let some v := u.dec | throwError "not a type{indentExpr α}"
+  have α : Q(Type v) := α
   have e₁ : Q($α) := e₁; have e₂ : Q($α) := e₂
-  let sα ← synthInstanceQ (q(CommSemiring $α) : Q(Type u))
+  let sα ← synthInstanceQ (q(CommSemiring $α) : Q(Type v))
   let c ← mkCache sα
   let tgt := (← parse sα c e₁).sub (← parse sα c e₂)
   let rec

Mathlib/Tactic/Ring/Basic.lean

@@ -1092,10 +1092,11 @@ initialize ringCleanupRef : IO.Ref (Expr → MetaM Expr) ← IO.mkRef pure
 def proveEq (g : MVarId) : AtomM Unit := do
   let some (α, e₁, e₂) := (← whnfR <|← instantiateMVars <|← g.getType).eq?
     | throwError "ring failed: not an equality"
-  let .sort (.succ u) ← whnf (← inferType α) | throwError "not a type{indentExpr α}"
-  have α : Q(Type u) := α
+  let .sort u ← whnf (← inferType α) | unreachable!
+  let v ← try u.dec catch _ => throwError "not a type{indentExpr α}"
+  have α : Q(Type v) := α
   have e₁ : Q($α) := e₁; have e₂ : Q($α) := e₂
-  let sα ← synthInstanceQ (q(CommSemiring $α) : Q(Type u))
+  let sα ← synthInstanceQ (q(CommSemiring $α) : Q(Type v))
   let c ← mkCache sα
   profileitM Exception "ring" (← getOptions) do
     let ⟨a, va, pa⟩ ← eval sα c e₁

Mathlib/Tactic/Ring/RingNF.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Tim Baanen
 -/
 import Mathlib.Tactic.Ring.Basic
 import Mathlib.Tactic.Conv
+import Mathlib.Util.Qq
 
 /-!
 # `ring_nf` tactic
@@ -90,7 +91,7 @@ def rewrite (parent : Expr) (root := true) : M Simp.Result :=
         guard <| root || parent != e -- recursion guard
         let e ← withReducible <| whnf e
         guard e.isApp -- all interesting ring expressions are applications
-        let ⟨.succ u, α, e⟩ ← inferTypeQ e | failure
+        let ⟨u, α, e⟩ ← inferTypeQ' e
         let sα ← synthInstanceQ (q(CommSemiring $α) : Q(Type u))
         let c ← mkCache sα
         let ⟨a, _, pa⟩ ← match ← isAtomOrDerivable sα c e rctx s with

Mathlib/Util/Qq.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2023 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Alex J. Best
+-/
+import Qq
+
+/-!
+# Extra `Qq` helpers
+
+This file contains some additional functions for using the quote4 library more conveniently.
+-/
+open Lean Elab Tactic Meta
+
+namespace Qq
+
+/-- Analogue of `inferTypeQ`, but that gets universe levels right for our application. -/
+-- See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Using.20.60QQ.60.20when.20you.20only.20have.20an.20.60Expr.60/near/303349037
+def inferTypeQ' (e : Expr) : MetaM ((u : Level) × (α : Q(Type $u)) × Q($α)) := do
+  let α ← inferType e
+  let .sort u ← instantiateMVars (← whnf (← inferType α)) | unreachable!
+  let some v := u.dec | throwError "not a type{indentExpr α}"
+  pure ⟨v, α, e⟩
+
+end Qq

test/linarith.lean

@@ -497,3 +497,10 @@ example (n : Nat) (h1 : ¬n = 1) (h2 : n ≥ 1) : n ≥ 2 := by
   by_contra h3
   suffices n = 1 by exact h1 this
   linarith
+
+-- simulate the type of MvPolynomial
+def R : Type u → Type v → Sort (max (u+1) (v+1)) := sorry
+instance : LinearOrderedField (R c d) := sorry
+
+example (p : R PUnit.{u+1} PUnit.{v+1}) (h : 0 < p) : 0 < 2 * p := by
+  linarith