finset.induction_on

Stream: general

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/2ef444afbbdcae10682b2d46479c3f267caca0b6/src/data/finset.lean#L309-L310

@[elab_as_eliminator] protected theorem induction_on {α : Type*} {p : finset α → Prop} [decidable_eq α]
  (s : finset α) (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a ∉ s → p s → p (insert a s)) : p s :=

[Kenny Lau]

should we have a classical version that removes decidable_eq?

[Yury G. Kudryashov]

Inside open_locale classical you already have this decidable_eq.

[Kenny Lau]

sometimes it's slow to infer the classical instance of decidable_eq

[Reid Barton]

I was vaguely under the impression that we had a linter about decidable_eq hypotheses of theorems

[Kenny Lau]

what does it do?

[Johan Commelin]

It checks that you didn't accidentally prove a constructive theorem if you might as well have proven it classically.

[Bhavik Mehta]

I think the insert here means you need a decidable eq in the statement

[Reid Barton]

Oh right we were just discussing this example last week.

[Reid Barton]

Maybe we should have a version that uses whatever the insert alternative was that didn't need decidable equality.

[Mario Carneiro]

I could have sworn I made this definition:

import data.finset

def finset.cons {α} (a : α) (s : finset α) (h : a ∉ s) : finset α :=
⟨a :: s.1, multiset.nodup_cons_of_nodup h s.2⟩