finset.induction_on to decide "contains such an element"?

Stream: new members

[Malvin Gattinger]

I want to use induction to show this decidability. Should I be using something else?

import data.set.finite

@[derive decidable_eq]
inductive formula : Type
| bottom : formula
| neg : formula → formula
| and : formula → formula → formula

open formula

instance has_NegNeg.decidable (X : finset formula) : decidable (∃ ϕ, neg (neg ϕ) ∈ X) :=
begin
  -- Why does this not work?
  --apply finset.induction_on X,

  -- I want to do something like this:
  refine if h : X = ∅ then _ else _,
  -- empty set never contains a NegNeg:
  rw h,
  simp, apply decidable.is_false, trivial,
  -- Set with at least one element:
  -- if it is a NegNeg, decide true, otherwishe recurse / use induction hypothesis?
  sorry,
end

[Yaël Dillies]

This is because the goal is data, not a prop, and docs#finset.induction_on only targets Prop. If you want to do induction on a finset, you have to first do induction on a list and then lift it to multiset by showing that what you constructed is preserved under list permutations.

[Mario Carneiro]

I would do it like this:

instance has_NegNeg.decidable (X : finset formula) : decidable (∃ ϕ, neg (neg ϕ) ∈ X) :=
begin
  haveI : ∀ X, decidable (∃ ϕ, X = neg (neg ϕ)) := by
    rintro (_|(_|_|_)|_); exact is_true ⟨_, rfl⟩ <|> { apply is_false, rintro ⟨_, ⟨⟩⟩ },
  exact decidable_of_iff (∃ f ∈ X, ∃ ϕ, f = neg (neg ϕ))
    ⟨λ ⟨_, h, ϕ, rfl⟩, ⟨ϕ, h⟩, λ ⟨ϕ, h⟩, ⟨_, h, ϕ, rfl⟩⟩,
end

[Eric Wieser]

I was about to say something similar but less complete!

[Mario Carneiro]

that is, instead of using induction, delegate to the decidability instance for "there exists an element of X such that bla"

[Eric Wieser]

What's the name of that instance?

[Mario Carneiro]

looks like the one I just posted uses docs#finset.decidable_dexists_finset

[Malvin Gattinger]

Aha, many thanks! I guess my mental error was to think of decidable as Prop -> Prop but it is Prop -> Type.

[Malvin Gattinger]

Will now try to understand the code by @Mario Carneiro thank you!!

[Malvin Gattinger]

Where/how can I look up <|>? My guess is that it tries both tactics and succeeds as soon as one of them succeeds?

[Mario Carneiro]

it tries the first tactic, and if it fails it tries the second tactic