feat(Tactic/Positivity): cover Finset.sum_pos' with the Finset.sum extension

Mathlib/Tactic/Positivity/Finset.lean

@@ -60,9 +60,19 @@ meta def evalFinsetDens : PositivityExt where eval {u 𝕜} _ pα? e :=
     return .positive q(@Nonempty.dens_pos $α $instα $s $ps)
   | _, _, _ => throwError "not Finset.dens"
 
+/-- Return whether `p` is a proposition of the form `?a ∈ s`. If so, return `a` and a Qq-proof that
+`p` is `a ∈ s`. -/
+private meta def isMemFinset? {u : Level} {α : Q(Type u)} (s : Q(Finset $α)) (p : Q(Prop)) :
+    MetaM <| Option <| (a : Q($α)) ×' $p =Q ($a ∈ $s) := withNewMCtxDepth do
+  let m ← mkFreshExprMVarQ q($α)
+  let .defEq _ ← withReducible <| isDefEqQ q($p) q($m ∈ $s) | return none
+  let ⟨m, _⟩ ← instantiateMVarsQ' q($m)
+  return some ⟨q($m), ⟨⟩⟩
+
 attribute [local instance] monadLiftOptionMetaM in
-/-- The `positivity` extension which proves that `∑ i ∈ s, f i` is nonnegative if `f` is, and
-positive if each `f i` is and `s` is nonempty.
+/-- The `positivity` extension which proves that `∑ a ∈ s, f a` is nonnegative if `f` is, and
+positive if either each `f i` is and `s` is nonempty, or some `f a` is where `a ∈ s` is an
+assumption.
 
 TODO: The following example does not work
 ```
@@ -83,22 +93,38 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
     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
-      let .some pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
+      let .some _pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
       assertInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
-      pure <| some q(@sum_pos $ι $α $instα (@PartialOrder.toPreorder _ $pα) $pα' $f $s _
-        (fun i _ ↦ $pr i) $ps)
-    -- Try to show that the sum is positive
+      pure <| some q(sum_pos (fun i _ ↦ $pr i) $ps)
+    -- Try to show that the sum is positive because all summands are
     if let some p_pos := p_pos then
       return .positive p_pos
+    let pbody ← rbody.toNonneg
+    let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
+    -- Else try to show that the sum is positive because one summand is. We look for the witness
+    -- among the assumptions of the form `a ∈ s`, since we have no other way of getting hold of an
+    -- element of `s` at which `f` might be positive.
+    let p_pos' : Option Q(0 < $e) ← (do
+      let .some _pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
+      for ldecl in ← getLCtx do
+        if ldecl.isImplementationDetail then continue
+        unless ← Meta.isProp ldecl.type do continue
+        have ty : Q(Prop) := ldecl.type
+        have ha : Q($ty) := ldecl.toExpr
+        let .some ⟨a, _⟩ ← isMemFinset? q($s) ty | continue
+        have fa : Q($α) := .betaRev f #[a]
+        let : $fa =Q $f $a := ⟨⟩
+        let .positive pa ← catchNone (core zα pα fa) | continue
+        assertInstancesCommute
+        return some q(sum_pos' (fun i _ ↦ $pr i) ⟨$a, $ha, $pa⟩)
+      return none)
+    if let some p_pos' := p_pos' then
+      return .positive p_pos'
     -- Fall back to showing that the sum is nonnegative
-    else
-      let pbody ← rbody.toNonneg
-      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
-      let pα' ← synthInstanceQ q(AddLeftMono $α)
-      assertInstancesCommute
-      return .nonnegative q(@sum_nonneg $ι $α $instα (@PartialOrder.toPreorder _ $pα) $f $s $pα'
-        fun i _ ↦ $pr i)
+    let _pα' ← synthInstanceQ q(AddLeftMono $α)
+    assertInstancesCommute
+    return .nonnegative q(sum_nonneg fun i _ ↦ $pr i)
   | _ => throwError "not Finset.sum"
 
 variable {α : Type*} {s : Finset α}
@@ -117,6 +143,19 @@ example [Nonempty α] : 0 < Fintype.card α := by positivity
 example [Nonempty α] : 0 < dens (univ : Finset α) := by positivity
 example [Nonempty α] : dens (univ : Finset α) ≠ 0 := by positivity
 
+example {f : α → ℕ} : 0 ≤ ∑ a ∈ s, f a := by positivity
+example {f : α → ℕ} (hs : s.Nonempty) : 0 < ∑ i ∈ s, (f i + 1) := by positivity
+example {f : α → ℕ} {a : α} (ha : a ∈ s) (hfa : 0 < f a) : 0 < ∑ a ∈ s, f a := by positivity
+example {f : α → ℕ} {a : α} (ha : a ∈ s) (hfa : f a ≠ 0) : ∑ a ∈ s, f a ≠ 0 := by positivity
+-- `f` need not be positive at the witness `a`, in which case we only get nonnegativity
+example {f : α → ℕ} {a : α} (_ha : a ∈ s) : 0 ≤ ∑ a ∈ s, f a := by positivity
+
+-- Extra `_ ∈ s` assumptions do not throw off `positivity`
+example {f : α → ℕ} {a b : α} (_ha : a ∈ s) (hb : b ∈ s) (hb : 0 < f b) : 0 < ∑ a ∈ s, f a := by
+  positivity
+example {f : α → ℕ} {a b : α} (ha : a ∈ s) (_hb : b ∈ s) (hfa : 0 < f a) : 0 < ∑ a ∈ s, f a := by
+  positivity
+
 example {G : Type*} {A : Finset G} :
     let f := fun _ : G ↦ 1; (∀ s, f s ^ 2 = 1) → 0 ≤ #A := by
   intros

Mathlib/Util/Qq.lean

@@ -87,4 +87,11 @@ def mkNatLitQ (n : Nat) : Q(Nat) := mkNatLit n
 This is a Qq version of `Lean.mkIntLit`. -/
 def mkIntLitQ (n : Int) : Q(Int) := mkIntLit n
 
+/-- Version of `instantiateMVarsQ` that returns the Qq-fact that the new expression is equal to the
+previous one. -/
+def instantiateMVarsQ' {u : Level} {α : Q(Sort u)} (e : Q($α)) :
+    MetaM <| (e' : Q($α)) ×' ($e' =Q $e) := do
+  let e' ← instantiateMVars e
+  return ⟨e', ⟨⟩⟩
+
 end Qq