feat: positivity extensions for Finset.card, Fintype.card (#10610)

Leverage the new `proveFinsetNonempty` prover to write a `positivity` extension about `Finset.card`. Also write the corresponding `positivity` extension for `Fintype.card`.

I put the two new extensions in a new file rather than `Tactic.Positivity.Basic` or `Data.Fintype.Card` because the former doesn't import any finiteness and the latter doesn't import linearly ordered fields. But I don't really mind where the extensions end up.

From LeanAPAP



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Alex J Best <alex.j.best@gmail.com>

Author: 3 people

Mathlib.lean

@@ -3579,6 +3579,7 @@ import Mathlib.Tactic.Polyrith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Positivity.Basic
 import Mathlib.Tactic.Positivity.Core
+import Mathlib.Tactic.Positivity.Finset
 import Mathlib.Tactic.ProdAssoc
 import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose

Mathlib/Tactic.lean

@@ -137,6 +137,7 @@ import Mathlib.Tactic.Polyrith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Positivity.Basic
 import Mathlib.Tactic.Positivity.Core
+import Mathlib.Tactic.Positivity.Finset
 import Mathlib.Tactic.ProdAssoc
 import Mathlib.Tactic.ProjectionNotation
 import Mathlib.Tactic.Propose

Mathlib/Tactic/Positivity/Finset.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Data.Fintype.Card
+import Mathlib.Tactic.Positivity.Core
+
+/-!
+# Positivity extensions for finsets
+
+This file provides a few `positivity` extensions that cannot be in either the finset files (because
+they don't know about ordered fields) or in `Tactic.Positivity.Basic` (because it doesn't want to
+know about finiteness).
+-/
+
+namespace Mathlib.Meta.Positivity
+
+open Qq Lean Meta Finset
+
+/-- Extension for `Finset.card`. `s.card` is positive if `s` is nonempty.
+
+It calls `Mathlib.Meta.proveFinsetNonempty` to attempt proving that the finset is nonempty. -/
+@[positivity Finset.card _]
+def evalFinsetCard : PositivityExt where eval {u α} _ _ e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(Finset.card $s) =>
+    let some ps ← proveFinsetNonempty s | return .none
+    assertInstancesCommute
+    return .positive q(Finset.Nonempty.card_pos $ps)
+  | _ => throwError "not Finset.card"
+
+/-- Extension for `Fintype.card`. `Fintype.card α` is positive if `α` is nonempty. -/
+@[positivity Fintype.card _]
+def evalFintypeCard : PositivityExt where eval {u α} _ _ e := do
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(@Fintype.card $β $instβ) =>
+    let instβno ← synthInstanceQ q(Nonempty $β)
+    assumeInstancesCommute
+    return .positive q(@Fintype.card_pos $β $instβ $instβno)
+  | _ => throwError "not Fintype.card"
+
+example {α : Type*} {s : Finset α} (hs : s.Nonempty) : 0 < s.card := by positivity
+example {α : Type*} {s : Finset α} : 0 ≤ s.card := by positivity
+example {α : Type*} [Fintype α] [Nonempty α] : 0 < (univ : Finset α).card := by positivity
+example {α : Type*} [Fintype α] [Nonempty α] : 0 < Fintype.card α := by positivity
+example {α : Type*} [Fintype α] : 0 ≤ Fintype.card α := by positivity
+
+end Mathlib.Meta.Positivity

scripts/noshake.json

@@ -216,6 +216,7 @@
   ["Mathlib.Data.ZMod.Basic", "Mathlib.RingTheory.Polynomial.Basic"],
   "Mathlib.Tactic.ProxyType": ["Mathlib.Logic.Equiv.Defs"],
   "Mathlib.Tactic.ProdAssoc": ["Mathlib.Logic.Equiv.Defs"],
+  "Mathlib.Tactic.Positivity.Finset": ["Mathlib.Data.Fintype.Card"],
   "Mathlib.Tactic.Positivity.Basic":
   ["Mathlib.Data.Int.CharZero", "Mathlib.Data.Nat.Factorial.Basic"],
   "Mathlib.Tactic.NormNum.Ineq":