feat: Qq version of mkDecideProof (#22283)

Originally coming from #22039
leanprover-community · Feb 25, 2025 · 5d68dc4 · 5d68dc4
1 parent 9d91737
commit 5d68dc4
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 4 deletions.
diff --git a/Mathlib/Tactic/IntervalCases.lean b/Mathlib/Tactic/IntervalCases.lean
@@ -218,8 +218,8 @@ def natMethods : Methods where
   eval e := do
     let ⟨z, e, p⟩ := (← NormNum.derive (α := (q(ℕ) : Q(Type))) e).toRawIntEq.get!
     pure (z, e, p)
-  proveLE (lhs rhs : Q(ℕ)) := mkDecideProof q($lhs ≤ $rhs)
-  proveLT (lhs rhs : Q(ℕ)) := mkDecideProof q(¬$rhs ≤ $lhs)
+  proveLE (lhs rhs : Q(ℕ)) := mkDecideProofQ q($lhs ≤ $rhs)
+  proveLT (lhs rhs : Q(ℕ)) := mkDecideProofQ q(¬$rhs ≤ $lhs)
   roundUp (lhs rhs _ : Q(ℕ)) (p : Q(¬$rhs ≤ $lhs)) := pure q(Nat.gt_of_not_le $p)
   roundDown (lhs _ rhs' : Q(ℕ)) (p : Q(¬Nat.succ $rhs' ≤ $lhs)) := pure q(Nat.ge_of_not_lt $p)
   mkNumeral
@@ -237,8 +237,8 @@ def intMethods : Methods where
   eval e := do
     let ⟨z, e, p⟩ := (← NormNum.derive (α := (q(ℤ) : Q(Type))) e).toRawIntEq.get!
     pure (z, e, p)
-  proveLE (lhs rhs : Q(ℤ)) := mkDecideProof q($lhs ≤ $rhs)
-  proveLT (lhs rhs : Q(ℤ)) := mkDecideProof q(¬$rhs ≤ $lhs)
+  proveLE (lhs rhs : Q(ℤ)) := mkDecideProofQ q($lhs ≤ $rhs)
+  proveLT (lhs rhs : Q(ℤ)) := mkDecideProofQ q(¬$rhs ≤ $lhs)
   roundUp (lhs rhs _ : Q(ℤ)) (p : Q(¬$rhs ≤ $lhs)) := pure q(Int.add_one_le_of_not_le $p)
   roundDown (lhs rhs _ : Q(ℤ)) (p : Q(¬$rhs ≤ $lhs)) := pure q(Int.le_sub_one_of_not_le $p)
   mkNumeral

diff --git a/Mathlib/Util/Qq.lean b/Mathlib/Util/Qq.lean
@@ -35,4 +35,9 @@ def findLocalDeclWithTypeQ? {u : Level} (sort : Q(Sort u)) : MetaM (Option Q($so
   let some fvarId ← findLocalDeclWithType? q($sort) | return none
   return some <| .fvar fvarId
 
+/-- Returns a proof of `p : Prop` using `decide p`.
+
+This is a Qq version of `Lean.Meta.mkDecideProof`. -/
+def mkDecideProofQ (p : Q(Prop)) : MetaM Q($p) := mkDecideProof p
+
 end Qq