From 450d95a7cb36cb88ca080f29728c4693ee4b7abd Mon Sep 17 00:00:00 2001 From: Pan Lin <58059503+HugLycan@users.noreply.github.com> Date: Thu, 6 Nov 2025 09:58:03 +0000 Subject: [PATCH 1/8] feat(positivity): make `PartialOrder` instance optional --- Mathlib/Tactic/Positivity/Core.lean | 268 +++++++++++++++++----------- 1 file changed, 162 insertions(+), 106 deletions(-) diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean index 1f3a11f7999507..82e60bb490debf 100644 --- a/Mathlib/Tactic/Positivity/Core.lean +++ b/Mathlib/Tactic/Positivity/Core.lean @@ -30,46 +30,53 @@ lemma ne_of_ne_of_eq' {α : Sort*} {a c b : α} (hab : (a : α) ≠ c) (hbc : a namespace Mathlib.Meta.Positivity -variable {u : Level} {α : Q(Type u)} (zα : Q(Zero $α)) (pα : Q(PartialOrder $α)) +variable {u : Level} {α : Q(Type u)} (zα : Q(Zero $α)) (pα? : Option Q(PartialOrder $α)) /-- The result of `positivity` running on an expression `e` of type `α`. -/ -inductive Strictness (e : Q($α)) where - | positive (pf : Q(0 < $e)) - | nonnegative (pf : Q(0 ≤ $e)) +inductive Strictness (pα? : Option Q(PartialOrder $α)) (e : Q($α)) where + | positive {ltα : Q(LT $α)} (pf : Q(0 < $e)) + | nonnegative {leα : Q(LE $α)} (pf : Q(0 ≤ $e)) | nonzero (pf : Q($e ≠ 0)) | none deriving Repr /-- Gives a generic description of the `positivity` result. -/ -def Strictness.toString {e : Q($α)} : Strictness zα pα e → String +def Strictness.toString {e : Q($α)} : Strictness zα pα? e → String | positive _ => "positive" | nonnegative _ => "nonnegative" | nonzero _ => "nonzero" | none => "none" /-- Extract a proof that `e` is positive, if possible, from `Strictness` information about `e`. -/ -def Strictness.toPositive {e} : Strictness zα pα e → Option Q(0 < $e) +def Strictness.toPositive (pα : Q(PartialOrder $α)) {e} : + Strictness zα (some pα) e → Option Q(0 < $e) | .positive pf => some pf | _ => .none /-- Extract a proof that `e` is nonnegative, if possible, from `Strictness` information about `e`. -/ -def Strictness.toNonneg {e} : Strictness zα pα e → Option Q(0 ≤ $e) - | .positive pf => some q(le_of_lt $pf) +def Strictness.toNonneg (pα : Q(PartialOrder $α)) {e} : + Strictness zα (some pα) e → Option Q(0 ≤ $e) + | .positive pf => do + assumeInstancesCommute + some q(le_of_lt $pf) | .nonnegative pf => some pf | _ => .none /-- Extract a proof that `e` is nonzero, if possible, from `Strictness` information about `e`. -/ -def Strictness.toNonzero {e} : Strictness zα pα e → Option Q($e ≠ 0) - | .positive pf => some q(ne_of_gt $pf) +def Strictness.toNonzero {e} : Strictness zα pα? e → Option Q($e ≠ 0) + | .positive pf => do + let some _ := pα? | .none + assumeInstancesCommute + some q(ne_of_gt $pf) | .nonzero pf => some pf | _ => .none /-- An extension for `positivity`. -/ structure PositivityExt where /-- Attempts to prove an expression `e : α` is `>0`, `≥0`, or `≠0`. -/ - eval {u : Level} {α : Q(Type u)} (zα : Q(Zero $α)) (pα : Q(PartialOrder $α)) (e : Q($α)) : - MetaM (Strictness zα pα e) + eval {u : Level} {α : Q(Type u)} (zα : Q(Zero $α)) (pα? : Option Q(PartialOrder $α)) (e : Q($α)) : + MetaM (Strictness zα pα? e) /-- Read a `positivity` extension from a declaration of the right type. -/ def mkPositivityExt (n : Name) : ImportM PositivityExt := do @@ -186,25 +193,26 @@ lemma nz_of_isRat {n : ℤ} {d : ℕ} [Ring A] [LinearOrder A] [IsStrictOrderedR rw [eq] exact ne_iff_lt_or_gt.2 (Or.inl neg) -variable {zα pα} in +variable {zα pα?} in /-- Converts a `MetaM Strictness` which can fail into one that never fails and returns `.none` instead. -/ -def catchNone {e : Q($α)} (t : MetaM (Strictness zα pα e)) : MetaM (Strictness zα pα e) := +def catchNone {e : Q($α)} (t : MetaM (Strictness zα pα? e)) : MetaM (Strictness zα pα? e) := try t catch e => trace[Tactic.positivity.failure] "{e.toMessageData}" pure .none -variable {zα pα} in +variable {zα pα?} in /-- Converts a `MetaM Strictness` which can return `.none` into one which never returns `.none` but fails instead. -/ def throwNone {m : Type → Type*} {e : Q($α)} [Monad m] [Alternative m] - (t : m (Strictness zα pα e)) : m (Strictness zα pα e) := do + (t : m (Strictness zα pα? e)) : m (Strictness zα pα? e) := do match ← t with | .none => failure | r => pure r /-- Attempts to prove a `Strictness` result when `e` evaluates to a literal number. -/ -def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone do +def normNumPositivity (e : Q($α)) + : MetaM (Strictness zα pα? e) := catchNone do match ← NormNum.derive e with | .isBool .. => failure | .isNat _ lit p => @@ -217,7 +225,7 @@ def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone d let _a ← synthInstanceQ q(PartialOrder $α) let _a ← synthInstanceQ q(IsOrderedRing $α) let _a ← synthInstanceQ q(Nontrivial $α) - assumeInstancesCommute + assertInstancesCommute have p : Q(NormNum.IsNat $e $lit) := p haveI' p' : Nat.ble 1 $lit =Q true := ⟨⟩ pure (.positive q(pos_of_isNat (A := $α) $p $p')) @@ -228,7 +236,7 @@ def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone d let _a ← synthInstanceQ q(AddLeftMono $α) let _a ← synthInstanceQ q(ZeroLEOneClass $α) let _a ← synthInstanceQ q(NeZero (1 : $α)) - assumeInstancesCommute + assertInstancesCommute have p : Q(NormNum.IsNat $e $lit) := p haveI' p' : Nat.ble 1 $lit =Q true := ⟨⟩ pure (.positive q(pos_of_isNat' (A := $α) $p $p')) @@ -240,7 +248,7 @@ def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone d let _a ← synthInstanceQ q(Semiring $α) let _a ← synthInstanceQ q(PartialOrder $α) let _a ← synthInstanceQ q(IsOrderedRing $α) - assumeInstancesCommute + assertInstancesCommute have p : Q(NormNum.IsNat $e $lit) := p pure (.nonnegative q(nonneg_of_isNat $p)) catch e : Exception => @@ -249,14 +257,14 @@ def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone d let _a ← synthInstanceQ q(PartialOrder $α) let _a ← synthInstanceQ q(AddLeftMono $α) let _a ← synthInstanceQ q(ZeroLEOneClass $α) - assumeInstancesCommute + assertInstancesCommute have p : Q(NormNum.IsNat $e $lit) := p pure (.nonnegative q(nonneg_of_isNat' $p)) | .isNegNat _ lit p => let _a ← synthInstanceQ q(Ring $α) let _a ← synthInstanceQ q(PartialOrder $α) let _a ← synthInstanceQ q(IsStrictOrderedRing $α) - assumeInstancesCommute + assertInstancesCommute have p : Q(NormNum.IsInt $e (Int.negOfNat $lit)) := p haveI' p' : Nat.ble 1 $lit =Q true := ⟨⟩ pure (.nonzero q(nz_of_isNegNat $p $p')) @@ -264,7 +272,7 @@ def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone d let _a ← synthInstanceQ q(Semiring $α) let _a ← synthInstanceQ q(LinearOrder $α) let _a ← synthInstanceQ q(IsStrictOrderedRing $α) - assumeInstancesCommute + assertInstancesCommute have p : Q(NormNum.IsNNRat $e $n $d) := p if 0 < q then haveI' w : decide (0 < $n) =Q true := ⟨⟩ @@ -276,7 +284,7 @@ def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone d let _a ← synthInstanceQ q(Ring $α) let _a ← synthInstanceQ q(LinearOrder $α) let _a ← synthInstanceQ q(IsStrictOrderedRing $α) - assumeInstancesCommute + assertInstancesCommute have p : Q(NormNum.IsRat $e (.negOfNat $n) $d) := p if q < 0 then haveI' w : decide (Int.negOfNat $n < 0) =Q true := ⟨⟩ @@ -286,122 +294,155 @@ def normNumPositivity (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone d pure (.nonnegative q(nonneg_of_isRat $p $w)) /-- Attempts to prove that `e ≥ 0` using `zero_le` in a `CanonicallyOrderedAdd` monoid. -/ -def positivityCanon (e : Q($α)) : MetaM (Strictness zα pα e) := do +def positivityCanon (e : Q($α)) : MetaM (Strictness zα pα? e) := do let _add ← synthInstanceQ q(AddMonoid $α) let _le ← synthInstanceQ q(PartialOrder $α) let _i ← synthInstanceQ q(CanonicallyOrderedAdd $α) - assumeInstancesCommute + assertInstancesCommute pure (.nonnegative q(zero_le $e)) /-- A variation on `assumption` when the hypothesis is `lo ≤ e` where `lo` is a numeral. -/ -def compareHypLE (lo e : Q($α)) (p₂ : Q($lo ≤ $e)) : MetaM (Strictness zα pα e) := do +def compareHypLE (pα : Q(PartialOrder $α)) (lo e : Q($α)) (p₂ : Q($lo ≤ $e)) : + MetaM (Strictness zα pα e) := do match ← normNumPositivity zα pα lo with - | .positive p₁ => pure (.positive q(lt_of_lt_of_le $p₁ $p₂)) - | .nonnegative p₁ => pure (.nonnegative q(le_trans $p₁ $p₂)) + | .positive p₁ => do + assertInstancesCommute + pure (.positive q(lt_of_lt_of_le $p₁ $p₂)) + | .nonnegative p₁ => do + assertInstancesCommute + pure (.nonnegative q(le_trans $p₁ $p₂)) | _ => pure .none /-- A variation on `assumption` when the hypothesis is `lo < e` where `lo` is a numeral. -/ -def compareHypLT (lo e : Q($α)) (p₂ : Q($lo < $e)) : MetaM (Strictness zα pα e) := do +def compareHypLT (pα : Q(PartialOrder $α)) (lo e : Q($α)) (p₂ : Q($lo < $e)) : + MetaM (Strictness zα pα e) := do match ← normNumPositivity zα pα lo with - | .positive p₁ => pure (.positive q(lt_trans $p₁ $p₂)) - | .nonnegative p₁ => pure (.positive q(lt_of_le_of_lt $p₁ $p₂)) + | .positive p₁ => do + assertInstancesCommute + pure (.positive q(lt_trans $p₁ $p₂)) + | .nonnegative p₁ => do + assertInstancesCommute + pure (.positive q(lt_of_le_of_lt $p₁ $p₂)) | _ => pure .none /-- A variation on `assumption` when the hypothesis is `x = e` where `x` is a numeral. -/ -def compareHypEq (e x : Q($α)) (p₂ : Q($x = $e)) : MetaM (Strictness zα pα e) := do +def compareHypEq (pα : Q(PartialOrder $α)) (e x : Q($α)) (p₂ : Q($x = $e)) : + MetaM (Strictness zα pα e) := do match ← normNumPositivity zα pα x with | .positive p₁ => pure (.positive q(lt_of_lt_of_eq $p₁ $p₂)) | .nonnegative p₁ => pure (.nonnegative q(le_of_le_of_eq $p₁ $p₂)) | .nonzero p₁ => pure (.nonzero q(ne_of_ne_of_eq' $p₁ $p₂)) | .none => pure .none + initialize registerTraceClass `Tactic.positivity initialize registerTraceClass `Tactic.positivity.failure /-- A variation on `assumption` which checks if the hypothesis `ldecl` is `a [ - let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return .none - let .defEq _ ← isDefEqQ e hi | return .none - match lo with - | ~q(0) => - assertInstancesCommute - return .nonnegative q($p) - | _ => compareHypLE zα pα lo e p - | ~q(@LT.lt.{u} $β $_lt $lo $hi) => - let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return .none - let .defEq _ ← isDefEqQ e hi | return .none - match lo with - | ~q(0) => - assertInstancesCommute - return .positive q($p) - | _ => compareHypLT zα pα lo e p - | ~q(@Eq.{u+1} $α' $lhs $rhs) => - let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none - match ← isDefEqQ e rhs with - | .defEq _ => - match lhs with - | ~q(0) => pure <| .nonnegative q(le_of_eq $p) - | _ => compareHypEq zα pα e lhs q($p) - | .notDefEq => - let .defEq _ ← isDefEqQ e lhs | pure .none - match rhs with - | ~q(0) => pure <| .nonnegative q(ge_of_eq $p) - | _ => compareHypEq zα pα e rhs q(Eq.symm $p) - | ~q(@Ne.{u + 1} $α' $lhs $rhs) => - let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none - match lhs, rhs with - | ~q(0), _ => - let .defEq _ ← isDefEqQ e rhs | pure .none - pure <| .nonzero q(Ne.symm $p) - | _, ~q(0) => - let .defEq _ ← isDefEqQ e lhs | pure .none - pure <| .nonzero q($p) - | _, _ => pure .none - | _ => pure .none - -variable {zα pα} in + if let some pα := pα? then + match e' with + | ~q(@LE.le.{u} $β $_le $lo $hi) => + let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return .none + let .defEq _ ← isDefEqQ e hi | return .none + match lo with + | ~q(0) => + assertInstancesCommute + return .nonnegative q($p) + | _ => compareHypLE zα pα lo e p + | ~q(@LT.lt.{u} $β $_lt $lo $hi) => + let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return .none + let .defEq _ ← isDefEqQ e hi | return .none + match lo with + | ~q(0) => + assertInstancesCommute + return .positive q($p) + | _ => compareHypLT zα pα lo e p + | ~q(@Eq.{u+1} $α' $lhs $rhs) => + let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none + match ← isDefEqQ e rhs with + | .defEq _ => + match lhs with + | ~q(0) => pure <| .nonnegative q(le_of_eq $p) + | _ => compareHypEq zα pα e lhs q($p) + | .notDefEq => + let .defEq _ ← isDefEqQ e lhs | pure .none + match rhs with + | ~q(0) => pure <| .nonnegative q(ge_of_eq $p) + | _ => compareHypEq zα pα e rhs q(Eq.symm $p) + | ~q(@Ne.{u+1} $α' $lhs $rhs) => + let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none + match lhs, rhs with + | ~q(0), _ => + let .defEq _ ← isDefEqQ e rhs | pure .none + pure <| .nonzero q(Ne.symm $p) + | _, ~q(0) => + let .defEq _ ← isDefEqQ e lhs | pure .none + pure <| .nonzero q($p) + | _, _ => pure .none + | _ => pure .none + else + match e' with + | ~q(@Ne.{u+1} $α' $lhs $rhs) => + let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none + match lhs, rhs with + | ~q(0), _ => + let .defEq _ ← isDefEqQ e rhs | pure .none + pure <| .nonzero q(Ne.symm $p) + | _, ~q(0) => + let .defEq _ ← isDefEqQ e lhs | pure .none + pure <| .nonzero q($p) + | _, _ => pure .none + | _ => pure .none + +variable {zα pα?} in /-- The main combinator which combines multiple `positivity` results. It assumes `t₁` has already been run for a result, and runs `t₂` and takes the best result. It will skip `t₂` if `t₁` is already a proof of `.positive`, and can also combine `.nonnegative` and `.nonzero` to produce a `.positive` result. -/ -def orElse {e : Q($α)} (t₁ : Strictness zα pα e) (t₂ : MetaM (Strictness zα pα e)) : - MetaM (Strictness zα pα e) := do +def orElse {e : Q($α)} (t₁ : Strictness zα pα? e) (t₂ : MetaM (Strictness zα pα? e)) : + MetaM (Strictness zα pα? e) := do match t₁ with | .none => catchNone t₂ | p@(.positive _) => pure p | .nonnegative p₁ => match ← catchNone t₂ with | p@(.positive _) => pure p - | .nonzero p₂ => pure (.positive q(lt_of_le_of_ne' $p₁ $p₂)) + | .nonzero p₂ => + let some _ := pα? | throwError "cannot synth PartialOrd for {α}" + assertInstancesCommute + pure (.positive q(lt_of_le_of_ne' $p₁ $p₂)) | _ => pure (.nonnegative p₁) | .nonzero p₁ => match ← catchNone t₂ with | p@(.positive _) => pure p - | .nonnegative p₂ => pure (.positive q(lt_of_le_of_ne' $p₂ $p₁)) + | .nonnegative p₂ => + let some _ := pα? | throwError "cannot synth PartialOrd for {α}" + assertInstancesCommute + pure (.positive q(lt_of_le_of_ne' $p₂ $p₁)) | _ => pure (.nonzero p₁) /-- Run each registered `positivity` extension on an expression, returning a `NormNum.Result`. -/ -def core (e : Q($α)) : MetaM (Strictness zα pα e) := do +def core (e : Q($α)) : MetaM (Strictness zα pα? e) := do let mut result := .none trace[Tactic.positivity] "trying to prove positivity of {e}" for ext in ← (positivityExt.getState (← getEnv)).2.getMatch e do try - result ← orElse result <| ext.eval zα pα e + result ← orElse result <| ext.eval zα pα? e catch err => trace[Tactic.positivity] "{e} failed: {err.toMessageData}" - result ← orElse result <| normNumPositivity zα pα e - result ← orElse result <| positivityCanon zα pα e + result ← orElse result <| normNumPositivity zα pα? e + result ← orElse result <| positivityCanon zα pα? e if let .positive _ := result then trace[Tactic.positivity] "{e} => {result.toString}" return result for ldecl in ← getLCtx do if !ldecl.isImplementationDetail then - result ← orElse result <| compareHyp zα pα e ldecl + result ← orElse result <| compareHyp zα pα? e ldecl trace[Tactic.positivity] "{e} => {result.toString}" throwNone (pure result) @@ -420,8 +461,8 @@ inequality was established) together with the proof as an expression. -/ def bestResult (e : Expr) : MetaM (Bool × Expr) := do let ⟨u, α, _⟩ ← inferTypeQ' e let zα ← synthInstanceQ q(Zero $α) - let pα ← synthInstanceQ q(PartialOrder $α) - match ← try? (Meta.Positivity.core zα pα e) with + let pα? ← try? <| synthInstanceQ q(PartialOrder $α) + match ← try? (Meta.Positivity.core zα pα? e) with | some (.positive pf) => pure (true, pf) | some (.nonnegative pf) => pure (false, pf) | _ => throwError "could not establish the nonnegativity of {e}" @@ -438,28 +479,43 @@ or fails. -/ def solve (t : Q(Prop)) : MetaM Expr := do let rest {u : Level} (α : Q(Type u)) z e (relDesired : OrderRel) : MetaM Expr := do let zα ← synthInstanceQ q(Zero $α) - assumeInstancesCommute + assertInstancesCommute let .true ← isDefEq z q(0 : $α) | throwError "not a positivity goal" - let pα ← synthInstanceQ q(PartialOrder $α) - assumeInstancesCommute - let r ← catchNone <| Meta.Positivity.core zα pα e + let pα? ← try? <| synthInstanceQ q(PartialOrder $α) + assertInstancesCommute + let r ← catchNone <| Meta.Positivity.core zα pα? e let throw (a b : String) : MetaM Expr := throwError "failed to prove {a}, but it would be possible to prove {b} if desired" - let p ← show MetaM Expr from match relDesired, r with - | .lt, .positive p - | .le, .nonnegative p - | .ne, .nonzero p => pure p - | .le, .positive p => pure q(le_of_lt $p) - | .ne, .positive p => pure q(ne_of_gt $p) - | .ne', .positive p => pure q(ne_of_lt $p) - | .ne', .nonzero p => pure q(Ne.symm $p) - | .lt, .nonnegative _ => throw "strict positivity" "nonnegativity" - | .lt, .nonzero _ => throw "strict positivity" "nonzeroness" - | .le, .nonzero _ => throw "nonnegativity" "nonzeroness" - | .ne, .nonnegative _ - | .ne', .nonnegative _ => throw "nonzeroness" "nonnegativity" - | _, .none => throwError "failed to prove positivity/nonnegativity/nonzeroness" - pure p + if let some _ := pα? then + let p ← show MetaM Expr from match relDesired, r with + | .lt, .positive p + | .le, .nonnegative p + | .ne, .nonzero p => pure p + | .le, .positive p => do + assertInstancesCommute + pure q(le_of_lt $p) + | .ne, .positive p => do + assertInstancesCommute + pure q(ne_of_gt $p) + | .ne', .positive p => do + assertInstancesCommute + pure q(ne_of_lt $p) + | .ne', .nonzero p => pure q(Ne.symm $p) + | .lt, .nonnegative _ => throw "strict positivity" "nonnegativity" + | .lt, .nonzero _ => throw "strict positivity" "nonzeroness" + | .le, .nonzero _ => throw "nonnegativity" "nonzeroness" + | .ne, .nonnegative _ + | .ne', .nonnegative _ => throw "nonzeroness" "nonnegativity" + | _, .none => throwError "failed to prove positivity/nonnegativity/nonzeroness" + pure p + else + let p ← show MetaM Expr from match relDesired, r with + | .ne, .nonzero p => pure p + | .ne', .nonzero p => pure q(Ne.symm $p) + | .lt, .nonzero _ => throw "strict positivity" "nonzeroness" + | .le, .nonzero _ => throw "nonnegativity" "nonzeroness" + | _, _ => throwError "failed to prove nonzeroness" + pure p match t with | ~q(@LE.le $α $_a $z $e) => rest α z e .le | ~q(@LT.lt $α $_a $z $e) => rest α z e .lt From e5a62ccfbf9dbd626864384dc33ee71fd9c0a17f Mon Sep 17 00:00:00 2001 From: Pan Lin <58059503+HugLycan@users.noreply.github.com> Date: Mon, 24 Nov 2025 09:13:44 +0000 Subject: [PATCH 2/8] feat(Positivity): Option PartialOrder updated 2 --- Mathlib/Tactic/Positivity/Basic.lean | 231 +++++++++++++------- Mathlib/Tactic/Positivity/Core.lean | 189 +++++++++-------- Mathlib/Tactic/Positivity/test_Basic.lean | 245 ++++++++++++++++++++++ 3 files changed, 503 insertions(+), 162 deletions(-) create mode 100644 Mathlib/Tactic/Positivity/test_Basic.lean diff --git a/Mathlib/Tactic/Positivity/Basic.lean b/Mathlib/Tactic/Positivity/Basic.lean index 2e767e0fdee23c..e0f423483b4a94 100644 --- a/Mathlib/Tactic/Positivity/Basic.lean +++ b/Mathlib/Tactic/Positivity/Basic.lean @@ -53,14 +53,15 @@ end ite /-- The `positivity` extension which identifies expressions of the form `ite p a b`, such that `positivity` successfully recognises both `a` and `b`. -/ -@[positivity ite _ _ _] def evalIte : PositivityExt where eval {u α} zα pα e := do +@[positivity ite _ _ _] def evalIte : PositivityExt where eval {u α} zα pα? e := do let .app (.app (.app (.app f (p : Q(Prop))) (_ : Q(Decidable $p))) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | throwError "not ite" haveI' : $e =Q ite $p $a $b := ⟨⟩ - let ra ← core zα pα a; let rb ← core zα pα b + let ra ← core zα pα? a; let rb ← core zα pα? b guard <|← withDefault <| withNewMCtxDepth <| isDefEq f q(ite (α := $α)) match ra, rb with | .positive pa, .positive pb => + assumeInstancesCommute pure (.positive q(ite_pos $p $pa $pb)) | .positive pa, .nonnegative pb => let _b ← synthInstanceQ q(Preorder $α) @@ -71,6 +72,7 @@ such that `positivity` successfully recognises both `a` and `b`. -/ assumeInstancesCommute pure (.nonnegative q(ite_nonneg_of_nonneg_of_pos $p $pa $pb)) | .nonnegative pa, .nonnegative pb => + assumeInstancesCommute pure (.nonnegative q(ite_nonneg $p $pa $pb)) | .positive pa, .nonzero pb => let _b ← synthInstanceQ q(Preorder $α) @@ -102,113 +104,149 @@ end LinearOrder /-- The `positivity` extension which identifies expressions of the form `min a b`, such that `positivity` successfully recognises both `a` and `b`. -/ -@[positivity min _ _] def evalMin : PositivityExt where eval {u α} zα pα e := do +@[positivity min _ _] def evalMin : PositivityExt where eval {u α} zα pα? e := do let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | throwError "not min" let _e_eq : $e =Q $f $a $b := ⟨⟩ - let _a ← synthInstanceQ q(LinearOrder $α) + let lα ← synthInstanceQ q(LinearOrder $α) assumeInstancesCommute let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(min) - match ← core zα pα a, ← core zα pα b with - | .positive pa, .positive pb => pure (.positive q(lt_min $pa $pb)) - | .positive pa, .nonnegative pb => pure (.nonnegative q(le_min_of_lt_of_le $pa $pb)) - | .nonnegative pa, .positive pb => pure (.nonnegative q(le_min_of_le_of_lt $pa $pb)) - | .nonnegative pa, .nonnegative pb => pure (.nonnegative q(le_min $pa $pb)) - | .positive pa, .nonzero pb => pure (.nonzero q(min_ne_of_lt_of_ne $pa $pb)) - | .nonzero pa, .positive pb => pure (.nonzero q(min_ne_of_ne_of_lt $pa $pb)) - | .nonzero pa, .nonzero pb => pure (.nonzero q(min_ne $pa $pb)) + match ← core zα pα? a, ← core zα pα? b with + | .positive (ltα := ltα) pa, .positive pb => + haveI' : $ltα =Q ($lα).toLT := ⟨⟩ + assumeInstancesCommute + pure (.positive q(lt_min $pa $pb)) + | .positive pa, .nonnegative pb => + assumeInstancesCommute + pure (.nonnegative q(le_min_of_lt_of_le $pa $pb)) + | .nonnegative pa, .positive pb => + assumeInstancesCommute + pure (.nonnegative q(le_min_of_le_of_lt $pa $pb)) + | .nonnegative pa (leα := leα), .nonnegative pb => + haveI' : $leα =Q ($lα).toLE := ⟨⟩ + assumeInstancesCommute + pure (.nonnegative q(le_min $pa $pb)) + | .positive pa, .nonzero pb => + assumeInstancesCommute + pure (.nonzero q(min_ne_of_lt_of_ne $pa $pb)) + | .nonzero pa, .positive pb => + assumeInstancesCommute + pure (.nonzero q(min_ne_of_ne_of_lt $pa $pb)) + | .nonzero pa, .nonzero pb => do + assumeInstancesCommute + pure (.nonzero q(min_ne $pa $pb)) | _, _ => pure .none /-- Extension for the `max` operator. The `max` of two numbers is nonnegative if at least one is nonnegative, strictly positive if at least one is positive, and nonzero if both are nonzero. -/ -@[positivity max _ _] def evalMax : PositivityExt where eval {u α} zα pα e := do +@[positivity max _ _] def evalMax : PositivityExt where eval {u α} zα pα? e := do let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | throwError "not max" let _e_eq : $e =Q $f $a $b := ⟨⟩ let _a ← synthInstanceQ q(LinearOrder $α) assumeInstancesCommute let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(max) - let result : Strictness zα pα e ← catchNone do - let ra ← core zα pα a + let result : Strictness zα pα? e ← catchNone do + let ra ← core zα pα? a match ra with - | .positive pa => pure (.positive q(lt_max_of_lt_left $pa)) - | .nonnegative pa => pure (.nonnegative q(le_max_of_le_left $pa)) + | .positive pa => + assumeInstancesCommute + pure (.positive q(lt_max_of_lt_left $pa)) + | .nonnegative pa => + assumeInstancesCommute + pure (.nonnegative q(le_max_of_le_left $pa)) -- If `a ≠ 0`, we might prove `max a b ≠ 0` if `b ≠ 0` but we don't want to evaluate -- `b` before having ruled out `0 < a`, for performance. So we do that in the second branch -- of the `orElse'`. | _ => pure .none orElse result do - let rb ← core zα pα b + let rb ← core zα pα? b match rb with - | .positive pb => pure (.positive q(lt_max_of_lt_right $pb)) - | .nonnegative pb => pure (.nonnegative q(le_max_of_le_right $pb)) + | .positive pb => + assumeInstancesCommute + pure (.positive q(lt_max_of_lt_right $pb)) + | .nonnegative pb => + assumeInstancesCommute + pure (.nonnegative q(le_max_of_le_right $pb)) | .nonzero pb => do - match ← core zα pα a with + match ← core zα pα? a with | .nonzero pa => pure (.nonzero q(max_ne $pa $pb)) | _ => pure .none | _ => pure .none /-- The `positivity` extension which identifies expressions of the form `a + b`, such that `positivity` successfully recognises both `a` and `b`. -/ -@[positivity _ + _] def evalAdd : PositivityExt where eval {u α} zα pα e := do +@[positivity _ + _] def evalAdd : PositivityExt where eval {u α} zα pα? e := do let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | throwError "not +" let _e_eq : $e =Q $f $a $b := ⟨⟩ let _a ← synthInstanceQ q(AddZeroClass $α) assumeInstancesCommute let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HAdd.hAdd) - let ra ← core zα pα a; let rb ← core zα pα b + let ra ← core zα pα? a; let rb ← core zα pα? b + let some pα := pα? | failure match ra, rb with - | .positive pa, .positive pb => + | .positive (ltα := ltα) pa, .positive pb => let _a ← synthInstanceQ q(AddLeftStrictMono $α) + haveI' : $ltα =Q ($pα).toLT := ⟨⟩ + assumeInstancesCommute pure (.positive q(add_pos $pa $pb)) | .positive pa, .nonnegative pb => let _a ← synthInstanceQ q(AddLeftMono $α) + assumeInstancesCommute pure (.positive q(add_pos_of_pos_of_nonneg $pa $pb)) | .nonnegative pa, .positive pb => let _a ← synthInstanceQ q(AddRightMono $α) + assumeInstancesCommute pure (.positive q(Right.add_pos_of_nonneg_of_pos $pa $pb)) - | .nonnegative pa, .nonnegative pb => + | .nonnegative (leα := leα) pa, .nonnegative pb => let _a ← synthInstanceQ q(AddLeftMono $α) + haveI' : $leα =Q ($pα).toLE := ⟨⟩ + assumeInstancesCommute pure (.nonnegative q(add_nonneg $pa $pb)) | _, _ => failure /-- The `positivity` extension which identifies expressions of the form `a * b`, such that `positivity` successfully recognises both `a` and `b`. -/ -@[positivity _ * _] def evalMul : PositivityExt where eval {u α} zα pα e := do +@[positivity _ * _] def evalMul : PositivityExt where eval {u α} zα pα? e := do let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | throwError "not *" let _e_eq : $e =Q $f $a $b := ⟨⟩ let _a ← synthInstanceQ q(Mul $α) let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HMul.hMul) - let ra ← core zα pα a; let rb ← core zα pα b - let tryProveNonzero (pa? : Option Q($a ≠ 0)) (pb? : Option Q($b ≠ 0)) : - MetaM (Strictness zα pα e) := do + let ra ← core zα pα? a; let rb ← core zα pα? b + let tryProveNonzero (pα? : Option Q(PartialOrder $α)) + (pa? : Option Q($a ≠ 0)) (pb? : Option Q($b ≠ 0)) : + MetaM (Strictness zα pα? e) := do let pa ← liftOption pa? let pb ← liftOption pb? let _a ← synthInstanceQ q(NoZeroDivisors $α) pure (.nonzero q(mul_ne_zero $pa $pb)) - let tryProveNonneg (pa? : Option Q(0 ≤ $a)) (pb? : Option Q(0 ≤ $b)) : - MetaM (Strictness zα pα e) := do + let tryProveNonneg (pα : Q(PartialOrder $α)) (pa? : Option Q(0 ≤ $a)) (pb? : Option Q(0 ≤ $b)) : + MetaM (Strictness zα (some pα) e) := do let pa ← liftOption pa? let pb ← liftOption pb? let _a ← synthInstanceQ q(MulZeroClass $α) let _a ← synthInstanceQ q(PosMulMono $α) assumeInstancesCommute pure (.nonnegative q(mul_nonneg $pa $pb)) - let tryProvePositive (pa? : Option Q(0 < $a)) (pb? : Option Q(0 < $b)) : - MetaM (Strictness zα pα e) := do + let tryProvePositive (pα : Q(PartialOrder $α)) (pa? : Option Q(0 < $a)) (pb? : Option Q(0 < $b)) : + MetaM (Strictness zα (some pα) e) := do let pa ← liftOption pa? let pb ← liftOption pb? let _a ← synthInstanceQ q(MulZeroClass $α) let _a ← synthInstanceQ q(PosMulStrictMono $α) assumeInstancesCommute pure (.positive q(mul_pos $pa $pb)) - let mut result := .none - result ← orElse result (tryProvePositive ra.toPositive rb.toPositive) - result ← orElse result (tryProveNonneg ra.toNonneg rb.toNonneg) - result ← orElse result (tryProveNonzero ra.toNonzero rb.toNonzero) - return result + match pα? with + | .some pα => + let mut result : Strictness zα (some pα) e := .none + result ← orElse result (tryProvePositive pα ra.toPositive rb.toPositive) + result ← orElse result (tryProveNonneg pα ra.toNonneg rb.toNonneg) + result ← orElse result (tryProveNonzero (some pα) ra.toNonzero rb.toNonzero) + return result + | .none => + return ← catchNone <| tryProveNonzero .none ra.toNonzero rb.toNonzero private lemma int_div_self_pos {a : ℤ} (ha : 0 < a) : 0 < a / a := by rw [Int.ediv_self ha.ne']; exact zero_lt_one @@ -227,8 +265,8 @@ where `a` and `b` are integers. -/ @[positivity (_ : ℤ) / (_ : ℤ)] def evalIntDiv : PositivityExt where eval {u α} _ _ e := do match u, α, e with | 0, ~q(ℤ), ~q($a / $b) => - let ra ← core q(inferInstance) q(inferInstance) a - let rb ← core q(inferInstance) q(inferInstance) b + let ra ← core q(inferInstance) (some q(inferInstance)) a + let rb ← core q(inferInstance) (some q(inferInstance)) b assertInstancesCommute match ra, rb with | .positive (pa : Q(0 < $a)), .positive (pb : Q(0 < $b)) => @@ -249,32 +287,44 @@ private theorem pow_zero_pos [Semiring α] [PartialOrder α] [IsOrderedRing α] (a : α) : 0 < a ^ 0 := zero_lt_one.trans_le (pow_zero a).ge +private theorem pow_zero_ne_zero [Semiring α] [Nontrivial α] (a : α) : a ^ 0 ≠ 0 := + pow_zero a ▸ one_ne_zero + /-- The `positivity` extension which identifies expressions of the form `a ^ (0 : ℕ)`. This extension is run in addition to the general `a ^ b` extension (they are overlapping). -/ @[positivity _ ^ (0 : ℕ)] -def evalPowZeroNat : PositivityExt where eval {u α} _zα _pα e := do +def evalPowZeroNat : PositivityExt where eval {u α} _zα pα? e := do let .app (.app _ (a : Q($α))) _ ← withReducible (whnf e) | throwError "not ^" let _a ← synthInstanceQ q(Semiring $α) - let _a ← synthInstanceQ q(PartialOrder $α) + assumeInstancesCommute + haveI' : $e =Q $a ^ 0 := ⟨⟩ + let _a ← synthInstanceQ q(Nontrivial $α) + let some _pα := pα? | pure (.nonzero q(pow_zero_ne_zero $a)) let _a ← synthInstanceQ q(IsOrderedRing $α) - _ ← synthInstanceQ q(Nontrivial $α) - pure (.positive (q(pow_zero_pos $a) : Expr)) + pure (.positive q(pow_zero_pos $a)) /-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℕ)`, such that `positivity` successfully recognises both `a` and `b`. -/ @[positivity _ ^ (_ : ℕ)] -def evalPow : PositivityExt where eval {u α} zα pα e := do +def evalPow : PositivityExt where eval {u α} zα pα? e := do let .app (.app _ (a : Q($α))) (b : Q(ℕ)) ← withReducible (whnf e) | throwError "not ^" + let some pα := pα? | do + let _a ← synthInstanceQ q(MonoidWithZero $α) + let _a ← synthInstanceQ q(NoZeroDivisors $α) + assumeInstancesCommute + haveI' : $e =Q $a ^ $b := ⟨⟩ + let .nonzero nza ← core zα .none a | pure .none + pure (.nonzero q(pow_ne_zero $b $nza)) + let _a ← synthInstanceQ q(Ring $α) + let _a ← synthInstanceQ q(LinearOrder $α) + let _a ← synthInstanceQ q(IsStrictOrderedRing $α) + assumeInstancesCommute let result ← catchNone do let .true := b.isAppOfArity ``OfNat.ofNat 3 | throwError "not a ^ n where n is a literal" let some n := (b.getRevArg! 1).rawNatLit? | throwError "not a ^ n where n is a literal" guard (n % 2 = 0) have m : Q(ℕ) := mkRawNatLit (n / 2) haveI' : $b =Q 2 * $m := ⟨⟩ - let _a ← synthInstanceQ q(Ring $α) - let _a ← synthInstanceQ q(LinearOrder $α) - let _a ← synthInstanceQ q(IsStrictOrderedRing $α) - assumeInstancesCommute haveI' : $e =Q $a ^ $b := ⟨⟩ pure (.nonnegative q((even_two_mul $m).pow_nonneg $a)) orElse result do @@ -302,10 +352,12 @@ def evalPow : PositivityExt where eval {u α} zα pα e := do trace[Tactic.positivity.failure] "{e.toMessageData}" let rα ← synthInstanceQ q(Semiring $α) let oα ← synthInstanceQ q(IsOrderedRing $α) + assumeInstancesCommute orElse (← catchNone (ofNonneg q(le_of_lt $pa) rα oα)) (ofNonzero q(ne_of_gt $pa) rα oα) | .nonnegative pa => let sα ← synthInstanceQ q(Semiring $α) let oα ← synthInstanceQ q(IsOrderedRing $α) + assumeInstancesCommute ofNonneg q($pa) q($sα) q($oα) | .nonzero pa => let sα ← synthInstanceQ q(Semiring $α) @@ -318,20 +370,21 @@ private theorem abs_pos_of_ne_zero {α : Type*} [AddGroup α] [LinearOrder α] /-- The `positivity` extension which identifies expressions of the form `|a|`. -/ @[positivity |_|] -def evalAbs : PositivityExt where eval {_u} (α zα pα) (e : Q($α)) := do +def evalAbs : PositivityExt where eval {_u} (α zα pα?) (e : Q($α)) := do let ~q(@abs _ (_) (_) $a) := e | throwError "not |·|" + let some pα := pα? | pure .none try - match ← core zα pα a with + match ← core zα (some pα) a with | .positive pa => let pa' ← mkAppM ``abs_pos_of_pos #[pa] - pure (.positive pa') + pure (.positive (ltα := q(($pα).toLT)) pa') | .nonzero pa => let pa' ← mkAppM ``abs_pos_of_ne_zero #[pa] - pure (.positive pa') + pure (.positive (ltα := q(($pα).toLT)) pa') | _ => pure .none catch _ => do let pa' ← mkAppM ``abs_nonneg #[a] - pure (.nonnegative pa') + pure (.nonnegative (leα := q(($pα).toLE)) pa') private theorem int_natAbs_pos {n : ℤ} (hn : 0 < n) : 0 < n.natAbs := Int.natAbs_pos.mpr hn.ne' @@ -363,17 +416,24 @@ def evalNatAbs : PositivityExt where eval {u α} _zα _pα e := do /-- Extension for the `positivity` tactic: `Nat.cast` is always non-negative, and positive when its input is. -/ @[positivity Nat.cast _] -def evalNatCast : PositivityExt where eval {u α} _zα _pα e := do +def evalNatCast : PositivityExt where eval {u α} _zα pα? e := do let ~q(@Nat.cast _ (_) ($a : ℕ)) := e | throwError "not Nat.cast" let zα' : Q(Zero Nat) := q(inferInstance) - let pα' : Q(PartialOrder Nat) := q(inferInstance) let (_i1 : Q(AddMonoidWithOne $α)) ← synthInstanceQ q(AddMonoidWithOne $α) + let some _pα := pα? | do + let (_cz : Q(CharZero $α)) ← synthInstanceQ q(CharZero $α) + assumeInstancesCommute + match ← core zα' .none a with + | .nonzero nza => pure (.nonzero q(Nat.cast_ne_zero.2 $nza)) + | _ => pure .none + let pα' : Q(PartialOrder Nat) := q(inferInstance) let (_i2 : Q(AddLeftMono $α)) ← synthInstanceQ q(AddLeftMono $α) let (_i3 : Q(ZeroLEOneClass $α)) ← synthInstanceQ q(ZeroLEOneClass $α) assumeInstancesCommute match ← core zα' pα' a with | .positive pa => let _nz ← synthInstanceQ q(NeZero (1 : $α)) + assumeInstancesCommute pure (.positive q(Nat.cast_pos'.2 $pa)) | _ => pure (.nonnegative q(Nat.cast_nonneg' _)) @@ -381,30 +441,30 @@ def evalNatCast : PositivityExt where eval {u α} _zα _pα e := do /-- Extension for the `positivity` tactic: `Int.cast` is positive (resp. non-negative) if its input is. -/ @[positivity Int.cast _] -def evalIntCast : PositivityExt where eval {u α} _zα _pα e := do +def evalIntCast : PositivityExt where eval {u α} _zα pα? e := do let ~q(@Int.cast _ (_) ($a : ℤ)) := e | throwError "not Int.cast" let zα' : Q(Zero Int) := q(inferInstance) let pα' : Q(PartialOrder Int) := q(inferInstance) let ra ← core zα' pα' a - match ra with - | .positive pa => + match ra, pα? with + | .positive pa, some _ => let _rα ← synthInstanceQ q(Ring $α) let _oα ← synthInstanceQ q(IsOrderedRing $α) let _nt ← synthInstanceQ q(Nontrivial $α) assumeInstancesCommute pure (.positive q(Int.cast_pos.mpr $pa)) - | .nonnegative pa => + | .nonnegative pa, some _ => let _rα ← synthInstanceQ q(Ring $α) let _oα ← synthInstanceQ q(IsOrderedRing $α) let _nt ← synthInstanceQ q(Nontrivial $α) assumeInstancesCommute pure (.nonnegative q(Int.cast_nonneg.mpr $pa)) - | .nonzero pa => + | .nonzero pa, _ => let _oα ← synthInstanceQ q(AddGroupWithOne $α) let _nt ← synthInstanceQ q(CharZero $α) assumeInstancesCommute pure (.nonzero q(Int.cast_ne_zero.mpr $pa)) - | .none => + | _ , _ => pure .none /-- Extension for `Nat.succ`. -/ @@ -453,10 +513,14 @@ def evalNatGCD : PositivityExt where eval {u α} z p e := do | 0, ~q(ℕ), ~q(Nat.gcd $a $b) => assertInstancesCommute match ← core z p a with - | .positive pa => return .positive q(Nat.gcd_pos_of_pos_left $b $pa) + | .positive pa => + assertInstancesCommute + return .positive q(Nat.gcd_pos_of_pos_left $b $pa) | _ => match ← core z p b with - | .positive pb => return .positive q(Nat.gcd_pos_of_pos_right $a $pb) + | .positive pb => + assertInstancesCommute + return .positive q(Nat.gcd_pos_of_pos_right $a $pb) | _ => failure | _, _, _ => throwError "not Nat.gcd" @@ -468,8 +532,10 @@ def evalNatLCM : PositivityExt where eval {u α} z p e := do assertInstancesCommute match ← core z p a with | .positive pa => + assertInstancesCommute match ← core z p b with | .positive pb => + assertInstancesCommute return .positive q(Nat.lcm_pos $pa $pb) | _ => failure | _ => failure @@ -482,7 +548,9 @@ def evalNatSqrt : PositivityExt where eval {u α} z p e := do | 0, ~q(ℕ), ~q(Nat.sqrt $n) => assumeInstancesCommute match ← core z p n with - | .positive pa => return .positive q(Nat.sqrt_pos.mpr $pa) + | .positive pa => + assumeInstancesCommute + return .positive q(Nat.sqrt_pos.mpr $pa) | _ => failure | _, _, _ => throwError "not Nat.sqrt" @@ -495,10 +563,10 @@ def evalIntGCD : PositivityExt where eval {u α} _ _ e := do let z ← synthInstanceQ (q(Zero ℤ) : Q(Type)) let p ← synthInstanceQ (q(PartialOrder ℤ) : Q(Type)) assertInstancesCommute - match (← catchNone (core z p a)).toNonzero with + match (← catchNone (core z (some p) a)).toNonzero with | some na => return .positive q(Int.gcd_pos_of_ne_zero_left $b $na) | none => - match (← core z p b).toNonzero with + match (← core z (some p) b).toNonzero with | some nb => return .positive q(Int.gcd_pos_of_ne_zero_right $a $nb) | none => failure | _, _, _ => throwError "not Int.gcd" @@ -511,9 +579,9 @@ def evalIntLCM : PositivityExt where eval {u α} _ _ e := do let z ← synthInstanceQ (q(Zero ℤ) : Q(Type)) let p ← synthInstanceQ (q(PartialOrder ℤ) : Q(Type)) assertInstancesCommute - match (← core z p a).toNonzero with + match (← core z (some p) a).toNonzero with | some na => - match (← core z p b).toNonzero with + match (← core z (some p) b).toNonzero with | some nb => return .positive q(Int.lcm_pos $na $nb) | _ => failure | _ => failure @@ -533,9 +601,12 @@ def evalNNRatNum : PositivityExt where eval {u α} _ _ e := do | 0, ~q(ℕ), ~q(NNRat.num $a) => let zα : Q(Zero ℚ≥0) := q(inferInstance) let pα : Q(PartialOrder ℚ≥0) := q(inferInstance) + trace[Tactic.positivity] "I'm evalNNRatNum: {e}" assumeInstancesCommute match ← core zα pα a with - | .positive pa => return .positive q(NNRat.num_pos_of_pos $pa) + | .positive pa => + assumeInstancesCommute + return .positive q(NNRat.num_pos_of_pos $pa) | .nonzero pa => return .nonzero q(NNRat.num_ne_zero_of_ne_zero $pa) | _ => return .none | _, _, _ => throwError "not NNRat.num" @@ -551,6 +622,9 @@ def evalNNRatDen : PositivityExt where eval {u α} _ _ e := do variable {q : ℚ≥0} +set_option trace.Tactic.positivity true +set_option trace.Tactic.positivity.failure true + example (hq : 0 < q) : 0 < q.num := by positivity example (hq : q ≠ 0) : q.num ≠ 0 := by positivity example : 0 < q.den := by positivity @@ -573,8 +647,12 @@ def evalRatNum : PositivityExt where eval {u α} _ _ e := do let pα : Q(PartialOrder ℚ) := q(inferInstance) assumeInstancesCommute match ← core zα pα a with - | .positive pa => pure <| .positive q(num_pos_of_pos $pa) - | .nonnegative pa => pure <| .nonnegative q(num_nonneg_of_nonneg $pa) + | .positive pa => + assumeInstancesCommute + pure <| .positive q(num_pos_of_pos $pa) + | .nonnegative pa => + assumeInstancesCommute + pure <| .nonnegative q(num_nonneg_of_nonneg $pa) | .nonzero pa => pure <| .nonzero q(num_ne_zero_of_ne_zero $pa) | .none => pure .none | _, _ => throwError "not Rat.num" @@ -600,7 +678,9 @@ def evalPosPart : PositivityExt where eval {u α} zα pα e := do -- `.none`) here sometimes. See e.g. the first test for `posPart`. This is why we need -- `catchNone` match ← catchNone (core zα pα a) with - | .positive pf => return .positive q(posPart_pos $pf) + | .positive pf => + assumeInstancesCommute + return .positive q(posPart_pos $pf) | _ => return .nonnegative q(posPart_nonneg $a) | _ => throwError "not `posPart`" @@ -617,11 +697,12 @@ def evalNegPart : PositivityExt where eval {u α} _ _ e := do /-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/ @[positivity DFunLike.coe _ _] -def evalMap : PositivityExt where eval {_ β} _ _ e := do +def evalMap : PositivityExt where eval {_ β} _ pβ? e := do let .app (.app _ f) a ← whnfR e | throwError "not ↑f · where f is of NonnegHomClass" + let some pβ := pβ? | throwError "not PartialOrder" let pa ← mkAppOptM ``apply_nonneg #[none, none, β, none, none, none, none, f, a] - pure (.nonnegative pa) + pure (.nonnegative (leα := pβ) pa) end Positivity diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean index 82e60bb490debf..af307a76b8a6c9 100644 --- a/Mathlib/Tactic/Positivity/Core.lean +++ b/Mathlib/Tactic/Positivity/Core.lean @@ -211,8 +211,8 @@ def throwNone {m : Type → Type*} {e : Q($α)} [Monad m] [Alternative m] | r => pure r /-- Attempts to prove a `Strictness` result when `e` evaluates to a literal number. -/ -def normNumPositivity (e : Q($α)) - : MetaM (Strictness zα pα? e) := catchNone do +def normNumPositivity (pα : Q(PartialOrder $α)) (e : Q($α)) + : MetaM (Strictness zα pα e) := catchNone do match ← NormNum.derive e with | .isBool .. => failure | .isNat _ lit p => @@ -225,7 +225,7 @@ def normNumPositivity (e : Q($α)) let _a ← synthInstanceQ q(PartialOrder $α) let _a ← synthInstanceQ q(IsOrderedRing $α) let _a ← synthInstanceQ q(Nontrivial $α) - assertInstancesCommute + assumeInstancesCommute have p : Q(NormNum.IsNat $e $lit) := p haveI' p' : Nat.ble 1 $lit =Q true := ⟨⟩ pure (.positive q(pos_of_isNat (A := $α) $p $p')) @@ -236,7 +236,7 @@ def normNumPositivity (e : Q($α)) let _a ← synthInstanceQ q(AddLeftMono $α) let _a ← synthInstanceQ q(ZeroLEOneClass $α) let _a ← synthInstanceQ q(NeZero (1 : $α)) - assertInstancesCommute + assumeInstancesCommute have p : Q(NormNum.IsNat $e $lit) := p haveI' p' : Nat.ble 1 $lit =Q true := ⟨⟩ pure (.positive q(pos_of_isNat' (A := $α) $p $p')) @@ -248,7 +248,7 @@ def normNumPositivity (e : Q($α)) let _a ← synthInstanceQ q(Semiring $α) let _a ← synthInstanceQ q(PartialOrder $α) let _a ← synthInstanceQ q(IsOrderedRing $α) - assertInstancesCommute + assumeInstancesCommute have p : Q(NormNum.IsNat $e $lit) := p pure (.nonnegative q(nonneg_of_isNat $p)) catch e : Exception => @@ -257,14 +257,14 @@ def normNumPositivity (e : Q($α)) let _a ← synthInstanceQ q(PartialOrder $α) let _a ← synthInstanceQ q(AddLeftMono $α) let _a ← synthInstanceQ q(ZeroLEOneClass $α) - assertInstancesCommute + assumeInstancesCommute have p : Q(NormNum.IsNat $e $lit) := p pure (.nonnegative q(nonneg_of_isNat' $p)) | .isNegNat _ lit p => let _a ← synthInstanceQ q(Ring $α) let _a ← synthInstanceQ q(PartialOrder $α) let _a ← synthInstanceQ q(IsStrictOrderedRing $α) - assertInstancesCommute + assumeInstancesCommute have p : Q(NormNum.IsInt $e (Int.negOfNat $lit)) := p haveI' p' : Nat.ble 1 $lit =Q true := ⟨⟩ pure (.nonzero q(nz_of_isNegNat $p $p')) @@ -272,7 +272,7 @@ def normNumPositivity (e : Q($α)) let _a ← synthInstanceQ q(Semiring $α) let _a ← synthInstanceQ q(LinearOrder $α) let _a ← synthInstanceQ q(IsStrictOrderedRing $α) - assertInstancesCommute + assumeInstancesCommute have p : Q(NormNum.IsNNRat $e $n $d) := p if 0 < q then haveI' w : decide (0 < $n) =Q true := ⟨⟩ @@ -284,7 +284,7 @@ def normNumPositivity (e : Q($α)) let _a ← synthInstanceQ q(Ring $α) let _a ← synthInstanceQ q(LinearOrder $α) let _a ← synthInstanceQ q(IsStrictOrderedRing $α) - assertInstancesCommute + assumeInstancesCommute have p : Q(NormNum.IsRat $e (.negOfNat $n) $d) := p if q < 0 then haveI' w : decide (Int.negOfNat $n < 0) =Q true := ⟨⟩ @@ -294,11 +294,11 @@ def normNumPositivity (e : Q($α)) pure (.nonnegative q(nonneg_of_isRat $p $w)) /-- Attempts to prove that `e ≥ 0` using `zero_le` in a `CanonicallyOrderedAdd` monoid. -/ -def positivityCanon (e : Q($α)) : MetaM (Strictness zα pα? e) := do +def positivityCanon (pα : Q(PartialOrder $α)) (e : Q($α)) : MetaM (Strictness zα pα e) := do let _add ← synthInstanceQ q(AddMonoid $α) let _le ← synthInstanceQ q(PartialOrder $α) let _i ← synthInstanceQ q(CanonicallyOrderedAdd $α) - assertInstancesCommute + assumeInstancesCommute pure (.nonnegative q(zero_le $e)) /-- A variation on `assumption` when the hypothesis is `lo ≤ e` where `lo` is a numeral. -/ @@ -306,10 +306,10 @@ def compareHypLE (pα : Q(PartialOrder $α)) (lo e : Q($α)) (p₂ : Q($lo ≤ $ MetaM (Strictness zα pα e) := do match ← normNumPositivity zα pα lo with | .positive p₁ => do - assertInstancesCommute + assumeInstancesCommute pure (.positive q(lt_of_lt_of_le $p₁ $p₂)) | .nonnegative p₁ => do - assertInstancesCommute + assumeInstancesCommute pure (.nonnegative q(le_trans $p₁ $p₂)) | _ => pure .none @@ -318,10 +318,10 @@ def compareHypLT (pα : Q(PartialOrder $α)) (lo e : Q($α)) (p₂ : Q($lo < $e) MetaM (Strictness zα pα e) := do match ← normNumPositivity zα pα lo with | .positive p₁ => do - assertInstancesCommute + assumeInstancesCommute pure (.positive q(lt_trans $p₁ $p₂)) | .nonnegative p₁ => do - assertInstancesCommute + assumeInstancesCommute pure (.positive q(lt_of_le_of_lt $p₁ $p₂)) | _ => pure .none @@ -340,64 +340,66 @@ initialize registerTraceClass `Tactic.positivity.failure /-- A variation on `assumption` which checks if the hypothesis `ldecl` is `a [ + let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return .none + let .defEq _ ← isDefEqQ e hi | return .none + match lo with + | ~q(0) => + assertInstancesCommute + return .nonnegative q($p) + | _ => compareHypLE zα pα lo e p + | ~q(@LT.lt.{u} $β $_lt $lo $hi) => + let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return .none + let .defEq _ ← isDefEqQ e hi | return .none + match lo with + | ~q(0) => + assertInstancesCommute + return .positive q($p) + | _ => compareHypLT zα pα lo e p + | ~q(@Eq.{u+1} $α' $lhs $rhs) => + let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none + match ← isDefEqQ e rhs with + | .defEq _ => + match lhs with + | ~q(0) => pure <| .nonnegative q(le_of_eq $p) + | _ => compareHypEq zα pα e lhs q($p) + | .notDefEq => + let .defEq _ ← isDefEqQ e lhs | pure .none + match rhs with + | ~q(0) => pure <| .nonnegative q(ge_of_eq $p) + | _ => compareHypEq zα pα e rhs q(Eq.symm $p) + | ~q(@Ne.{u+1} $α' $lhs $rhs) => + let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none + match lhs, rhs with + | ~q(0), _ => + let .defEq _ ← isDefEqQ e rhs | pure .none + pure <| .nonzero q(Ne.symm $p) + | _, ~q(0) => + let .defEq _ ← isDefEqQ e lhs | pure .none + pure <| .nonzero q($p) + | _, _ => pure .none + | _ => pure .none + +def compareHypNonzero (e : Q($α)) (ldecl : LocalDecl) : MetaM (Strictness zα .none e) := do have e' : Q(Prop) := ldecl.type let p : Q($e') := .fvar ldecl.fvarId - if let some pα := pα? then - match e' with - | ~q(@LE.le.{u} $β $_le $lo $hi) => - let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return .none - let .defEq _ ← isDefEqQ e hi | return .none - match lo with - | ~q(0) => - assertInstancesCommute - return .nonnegative q($p) - | _ => compareHypLE zα pα lo e p - | ~q(@LT.lt.{u} $β $_lt $lo $hi) => - let .defEq (_ : $α =Q $β) ← isDefEqQ α β | return .none - let .defEq _ ← isDefEqQ e hi | return .none - match lo with - | ~q(0) => - assertInstancesCommute - return .positive q($p) - | _ => compareHypLT zα pα lo e p - | ~q(@Eq.{u+1} $α' $lhs $rhs) => - let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none - match ← isDefEqQ e rhs with - | .defEq _ => - match lhs with - | ~q(0) => pure <| .nonnegative q(le_of_eq $p) - | _ => compareHypEq zα pα e lhs q($p) - | .notDefEq => - let .defEq _ ← isDefEqQ e lhs | pure .none - match rhs with - | ~q(0) => pure <| .nonnegative q(ge_of_eq $p) - | _ => compareHypEq zα pα e rhs q(Eq.symm $p) - | ~q(@Ne.{u+1} $α' $lhs $rhs) => - let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none - match lhs, rhs with - | ~q(0), _ => - let .defEq _ ← isDefEqQ e rhs | pure .none - pure <| .nonzero q(Ne.symm $p) - | _, ~q(0) => - let .defEq _ ← isDefEqQ e lhs | pure .none - pure <| .nonzero q($p) - | _, _ => pure .none - | _ => pure .none - else - match e' with - | ~q(@Ne.{u+1} $α' $lhs $rhs) => - let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none - match lhs, rhs with - | ~q(0), _ => - let .defEq _ ← isDefEqQ e rhs | pure .none - pure <| .nonzero q(Ne.symm $p) - | _, ~q(0) => - let .defEq _ ← isDefEqQ e lhs | pure .none - pure <| .nonzero q($p) - | _, _ => pure .none - | _ => pure .none + match e' with + | ~q(@Ne.{u+1} $α' $lhs $rhs) => + let .defEq (_ : $α =Q $α') ← isDefEqQ α α' | pure .none + match lhs, rhs with + | ~q(0), _ => + let .defEq _ ← isDefEqQ e rhs | pure .none + pure <| .nonzero q(Ne.symm $p) + | _, ~q(0) => + let .defEq _ ← isDefEqQ e lhs | pure .none + pure <| .nonzero q($p) + | _, _ => pure .none + | _ => pure .none variable {zα pα?} in /-- The main combinator which combines multiple `positivity` results. @@ -414,7 +416,7 @@ def orElse {e : Q($α)} (t₁ : Strictness zα pα? e) (t₂ : MetaM (Strictness | p@(.positive _) => pure p | .nonzero p₂ => let some _ := pα? | throwError "cannot synth PartialOrd for {α}" - assertInstancesCommute + assumeInstancesCommute pure (.positive q(lt_of_le_of_ne' $p₁ $p₂)) | _ => pure (.nonnegative p₁) | .nonzero p₁ => @@ -422,7 +424,7 @@ def orElse {e : Q($α)} (t₁ : Strictness zα pα? e) (t₂ : MetaM (Strictness | p@(.positive _) => pure p | .nonnegative p₂ => let some _ := pα? | throwError "cannot synth PartialOrd for {α}" - assertInstancesCommute + assumeInstancesCommute pure (.positive q(lt_of_le_of_ne' $p₂ $p₁)) | _ => pure (.nonzero p₁) @@ -435,16 +437,29 @@ def core (e : Q($α)) : MetaM (Strictness zα pα? e) := do result ← orElse result <| ext.eval zα pα? e catch err => trace[Tactic.positivity] "{e} failed: {err.toMessageData}" - result ← orElse result <| normNumPositivity zα pα? e - result ← orElse result <| positivityCanon zα pα? e - if let .positive _ := result then + trace[Tactic.positivity] "current result from ext: {result.toString}" -- ?? + match pα? with + | some pα => + result ← orElse result <| normNumPositivity zα pα e + result ← orElse result <| positivityCanon zα pα e + if let .positive _ := result then + trace[Tactic.positivity] "{e} => {result.toString}" + return result + for ldecl in ← getLCtx do + if !ldecl.isImplementationDetail then + result ← orElse result <| compareHyp zα pα e ldecl + trace[Tactic.positivity] "{e} => {result.toString}" + throwNone (pure result) + | .none => + if let .nonzero _ := result then + trace[Tactic.positivity] "{e} => {result.toString}" + return result + for ldecl in ← getLCtx do + if !ldecl.isImplementationDetail then + result ← orElse result <| compareHypNonzero zα e ldecl trace[Tactic.positivity] "{e} => {result.toString}" - return result - for ldecl in ← getLCtx do - if !ldecl.isImplementationDetail then - result ← orElse result <| compareHyp zα pα? e ldecl - trace[Tactic.positivity] "{e} => {result.toString}" - throwNone (pure result) + throwNone (pure result) + private inductive OrderRel : Type | le : OrderRel -- `0 ≤ a` @@ -479,10 +494,10 @@ or fails. -/ def solve (t : Q(Prop)) : MetaM Expr := do let rest {u : Level} (α : Q(Type u)) z e (relDesired : OrderRel) : MetaM Expr := do let zα ← synthInstanceQ q(Zero $α) - assertInstancesCommute + assumeInstancesCommute let .true ← isDefEq z q(0 : $α) | throwError "not a positivity goal" let pα? ← try? <| synthInstanceQ q(PartialOrder $α) - assertInstancesCommute + assumeInstancesCommute let r ← catchNone <| Meta.Positivity.core zα pα? e let throw (a b : String) : MetaM Expr := throwError "failed to prove {a}, but it would be possible to prove {b} if desired" @@ -492,13 +507,13 @@ def solve (t : Q(Prop)) : MetaM Expr := do | .le, .nonnegative p | .ne, .nonzero p => pure p | .le, .positive p => do - assertInstancesCommute + assumeInstancesCommute pure q(le_of_lt $p) | .ne, .positive p => do - assertInstancesCommute + assumeInstancesCommute pure q(ne_of_gt $p) | .ne', .positive p => do - assertInstancesCommute + assumeInstancesCommute pure q(ne_of_lt $p) | .ne', .nonzero p => pure q(Ne.symm $p) | .lt, .nonnegative _ => throw "strict positivity" "nonnegativity" diff --git a/Mathlib/Tactic/Positivity/test_Basic.lean b/Mathlib/Tactic/Positivity/test_Basic.lean new file mode 100644 index 00000000000000..83d4eaa7133d1a --- /dev/null +++ b/Mathlib/Tactic/Positivity/test_Basic.lean @@ -0,0 +1,245 @@ +import Mathlib.Tactic.Positivity.Basic + +/-! # Tests for the `positivity` tactic + +This tactic proves goals of the form `0 ≤ a` and `0 < a`. +-/ +set_option autoImplicit true +set_option trace.Tactic.positivity true +set_option trace.Tactic.positivity.failure true + +open Function Nat + +variable {ι α β E : Type*} + +/- ## Numeric goals -/ + +example : 0 ≤ 0 := by positivity + +example : 0 ≤ 3 := by positivity + +example : 0 < 3 := by positivity +-- example : (0 : EReal) < 2 := by positivity +-- example : 0 < (2 : EReal) := by positivity +-- example : (0 : EReal) < 2 := by positivity + +-- example : (0 : ℝ≥0∞) ≤ 1 := by positivity +-- example : (0 : ℝ≥0∞) ≤ 0 := by positivity +-- example : (0 : EReal) ≤ 0 := by positivity +-- example : 0 ≤ (2 : EReal) := by positivity + +/- ## Goals working directly from a hypothesis -/ + +section FromHypothesis + +-- set_option trace.Meta.debug true +-- sudo set_option trace.Tactic.positivity true +example {a : ℤ} (ha : 0 < a) : 0 < a := by positivity +example {a : ℤ} (ha : 0 < a) : 0 ≤ a := by positivity +example {a : ℤ} (ha : 0 < a) : a ≠ 0 := by positivity +example {a : ℤ} (ha : 0 ≤ a) : 0 ≤ a := by positivity +example {a : ℤ} (ha : a ≠ 0) : a ≠ 0 := by positivity +example {a : ℤ} (ha : a = 0) : 0 ≤ a := by positivity + +section + +variable [Zero α] [PartialOrder α] {a : α} + +example (ha : 0 < a) : 0 < a := by positivity +example (ha : 0 < a) : 0 ≤ a := by positivity +example (ha : 0 < a) : a ≠ 0 := by positivity +example (ha : 0 ≤ a) : 0 ≤ a := by positivity +example (ha : a ≠ 0) : a ≠ 0 := by positivity +example (ha : a = 0) : 0 ≤ a := by positivity + +end + +/- ### Reversing hypotheses -/ + +example {a : ℤ} (ha : a > 0) : 0 < a := by positivity +example {a : ℤ} (ha : a > 0) : 0 ≤ a := by positivity +example {a : ℤ} (ha : a > 0) : a ≥ 0 := by positivity +example {a : ℤ} (ha : a > 0) : a ≠ 0 := by positivity +example {a : ℤ} (ha : a ≥ 0) : 0 ≤ a := by positivity +example {a : ℤ} (ha : 0 ≠ a) : a ≠ 0 := by positivity +example {a : ℤ} (ha : 0 < a) : a > 0 := by positivity +example {a : ℤ} (ha : 0 < a) : a ≥ 0 := by positivity +example {a : ℤ} (ha : 0 < a) : 0 ≠ a := by positivity +example {a : ℤ} (ha : 0 ≤ a) : a ≥ 0 := by positivity +example {a : ℤ} (ha : a ≠ 0) : 0 ≠ a := by positivity +example {a : ℤ} (ha : a = 0) : a ≥ 0 := by positivity +example {a : ℤ} (ha : 0 = a) : 0 ≤ a := by positivity +example {a : ℤ} (ha : 0 = a) : a ≥ 0 := by positivity + +end FromHypothesis + +/- ### Calling `norm_num` -/ + +example {a : ℤ} (ha : 3 = a) : 0 ≤ a := by positivity +example {a : ℤ} (ha : 3 = a) : a ≠ 0 := by positivity +example {a : ℤ} (ha : 3 = a) : 0 < a := by positivity +example {a : ℤ} (ha : a = -1) : a ≠ 0 := by positivity + +example {a : ℤ} (ha : 3 ≤ a) : 0 ≤ a := by positivity +example {a : ℤ} (ha : 3 ≤ a) : a ≠ 0 := by positivity +example {a : ℤ} (ha : 3 ≤ a) : 0 < a := by positivity + +example {a : ℤ} (ha : 3 < a) : 0 ≤ a := by positivity +example {a : ℤ} (ha : 3 < a) : a ≠ 0 := by positivity +example {a : ℤ} (ha : 3 < a) : 0 < a := by positivity + +example {a b : ℤ} (h : 0 ≤ a + b) : 0 ≤ a + b := by positivity + +example {a : ℤ} (hlt : 0 ≤ a) (hne : a ≠ 0) : 0 < a := by positivity + +example {a b c d : ℤ} (ha : c < a) (hb : d < b) : 0 < (a - c) * (b - d) := by + positivity [sub_pos_of_lt ha, sub_pos_of_lt hb] + +section + +variable [Field α] [LinearOrder α] [IsStrictOrderedRing α] + +example : (1/4 - 2/3 : ℚ) ≠ 0 := by positivity +example : (1/4 - 2/3 : α) ≠ 0 := by positivity + +end + +/- ### `ArithmeticFunction.sigma` and `ArithmeticFunction.zeta` -/ + +-- example (a b : ℕ) (hb : 0 < b) : 0 < ArithmeticFunction.sigma a b := by positivity +-- example (a : ℕ) (ha : 0 < a) : 0 < ArithmeticFunction.zeta a := by positivity + +/- +## Test for meta-variable instantiation + +Reported on +https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/New.20tactic.3A.20.60positivity.60/near/300639970 +-/ + +example : 0 ≤ 0 := by apply le_trans _ (le_refl _); positivity + + +/- ## Tests of the @[positivity] plugin tactics (addition, multiplication, division) -/ + +-- example [Nonempty ι] [Zero α] {a : α} (ha : a ≠ 0) : const ι a ≠ 0 := by positivity +-- example [Zero α] [PartialOrder α] {a : α} (ha : 0 < a) : 0 ≤ const ι a := by positivity +-- example [Zero α] [PartialOrder α] {a : α} (ha : 0 ≤ a) : 0 ≤ const ι a := by positivity +-- example [Nonempty ι] [Zero α] [PartialOrder α] {a : α} (ha : 0 < a) : 0 < const ι a := by +-- positivity + +section ite +variable {p : Prop} [Decidable p] {a b : ℤ} + +example (ha : 0 < a) (hb : 0 < b) : 0 < ite p a b := by positivity +example (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ ite p a b := by positivity +example (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ ite p a b := by positivity +example (ha : 0 < a) (hb : b ≠ 0) : ite p a b ≠ 0 := by positivity +example (ha : a ≠ 0) (hb : 0 < b) : ite p a b ≠ 0 := by positivity +example (ha : a ≠ 0) (hb : b ≠ 0) : ite p a b ≠ 0 := by positivity + +end ite + +section MinMax + +example {a b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < min a b := by positivity +example {a b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ min a b := by positivity +example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ min a b := by positivity +example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ min a b := by positivity +example {a b : ℚ} (ha : 0 < a) (hb : b ≠ 0) : min a b ≠ 0 := by positivity +example {a b : ℚ} (ha : a ≠ 0) (hb : 0 < b) : min a b ≠ 0 := by positivity +example {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : min a b ≠ 0 := by positivity + +example {a b : ℚ} (ha : 0 < a) : 0 < max a b := by positivity +example {a b : ℚ} (hb : 0 < b) : 0 < max a b := by positivity +example {a b : ℚ} (ha : 0 ≤ a) : 0 ≤ max a b := by positivity +example {a b : ℚ} (hb : 0 ≤ b) : 0 ≤ max a b := by positivity +example {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : max a b ≠ 0 := by positivity + +example : 0 ≤ max 3 4 := by positivity +example : 0 ≤ max (0 : ℤ) (-3) := by positivity +example : 0 ≤ max (-3 : ℤ) 5 := by positivity + +end MinMax + +example {a b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by positivity +example {a b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a * b := by positivity +example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a * b := by positivity +example {a b : ℚ} (ha : 0 < a) (hb : b ≠ 0) : a * b ≠ 0 := by positivity +example {a b : ℚ} (ha : a ≠ 0) (hb : 0 < b) : a * b ≠ 0 := by positivity +example {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := by positivity + +example {a b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by positivity +example {a b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a / b := by positivity +example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a / b := by positivity +example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by positivity +example {a b : ℚ} (ha : 0 < a) (hb : b ≠ 0) : a / b ≠ 0 := by positivity +example {a b : ℚ} (ha : a ≠ 0) (hb : 0 < b) : a / b ≠ 0 := by positivity +example {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 := by positivity + +example {a b : ℤ} (ha : 0 < a) (hb : 0 < b) : 0 ≤ a / b := by positivity +example {a : ℤ} (ha : 0 < a) : 0 < a / a := by positivity +example {a b : ℤ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a / b := by positivity +example {a b : ℤ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a / b := by positivity +example {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by positivity + +example {a : ℚ} (ha : 0 < a) : 0 < a⁻¹ := by positivity +example {a : ℚ} (ha : 0 ≤ a) : 0 ≤ a⁻¹ := by positivity +example {a : ℚ} (ha : a ≠ 0) : a⁻¹ ≠ 0 := by positivity + +example {a : ℚ} (n : ℕ) (ha : 0 < a) : 0 < a ^ n := by positivity +example {a : ℚ} (n : ℕ) (ha : 0 ≤ a) : 0 ≤ a ^ n := by positivity +example {a : ℚ} (n : ℕ) (ha : a ≠ 0) : a ^ n ≠ 0 := by positivity +example {a : ℚ} : 0 ≤ a ^ 18 := by positivity +example {a : ℚ} (ha : a ≠ 0) : 0 < a ^ 18 := by positivity + +example {a : ℚ} (ha : 0 < a) : 0 < |a| := by positivity +example {a : ℚ} (ha : a ≠ 0) : 0 < |a| := by positivity +example (a : ℚ) : 0 ≤ |a| := by positivity + +example {a : ℤ} {b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < a • b := by positivity +example {a : ℤ} {b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a • b := by positivity +example {a : ℤ} {b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a • b := by positivity +example {a : ℤ} {b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a • b := by positivity +example {a : ℤ} {b : ℚ} (ha : 0 < a) (hb : b ≠ 0) : a • b ≠ 0 := by positivity +example {a : ℤ} {b : ℚ} (ha : a ≠ 0) (hb : 0 < b) : a • b ≠ 0 := by positivity +example {a : ℤ} {b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : a • b ≠ 0 := by positivity + +-- Test that the positivity extension for `a • b` can handle universe polymorphism. +-- example {R M : Type*} [Semiring R] [PartialOrder R] [IsOrderedRing R] +-- [Semiring M] [PartialOrder M] [IsStrictOrderedRing M] +-- [SMulWithZero R M] [PosSMulStrictMono R M] {a : R} {b : M} (ha : 0 < a) (hb : 0 < b) : +-- 0 < a • b := by positivity + +example {a : ℤ} (ha : 3 < a) : 0 ≤ a + a := by positivity + +example {a b : ℤ} (ha : 3 < a) (hb : 4 ≤ b) : 0 ≤ 3 + a + b + b + 14 := by positivity + +example {H : Type*} [AddCommGroup H] [LinearOrder H] [IsOrderedAddMonoid H] + {a b : H} (ha : 0 < a) (hb : 0 ≤ b) : + 0 ≤ a + a + b := by + positivity + +example {a : ℤ} (ha : 3 < a) : 0 < a + a := by positivity + +example {a b : ℚ} (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity + +example {a b : ℤ} (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity + +section +variable {q : ℚ} + +example (hq : q ≠ 0) : q.num ≠ 0 := by positivity +example : 0 < q.den := by positivity +example (hq : 0 < q) : 0 < q := by positivity +example (hq : 0 ≤ q) : 0 ≤ q.num := by positivity + +end + +example (a b : ℕ) (ha : a ≠ 0) : 0 < a.gcd b := by positivity +example (a b : ℤ) (ha : a ≠ 0) : 0 < a.gcd b := by positivity +example (a b : ℕ) (hb : b ≠ 0) : 0 < a.gcd b := by positivity +example (a b : ℤ) (hb : b ≠ 0) : 0 < a.gcd b := by positivity +example (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a.lcm b := by positivity +example (a b : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a.lcm b := by positivity +example (a : ℕ) (ha : a ≠ 0) : 0 < a.sqrt := by positivity +-- example (a : ℕ) (ha : a ≠ 0) : 0 < a.totient := by positivity From e48dfe7905aa8ee8330f9867ab3478ea5e181344 Mon Sep 17 00:00:00 2001 From: Pan Lin <58059503+HugLycan@users.noreply.github.com> Date: Mon, 19 Jan 2026 10:27:34 +0100 Subject: [PATCH 3/8] more positivity extensions --- .../Algebra/Order/AbsoluteValue/Basic.lean | 5 +- .../Algebra/Order/BigOperators/Expect.lean | 3 +- .../Order/BigOperators/Ring/Finset.lean | 3 +- Mathlib/Algebra/Order/Field/Basic.lean | 65 ++++++++++++++----- Mathlib/Algebra/Order/Field/Power.lean | 13 +++- Mathlib/Algebra/Order/Module/Algebra.lean | 2 +- Mathlib/Tactic/Positivity/Basic.lean | 15 ++--- Mathlib/Tactic/Positivity/Core.lean | 7 +- Mathlib/Tactic/Positivity/Finset.lean | 5 +- Mathlib/Tactic/Positivity/test_Basic.lean | 14 +++- 10 files changed, 95 insertions(+), 37 deletions(-) diff --git a/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean b/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean index d5793a666368c6..61596c41afe136 100644 --- a/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean +++ b/Mathlib/Algebra/Order/AbsoluteValue/Basic.lean @@ -410,10 +410,11 @@ lemma abv_nonneg (x) : 0 ≤ abv x := abv_nonneg' x open Lean Meta Mathlib Meta Positivity Qq in /-- The `positivity` extension which identifies expressions of the form `abv a`. -/ @[positivity _] -meta def Mathlib.Meta.Positivity.evalAbv : PositivityExt where eval {_ _α} _zα _pα e := do +meta def Mathlib.Meta.Positivity.evalAbv : PositivityExt where eval {_ _α} _zα pα? e := do + let some pα := pα? | pure .none let (.app f a) ← whnfR e | throwError "not abv ·" let pa' ← mkAppM ``abv_nonneg #[f, a] - pure (.nonnegative pa') + pure (.nonnegative (leα := q(($pα).toLE)) pa') lemma abv_eq_zero {x} : abv x = 0 ↔ x = 0 := abv_eq_zero' diff --git a/Mathlib/Algebra/Order/BigOperators/Expect.lean b/Mathlib/Algebra/Order/BigOperators/Expect.lean index 5f304c8fd31039..ae6205aac28908 100644 --- a/Mathlib/Algebra/Order/BigOperators/Expect.lean +++ b/Mathlib/Algebra/Order/BigOperators/Expect.lean @@ -186,7 +186,8 @@ open scoped BigOperators attribute [local instance] monadLiftOptionMetaM in /-- Positivity extension for `Finset.expect`. -/ @[positivity Finset.expect _ _] -meta def evalFinsetExpect : PositivityExt where eval {u α} zα pα e := do +meta def evalFinsetExpect : PositivityExt where eval {u α} zα pα? e := do + let some pα := pα? | pure .none match e with | ~q(@Finset.expect $ι _ $instα $instmod $s $f) => let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque diff --git a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean index b74541c1b9ff44..21af378c2af5b9 100644 --- a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean +++ b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean @@ -275,7 +275,8 @@ example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.pro because `compareHyp` can't look for assumptions behind binders. -/ @[positivity Finset.prod _ _] -meta def evalFinsetProd : PositivityExt where eval {u α} zα pα e := do +meta def evalFinsetProd : PositivityExt where eval {u α} zα pα? e := do + let some pα := pα? | pure .none match e with | ~q(@Finset.prod $ι _ $instα $s $f) => let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index e33b927f3ef18a..4946b34cda95ad 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -681,47 +681,80 @@ end LinearOrderedSemifield /-- The `positivity` extension which identifies expressions of the form `a / b`, such that `positivity` successfully recognises both `a` and `b`. -/ -@[positivity _ / _] meta def evalDiv : PositivityExt where eval {u α} zα pα e := do +@[positivity _ / _] meta def evalDiv : PositivityExt where eval {u α} zα pα? e := do let .app (.app (f : Q($α → $α → $α)) (a : Q($α))) (b : Q($α)) ← withReducible (whnf e) | throwError "not /" let _e_eq : $e =Q $f $a $b := ⟨⟩ + trace[Tactic.positivity.zeroness] "evalDiv: {a} divided by {b}" let _a ← synthInstanceQ q(Semifield $α) - let _a ← synthInstanceQ q(LinearOrder $α) + let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HDiv.hDiv) + let some _ := pα? | + match ← core zα pα? a, ← core zα pα? b with + | .nonzero pa, .nonzero pb => + let _a ← synthInstanceQ q(GroupWithZero $α) + assumeInstancesCommute + pure (.nonzero q(div_ne_zero $pa $pb)) + | _, _ => pure .none + let lα ← synthInstanceQ q(LinearOrder $α) let _a ← synthInstanceQ q(IsStrictOrderedRing $α) assumeInstancesCommute - let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HDiv.hDiv) - let ra ← core zα pα a; let rb ← core zα pα b + let ra ← core zα pα? a; let rb ← core zα pα? b match ra, rb with - | .positive pa, .positive pb => pure (.positive q(div_pos $pa $pb)) - | .positive pa, .nonnegative pb => pure (.nonnegative q(div_nonneg_of_pos_of_nonneg $pa $pb)) - | .nonnegative pa, .positive pb => pure (.nonnegative q(div_nonneg_of_nonneg_of_pos $pa $pb)) - | .nonnegative pa, .nonnegative pb => pure (.nonnegative q(div_nonneg $pa $pb)) - | .positive pa, .nonzero pb => pure (.nonzero q(div_ne_zero_of_pos_of_ne_zero $pa $pb)) - | .nonzero pa, .positive pb => pure (.nonzero q(div_ne_zero_of_ne_zero_of_pos $pa $pb)) + | .positive (ltα := ltα) pa, .positive pb => + haveI' : $ltα =Q ($lα).toLT := ⟨⟩ + assumeInstancesCommute + pure (.positive q(div_pos $pa $pb)) + | .positive pa, .nonnegative pb => + assumeInstancesCommute + pure (.nonnegative q(div_nonneg_of_pos_of_nonneg $pa $pb)) + | .nonnegative pa, .positive pb => + assumeInstancesCommute + pure (.nonnegative q(div_nonneg_of_nonneg_of_pos $pa $pb)) + | .nonnegative (leα := leα) pa, .nonnegative pb => + haveI' : $leα =Q ($lα).toLE := ⟨⟩ + assumeInstancesCommute + pure (.nonnegative q(div_nonneg $pa $pb)) + | .positive pa, .nonzero pb => + assumeInstancesCommute + pure (.nonzero q(div_ne_zero_of_pos_of_ne_zero $pa $pb)) + | .nonzero pa, .positive pb => + assumeInstancesCommute + pure (.nonzero q(div_ne_zero_of_ne_zero_of_pos $pa $pb)) | .nonzero pa, .nonzero pb => pure (.nonzero q(div_ne_zero $pa $pb)) | _, _ => pure .none /-- The `positivity` extension which identifies expressions of the form `a⁻¹`, such that `positivity` successfully recognises `a`. -/ @[positivity _⁻¹] -meta def evalInv : PositivityExt where eval {u α} zα pα e := do +meta def evalInv : PositivityExt where eval {u α} zα pα? e := do let .app (f : Q($α → $α)) (a : Q($α)) ← withReducible (whnf e) | throwError "not ⁻¹" let _e_eq : $e =Q $f $a := ⟨⟩ let _a ← synthInstanceQ q(Semifield $α) + let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(Inv.inv) + let some _ := pα? | + match ← core zα pα? a with + | .nonzero pa => + let _a ← synthInstanceQ q(GroupWithZero $α) + assumeInstancesCommute + pure (.nonzero q(inv_ne_zero $pa)) + | _ => pure .none let _a ← synthInstanceQ q(LinearOrder $α) let _a ← synthInstanceQ q(IsStrictOrderedRing $α) assumeInstancesCommute - let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(Inv.inv) - let ra ← core zα pα a + let ra ← core zα pα? a match ra with - | .positive pa => pure (.positive q(inv_pos_of_pos $pa)) - | .nonnegative pa => pure (.nonnegative q(inv_nonneg_of_nonneg $pa)) + | .positive pa => + assumeInstancesCommute + pure (.positive q(inv_pos_of_pos $pa)) + | .nonnegative pa => + assumeInstancesCommute + pure (.nonnegative q(inv_nonneg_of_nonneg $pa)) | .nonzero pa => pure (.nonzero q(inv_ne_zero $pa)) | .none => pure .none /-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℤ)`. -/ @[positivity _ ^ (0 : ℤ), Pow.pow _ (0 : ℤ)] -meta def evalPowZeroInt : PositivityExt where eval {u α} _zα _pα e := do +meta def evalPowZeroInt : PositivityExt where eval {u α} _zα _pα? e := do let .app (.app _ (a : Q($α))) _ ← withReducible (whnf e) | throwError "not ^" let _a ← synthInstanceQ q(Semifield $α) let _a ← synthInstanceQ q(LinearOrder $α) diff --git a/Mathlib/Algebra/Order/Field/Power.lean b/Mathlib/Algebra/Order/Field/Power.lean index 7f4561420ef2ae..51546b88b82585 100644 --- a/Mathlib/Algebra/Order/Field/Power.lean +++ b/Mathlib/Algebra/Order/Field/Power.lean @@ -123,8 +123,16 @@ open Lean Meta Qq /-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℤ)`, such that `positivity` successfully recognises both `a` and `b`. -/ @[positivity _ ^ (_ : ℤ), Pow.pow _ (_ : ℤ)] -meta def evalZPow : PositivityExt where eval {u α} zα pα e := do +meta def evalZPow : PositivityExt where eval {u α} zα pα? e := do let .app (.app _ (a : Q($α))) (b : Q(ℤ)) ← withReducible (whnf e) | throwError "not ^" + let some pα := pα? | + match ← core zα pα? a with + | .nonzero pa => + let _a ← synthInstanceQ q(GroupWithZero $α) + assumeInstancesCommute + haveI' : $e =Q $a ^ $b := ⟨⟩ + pure (.nonzero q(zpow_ne_zero $b $pa)) + | _ => pure .none let result ← catchNone do let _a ← synthInstanceQ q(Field $α) let _a ← synthInstanceQ q(LinearOrder $α) @@ -148,7 +156,7 @@ meta def evalZPow : PositivityExt where eval {u α} zα pα e := do pure (.nonnegative q(Even.zpow_nonneg (Even.add_self _) $a)) | _ => throwError "not a ^ n where n is a literal or a negated literal" orElse result do - let ra ← core zα pα a + let ra ← core zα pα? a let ofNonneg (pa : Q(0 ≤ $a)) (_oα : Q(Semifield $α)) (_oα : Q(LinearOrder $α)) (_oα : Q(IsStrictOrderedRing $α)) : MetaM (Strictness zα pα e) := do @@ -174,6 +182,7 @@ meta def evalZPow : PositivityExt where eval {u α} zα pα e := do let sα ← synthInstanceQ q(Semifield $α) let oα ← synthInstanceQ q(LinearOrder $α) let iα ← synthInstanceQ q(IsStrictOrderedRing $α) + assumeInstancesCommute orElse (← catchNone (ofNonneg q(le_of_lt $pa) sα oα iα)) (ofNonzero q(ne_of_gt $pa) q(inferInstance)) | .nonnegative pa => diff --git a/Mathlib/Algebra/Order/Module/Algebra.lean b/Mathlib/Algebra/Order/Module/Algebra.lean index aa52d750565212..a412d8cd6d4af7 100644 --- a/Mathlib/Algebra/Order/Module/Algebra.lean +++ b/Mathlib/Algebra/Order/Module/Algebra.lean @@ -73,7 +73,7 @@ open Lean Meta Qq Function @[positivity algebraMap _ _ _] meta def evalAlgebraMap : PositivityExt where eval {u β} _zβ _pβ e := do let ~q(@algebraMap $α _ $instα $instβ $instαβ $a) := e | throwError "not `algebraMap`" - let pα ← synthInstanceQ q(PartialOrder $α) + let pα ← try? <| synthInstanceQ q(PartialOrder $α) match ← core q(inferInstance) pα a with | .positive pa => let _instαSemiring ← synthInstanceQ q(Semiring $α) diff --git a/Mathlib/Tactic/Positivity/Basic.lean b/Mathlib/Tactic/Positivity/Basic.lean index f6cf84b1f0fcae..4bc839429dde39 100644 --- a/Mathlib/Tactic/Positivity/Basic.lean +++ b/Mathlib/Tactic/Positivity/Basic.lean @@ -297,7 +297,7 @@ private theorem pow_zero_ne_zero [Semiring α] [Nontrivial α] (a : α) : a ^ 0 /-- The `positivity` extension which identifies expressions of the form `a ^ (0 : ℕ)`. This extension is run in addition to the general `a ^ b` extension (they are overlapping). -/ @[positivity _ ^ (0 : ℕ)] -meta def evalPowZeroNat : PositivityExt where eval {u α} _zα _pα e := do +meta def evalPowZeroNat : PositivityExt where eval {u α} _zα pα? e := do let .app (.app _ (a : Q($α))) _ ← withReducible (whnf e) | throwError "not ^" let _a ← synthInstanceQ q(Semiring $α) assumeInstancesCommute @@ -310,7 +310,7 @@ meta def evalPowZeroNat : PositivityExt where eval {u α} _zα _pα e := do /-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℕ)`, such that `positivity` successfully recognises both `a` and `b`. -/ @[positivity _ ^ (_ : ℕ)] -meta def evalPow : PositivityExt where eval {u α} zα pα e := do +meta def evalPow : PositivityExt where eval {u α} zα pα? e := do let .app (.app _ (a : Q($α))) (b : Q(ℕ)) ← withReducible (whnf e) | throwError "not ^" let some pα := pα? | do let _a ← synthInstanceQ q(MonoidWithZero $α) @@ -374,7 +374,7 @@ private theorem abs_pos_of_ne_zero {α : Type*} [AddGroup α] [LinearOrder α] /-- The `positivity` extension which identifies expressions of the form `|a|`. -/ @[positivity |_|] -meta def evalAbs : PositivityExt where eval {_u} (α zα pα) (e : Q($α)) := do +meta def evalAbs : PositivityExt where eval {_u} (α zα pα?) (e : Q($α)) := do let ~q(@abs _ (_) (_) $a) := e | throwError "not |·|" let some pα := pα? | pure .none try @@ -420,7 +420,7 @@ meta def evalNatAbs : PositivityExt where eval {u α} _zα _pα e := do /-- Extension for the `positivity` tactic: `Nat.cast` is always non-negative, and positive when its input is. -/ @[positivity Nat.cast _] -meta def evalNatCast : PositivityExt where eval {u α} _zα _pα e := do +meta def evalNatCast : PositivityExt where eval {u α} _zα pα? e := do let ~q(@Nat.cast _ (_) ($a : ℕ)) := e | throwError "not Nat.cast" let zα' : Q(Zero Nat) := q(inferInstance) let (_i1 : Q(AddMonoidWithOne $α)) ← synthInstanceQ q(AddMonoidWithOne $α) @@ -445,7 +445,7 @@ meta def evalNatCast : PositivityExt where eval {u α} _zα _pα e := do /-- Extension for the `positivity` tactic: `Int.cast` is positive (resp. non-negative) if its input is. -/ @[positivity Int.cast _] -meta def evalIntCast : PositivityExt where eval {u α} _zα _pα e := do +meta def evalIntCast : PositivityExt where eval {u α} _zα pα? e := do let ~q(@Int.cast _ (_) ($a : ℤ)) := e | throwError "not Int.cast" let zα' : Q(Zero Int) := q(inferInstance) let pα' : Q(PartialOrder Int) := q(inferInstance) @@ -626,9 +626,6 @@ meta def evalNNRatDen : PositivityExt where eval {u α} _ _ e := do variable {q : ℚ≥0} -set_option trace.Tactic.positivity true -set_option trace.Tactic.positivity.failure true - example (hq : 0 < q) : 0 < q.num := by positivity example (hq : q ≠ 0) : q.num ≠ 0 := by positivity example : 0 < q.den := by positivity @@ -701,7 +698,7 @@ meta def evalNegPart : PositivityExt where eval {u α} _ _ e := do /-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/ @[positivity DFunLike.coe _ _] -meta def evalMap : PositivityExt where eval {_ β} _ _ e := do +meta def evalMap : PositivityExt where eval {_ β} _ pβ? e := do let .app (.app _ f) a ← whnfR e | throwError "not ↑f · where f is of NonnegHomClass" let some pβ := pβ? | throwError "not PartialOrder" diff --git a/Mathlib/Tactic/Positivity/Core.lean b/Mathlib/Tactic/Positivity/Core.lean index a0720a54831fcd..e92c20d3b79714 100644 --- a/Mathlib/Tactic/Positivity/Core.lean +++ b/Mathlib/Tactic/Positivity/Core.lean @@ -218,6 +218,7 @@ def throwNone {m : Type → Type*} {e : Q($α)} [Monad m] [Alternative m] /-- Attempts to prove a `Strictness` result when `e` evaluates to a literal number. -/ def normNumPositivity (pα : Q(PartialOrder $α)) (e : Q($α)) : MetaM (Strictness zα pα e) := catchNone do + trace[Tactic.positivity] "Is {e} rawNatLit? : {e.isRawNatLit}" match ← NormNum.derive e with | .isBool .. => failure | .isNat _ lit p => @@ -441,12 +442,15 @@ def core (e : Q($α)) : MetaM (Strictness zα pα? e) := do try result ← orElse result <| ext.eval zα pα? e catch err => - trace[Tactic.positivity] "{e} failed: {err.toMessageData}" + trace[Tactic.positivity] "{e} ext failed: {err.toMessageData}" trace[Tactic.positivity] "current result from ext: {result.toString}" -- ?? match pα? with | some pα => + trace[Tactic.positivity] "{α} has some {pα}" result ← orElse result <| normNumPositivity zα pα e + trace[Tactic.positivity] "current result from normNum: {result.toString}" result ← orElse result <| positivityCanon zα pα e + trace[Tactic.positivity] "current result from canonicity: {result.toString}" if let .positive _ := result then trace[Tactic.positivity] "{e} => {result.toString}" return result @@ -456,6 +460,7 @@ def core (e : Q($α)) : MetaM (Strictness zα pα? e) := do trace[Tactic.positivity] "{e} => {result.toString}" throwNone (pure result) | .none => + trace[Tactic.positivity] "{α} has no PartialOrder" if let .nonzero _ := result then trace[Tactic.positivity] "{e} => {result.toString}" return result diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean index c05f7877454562..e85b970b2d334e 100644 --- a/Mathlib/Tactic/Positivity/Finset.lean +++ b/Mathlib/Tactic/Positivity/Finset.lean @@ -69,12 +69,13 @@ example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.sum because `compareHyp` can't look for assumptions behind binders. -/ @[positivity Finset.sum _ _] -meta def evalFinsetSum : PositivityExt where eval {u α} zα pα e := do +meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e := do match e with | ~q(@Finset.sum $ι _ $instα $s $f) => let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque have body : Q($α) := .betaRev f #[i] - let rbody ← core zα pα body + let rbody ← core zα pα? body + let some pα := pα? | pure .none -- TODO: the case without PartialOrder let p_pos : Option Q(0 < $e) := ← (do let .positive pbody := rbody | pure none -- Fail if the body is not provably positive let some ps ← proveFinsetNonempty s | pure none diff --git a/Mathlib/Tactic/Positivity/test_Basic.lean b/Mathlib/Tactic/Positivity/test_Basic.lean index 83d4eaa7133d1a..0904d558dd7b18 100644 --- a/Mathlib/Tactic/Positivity/test_Basic.lean +++ b/Mathlib/Tactic/Positivity/test_Basic.lean @@ -1,4 +1,5 @@ -import Mathlib.Tactic.Positivity.Basic +import Mathlib.Tactic.Positivity +import Mathlib.Algebra.Order.Field.Basic /-! # Tests for the `positivity` tactic @@ -7,18 +8,24 @@ This tactic proves goals of the form `0 ≤ a` and `0 < a`. set_option autoImplicit true set_option trace.Tactic.positivity true set_option trace.Tactic.positivity.failure true +set_option trace.Tactic.norm_num true open Function Nat variable {ι α β E : Type*} /- ## Numeric goals -/ +#norm_num 3 example : 0 ≤ 0 := by positivity example : 0 ≤ 3 := by positivity -example : 0 < 3 := by positivity +example : 0 < 3 := by norm_num + +example : 0 < (3 : ℤ) := by positivity + +example : 0 < nat_lit 3 := by positivity -- example : (0 : EReal) < 2 := by positivity -- example : 0 < (2 : EReal) := by positivity -- example : (0 : EReal) < 2 := by positivity @@ -99,6 +106,9 @@ section variable [Field α] [LinearOrder α] [IsStrictOrderedRing α] +example : (1/4 : ℚ) > 0 := by norm_num +example : (4 : ℚ) > 0 := by positivity +example : (1/4 : ℚ) > 0 := by positivity example : (1/4 - 2/3 : ℚ) ≠ 0 := by positivity example : (1/4 - 2/3 : α) ≠ 0 := by positivity From 9e36ffa959b41e911aa60c9f2870ab0dcb94bd86 Mon Sep 17 00:00:00 2001 From: Pan Lin <58059503+HugLycan@users.noreply.github.com> Date: Mon, 16 Feb 2026 10:03:30 +0100 Subject: [PATCH 4/8] positivity extension compatibility --- Mathlib/Algebra/Order/Floor/Extended.lean | 4 +- Mathlib/Algebra/Order/Floor/Ring.lean | 12 +- Mathlib/Algebra/Order/Module/Field.lean | 15 +-- Mathlib/Analysis/Complex/Order.lean | 25 +++-- .../Analysis/SpecialFunctions/Bernstein.lean | 5 +- .../SpecialFunctions/Gamma/Basic.lean | 2 +- .../Analysis/SpecialFunctions/Pow/NNReal.lean | 30 +++-- .../Analysis/SpecialFunctions/Pow/Real.lean | 9 +- .../Trigonometric/Arctan.lean | 26 +++-- .../SpecialFunctions/Trigonometric/Deriv.lean | 13 ++- .../Combinatorics/Enumerative/DyckWord.lean | 13 ++- .../SimpleGraph/Triangle/Removal.lean | 2 +- Mathlib/Data/ENNReal/Basic.lean | 11 +- Mathlib/Data/ENNReal/Real.lean | 9 +- Mathlib/Data/EReal/Basic.lean | 43 ++++--- Mathlib/Data/EReal/Inv.lean | 10 +- Mathlib/Data/EReal/Operations.lean | 42 +++++-- Mathlib/Data/NNReal/Defs.lean | 21 ++-- Mathlib/Data/Nat/Totient.lean | 5 +- Mathlib/Data/Rat/Cast/Order.lean | 8 +- Mathlib/Data/Real/Sqrt.lean | 20 ++-- .../MeasureTheory/Integral/Bochner/Basic.lean | 4 +- Mathlib/MeasureTheory/Measure/Real.lean | 5 +- .../NumberTheory/ArithmeticFunction/Misc.lean | 9 +- .../NumberTheory/ArithmeticFunction/Zeta.lean | 9 +- Mathlib/NumberTheory/LucasLehmer.lean | 11 +- Mathlib/Tactic/Positivity/Basic.lean | 14 +-- .../Topology/Algebra/InfiniteSum/Order.lean | 3 +- POS_EXT_REVIEW.md | 105 ++++++++++++++++++ 29 files changed, 340 insertions(+), 145 deletions(-) create mode 100644 POS_EXT_REVIEW.md diff --git a/Mathlib/Algebra/Order/Floor/Extended.lean b/Mathlib/Algebra/Order/Floor/Extended.lean index 4847d1a1544737..a808c9c6ae003e 100644 --- a/Mathlib/Algebra/Order/Floor/Extended.lean +++ b/Mathlib/Algebra/Order/Floor/Extended.lean @@ -223,11 +223,11 @@ private alias ⟨_, natCeil_pos⟩ := ENat.ceil_pos /-- Extension for the `positivity` tactic: `ENat.ceil` is positive if its input is. -/ @[positivity ⌈_⌉ₑ] -meta def evalENatCeil : PositivityExt where eval {u α} _zα _pα e := do +meta def evalENatCeil : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(ℕ∞), ~q(ENat.ceil $r) => assertInstancesCommute - match ← core q(inferInstance) q(inferInstance) r with + match ← core q(inferInstance) (some q(inferInstance)) r with | .positive pr => assertInstancesCommute pure (.positive q(natCeil_pos $pr)) diff --git a/Mathlib/Algebra/Order/Floor/Ring.lean b/Mathlib/Algebra/Order/Floor/Ring.lean index 3d8f6eaa007b22..71de74dd516eaf 100644 --- a/Mathlib/Algebra/Order/Floor/Ring.lean +++ b/Mathlib/Algebra/Order/Floor/Ring.lean @@ -50,10 +50,10 @@ private theorem int_floor_nonneg_of_pos [Ring α] [LinearOrder α] [FloorRing α /-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is. -/ @[positivity ⌊_⌋] -meta def evalIntFloor : PositivityExt where eval {u α} _zα _pα e := do +meta def evalIntFloor : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(ℤ), ~q(@Int.floor $α' $ir $io $j $a) => - match ← core q(inferInstance) q(inferInstance) a with + match ← core q(inferInstance) (some q(inferInstance)) a with | .positive pa => assertInstancesCommute pure (.nonnegative q(int_floor_nonneg_of_pos (α := $α') $pa)) @@ -69,13 +69,13 @@ private theorem nat_ceil_pos [Semiring α] [LinearOrder α] [FloorSemiring α] { /-- Extension for the `positivity` tactic: `Nat.ceil` is positive if its input is. -/ @[positivity ⌈_⌉₊] -meta def evalNatCeil : PositivityExt where eval {u α} _zα _pα e := do +meta def evalNatCeil : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(ℕ), ~q(@Nat.ceil $α' $ir $io $j $a) => let _i ← synthInstanceQ q(LinearOrder $α') let _i ← synthInstanceQ q(IsStrictOrderedRing $α') assertInstancesCommute - match ← core q(inferInstance) q(inferInstance) a with + match ← core q(inferInstance) (some q(inferInstance)) a with | .positive pa => assertInstancesCommute pure (.positive q(nat_ceil_pos (α := $α') $pa)) @@ -87,10 +87,10 @@ private theorem int_ceil_pos [Ring α] [LinearOrder α] [FloorRing α] {a : α} /-- Extension for the `positivity` tactic: `Int.ceil` is positive/nonnegative if its input is. -/ @[positivity ⌈_⌉] -meta def evalIntCeil : PositivityExt where eval {u α} _zα _pα e := do +meta def evalIntCeil : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(ℤ), ~q(@Int.ceil $α' $ir $io $j $a) => - match ← core q(inferInstance) q(inferInstance) a with + match ← core q(inferInstance) (some q(inferInstance)) a with | .positive pa => assertInstancesCommute pure (.positive q(int_ceil_pos (α := $α') $pa)) diff --git a/Mathlib/Algebra/Order/Module/Field.lean b/Mathlib/Algebra/Order/Module/Field.lean index baff7037ffb590..3989c70b08d165 100644 --- a/Mathlib/Algebra/Order/Module/Field.lean +++ b/Mathlib/Algebra/Order/Module/Field.lean @@ -101,7 +101,8 @@ end NoZeroSMulDivisors /-- Positivity extension for scalar multiplication. -/ @[positivity HSMul.hSMul _ _] -meta def evalSMul : PositivityExt where eval {_u α} zα pα (e : Q($α)) := do +meta def evalSMul : PositivityExt where eval {_u α} zα pα? (e : Q($α)) := do + let some pα := pα? | pure .none let .app (.app (.app (.app (.app (.app (.const ``HSMul.hSMul [u1, _, _]) (β : Q(Type u1))) _) _) _) (a : Q($β))) (b : Q($α)) ← whnfR e | throwError "failed to match hSMul" @@ -109,20 +110,20 @@ meta def evalSMul : PositivityExt where eval {_u α} zα pα (e : Q($α)) := do let pM : Q(PartialOrder $β) ← synthInstanceQ q(PartialOrder $β) -- Using `q()` here would be impractical, as we would have to manually `synthInstanceQ` all the -- required typeclasses. Ideally we could tell `q()` to do this automatically. - match ← core zM pM a, ← core zα pα b with + match ← core zM pM a, ← core zα pα? b with | .positive pa, .positive pb => try { let _hαβ : Q(SMul $β $α) ← synthInstanceQ q(SMul $β $α) let _hαβ : Q(PosSMulStrictMono $β $α) ← synthInstanceQ q(PosSMulStrictMono $β $α) - pure (.positive (← mkAppM ``smul_pos #[pa, pb])) + pure (.positive (ltα := q(($pα).toLT)) (← mkAppM ``smul_pos #[pa, pb])) } catch _ => - pure (.nonnegative (← mkAppM ``smul_nonneg_of_pos_of_pos #[pa, pb])) + pure (.nonnegative (leα := q(($pα).toLE)) (← mkAppM ``smul_nonneg_of_pos_of_pos #[pa, pb])) | .positive pa, .nonnegative pb => - pure (.nonnegative (← mkAppM ``smul_nonneg_of_pos_of_nonneg #[pa, pb])) + pure (.nonnegative (leα := q(($pα).toLE)) (← mkAppM ``smul_nonneg_of_pos_of_nonneg #[pa, pb])) | .nonnegative pa, .positive pb => - pure (.nonnegative (← mkAppM ``smul_nonneg_of_nonneg_of_pos #[pa, pb])) + pure (.nonnegative (leα := q(($pα).toLE)) (← mkAppM ``smul_nonneg_of_nonneg_of_pos #[pa, pb])) | .nonnegative pa, .nonnegative pb => - pure (.nonnegative (← mkAppM ``smul_nonneg #[pa, pb])) + pure (.nonnegative (leα := q(($pα).toLE)) (← mkAppM ``smul_nonneg #[pa, pb])) | .positive pa, .nonzero pb => pure (.nonzero (← mkAppM ``smul_ne_zero_of_pos_of_ne_zero #[pa, pb])) | .nonzero pa, .positive pb => diff --git a/Mathlib/Analysis/Complex/Order.lean b/Mathlib/Analysis/Complex/Order.lean index 4d5052b89efb08..ad286a2b803406 100644 --- a/Mathlib/Analysis/Complex/Order.lean +++ b/Mathlib/Analysis/Complex/Order.lean @@ -145,17 +145,26 @@ meta def evalComplexOfReal : PositivityExt where eval {u α} _ _ e := do -- TODO: Can we avoid duplicating the code? match u, α, e with | 0, ~q(ℂ), ~q(Complex.ofReal $a) => - assumeInstancesCommute - match ← core q(inferInstance) q(inferInstance) a with - | .positive pa => return .positive q(ofReal_pos $pa) - | .nonnegative pa => return .nonnegative q(ofReal_nonneg $pa) - | .nonzero pa => return .nonzero q(ofReal_ne_zero_of_ne_zero $pa) + match ← core q(inferInstance) (some q(inferInstance)) a with + | .positive pa => + assumeInstancesCommute + return .positive q(ofReal_pos $pa) + | .nonnegative pa => + assumeInstancesCommute + return .nonnegative q(ofReal_nonneg $pa) + | .nonzero pa => + assumeInstancesCommute + return .nonzero q(ofReal_ne_zero_of_ne_zero $pa) | _ => return .none | 0, ~q(ℂ), ~q(Complex.ofReal $a) => assumeInstancesCommute - match ← core q(inferInstance) q(inferInstance) a with - | .positive pa => return .positive q(ofReal_pos $pa) - | .nonnegative pa => return .nonnegative q(ofReal_nonneg $pa) + match ← core q(inferInstance) (some q(inferInstance)) a with + | .positive pa => + assumeInstancesCommute + return .positive q(ofReal_pos $pa) + | .nonnegative pa => + assumeInstancesCommute + return .nonnegative q(ofReal_nonneg $pa) | .nonzero pa => return .nonzero q(ofReal_ne_zero_of_ne_zero $pa) | _ => return .none | _, _ => throwError "not Complex.ofReal" diff --git a/Mathlib/Analysis/SpecialFunctions/Bernstein.lean b/Mathlib/Analysis/SpecialFunctions/Bernstein.lean index 54784039bfc4f9..08d7514bd0286b 100644 --- a/Mathlib/Analysis/SpecialFunctions/Bernstein.lean +++ b/Mathlib/Analysis/SpecialFunctions/Bernstein.lean @@ -80,10 +80,11 @@ open Lean Meta Qq Function /-- Extension of the `positivity` tactic for Bernstein polynomials: they are always non-negative. -/ @[positivity DFunLike.coe (bernstein _ _) _] -meta def evalBernstein : PositivityExt where eval {_ _} _zα _pα e := do +meta def evalBernstein : PositivityExt where eval {_ _} _zα pα? e := do + let some pα := pα? | pure .none let .app (.app _coe (.app (.app _ n) ν)) x ← whnfR e | throwError "not bernstein polynomial" let p ← mkAppOptM ``bernstein_nonneg #[n, ν, x] - pure (.nonnegative p) + pure (.nonnegative (leα := q(($pα).toLE)) p) end Mathlib.Meta.Positivity diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean index 87688e702bf5db..9446cee7e61d9b 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean @@ -489,7 +489,7 @@ open Lean.Meta Qq Mathlib.Meta.Positivity in meta def _root_.Mathlib.Meta.Positivity.evalGamma : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(ℝ), ~q(Gamma $a) => - match ← core q(inferInstance) q(inferInstance) a with + match ← core q(inferInstance) (some q(inferInstance)) a with | .positive pa => assertInstancesCommute pure (.positive q(Gamma_pos_of_pos $pa)) diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean index 2660a031b15423..256b5b97242245 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean @@ -1088,12 +1088,14 @@ meta def evalNNRealRpow : PositivityExt where eval {u α} _ _ e := do assertInstancesCommute pure (.positive q(NNReal.rpow_zero_pos $a)) | 0, ~q(ℝ≥0), ~q($a ^ ($b : ℝ)) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with | .positive pa => - pure (.positive q(NNReal.rpow_pos $pa)) - | _ => pure (.nonnegative q(zero_le $e)) + assertInstancesCommute + pure (.positive q(NNReal.rpow_pos $pa)) + | _ => + assertInstancesCommute + pure (.nonnegative q(zero_le $e)) | _, _, _ => throwError "not NNReal.rpow" private meta def isFiniteM? (x : Q(ℝ≥0∞)) : MetaM (Option Q($x ≠ (⊤ : ℝ≥0∞))) := do @@ -1116,18 +1118,22 @@ meta def evalENNRealRpow : PositivityExt where eval {u α} _ _ e := do assertInstancesCommute pure (.positive q(ENNReal.rpow_zero_pos $a)) | 0, ~q(ℝ≥0∞), ~q($a ^ ($b : ℝ)) => - let ra ← core q(inferInstance) q(inferInstance) a - let rb ← catchNone <| core q(inferInstance) q(inferInstance) b - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a + let rb ← catchNone <| core q(inferInstance) (some q(inferInstance)) b match ra, rb with | .positive pa, .positive pb => - pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa <| le_of_lt $pb)) + assertInstancesCommute + pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa <| le_of_lt $pb)) | .positive pa, .nonnegative pb => - pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa $pb)) + assertInstancesCommute + pure (.positive q(ENNReal.rpow_pos_of_nonneg $pa $pb)) | .positive pa, _ => - let some ha ← isFiniteM? a | pure <| .nonnegative q(zero_le $e) - pure <| .positive q(ENNReal.rpow_pos $pa $ha) - | _, _ => pure <| .nonnegative q(zero_le $e) + assertInstancesCommute + let some ha ← isFiniteM? a | pure <| .nonnegative q(zero_le $e) + pure <| .positive q(ENNReal.rpow_pos $pa $ha) + | _, _ => + assertInstancesCommute + pure <| .nonnegative q(zero_le $e) | _, _, _ => throwError "not ENNReal.rpow" end Mathlib.Meta.Positivity diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean index bfe641a6044bc1..e8eb2728a68320 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Real.lean @@ -381,13 +381,14 @@ the base is nonnegative and positive when the base is positive. -/ meta def evalRpow : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(ℝ), ~q($a ^ ($b : ℝ)) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with | .positive pa => - pure (.positive q(Real.rpow_pos_of_pos $pa $b)) + assertInstancesCommute + pure (.positive q(Real.rpow_pos_of_pos $pa $b)) | .nonnegative pa => - pure (.nonnegative q(Real.rpow_nonneg $pa $b)) + assertInstancesCommute + pure (.nonnegative q(Real.rpow_nonneg $pa $b)) | _ => pure .none | _, _, _ => throwError "not Real.rpow" diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean index 439d49cf2f997e..8eec06cfa2f454 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean @@ -393,11 +393,16 @@ meta def evalRealArctan : PositivityExt where eval {u α} z p e := do match u, α, e with | 0, ~q(ℝ), ~q(Real.arctan $a) => let ra ← core z p a - assumeInstancesCommute match ra with - | .positive pa => return .positive q(Real.arctan_pos.mpr $pa) - | .nonnegative na => return .nonnegative q(Real.arctan_nonneg.mpr $na) - | .nonzero na => return .nonzero q(mt Real.arctan_eq_zero_iff.mp $na) + | .positive pa => + assumeInstancesCommute + return .positive q(Real.arctan_pos.mpr $pa) + | .nonnegative na => + assumeInstancesCommute + return .nonnegative q(Real.arctan_nonneg.mpr $na) + | .nonzero na => + assumeInstancesCommute + return .nonzero q(mt Real.arctan_eq_zero_iff.mp $na) | .none => return .none | _ => throwError "not Real.arctan" @@ -415,11 +420,16 @@ meta def evalRealCosArctan : PositivityExt where eval {u α} _ _ e := do meta def evalRealSinArctan : PositivityExt where eval {u α} z p e := do match u, α, e with | 0, ~q(ℝ), ~q(Real.sin (Real.arctan $a)) => - assumeInstancesCommute match ← core z p a with - | .positive pa => return .positive q(Real.sin_arctan_pos.mpr $pa) - | .nonnegative na => return .nonnegative q(Real.sin_arctan_nonneg.mpr $na) - | .nonzero na => return .nonzero q(mt Real.sin_arctan_eq_zero.mp $na) + | .positive pa => + assumeInstancesCommute + return .positive q(Real.sin_arctan_pos.mpr $pa) + | .nonnegative na => + assumeInstancesCommute + return .nonnegative q(Real.sin_arctan_nonneg.mpr $na) + | .nonzero na => + assumeInstancesCommute + return .nonzero q(mt Real.sin_arctan_eq_zero.mp $na) | .none => return .none | _ => throwError "not Real.sin (Real.arctan _)" diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean index 2cbb74253eb641..f7efb5c68cd941 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean @@ -1472,11 +1472,16 @@ meta def evalSinh : PositivityExt where eval {u α} _ _ e := do let pα : Q(PartialOrder ℝ) := q(inferInstance) match u, α, e with | 0, ~q(ℝ), ~q(Real.sinh $a) => - assumeInstancesCommute match ← core zα pα a with - | .positive pa => return .positive q(sinh_pos_of_pos $pa) - | .nonnegative pa => return .nonnegative q(sinh_nonneg_of_nonneg $pa) - | .nonzero pa => return .nonzero q(sinh_ne_zero_of_ne_zero $pa) + | .positive pa => + assumeInstancesCommute + return .positive q(sinh_pos_of_pos $pa) + | .nonnegative pa => + assumeInstancesCommute + return .nonnegative q(sinh_nonneg_of_nonneg $pa) + | .nonzero pa => + assumeInstancesCommute + return .nonzero q(sinh_ne_zero_of_ne_zero $pa) | _ => return .none | _, _, _ => throwError "not Real.sinh" diff --git a/Mathlib/Combinatorics/Enumerative/DyckWord.lean b/Mathlib/Combinatorics/Enumerative/DyckWord.lean index 03f018d0f146c1..eebe1f05c48919 100644 --- a/Mathlib/Combinatorics/Enumerative/DyckWord.lean +++ b/Mathlib/Combinatorics/Enumerative/DyckWord.lean @@ -568,14 +568,17 @@ open Lean Meta Qq /-- Extension for the `positivity` tactic: `p.firstReturn` is positive if `p` is nonzero. -/ @[positivity DyckWord.firstReturn _] -meta def evalDyckWordFirstReturn : PositivityExt where eval {u α} _zα _pα e := do +meta def evalDyckWordFirstReturn : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(ℕ), ~q(DyckWord.firstReturn $a) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with - | .positive pa => pure (.positive q(DyckWord.firstReturn_pos ($pa).ne')) - | .nonzero pa => pure (.positive q(DyckWord.firstReturn_pos $pa)) + | .positive pa => + assertInstancesCommute + pure (.positive q(DyckWord.firstReturn_pos ($pa).ne')) + | .nonzero pa => + assertInstancesCommute + pure (.positive q(DyckWord.firstReturn_pos $pa)) | _ => pure .none | _, _, _ => throwError "not DyckWord.firstReturn" diff --git a/Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean b/Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean index 21ae1cf9a43906..6c8a5014d023cb 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean @@ -179,7 +179,7 @@ This exploits the positivity of the junk value of `triangleRemovalBound ε` for meta def evalTriangleRemovalBound : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(ℝ), ~q(triangleRemovalBound $ε) => - let .positive hε ← core q(inferInstance) q(inferInstance) ε | failure + let .positive hε ← core q(inferInstance) (some q(inferInstance)) ε | failure assertInstancesCommute pure (.positive q(triangleRemovalBound_pos $hε)) | _, _, _ => throwError "failed to match on Int.ceil application" diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean index bfab60834b4d7a..b090b824fb94de 100644 --- a/Mathlib/Data/ENNReal/Basic.lean +++ b/Mathlib/Data/ENNReal/Basic.lean @@ -731,7 +731,7 @@ open Lean Meta Qq /-- Extension for the `positivity` tactic: `ENNReal.toReal`. -/ @[positivity ENNReal.toReal _] -meta def evalENNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do +meta def evalENNRealtoReal : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(ℝ), ~q(ENNReal.toReal $a) => assertInstancesCommute @@ -740,13 +740,14 @@ meta def evalENNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do /-- Extension for the `positivity` tactic: `ENNReal.ofNNReal`. -/ @[positivity ENNReal.ofNNReal _] -meta def evalENNRealOfNNReal : PositivityExt where eval {u α} _zα _pα e := do +meta def evalENNRealOfNNReal : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(ℝ≥0∞), ~q(ENNReal.ofNNReal $a) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with - | .positive pa => pure <| .positive q(ENNReal.coe_pos.mpr $pa) + | .positive pa => + assertInstancesCommute + pure <| .positive q(ENNReal.coe_pos.mpr $pa) | _ => pure .none | _, _, _ => throwError "not ENNReal.ofNNReal" diff --git a/Mathlib/Data/ENNReal/Real.lean b/Mathlib/Data/ENNReal/Real.lean index 2be95128e38f8c..f647159cb91dbb 100644 --- a/Mathlib/Data/ENNReal/Real.lean +++ b/Mathlib/Data/ENNReal/Real.lean @@ -395,13 +395,14 @@ open Lean Meta Qq /-- Extension for the `positivity` tactic: `ENNReal.ofReal`. -/ @[positivity ENNReal.ofReal _] -meta def evalENNRealOfReal : PositivityExt where eval {u α} _zα _pα e := do +meta def evalENNRealOfReal : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(ℝ≥0∞), ~q(ENNReal.ofReal $a) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with - | .positive pa => pure (.positive q(Iff.mpr (@ENNReal.ofReal_pos $a) $pa)) + | .positive pa => + assertInstancesCommute + pure (.positive q(Iff.mpr (@ENNReal.ofReal_pos $a) $pa)) | _ => pure .none | _, _, _ => throwError "not ENNReal.ofReal" end Mathlib.Meta.Positivity diff --git a/Mathlib/Data/EReal/Basic.lean b/Mathlib/Data/EReal/Basic.lean index 33015e46a16131..2ccab27da45e29 100644 --- a/Mathlib/Data/EReal/Basic.lean +++ b/Mathlib/Data/EReal/Basic.lean @@ -856,12 +856,17 @@ open Lean Meta Qq Function meta def evalRealToEReal : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(EReal), ~q(Real.toEReal $a) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with - | .positive pa => pure (.positive q(EReal.coe_pos.2 $pa)) - | .nonnegative pa => pure (.nonnegative q(EReal.coe_nonneg.2 $pa)) - | .nonzero pa => pure (.nonzero q(EReal.coe_ne_zero.2 $pa)) + | .positive pa => + assertInstancesCommute + pure (.positive q(EReal.coe_pos.2 $pa)) + | .nonnegative pa => + assertInstancesCommute + pure (.nonnegative q(EReal.coe_nonneg.2 $pa)) + | .nonzero pa => + assertInstancesCommute + pure (.nonzero q(EReal.coe_ne_zero.2 $pa)) | _ => pure .none | _, _, _ => throwError "not Real.toEReal" @@ -870,12 +875,17 @@ meta def evalRealToEReal : PositivityExt where eval {u α} _zα _pα e := do meta def evalENNRealToEReal : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(EReal), ~q(ENNReal.toEReal $a) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with - | .positive pa => pure (.positive q(EReal.coe_ennreal_pos.2 $pa)) - | .nonzero pa => pure (.positive q(EReal.coe_ennreal_pos_iff_ne_zero.2 $pa)) - | _ => pure (.nonnegative q(EReal.coe_ennreal_nonneg $a)) + | .positive pa => + assertInstancesCommute + pure (.positive q(EReal.coe_ennreal_pos.2 $pa)) + | .nonzero pa => + assertInstancesCommute + pure (.positive q(EReal.coe_ennreal_pos_iff_ne_zero.2 $pa)) + | _ => + assertInstancesCommute + pure (.nonnegative q(EReal.coe_ennreal_nonneg $a)) | _, _, _ => throwError "not ENNReal.toEReal" /-- Extension for the `positivity` tactic: projection from `EReal` to `ℝ`. @@ -888,7 +898,7 @@ meta def evalERealToReal : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(Real), ~q(EReal.toReal $a) => assertInstancesCommute - match (← core q(inferInstance) q(inferInstance) a).toNonneg with + match (← core q(inferInstance) (some q(inferInstance)) a).toNonneg with | .some pa => pure (.nonnegative q(EReal.toReal_nonneg $pa)) | _ => pure .none | _, _, _ => throwError "not EReal.toReal" @@ -903,10 +913,13 @@ We cannot deduce any corollaries from `x ≠ 0`, since `EReal.toENNReal x = 0` f meta def evalERealToENNReal : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(ENNReal), ~q(EReal.toENNReal $a) => - assertInstancesCommute - match ← core q(inferInstance) q(inferInstance) a with - | .positive pa => pure (.positive q(EReal.toENNReal_pos_iff.2 $pa)) - | _ => pure (.nonnegative q(zero_le $e)) + match ← core q(inferInstance) (some q(inferInstance)) a with + | .positive pa => + assertInstancesCommute + pure (.positive q(EReal.toENNReal_pos_iff.2 $pa)) + | _ => + assertInstancesCommute + pure (.nonnegative q(zero_le $e)) | _, _, _ => throwError "not EReal.toENNReal" end Mathlib.Meta.Positivity diff --git a/Mathlib/Data/EReal/Inv.lean b/Mathlib/Data/EReal/Inv.lean index abd65a27b0a475..b5870e9bbdfda6 100644 --- a/Mathlib/Data/EReal/Inv.lean +++ b/Mathlib/Data/EReal/Inv.lean @@ -551,24 +551,24 @@ open Lean Meta Qq Function /-- Extension for the `positivity` tactic: inverse of an `EReal`. -/ @[positivity (_⁻¹ : EReal)] -meta def evalERealInv : PositivityExt where eval {u α} zα pα e := do +meta def evalERealInv : PositivityExt where eval {u α} _ _ e := do match u, α, e with | 0, ~q(EReal), ~q($a⁻¹) => assertInstancesCommute - match (← core zα pα a).toNonneg with + match (← core q(inferInstance) (some q(inferInstance)) a).toNonneg with | some pa => pure (.nonnegative q(EReal.inv_nonneg_of_nonneg <| $pa)) | none => pure .none | _, _, _ => throwError "not an inverse of an `EReal`" /-- Extension for the `positivity` tactic: ratio of two `EReal`s. -/ @[positivity (_ / _ : EReal)] -meta def evalERealDiv : PositivityExt where eval {u α} zα pα e := do +meta def evalERealDiv : PositivityExt where eval {u α} _ _ e := do match u, α, e with | 0, ~q(EReal), ~q($a / $b) => assertInstancesCommute - match (← core zα pα a).toNonneg with + match (← core q(inferInstance) (some q(inferInstance)) a).toNonneg with | some pa => - match (← core zα pα b).toNonneg with + match (← core q(inferInstance) (some q(inferInstance)) b).toNonneg with | some pb => pure (.nonnegative q(EReal.div_nonneg $pa $pb)) | none => pure .none | _ => pure .none diff --git a/Mathlib/Data/EReal/Operations.lean b/Mathlib/Data/EReal/Operations.lean index 9607fc415ee0a4..eb502083e624c2 100644 --- a/Mathlib/Data/EReal/Operations.lean +++ b/Mathlib/Data/EReal/Operations.lean @@ -838,43 +838,61 @@ open Lean Meta Qq Function /-- Extension for the `positivity` tactic: sum of two `EReal`s. -/ @[positivity (_ + _ : EReal)] -meta def evalERealAdd : PositivityExt where eval {u α} zα pα e := do +meta def evalERealAdd : PositivityExt where eval {u α} zα pα? e := do + let some pα := pα? | pure .none match u, α, e with | 0, ~q(EReal), ~q($a + $b) => - assertInstancesCommute match ← core zα pα a with | .positive pa => match (← core zα pα b).toNonneg with - | some pb => pure (.positive q(EReal.add_pos_of_pos_of_nonneg $pa $pb)) + | some pb => + assertInstancesCommute + pure (.positive q(EReal.add_pos_of_pos_of_nonneg $pa $pb)) | _ => pure .none | .nonnegative pa => match ← core zα pα b with - | .positive pb => pure (.positive q(Right.add_pos_of_nonneg_of_pos $pa $pb)) - | .nonnegative pb => pure (.nonnegative q(add_nonneg $pa $pb)) + | .positive pb => + assertInstancesCommute + pure (.positive q(Right.add_pos_of_nonneg_of_pos $pa $pb)) + | .nonnegative (leα := leα) pb => + haveI' : $leα =Q ($pα).toLE := ⟨⟩ + assertInstancesCommute + pure (.nonnegative q(add_nonneg $pa $pb)) | _ => pure .none | _ => pure .none | _, _, _ => throwError "not a sum of 2 `EReal`s" /-- Extension for the `positivity` tactic: product of two `EReal`s. -/ @[positivity (_ * _ : EReal)] -meta def evalERealMul : PositivityExt where eval {u α} zα pα e := do +meta def evalERealMul : PositivityExt where eval {u α} zα pα? e := do + let some pα := pα? | pure .none match u, α, e with | 0, ~q(EReal), ~q($a * $b) => - assertInstancesCommute match ← core zα pα a with | .positive pa => match ← core zα pα b with - | .positive pb => pure <| .positive q(EReal.mul_pos $pa $pb) - | .nonnegative pb => pure <| .nonnegative q(EReal.mul_nonneg (le_of_lt $pa) $pb) - | .nonzero pb => pure <| .nonzero q(mul_ne_zero (ne_of_gt $pa) $pb) + | .positive (ltα := ltα) pb => + haveI' : $ltα =Q ($pα).toLT := ⟨⟩ + assertInstancesCommute + pure <| .positive q(EReal.mul_pos $pa $pb) + | .nonnegative pb => + assertInstancesCommute + pure <| .nonnegative q(EReal.mul_nonneg (le_of_lt $pa) $pb) + | .nonzero pb => + assertInstancesCommute + pure <| .nonzero q(mul_ne_zero (ne_of_gt $pa) $pb) | _ => pure .none | .nonnegative pa => match (← core zα pα b).toNonneg with - | some pb => pure (.nonnegative q(EReal.mul_nonneg $pa $pb)) + | some pb => + assertInstancesCommute + pure (.nonnegative q(EReal.mul_nonneg $pa $pb)) | none => pure .none | .nonzero pa => match (← core zα pα b).toNonzero with - | some pb => pure (.nonzero q(mul_ne_zero $pa $pb)) + | some pb => + assertInstancesCommute + pure (.nonzero q(mul_ne_zero $pa $pb)) | none => pure .none | _ => pure .none | _, _, _ => throwError "not a product of 2 `EReal`s" diff --git a/Mathlib/Data/NNReal/Defs.lean b/Mathlib/Data/NNReal/Defs.lean index 53b0d7b4fb8c67..842d5dbc680eb0 100644 --- a/Mathlib/Data/NNReal/Defs.lean +++ b/Mathlib/Data/NNReal/Defs.lean @@ -988,14 +988,17 @@ private alias ⟨_, nnreal_coe_pos⟩ := coe_pos /-- Extension for the `positivity` tactic: cast from `ℝ≥0` to `ℝ`. -/ @[positivity NNReal.toReal _] -meta def evalNNRealtoReal : PositivityExt where eval {u α} _zα _pα e := do +meta def evalNNRealtoReal : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(ℝ), ~q(NNReal.toReal $a) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with - | .positive pa => pure (.positive q(nnreal_coe_pos $pa)) - | _ => pure (.nonnegative q(NNReal.coe_nonneg $a)) + | .positive pa => + assertInstancesCommute + pure (.positive q(nnreal_coe_pos $pa)) + | _ => + assertInstancesCommute + pure (.nonnegative q(NNReal.coe_nonneg $a)) | _, _, _ => throwError "not NNReal.toReal" /-- Extension for the `positivity` tactic: `Real.toNNReal. -/ @@ -1004,8 +1007,10 @@ meta def evalRealToNNReal : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(ℝ≥0), ~q(Real.toNNReal $a) => assertInstancesCommute - match (← core q(inferInstance) q(inferInstance) a) with - | .positive pa => pure (.positive q(toNNReal_pos.mpr $pa)) + match (← core q(inferInstance) (some q(inferInstance)) a) with + | .positive pa => + assertInstancesCommute + pure (.positive q(toNNReal_pos.mpr $pa)) | _ => failure | _, _, _ => throwError "not Real.toNNReal" @@ -1017,7 +1022,7 @@ meta def evalRealNNAbs : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(ℝ≥0), ~q(Real.nnabs $a) => assertInstancesCommute - match (← core q(inferInstance) q(inferInstance) a).toNonzero with + match (← core q(inferInstance) (some q(inferInstance)) a).toNonzero with | some pa => pure (.positive q(nnabs_pos_of_pos $pa)) | _ => failure | _, _, _ => throwError "not Real.nnabs" diff --git a/Mathlib/Data/Nat/Totient.lean b/Mathlib/Data/Nat/Totient.lean index be6f4f3314be53..4bbf05ab0e072a 100644 --- a/Mathlib/Data/Nat/Totient.lean +++ b/Mathlib/Data/Nat/Totient.lean @@ -404,9 +404,10 @@ open Lean Meta Qq meta def evalNatTotient : PositivityExt where eval {u α} z p e := do match u, α, e with | 0, ~q(ℕ), ~q(Nat.totient $n) => - assumeInstancesCommute match ← core z p n with - | .positive pa => return .positive q(Nat.totient_pos.mpr $pa) + | .positive pa => + assumeInstancesCommute + return .positive q(Nat.totient_pos.mpr $pa) | _ => failure | _, _, _ => throwError "not Nat.totient" diff --git a/Mathlib/Data/Rat/Cast/Order.lean b/Mathlib/Data/Rat/Cast/Order.lean index 76212c9c0f2df6..dec67caef1138e 100644 --- a/Mathlib/Data/Rat/Cast/Order.lean +++ b/Mathlib/Data/Rat/Cast/Order.lean @@ -260,9 +260,9 @@ open Lean Meta Qq Function /-- Extension for Rat.cast. -/ @[positivity Rat.cast _] -meta def evalRatCast : PositivityExt where eval {u α} _zα _pα e := do +meta def evalRatCast : PositivityExt where eval {u α} _zα _pα? e := do let ~q(@Rat.cast _ (_) ($a : ℚ)) := e | throwError "not Rat.cast" - match ← core q(inferInstance) q(inferInstance) a with + match ← core q(inferInstance) (some q(inferInstance)) a with | .positive pa => let _oα ← synthInstanceQ q(Field $α) let _oα ← synthInstanceQ q(LinearOrder $α) @@ -284,9 +284,9 @@ meta def evalRatCast : PositivityExt where eval {u α} _zα _pα e := do /-- Extension for NNRat.cast. -/ @[positivity NNRat.cast _] -meta def evalNNRatCast : PositivityExt where eval {u α} _zα _pα e := do +meta def evalNNRatCast : PositivityExt where eval {u α} _zα _pα? e := do let ~q(@NNRat.cast _ (_) ($a : ℚ≥0)) := e | throwError "not NNRat.cast" - match ← core q(inferInstance) q(inferInstance) a with + match ← core q(inferInstance) (some q(inferInstance)) a with | .positive pa => let _oα ← synthInstanceQ q(Semifield $α) let _oα ← synthInstanceQ q(LinearOrder $α) diff --git a/Mathlib/Data/Real/Sqrt.lean b/Mathlib/Data/Real/Sqrt.lean index a154d03d7b7ccf..165664cd7856c3 100644 --- a/Mathlib/Data/Real/Sqrt.lean +++ b/Mathlib/Data/Real/Sqrt.lean @@ -294,13 +294,14 @@ open Lean Meta Qq Function /-- Extension for the `positivity` tactic: a square root of a strictly positive nonnegative real is positive. -/ @[positivity NNReal.sqrt _] -meta def evalNNRealSqrt : PositivityExt where eval {u α} _zα _pα e := do +meta def evalNNRealSqrt : PositivityExt where eval {u α} _zα _pα? e := do match u, α, e with | 0, ~q(NNReal), ~q(NNReal.sqrt $a) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with - | .positive pa => pure (.positive q(NNReal.sqrt_pos_of_pos $pa)) + | .positive pa => + assertInstancesCommute + pure (.positive q(NNReal.sqrt_pos_of_pos $pa)) | _ => failure -- this case is dealt with by generic nonnegativity of nnreals | _, _, _ => throwError "not NNReal.sqrt" @@ -310,11 +311,14 @@ its input is. -/ meta def evalSqrt : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(ℝ), ~q(√$a) => - let ra ← catchNone <| core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← catchNone <| core q(inferInstance) (some q(inferInstance)) a match ra with - | .positive pa => pure (.positive q(Real.sqrt_pos_of_pos $pa)) - | _ => pure (.nonnegative q(Real.sqrt_nonneg $a)) + | .positive pa => + assertInstancesCommute + pure (.positive q(Real.sqrt_pos_of_pos $pa)) + | _ => + assertInstancesCommute + pure (.nonnegative q(Real.sqrt_nonneg $a)) | _, _, _ => throwError "not Real.sqrt" end Mathlib.Meta.Positivity diff --git a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean index 992c462bd5ae61..bab8ecd2c2fd4e 100644 --- a/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/Bochner/Basic.lean @@ -1456,12 +1456,12 @@ attribute [local instance] monadLiftOptionMetaM in This extension only proves non-negativity, strict positivity is more delicate for integration and requires more assumptions. -/ @[positivity MeasureTheory.integral _ _] -meta def evalIntegral : PositivityExt where eval {u α} zα pα e := do +meta def evalIntegral : PositivityExt where eval {u α} _ _ e := do match u, α, e with | 0, ~q(ℝ), ~q(@MeasureTheory.integral $i ℝ _ $inst2 _ _ $f) => let i : Q($i) ← mkFreshExprMVarQ q($i) .syntheticOpaque have body : Q(ℝ) := .betaRev f #[i] - let rbody ← core zα pα body + let rbody ← core q(inferInstance) (some q(inferInstance)) body let pbody ← rbody.toNonneg let pr : Q(∀ x, 0 ≤ $f x) ← mkLambdaFVars #[i] pbody assertInstancesCommute diff --git a/Mathlib/MeasureTheory/Measure/Real.lean b/Mathlib/MeasureTheory/Measure/Real.lean index fd3d507eb10b33..99f0340047f9e7 100644 --- a/Mathlib/MeasureTheory/Measure/Real.lean +++ b/Mathlib/MeasureTheory/Measure/Real.lean @@ -450,9 +450,10 @@ open Lean Meta Qq Function /-- Extension for the `positivity` tactic: applications of `μ.real` are nonnegative. -/ @[positivity MeasureTheory.Measure.real _ _] -meta def evalMeasureReal : PositivityExt where eval {_ _} _zα _pα e := do +meta def evalMeasureReal : PositivityExt where eval {_ _} _zα pα? e := do + let some pα := pα? | pure .none let .app (.app _ a) b ← whnfR e | throwError "not measureReal" let p ← mkAppOptM ``MeasureTheory.measureReal_nonneg #[none, none, a, b] - pure (.nonnegative p) + pure (.nonnegative (leα := q(($pα).toLE)) p) end Mathlib.Meta.Positivity diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean b/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean index dda90d5c3c5c49..dd9633f2149ccd 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean @@ -454,10 +454,13 @@ meta def evalArithmeticFunctionSigma : PositivityExt where eval {u α} z p e := match u, α, e with | 0, ~q(ℕ), ~q(ArithmeticFunction.sigma $k $n) => let rn ← core z p n - assumeInstancesCommute match rn with - | .positive pn => return .positive q(Iff.mpr ArithmeticFunction.sigma_pos_iff $pn) - | _ => return .nonnegative q(Nat.zero_le _) + | .positive pn => + assumeInstancesCommute + return .positive q(Iff.mpr ArithmeticFunction.sigma_pos_iff $pn) + | _ => + assumeInstancesCommute + return .nonnegative q(Nat.zero_le _) | _, _, _ => throwError "not ArithmeticFunction.sigma" diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean index a253c162b8e12d..f6ec29428a2bb7 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean @@ -230,10 +230,13 @@ meta def evalArithmeticFunctionZeta : PositivityExt where eval {u α} z p e := d match u, α, e with | 0, ~q(ℕ), ~q(ArithmeticFunction.zeta $n) => let rn ← core z p n - assumeInstancesCommute match rn with - | .positive pn => return .positive q(Iff.mpr ArithmeticFunction.zeta_pos $pn) - | _ => return .nonnegative q(Nat.zero_le _) + | .positive pn => + assumeInstancesCommute + return .positive q(Iff.mpr ArithmeticFunction.zeta_pos $pn) + | _ => + assumeInstancesCommute + return .nonnegative q(Nat.zero_le _) | _, _, _ => throwError "not ArithmeticFunction.zeta" end Mathlib.Meta.Positivity diff --git a/Mathlib/NumberTheory/LucasLehmer.lean b/Mathlib/NumberTheory/LucasLehmer.lean index 4c45259d1ec8e6..aa34a6a1494237 100644 --- a/Mathlib/NumberTheory/LucasLehmer.lean +++ b/Mathlib/NumberTheory/LucasLehmer.lean @@ -85,11 +85,14 @@ alias ⟨_, mersenne_pos_of_pos⟩ := mersenne_pos meta def evalMersenne : PositivityExt where eval {u α} _zα _pα e := do match u, α, e with | 0, ~q(ℕ), ~q(mersenne $a) => - let ra ← core q(inferInstance) q(inferInstance) a - assertInstancesCommute + let ra ← core q(inferInstance) (some q(inferInstance)) a match ra with - | .positive pa => pure (.positive q(mersenne_pos_of_pos $pa)) - | _ => pure (.nonnegative q(Nat.zero_le (mersenne $a))) + | .positive pa => + assertInstancesCommute + pure (.positive q(mersenne_pos_of_pos $pa)) + | _ => + assertInstancesCommute + pure (.nonnegative q(Nat.zero_le (mersenne $a))) | _, _, _ => throwError "not mersenne" end Mathlib.Meta.Positivity diff --git a/Mathlib/Tactic/Positivity/Basic.lean b/Mathlib/Tactic/Positivity/Basic.lean index 4bc839429dde39..319a744655d687 100644 --- a/Mathlib/Tactic/Positivity/Basic.lean +++ b/Mathlib/Tactic/Positivity/Basic.lean @@ -188,7 +188,7 @@ such that `positivity` successfully recognises both `a` and `b`. -/ assumeInstancesCommute let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HAdd.hAdd) let ra ← core zα pα? a; let rb ← core zα pα? b - let some pα := pα? | failure + let some pα := pα? | pure .none match ra, rb with | .positive (ltα := ltα) pa, .positive pb => let _a ← synthInstanceQ q(AddLeftStrictMono $α) @@ -319,11 +319,11 @@ meta def evalPow : PositivityExt where eval {u α} zα pα? e := do haveI' : $e =Q $a ^ $b := ⟨⟩ let .nonzero nza ← core zα .none a | pure .none pure (.nonzero q(pow_ne_zero $b $nza)) - let _a ← synthInstanceQ q(Ring $α) - let _a ← synthInstanceQ q(LinearOrder $α) - let _a ← synthInstanceQ q(IsStrictOrderedRing $α) - assumeInstancesCommute let result ← catchNone do + let _a ← synthInstanceQ q(Ring $α) + let _a ← synthInstanceQ q(LinearOrder $α) + let _a ← synthInstanceQ q(IsStrictOrderedRing $α) + assumeInstancesCommute let .true := b.isAppOfArity ``OfNat.ofNat 3 | throwError "not a ^ n where n is a literal" let some n := (b.getRevArg! 1).rawNatLit? | throwError "not a ^ n where n is a literal" guard (n % 2 = 0) @@ -699,11 +699,11 @@ meta def evalNegPart : PositivityExt where eval {u α} _ _ e := do /-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/ @[positivity DFunLike.coe _ _] meta def evalMap : PositivityExt where eval {_ β} _ pβ? e := do + let some pβ := pβ? | pure .none let .app (.app _ f) a ← whnfR e | throwError "not ↑f · where f is of NonnegHomClass" - let some pβ := pβ? | throwError "not PartialOrder" let pa ← mkAppOptM ``apply_nonneg #[none, none, β, none, none, none, none, f, a] - pure (.nonnegative (leα := pβ) pa) + pure (.nonnegative (leα := q(($pβ).toLE)) pa) end Positivity diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean index 0dd7bd13d2d4c2..ddc2000a517b11 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Order.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Order.lean @@ -369,7 +369,8 @@ attribute [local instance] monadLiftOptionMetaM in This extension only proves non-negativity, strict positivity is more delicate for infinite sums and requires more assumptions. -/ @[positivity tsum _] -meta def evalTsum : PositivityExt where eval {u α} zα pα e := do +meta def evalTsum : PositivityExt where eval {u α} zα pα? e := do + let some pα := pα? | pure .none match e with | ~q(@tsum _ $ι $instCommMonoid $instTopSpace $f $L) => lambdaBoundedTelescope f 1 fun args (body : Q($α)) => do diff --git a/POS_EXT_REVIEW.md b/POS_EXT_REVIEW.md new file mode 100644 index 00000000000000..0dc155610ec9ee --- /dev/null +++ b/POS_EXT_REVIEW.md @@ -0,0 +1,105 @@ +# PositivityExt review list + +- [ ] Mathlib\Combinatorics\Enumerative\DyckWord.lean:571 ? evalDyckWordFirstReturn +- [ ] Mathlib\Combinatorics\SimpleGraph\Triangle\Removal.lean:179 ? evalTriangleRemovalBound +- [ ] Mathlib\Combinatorics\SimpleGraph\Regularity\Bound.lean:240 ? evalInitialBound +- [ ] Mathlib\Combinatorics\SimpleGraph\Regularity\Bound.lean:252 ? evalBound + - [ ] Mathlib\Analysis\SpecialFunctions\Pow\Real.lean:369 ? evalRpowZero + - [ ] Mathlib\Analysis\SpecialFunctions\Pow\Real.lean:379 ? evalRpow +- [ ] Mathlib\Data\Nat\Totient.lean:404 ? evalNatTotient + - [+] Mathlib\Algebra\Order\BigOperators\Ring\Finset.lean:278 ? evalFinsetProd + - [+] Mathlib\Algebra\Order\AbsoluteValue\Basic.lean:413 ? Mathlib.Meta.Positivity.evalAbv +- [+] Mathlib\Tactic\Positivity\Finset.lean:31 ? evalFinsetCard +- [+] Mathlib\Tactic\Positivity\Finset.lean:41 ? evalFintypeCard +- [+] Mathlib\Tactic\Positivity\Finset.lean:53 ? evalFinsetDens +- [+] Mathlib\Tactic\Positivity\Finset.lean:72 ? evalFinsetSum +- [+] Mathlib\Tactic\Positivity\Basic.lean:60 ? evalIte +- [+] Mathlib\Tactic\Positivity\Basic.lean:111 ? evalMin +- [+] Mathlib\Tactic\Positivity\Basic.lean:146 ? evalMax +- [+] Mathlib\Tactic\Positivity\Basic.lean:183 ? evalAdd +- [+] Mathlib\Tactic\Positivity\Basic.lean:215 ? evalMul +- [+] Mathlib\Tactic\Positivity\Basic.lean:269 ? evalIntDiv +- [+] Mathlib\Tactic\Positivity\Basic.lean:300 ? evalPowZeroNat +- [+] Mathlib\Tactic\Positivity\Basic.lean:313 ? evalPow +- [+] Mathlib\Tactic\Positivity\Basic.lean:377 ? evalAbs +- [+] Mathlib\Tactic\Positivity\Basic.lean:401 ? evalNatAbs +- [+] Mathlib\Tactic\Positivity\Basic.lean:423 ? evalNatCast +- [+] Mathlib\Tactic\Positivity\Basic.lean:448 ? evalIntCast +- [+] Mathlib\Tactic\Positivity\Basic.lean:476 ? evalNatSucc +- [+] Mathlib\Tactic\Positivity\Basic.lean:485 ? evalPNatVal +- [+] Mathlib\Tactic\Positivity\Basic.lean:494 ? evalFactorial +- [+] Mathlib\Tactic\Positivity\Basic.lean:503 ? evalAscFactorial +- [+] Mathlib\Tactic\Positivity\Basic.lean:515 ? evalNatGCD +- [+] Mathlib\Tactic\Positivity\Basic.lean:533 ? evalNatLCM +- [+] Mathlib\Tactic\Positivity\Basic.lean:550 ? evalNatSqrt +- [+] Mathlib\Tactic\Positivity\Basic.lean:564 ? evalIntGCD +- [+] Mathlib\Tactic\Positivity\Basic.lean:580 ? evalIntLCM +- [+] Mathlib\Tactic\Positivity\Basic.lean:603 ? evalNNRatNum +- [+] Mathlib\Tactic\Positivity\Basic.lean:620 ? evalNNRatDen +- [+] Mathlib\Tactic\Positivity\Basic.lean:644 ? evalRatNum +- [+] Mathlib\Tactic\Positivity\Basic.lean:663 ? evalRatDen +- [+] Mathlib\Tactic\Positivity\Basic.lean:672 ? evalPosPart +- [+] Mathlib\Tactic\Positivity\Basic.lean:690 ? evalNegPart +- [+] Mathlib\Tactic\Positivity\Basic.lean:701 ? evalMap +- [ ] Mathlib\Data\Nat\Factorial\DoubleFactorial.lean:90 ? evalDoubleFactorial +- [ ] Mathlib\MeasureTheory\Covering\Besicovitch.lean:141 ? evalBesicovitchSatelliteConfigR +- [ ] Mathlib\Data\Real\Sqrt.lean:297 ? evalNNRealSqrt +- [ ] Mathlib\Data\Real\Sqrt.lean:310 ? evalSqrt +- [ ] Mathlib\Data\Rat\Cast\Order.lean:263 ? evalRatCast +- [ ] Mathlib\Data\Rat\Cast\Order.lean:287 ? evalNNRatCast +- [ ] Mathlib\Topology\MetricSpace\Pseudo\Defs.lean:240 ? evalDist + - [ ] Mathlib\Data\ENNReal\Real.lean:398 ? evalENNRealOfReal + - [ ] Mathlib\Data\ENNReal\Basic.lean:734 ? evalENNRealtoReal + - [ ] Mathlib\Data\ENNReal\Basic.lean:743 ? evalENNRealOfNNReal + - [ ] Mathlib\Data\NNReal\Defs.lean:991 ? evalNNRealtoReal + - [ ] Mathlib\Data\NNReal\Defs.lean:1003 ? evalRealToNNReal + - [ ] Mathlib\Data\NNReal\Defs.lean:1016 ? evalRealNNAbs +- [ ] Mathlib\MeasureTheory\Integral\Bochner\Basic.lean:1459 ? evalIntegral + - [ ] Mathlib\MeasureTheory\Measure\Real.lean:453 ? evalMeasureReal +- [ ] Mathlib\Topology\MetricSpace\Bounded.lean:571 ? evalDiam +- [ ] Mathlib\NumberTheory\SelbergSieve.lean:89 ? evalBoundingSieveWeights +- [ ] Mathlib\NumberTheory\ArithmeticFunction.lean:1509 ? evalArithmeticFunctionSigma +- [ ] Mathlib\NumberTheory\ArithmeticFunction.lean:1521 ? evalArithmeticFunctionZeta +- [ ] Mathlib\Data\EReal\Inv.lean:554 ? evalERealInv +- [ ] Mathlib\Data\EReal\Inv.lean:565 ? evalERealDiv + - [ ] Mathlib\Data\EReal\Operations.lean:838 ? evalERealAdd + - [ ] Mathlib\Data\EReal\Operations.lean:857 ? evalERealMul + - [ ] Mathlib\Data\EReal\Basic.lean:856 ? evalRealToEReal + - [ ] Mathlib\Data\EReal\Basic.lean:870 ? evalENNRealToEReal + - [ ] Mathlib\Data\EReal\Basic.lean:887 ? evalERealToReal + - [ ] Mathlib\Data\EReal\Basic.lean:903 ? evalERealToENNReal +- [ ] Mathlib\NumberTheory\LucasLehmer.lean:85 ? evalMersenne +- [ ] Mathlib\Topology\Algebra\InfiniteSum\Order.lean:365 ? evalTsum +- [ ] Mathlib\Algebra\Order\Module\Algebra.lean:74 ? evalAlgebraMap +- [ ] Mathlib\Algebra\Order\Interval\Basic.lean:666 ? evalNonemptyIntervalLength +- [ ] Mathlib\Algebra\Order\Interval\Basic.lean:676 ? evalIntervalLength +- [+] Mathlib\Algebra\Order\Field\Power.lean:126 ? evalZPow +- [-] Mathlib\Algebra\Order\Floor\Ring.lean:53 ? evalIntFloor +- [-] Mathlib\Algebra\Order\Floor\Ring.lean:72 ? evalNatCeil +- [-] Mathlib\Algebra\Order\Floor\Ring.lean:90 ? evalIntCeil + - [+] Mathlib\Algebra\Order\Field\Basic.lean:684 ? evalDiv + - [+] Mathlib\Algebra\Order\Field\Basic.lean:729 ? evalInv + - [+] Mathlib\Algebra\Order\Field\Basic.lean:757 ? evalPowZeroInt +- [-] Mathlib\Algebra\Order\Floor\Extended.lean:226 ? evalENatCeil +- [-] Mathlib\Algebra\Order\BigOperators\Expect.lean:189 ? evalFinsetExpect + - [?] Mathlib\Algebra\Order\Module\Field.lean:104 ? evalSMul +- [-] Mathlib\Geometry\Euclidean\Altitude.lean:189 ? evalHeight +- [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Deriv.lean:1470 ? evalSinh + - [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Basic.lean:179 ? evalRealPi +- [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Arctan.lean:393 ? evalRealArctan +- [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Arctan.lean:407 ? evalRealCosArctan +- [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Arctan.lean:416 ? evalRealSinArctan +- [ ] Mathlib\Analysis\SpecialFunctions\Pow\NNReal.lean:1083 ? evalNNRealRpow +- [ ] Mathlib\Analysis\SpecialFunctions\Pow\NNReal.lean:1111 ? evalENNRealRpow +- [ ] Mathlib\Analysis\SpecialFunctions\Bernstein.lean:83 ? evalBernstein +- [ ] Mathlib\Analysis\Complex\UpperHalfPlane\Basic.lean:126 ? evalUpperHalfPlaneIm +- [ ] Mathlib\Analysis\Complex\UpperHalfPlane\Basic.lean:135 ? evalUpperHalfPlaneCoe +- [ ] Mathlib\Analysis\Complex\Trigonometric.lean:920 ? evalCosh + - [ ] Mathlib\Analysis\Complex\Exponential.lean:681 ? evalExp +- [ ] Mathlib\Analysis\Complex\Order.lean:144 ? evalComplexOfReal +- [ ] Mathlib\Analysis\SpecialFunctions\Log\Basic.lean:547 ? evalLogNatCast +- [ ] Mathlib\Analysis\SpecialFunctions\Log\Basic.lean:556 ? evalLogIntCast +- [ ] Mathlib\Analysis\SpecialFunctions\Log\Basic.lean:565 ? evalLogNatLit +- [ ] Mathlib\Analysis\SpecialFunctions\Gamma\Basic.lean:489 ? _root_.Mathlib.Meta.Positivity.evalGamma +- [ ] Mathlib\Analysis\Normed\Group\Basic.lean:1398 ? evalMulNorm +- [ ] Mathlib\Analysis\Normed\Group\Basic.lean:1420 ? evalAddNorm From af030aff42f7f807a5f02e004fc34b788924388a Mon Sep 17 00:00:00 2001 From: Pan Lin <58059503+HugLycan@users.noreply.github.com> Date: Mon, 16 Feb 2026 10:04:13 +0100 Subject: [PATCH 5/8] delete tmp file --- POS_EXT_REVIEW.md | 105 ---------------------------------------------- 1 file changed, 105 deletions(-) delete mode 100644 POS_EXT_REVIEW.md diff --git a/POS_EXT_REVIEW.md b/POS_EXT_REVIEW.md deleted file mode 100644 index 0dc155610ec9ee..00000000000000 --- a/POS_EXT_REVIEW.md +++ /dev/null @@ -1,105 +0,0 @@ -# PositivityExt review list - -- [ ] Mathlib\Combinatorics\Enumerative\DyckWord.lean:571 ? evalDyckWordFirstReturn -- [ ] Mathlib\Combinatorics\SimpleGraph\Triangle\Removal.lean:179 ? evalTriangleRemovalBound -- [ ] Mathlib\Combinatorics\SimpleGraph\Regularity\Bound.lean:240 ? evalInitialBound -- [ ] Mathlib\Combinatorics\SimpleGraph\Regularity\Bound.lean:252 ? evalBound - - [ ] Mathlib\Analysis\SpecialFunctions\Pow\Real.lean:369 ? evalRpowZero - - [ ] Mathlib\Analysis\SpecialFunctions\Pow\Real.lean:379 ? evalRpow -- [ ] Mathlib\Data\Nat\Totient.lean:404 ? evalNatTotient - - [+] Mathlib\Algebra\Order\BigOperators\Ring\Finset.lean:278 ? evalFinsetProd - - [+] Mathlib\Algebra\Order\AbsoluteValue\Basic.lean:413 ? Mathlib.Meta.Positivity.evalAbv -- [+] Mathlib\Tactic\Positivity\Finset.lean:31 ? evalFinsetCard -- [+] Mathlib\Tactic\Positivity\Finset.lean:41 ? evalFintypeCard -- [+] Mathlib\Tactic\Positivity\Finset.lean:53 ? evalFinsetDens -- [+] Mathlib\Tactic\Positivity\Finset.lean:72 ? evalFinsetSum -- [+] Mathlib\Tactic\Positivity\Basic.lean:60 ? evalIte -- [+] Mathlib\Tactic\Positivity\Basic.lean:111 ? evalMin -- [+] Mathlib\Tactic\Positivity\Basic.lean:146 ? evalMax -- [+] Mathlib\Tactic\Positivity\Basic.lean:183 ? evalAdd -- [+] Mathlib\Tactic\Positivity\Basic.lean:215 ? evalMul -- [+] Mathlib\Tactic\Positivity\Basic.lean:269 ? evalIntDiv -- [+] Mathlib\Tactic\Positivity\Basic.lean:300 ? evalPowZeroNat -- [+] Mathlib\Tactic\Positivity\Basic.lean:313 ? evalPow -- [+] Mathlib\Tactic\Positivity\Basic.lean:377 ? evalAbs -- [+] Mathlib\Tactic\Positivity\Basic.lean:401 ? evalNatAbs -- [+] Mathlib\Tactic\Positivity\Basic.lean:423 ? evalNatCast -- [+] Mathlib\Tactic\Positivity\Basic.lean:448 ? evalIntCast -- [+] Mathlib\Tactic\Positivity\Basic.lean:476 ? evalNatSucc -- [+] Mathlib\Tactic\Positivity\Basic.lean:485 ? evalPNatVal -- [+] Mathlib\Tactic\Positivity\Basic.lean:494 ? evalFactorial -- [+] Mathlib\Tactic\Positivity\Basic.lean:503 ? evalAscFactorial -- [+] Mathlib\Tactic\Positivity\Basic.lean:515 ? evalNatGCD -- [+] Mathlib\Tactic\Positivity\Basic.lean:533 ? evalNatLCM -- [+] Mathlib\Tactic\Positivity\Basic.lean:550 ? evalNatSqrt -- [+] Mathlib\Tactic\Positivity\Basic.lean:564 ? evalIntGCD -- [+] Mathlib\Tactic\Positivity\Basic.lean:580 ? evalIntLCM -- [+] Mathlib\Tactic\Positivity\Basic.lean:603 ? evalNNRatNum -- [+] Mathlib\Tactic\Positivity\Basic.lean:620 ? evalNNRatDen -- [+] Mathlib\Tactic\Positivity\Basic.lean:644 ? evalRatNum -- [+] Mathlib\Tactic\Positivity\Basic.lean:663 ? evalRatDen -- [+] Mathlib\Tactic\Positivity\Basic.lean:672 ? evalPosPart -- [+] Mathlib\Tactic\Positivity\Basic.lean:690 ? evalNegPart -- [+] Mathlib\Tactic\Positivity\Basic.lean:701 ? evalMap -- [ ] Mathlib\Data\Nat\Factorial\DoubleFactorial.lean:90 ? evalDoubleFactorial -- [ ] Mathlib\MeasureTheory\Covering\Besicovitch.lean:141 ? evalBesicovitchSatelliteConfigR -- [ ] Mathlib\Data\Real\Sqrt.lean:297 ? evalNNRealSqrt -- [ ] Mathlib\Data\Real\Sqrt.lean:310 ? evalSqrt -- [ ] Mathlib\Data\Rat\Cast\Order.lean:263 ? evalRatCast -- [ ] Mathlib\Data\Rat\Cast\Order.lean:287 ? evalNNRatCast -- [ ] Mathlib\Topology\MetricSpace\Pseudo\Defs.lean:240 ? evalDist - - [ ] Mathlib\Data\ENNReal\Real.lean:398 ? evalENNRealOfReal - - [ ] Mathlib\Data\ENNReal\Basic.lean:734 ? evalENNRealtoReal - - [ ] Mathlib\Data\ENNReal\Basic.lean:743 ? evalENNRealOfNNReal - - [ ] Mathlib\Data\NNReal\Defs.lean:991 ? evalNNRealtoReal - - [ ] Mathlib\Data\NNReal\Defs.lean:1003 ? evalRealToNNReal - - [ ] Mathlib\Data\NNReal\Defs.lean:1016 ? evalRealNNAbs -- [ ] Mathlib\MeasureTheory\Integral\Bochner\Basic.lean:1459 ? evalIntegral - - [ ] Mathlib\MeasureTheory\Measure\Real.lean:453 ? evalMeasureReal -- [ ] Mathlib\Topology\MetricSpace\Bounded.lean:571 ? evalDiam -- [ ] Mathlib\NumberTheory\SelbergSieve.lean:89 ? evalBoundingSieveWeights -- [ ] Mathlib\NumberTheory\ArithmeticFunction.lean:1509 ? evalArithmeticFunctionSigma -- [ ] Mathlib\NumberTheory\ArithmeticFunction.lean:1521 ? evalArithmeticFunctionZeta -- [ ] Mathlib\Data\EReal\Inv.lean:554 ? evalERealInv -- [ ] Mathlib\Data\EReal\Inv.lean:565 ? evalERealDiv - - [ ] Mathlib\Data\EReal\Operations.lean:838 ? evalERealAdd - - [ ] Mathlib\Data\EReal\Operations.lean:857 ? evalERealMul - - [ ] Mathlib\Data\EReal\Basic.lean:856 ? evalRealToEReal - - [ ] Mathlib\Data\EReal\Basic.lean:870 ? evalENNRealToEReal - - [ ] Mathlib\Data\EReal\Basic.lean:887 ? evalERealToReal - - [ ] Mathlib\Data\EReal\Basic.lean:903 ? evalERealToENNReal -- [ ] Mathlib\NumberTheory\LucasLehmer.lean:85 ? evalMersenne -- [ ] Mathlib\Topology\Algebra\InfiniteSum\Order.lean:365 ? evalTsum -- [ ] Mathlib\Algebra\Order\Module\Algebra.lean:74 ? evalAlgebraMap -- [ ] Mathlib\Algebra\Order\Interval\Basic.lean:666 ? evalNonemptyIntervalLength -- [ ] Mathlib\Algebra\Order\Interval\Basic.lean:676 ? evalIntervalLength -- [+] Mathlib\Algebra\Order\Field\Power.lean:126 ? evalZPow -- [-] Mathlib\Algebra\Order\Floor\Ring.lean:53 ? evalIntFloor -- [-] Mathlib\Algebra\Order\Floor\Ring.lean:72 ? evalNatCeil -- [-] Mathlib\Algebra\Order\Floor\Ring.lean:90 ? evalIntCeil - - [+] Mathlib\Algebra\Order\Field\Basic.lean:684 ? evalDiv - - [+] Mathlib\Algebra\Order\Field\Basic.lean:729 ? evalInv - - [+] Mathlib\Algebra\Order\Field\Basic.lean:757 ? evalPowZeroInt -- [-] Mathlib\Algebra\Order\Floor\Extended.lean:226 ? evalENatCeil -- [-] Mathlib\Algebra\Order\BigOperators\Expect.lean:189 ? evalFinsetExpect - - [?] Mathlib\Algebra\Order\Module\Field.lean:104 ? evalSMul -- [-] Mathlib\Geometry\Euclidean\Altitude.lean:189 ? evalHeight -- [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Deriv.lean:1470 ? evalSinh - - [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Basic.lean:179 ? evalRealPi -- [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Arctan.lean:393 ? evalRealArctan -- [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Arctan.lean:407 ? evalRealCosArctan -- [ ] Mathlib\Analysis\SpecialFunctions\Trigonometric\Arctan.lean:416 ? evalRealSinArctan -- [ ] Mathlib\Analysis\SpecialFunctions\Pow\NNReal.lean:1083 ? evalNNRealRpow -- [ ] Mathlib\Analysis\SpecialFunctions\Pow\NNReal.lean:1111 ? evalENNRealRpow -- [ ] Mathlib\Analysis\SpecialFunctions\Bernstein.lean:83 ? evalBernstein -- [ ] Mathlib\Analysis\Complex\UpperHalfPlane\Basic.lean:126 ? evalUpperHalfPlaneIm -- [ ] Mathlib\Analysis\Complex\UpperHalfPlane\Basic.lean:135 ? evalUpperHalfPlaneCoe -- [ ] Mathlib\Analysis\Complex\Trigonometric.lean:920 ? evalCosh - - [ ] Mathlib\Analysis\Complex\Exponential.lean:681 ? evalExp -- [ ] Mathlib\Analysis\Complex\Order.lean:144 ? evalComplexOfReal -- [ ] Mathlib\Analysis\SpecialFunctions\Log\Basic.lean:547 ? evalLogNatCast -- [ ] Mathlib\Analysis\SpecialFunctions\Log\Basic.lean:556 ? evalLogIntCast -- [ ] Mathlib\Analysis\SpecialFunctions\Log\Basic.lean:565 ? evalLogNatLit -- [ ] Mathlib\Analysis\SpecialFunctions\Gamma\Basic.lean:489 ? _root_.Mathlib.Meta.Positivity.evalGamma -- [ ] Mathlib\Analysis\Normed\Group\Basic.lean:1398 ? evalMulNorm -- [ ] Mathlib\Analysis\Normed\Group\Basic.lean:1420 ? evalAddNorm From 005f0da6a7616d07fb144e89823016595999088a Mon Sep 17 00:00:00 2001 From: Pan Lin <58059503+HugLycan@users.noreply.github.com> Date: Mon, 16 Feb 2026 10:42:20 +0100 Subject: [PATCH 6/8] Delete Mathlib/Tactic/Positivity/test_Basic.lean --- Mathlib/Tactic/Positivity/test_Basic.lean | 255 ---------------------- 1 file changed, 255 deletions(-) delete mode 100644 Mathlib/Tactic/Positivity/test_Basic.lean diff --git a/Mathlib/Tactic/Positivity/test_Basic.lean b/Mathlib/Tactic/Positivity/test_Basic.lean deleted file mode 100644 index 0904d558dd7b18..00000000000000 --- a/Mathlib/Tactic/Positivity/test_Basic.lean +++ /dev/null @@ -1,255 +0,0 @@ -import Mathlib.Tactic.Positivity -import Mathlib.Algebra.Order.Field.Basic - -/-! # Tests for the `positivity` tactic - -This tactic proves goals of the form `0 ≤ a` and `0 < a`. --/ -set_option autoImplicit true -set_option trace.Tactic.positivity true -set_option trace.Tactic.positivity.failure true -set_option trace.Tactic.norm_num true - -open Function Nat - -variable {ι α β E : Type*} - -/- ## Numeric goals -/ -#norm_num 3 - -example : 0 ≤ 0 := by positivity - -example : 0 ≤ 3 := by positivity - -example : 0 < 3 := by norm_num - -example : 0 < (3 : ℤ) := by positivity - -example : 0 < nat_lit 3 := by positivity --- example : (0 : EReal) < 2 := by positivity --- example : 0 < (2 : EReal) := by positivity --- example : (0 : EReal) < 2 := by positivity - --- example : (0 : ℝ≥0∞) ≤ 1 := by positivity --- example : (0 : ℝ≥0∞) ≤ 0 := by positivity --- example : (0 : EReal) ≤ 0 := by positivity --- example : 0 ≤ (2 : EReal) := by positivity - -/- ## Goals working directly from a hypothesis -/ - -section FromHypothesis - --- set_option trace.Meta.debug true --- sudo set_option trace.Tactic.positivity true -example {a : ℤ} (ha : 0 < a) : 0 < a := by positivity -example {a : ℤ} (ha : 0 < a) : 0 ≤ a := by positivity -example {a : ℤ} (ha : 0 < a) : a ≠ 0 := by positivity -example {a : ℤ} (ha : 0 ≤ a) : 0 ≤ a := by positivity -example {a : ℤ} (ha : a ≠ 0) : a ≠ 0 := by positivity -example {a : ℤ} (ha : a = 0) : 0 ≤ a := by positivity - -section - -variable [Zero α] [PartialOrder α] {a : α} - -example (ha : 0 < a) : 0 < a := by positivity -example (ha : 0 < a) : 0 ≤ a := by positivity -example (ha : 0 < a) : a ≠ 0 := by positivity -example (ha : 0 ≤ a) : 0 ≤ a := by positivity -example (ha : a ≠ 0) : a ≠ 0 := by positivity -example (ha : a = 0) : 0 ≤ a := by positivity - -end - -/- ### Reversing hypotheses -/ - -example {a : ℤ} (ha : a > 0) : 0 < a := by positivity -example {a : ℤ} (ha : a > 0) : 0 ≤ a := by positivity -example {a : ℤ} (ha : a > 0) : a ≥ 0 := by positivity -example {a : ℤ} (ha : a > 0) : a ≠ 0 := by positivity -example {a : ℤ} (ha : a ≥ 0) : 0 ≤ a := by positivity -example {a : ℤ} (ha : 0 ≠ a) : a ≠ 0 := by positivity -example {a : ℤ} (ha : 0 < a) : a > 0 := by positivity -example {a : ℤ} (ha : 0 < a) : a ≥ 0 := by positivity -example {a : ℤ} (ha : 0 < a) : 0 ≠ a := by positivity -example {a : ℤ} (ha : 0 ≤ a) : a ≥ 0 := by positivity -example {a : ℤ} (ha : a ≠ 0) : 0 ≠ a := by positivity -example {a : ℤ} (ha : a = 0) : a ≥ 0 := by positivity -example {a : ℤ} (ha : 0 = a) : 0 ≤ a := by positivity -example {a : ℤ} (ha : 0 = a) : a ≥ 0 := by positivity - -end FromHypothesis - -/- ### Calling `norm_num` -/ - -example {a : ℤ} (ha : 3 = a) : 0 ≤ a := by positivity -example {a : ℤ} (ha : 3 = a) : a ≠ 0 := by positivity -example {a : ℤ} (ha : 3 = a) : 0 < a := by positivity -example {a : ℤ} (ha : a = -1) : a ≠ 0 := by positivity - -example {a : ℤ} (ha : 3 ≤ a) : 0 ≤ a := by positivity -example {a : ℤ} (ha : 3 ≤ a) : a ≠ 0 := by positivity -example {a : ℤ} (ha : 3 ≤ a) : 0 < a := by positivity - -example {a : ℤ} (ha : 3 < a) : 0 ≤ a := by positivity -example {a : ℤ} (ha : 3 < a) : a ≠ 0 := by positivity -example {a : ℤ} (ha : 3 < a) : 0 < a := by positivity - -example {a b : ℤ} (h : 0 ≤ a + b) : 0 ≤ a + b := by positivity - -example {a : ℤ} (hlt : 0 ≤ a) (hne : a ≠ 0) : 0 < a := by positivity - -example {a b c d : ℤ} (ha : c < a) (hb : d < b) : 0 < (a - c) * (b - d) := by - positivity [sub_pos_of_lt ha, sub_pos_of_lt hb] - -section - -variable [Field α] [LinearOrder α] [IsStrictOrderedRing α] - -example : (1/4 : ℚ) > 0 := by norm_num -example : (4 : ℚ) > 0 := by positivity -example : (1/4 : ℚ) > 0 := by positivity -example : (1/4 - 2/3 : ℚ) ≠ 0 := by positivity -example : (1/4 - 2/3 : α) ≠ 0 := by positivity - -end - -/- ### `ArithmeticFunction.sigma` and `ArithmeticFunction.zeta` -/ - --- example (a b : ℕ) (hb : 0 < b) : 0 < ArithmeticFunction.sigma a b := by positivity --- example (a : ℕ) (ha : 0 < a) : 0 < ArithmeticFunction.zeta a := by positivity - -/- -## Test for meta-variable instantiation - -Reported on -https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/New.20tactic.3A.20.60positivity.60/near/300639970 --/ - -example : 0 ≤ 0 := by apply le_trans _ (le_refl _); positivity - - -/- ## Tests of the @[positivity] plugin tactics (addition, multiplication, division) -/ - --- example [Nonempty ι] [Zero α] {a : α} (ha : a ≠ 0) : const ι a ≠ 0 := by positivity --- example [Zero α] [PartialOrder α] {a : α} (ha : 0 < a) : 0 ≤ const ι a := by positivity --- example [Zero α] [PartialOrder α] {a : α} (ha : 0 ≤ a) : 0 ≤ const ι a := by positivity --- example [Nonempty ι] [Zero α] [PartialOrder α] {a : α} (ha : 0 < a) : 0 < const ι a := by --- positivity - -section ite -variable {p : Prop} [Decidable p] {a b : ℤ} - -example (ha : 0 < a) (hb : 0 < b) : 0 < ite p a b := by positivity -example (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ ite p a b := by positivity -example (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ ite p a b := by positivity -example (ha : 0 < a) (hb : b ≠ 0) : ite p a b ≠ 0 := by positivity -example (ha : a ≠ 0) (hb : 0 < b) : ite p a b ≠ 0 := by positivity -example (ha : a ≠ 0) (hb : b ≠ 0) : ite p a b ≠ 0 := by positivity - -end ite - -section MinMax - -example {a b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < min a b := by positivity -example {a b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ min a b := by positivity -example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ min a b := by positivity -example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ min a b := by positivity -example {a b : ℚ} (ha : 0 < a) (hb : b ≠ 0) : min a b ≠ 0 := by positivity -example {a b : ℚ} (ha : a ≠ 0) (hb : 0 < b) : min a b ≠ 0 := by positivity -example {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : min a b ≠ 0 := by positivity - -example {a b : ℚ} (ha : 0 < a) : 0 < max a b := by positivity -example {a b : ℚ} (hb : 0 < b) : 0 < max a b := by positivity -example {a b : ℚ} (ha : 0 ≤ a) : 0 ≤ max a b := by positivity -example {a b : ℚ} (hb : 0 ≤ b) : 0 ≤ max a b := by positivity -example {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : max a b ≠ 0 := by positivity - -example : 0 ≤ max 3 4 := by positivity -example : 0 ≤ max (0 : ℤ) (-3) := by positivity -example : 0 ≤ max (-3 : ℤ) 5 := by positivity - -end MinMax - -example {a b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < a * b := by positivity -example {a b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a * b := by positivity -example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a * b := by positivity -example {a b : ℚ} (ha : 0 < a) (hb : b ≠ 0) : a * b ≠ 0 := by positivity -example {a b : ℚ} (ha : a ≠ 0) (hb : 0 < b) : a * b ≠ 0 := by positivity -example {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : a * b ≠ 0 := by positivity - -example {a b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < a / b := by positivity -example {a b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a / b := by positivity -example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a / b := by positivity -example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by positivity -example {a b : ℚ} (ha : 0 < a) (hb : b ≠ 0) : a / b ≠ 0 := by positivity -example {a b : ℚ} (ha : a ≠ 0) (hb : 0 < b) : a / b ≠ 0 := by positivity -example {a b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : a / b ≠ 0 := by positivity - -example {a b : ℤ} (ha : 0 < a) (hb : 0 < b) : 0 ≤ a / b := by positivity -example {a : ℤ} (ha : 0 < a) : 0 < a / a := by positivity -example {a b : ℤ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a / b := by positivity -example {a b : ℤ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a / b := by positivity -example {a b : ℤ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b := by positivity - -example {a : ℚ} (ha : 0 < a) : 0 < a⁻¹ := by positivity -example {a : ℚ} (ha : 0 ≤ a) : 0 ≤ a⁻¹ := by positivity -example {a : ℚ} (ha : a ≠ 0) : a⁻¹ ≠ 0 := by positivity - -example {a : ℚ} (n : ℕ) (ha : 0 < a) : 0 < a ^ n := by positivity -example {a : ℚ} (n : ℕ) (ha : 0 ≤ a) : 0 ≤ a ^ n := by positivity -example {a : ℚ} (n : ℕ) (ha : a ≠ 0) : a ^ n ≠ 0 := by positivity -example {a : ℚ} : 0 ≤ a ^ 18 := by positivity -example {a : ℚ} (ha : a ≠ 0) : 0 < a ^ 18 := by positivity - -example {a : ℚ} (ha : 0 < a) : 0 < |a| := by positivity -example {a : ℚ} (ha : a ≠ 0) : 0 < |a| := by positivity -example (a : ℚ) : 0 ≤ |a| := by positivity - -example {a : ℤ} {b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < a • b := by positivity -example {a : ℤ} {b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ a • b := by positivity -example {a : ℤ} {b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a • b := by positivity -example {a : ℤ} {b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a • b := by positivity -example {a : ℤ} {b : ℚ} (ha : 0 < a) (hb : b ≠ 0) : a • b ≠ 0 := by positivity -example {a : ℤ} {b : ℚ} (ha : a ≠ 0) (hb : 0 < b) : a • b ≠ 0 := by positivity -example {a : ℤ} {b : ℚ} (ha : a ≠ 0) (hb : b ≠ 0) : a • b ≠ 0 := by positivity - --- Test that the positivity extension for `a • b` can handle universe polymorphism. --- example {R M : Type*} [Semiring R] [PartialOrder R] [IsOrderedRing R] --- [Semiring M] [PartialOrder M] [IsStrictOrderedRing M] --- [SMulWithZero R M] [PosSMulStrictMono R M] {a : R} {b : M} (ha : 0 < a) (hb : 0 < b) : --- 0 < a • b := by positivity - -example {a : ℤ} (ha : 3 < a) : 0 ≤ a + a := by positivity - -example {a b : ℤ} (ha : 3 < a) (hb : 4 ≤ b) : 0 ≤ 3 + a + b + b + 14 := by positivity - -example {H : Type*} [AddCommGroup H] [LinearOrder H] [IsOrderedAddMonoid H] - {a b : H} (ha : 0 < a) (hb : 0 ≤ b) : - 0 ≤ a + a + b := by - positivity - -example {a : ℤ} (ha : 3 < a) : 0 < a + a := by positivity - -example {a b : ℚ} (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity - -example {a b : ℤ} (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 := by positivity - -section -variable {q : ℚ} - -example (hq : q ≠ 0) : q.num ≠ 0 := by positivity -example : 0 < q.den := by positivity -example (hq : 0 < q) : 0 < q := by positivity -example (hq : 0 ≤ q) : 0 ≤ q.num := by positivity - -end - -example (a b : ℕ) (ha : a ≠ 0) : 0 < a.gcd b := by positivity -example (a b : ℤ) (ha : a ≠ 0) : 0 < a.gcd b := by positivity -example (a b : ℕ) (hb : b ≠ 0) : 0 < a.gcd b := by positivity -example (a b : ℤ) (hb : b ≠ 0) : 0 < a.gcd b := by positivity -example (a b : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a.lcm b := by positivity -example (a b : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a.lcm b := by positivity -example (a : ℕ) (ha : a ≠ 0) : 0 < a.sqrt := by positivity --- example (a : ℕ) (ha : a ≠ 0) : 0 < a.totient := by positivity From b4827674ad210e0250024f5d1fec2f3beff101f6 Mon Sep 17 00:00:00 2001 From: Pan Lin <58059503+HugLycan@users.noreply.github.com> Date: Mon, 16 Feb 2026 22:06:47 +0100 Subject: [PATCH 7/8] fix error in evalDiv --- Mathlib/Algebra/Order/Field/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index a0611da510e25f..51e957fc981ad9 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -743,13 +743,13 @@ such that `positivity` successfully recognises both `a` and `b`. -/ pure (.nonzero q(div_ne_zero $pa $pb)) | _, _ => pure .none let _a ← synthInstanceQ q(GroupWithZero $α) - let _a ← synthInstanceQ q(PartialOrder $α) + let pα' ← synthInstanceQ q(PartialOrder $α) let _a ← synthInstanceQ q(PosMulReflectLT $α) assumeInstancesCommute let ra ← core zα pα? a; let rb ← core zα pα? b match ra, rb with | .positive (ltα := ltα) pa, .positive pb => - haveI' : $ltα =Q ($lα).toLT := ⟨⟩ + haveI' : $ltα =Q ($pα').toLT := ⟨⟩ assumeInstancesCommute pure (.positive q(div_pos $pa $pb)) | .positive pa, .nonnegative pb => @@ -759,7 +759,7 @@ such that `positivity` successfully recognises both `a` and `b`. -/ assumeInstancesCommute pure (.nonnegative q(div_nonneg_of_nonneg_of_pos $pa $pb)) | .nonnegative (leα := leα) pa, .nonnegative pb => - haveI' : $leα =Q ($lα).toLE := ⟨⟩ + haveI' : $leα =Q ($pα').toLE := ⟨⟩ assumeInstancesCommute pure (.nonnegative q(div_nonneg $pa $pb)) | .positive pa, .nonzero pb => From 0cada3f3c7183adaa53d1e83d31f227b4fe1c2a1 Mon Sep 17 00:00:00 2001 From: Pan Lin <58059503+HugLycan@users.noreply.github.com> Date: Tue, 17 Feb 2026 02:02:02 +0100 Subject: [PATCH 8/8] update lean version --- lake-manifest.json | 14 +++++++------- lean-toolchain | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 0479fe89d2d65d..477fa87b41c65d 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7311586e1a56af887b1081d05e80c11b6c41d212", + "rev": "55c8532eb21ec9f6d565d51d96b8ca50bd1fbef3", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b5908dbac486279f1133cb937648c63c30b455af", + "rev": "85b59af46828c029a9168f2f9c35119bd0721e6e", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0", + "rev": "f642a64c76df8ba9cb53dba3b919425a0c2aeaf1", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "23324752757bf28124a518ec284044c8db79fee5", + "rev": "b8f98e9087e02c8553945a2c5abf07cec8e798c3", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7d7a6dd24b615f11ef20053195c144f1b92147b0", + "rev": "495c008c3e3f4fb4256ff5582ddb3abf3198026f", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,10 +75,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "28e0856d4424863a85b18f38868c5420c55f9bae", + "rev": "4f10f47646cb7d5748d6f423f4a07f98f7bbcc9e", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.28.0-rc1", + "inputRev": "v4.28.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "mathlib", diff --git a/lean-toolchain b/lean-toolchain index 4bafde2055a4b4..4c685fa085fa1c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.28.0-rc1 +leanprover/lean4:v4.28.0