Coercions from finset to set

Stream: new members

[MinusGix]

I'm trying to prove that the complement of each element of the set-of-sets Fis within F. (This is for learning so that I can work up to more complicated proofs similar to it)
The confusion I'm having is on how to handle coercions, I don't feel like I have a good handle on manipulating those.
It seems like being able to tell Lean that (↑{val := {0}, nodup := _})ᶜ ∈ F should be turned into a {(0 : fin 3)}ᶜ ∈ F would simplify proving.
(Other comments on whether this is a bad way to be proving this would also be appreciated)

-- Minor question: is there a nicer way of writing something like this where it needs to use
-- some constant?
example :
  ∀ E ∈ ({∅, {fin.of_nat' 0}, {fin.of_nat' 1, fin.of_nat' 2}, set.univ} : set (set (fin 3))),
    Eᶜ ∈ ({∅, {fin.of_nat' 0}, {fin.of_nat' 1, fin.of_nat' 2}, set.univ} : set (set (fin 3)))  :=
begin
  let F : set (set (fin 3)) := {∅, {fin.of_nat' 0}, {fin.of_nat' 1, fin.of_nat' 2}, set.univ},
  -- I have proofs for both of the below, but cutting them out for a smaller example
  let compl0 : ({fin.of_nat' 0} : set (fin 3))ᶜ = ({fin.of_nat' 1, fin.of_nat' 2} : set (fin 3)),  sorry,
  let compl0_in : {fin.of_nat' 0}ᶜ ∈ F, sorry,

  intros E Einp,
  fin_cases E,
    -- `∅ᶜ ∈ F`
    -- This case is easy since it seems to turn it into a set automatically
    { sorry },
    -- `(↑{val := {0}, nodup := _})ᶜ ∈ F`
    {
      convert compl0_in,
      -- simp? is how I found this coe_eq_singleton theorem, but it would have been nicer to just have it be a set in the first place
      simp only [finset.coe_eq_singleton], refl,
    },
    -- `(↑{val := {1}, nodup := _})ᶜ ∈ F`
    {
      exfalso,
      -- use Einp to prove false, since `{1} ∉ F`
      sorry,
    },
    -- todo, the rest of them
end

[Kyle Miller]

You can write that set you have by ({∅, {0}, {1, 2}, set.univ} : set (set (fin 3))) by the way

[Kyle Miller]

Regarding these (↑{val := {0}, nodup := _}) terms, I'm not sure exactly what's happening with fin_cases here, but something seems like it's not working in an ideal way.

[Kyle Miller]

Here's how I might approach your statement:

import tactic.fin_cases
import tactic.norm_fin

def F : set (set (fin 3)) := {∅, {0}, {1, 2}, set.univ}

example : ∀ E ∈ F, Eᶜ ∈ F :=
begin
  intro E,
  simp [F],
  rintro (rfl | rfl | rfl | rfl),
  { simp },
  { right, right, left, ext i, fin_cases i; norm_fin },
  { right, left, ext i, fin_cases i; norm_fin },
  { simp }
end

The tactic#rintro tactic is a way to do destructuring while doing intro. When you give it rfl then it will substitute the variable for you automatically.

[Patrick Johnson]

Nonterminal simp [F] !