feat(Tactic/Positivity): make positivity work for types that are not partial orders (leanprover-community#35394)

Make positivity work for types that are not partial orders

Most PositivityExt haven't been updated for non partial order cases yet. They will be updated in the later PR.

`Strictness` now depends on `Option Q(PartialOrder $α)` instead of `Q(PartialOrder $α)`, and the constructors `Strictness.positive`/`Strictness.nonnegative` now have their `Q(PartialOrder $α)` typeclass arguments.

Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: 2 people

Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

@@ -416,7 +416,8 @@ open Lean Meta Mathlib Meta Positivity Qq in
 For performance reasons, we only attempt to apply this when `abv` is a variable.
 If it is an explicit function, e.g. `|_|` or `‖_‖`, another extension should apply. -/
 @[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α? | pure .none
   let (.app f a) ← whnfR e | throwError "not abv ·"
   if !f.getAppFn.isFVar then
     throwError "abv: function is not a variable"

Mathlib/Algebra/Order/Algebra.lean

@@ -95,11 +95,12 @@ open Lean Meta Qq Function
 
 /-- Extension for `algebraMap`. -/
 @[positivity algebraMap _ _ _]
-meta def evalAlgebraMap : PositivityExt where eval {u β} _zβ _pβ e := do
+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 some _ := pβ? | pure .none
     let _instαSemiring ← synthInstanceQ q(Semiring $α)
     let _instαPartialOrder ← synthInstanceQ q(PartialOrder $α)
     try
@@ -117,6 +118,7 @@ meta def evalAlgebraMap : PositivityExt where eval {u β} _zβ _pβ e := do
       assertInstancesCommute
       return .nonnegative q(algebraMap_nonneg $β <| le_of_lt $pa)
   | .nonnegative pa =>
+    let some _ := pβ? | pure .none
     let _instαSemiring ← synthInstanceQ q(CommSemiring $α)
     let _instαPartialOrder ← synthInstanceQ q(PartialOrder $α)
     let _instβSemiring ← synthInstanceQ q(Semiring $β)

Mathlib/Algebra/Order/BigOperators/Expect.lean

@@ -220,7 +220,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

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -225,9 +225,10 @@ 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
   match e with
   | ~q(@Finset.prod $ι _ $instα $s $f) =>
+    let some pα := pα? | pure .none
     let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque
     have body : Q($α) := Expr.betaRev f #[i]
     let rbody ← core zα pα body

Mathlib/Algebra/Order/Field/Basic.lean

@@ -733,15 +733,23 @@ lemma zpow_zero_pos {α : Type*} [Semifield α] [PartialOrder α] [IsStrictOrder
 
 /-- 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 ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HDiv.hDiv)
+  let some pα := 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 _a ← synthInstanceQ q(GroupWithZero $α)
-  let _a ← synthInstanceQ q(PartialOrder $α)
   let _a ← synthInstanceQ q(PosMulReflectLT $α)
   assumeInstancesCommute
-  let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HDiv.hDiv)
   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))
@@ -756,25 +764,38 @@ such that `positivity` successfully recognises both `a` and `b`. -/
 /-- 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(GroupWithZero $α)
   let _a ← synthInstanceQ q(PartialOrder $α)
   let _a ← synthInstanceQ q(PosMulReflectLT $α)
   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 some _ := pα? | pure .none
   let _a ← synthInstanceQ q(Semifield $α)
   let _a ← synthInstanceQ q(LinearOrder $α)
   let _a ← synthInstanceQ q(IsStrictOrderedRing $α)

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 $α)
@@ -151,11 +159,11 @@ meta def evalZPow : PositivityExt where eval {u α} zα pα e := do
     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
+        MetaM (Strictness zα e pα) := do
       haveI' : $e =Q $a ^ $b := ⟨⟩
       assumeInstancesCommute
       pure (.nonnegative q(zpow_nonneg $pa $b))
-    let ofNonzero (pa : Q($a ≠ 0)) (_oα : Q(GroupWithZero $α)) : MetaM (Strictness zα pα e) := do
+    let ofNonzero (pa : Q($a ≠ 0)) (_oα : Q(GroupWithZero $α)) : MetaM (Strictness zα e pα) := do
       haveI' : $e =Q $a ^ $b := ⟨⟩
       let _a ← synthInstanceQ q(GroupWithZero $α)
       assumeInstancesCommute

Mathlib/Algebra/Order/Floor/Extended.lean

@@ -256,11 +256,11 @@ 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
+    let some _ := pα? | pure .none
+    match ← core q(inferInstance) (some q(inferInstance)) r with
     | .positive pr =>
       assertInstancesCommute
       pure (.positive q(natCeil_pos $pr))

Mathlib/Algebra/Order/Floor/Ring.lean

@@ -50,10 +50,11 @@ theorem int_floor_nonneg_of_pos [Ring α] [LinearOrder α] [FloorRing α] {a : 
 
 /-- 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
+    let some _ := pα? | pure .none
+    match ← core q(inferInstance) (some q(inferInstance)) a with
     | .positive pa =>
         assertInstancesCommute
         pure (.nonnegative q(int_floor_nonneg_of_pos (α := $α') $pa))
@@ -69,13 +70,14 @@ theorem nat_ceil_pos [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α}
 
 /-- 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 some _ := pα? | pure .none
     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 +89,11 @@ theorem int_ceil_pos [Ring α] [LinearOrder α] [FloorRing α] {a : α} : 0 < 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
+    let some _ := pα? | pure .none
+    match ← core q(inferInstance) (some q(inferInstance)) a with
     | .positive pa =>
         assertInstancesCommute
         pure (.positive q(int_ceil_pos (α := $α') $pa))

Mathlib/Algebra/Order/Interval/Basic.lean

@@ -660,18 +660,20 @@ open Lean Meta Qq
 /-- Extension for the `positivity` tactic: The length of an interval is always nonnegative. -/
 @[positivity NonemptyInterval.length _]
 meta def evalNonemptyIntervalLength : PositivityExt where
-  eval {u α} _ _ e := do
+  eval {u α} _ pα? e := do
     let ~q(@NonemptyInterval.length _ $ig $ipo $a) := e |
       throwError "not NonemptyInterval.length"
+    let some _ := pα? | pure .none
     let _i ← synthInstanceQ q(IsOrderedAddMonoid $α)
     assertInstancesCommute
     return .nonnegative q(NonemptyInterval.length_nonneg $a)
 
 /-- Extension for the `positivity` tactic: The length of an interval is always nonnegative. -/
 @[positivity Interval.length _]
 meta def evalIntervalLength : PositivityExt where
-  eval {u α} _ _ e := do
+  eval {u α} _ pα? e := do
     let ~q(@Interval.length _ $ig $ipo $a) := e | throwError "not Interval.length"
+    let some _ := pα? | pure .none
     let _i ← synthInstanceQ q(IsOrderedAddMonoid $α)
     assumeInstancesCommute
     return .nonnegative q(Interval.length_nonneg $a)

Mathlib/Algebra/Order/Module/Field.lean

@@ -103,7 +103,8 @@ end Module.IsTorsionFree
 
 /-- 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"