feat(tactic/positivity): Extension for finset.card (#16637)

A best effort `positivity` extension for `finset.card`. This looks for an assumption of the form `s.nonempty` in context to prove `0 < s.card`.

src/tactic/positivity.lean

@@ -441,7 +441,7 @@ meta def positivity_coe : expr → tactic strictness
   | `(@coe_to_lift _ _ %%inst) := do
     strictness_a ← core a,
     match inst, strictness_a with -- `mk_mapp` is necessary in some places. Why?
-    | `(nat.cast_coe), positive p := positive <$> mk_app ``nat_cast_pos [p]
+    | `(nat.cast_coe), positive p := positive <$> mk_mapp ``nat_cast_pos [typ, none, none, none, p]
     | `(nat.cast_coe), _ := nonnegative <$> mk_mapp ``nat.cast_nonneg [typ, none, a]
     | `(int.cast_coe), positive p := positive <$> mk_mapp ``int_cast_pos [typ, none, none, none, p]
     | `(int.cast_coe), nonnegative p := nonnegative <$>
@@ -457,4 +457,18 @@ meta def positivity_coe : expr → tactic strictness
   end
 | _ := failed
 
+private lemma card_univ_pos (α : Type*) [fintype α] [nonempty α] :
+  0 < (finset.univ : finset α).card :=
+finset.univ_nonempty.card_pos
+
+/-- Extension for the `positivity` tactic: `finset.card s` is positive if `s` is nonempty. -/
+@[positivity]
+meta def positivity_finset_card : expr → tactic strictness
+| `(finset.card %%s) := do -- TODO: Partial decision procedure for `finset.nonempty`
+                          p ← to_expr ``(finset.nonempty %%s) >>= find_assumption,
+                          positive <$> mk_app ``finset.nonempty.card_pos [p]
+| `(@fintype.card %%α %%i) := positive <$> mk_mapp ``fintype.card_pos [α, i, none]
+| e := pp e >>= fail ∘ format.bracket "The expression `"
+    "` isn't of the form `finset.card s` or `fintype.card α`"
+
 end tactic

test/positivity.lean

@@ -142,6 +142,9 @@ example : 0 ≤ max (-3 : ℤ) 5 := by positivity
 example [ordered_semiring α] [ordered_add_comm_monoid β] [smul_with_zero α β]
   [ordered_smul α β] {a : α} (ha : 0 < a) {b : β} (hb : 0 < b) : 0 ≤ a • b := by positivity
 
+example {α : Type*} (s : finset α) (hs : s.nonempty) : 0 < s.card := by positivity
+example {α : Type*} [fintype α] [nonempty α] : 0 < fintype.card α := by positivity
+
 example {r : ℝ} : 0 < real.exp r := by positivity
 
 example {V : Type*} [normed_add_comm_group V] (x : V) : 0 ≤ ∥x∥ := by positivity