I want to write a lemma eq_empty_iff_forall_not_mem

Stream: new members

[Nick_adfor]

import Mathlib

lemma eq_empty_iff_forall_not_mem {α : Type*} {s : Finset α} :
    s = ∅ ↔ ∀ x, x ∉ s := by
  rw [Finset.ext_iff]
  simp only [Finset.not_mem_empty, true_iff]
  exact fun h x => h x

But it cannot run as vscode tell me that

type mismatch
  fun h x => ?m.18219
has type
  (h : ?m.18212) → (x : ?m.18220 h) → ?m.18221 h x : Sort (imax ?u.18211 ?u.18214 ?u.18217)
but is expected to have type
  (∀ (a : α), a ∈ s ↔ False) ↔ ∀ (x : α), x ∉ s : Prop

[Robin Arnez]

You have an iff (↔) not an implication! Putting iff_false in the simp before should do the trick

[Nick_adfor]

import Mathlib

open Equiv Perm

def IsDoubleTransposition (σ : Perm (Fin 4)) : Prop :=
  ∃ (a b c d : Fin 4), a ≠ b ∧ c ≠ d ∧
  Disjoint (support (swap a b)) (support (swap c d)) ∧
  σ = swap a b * swap c d

def doubleTranspositions : List (Perm (Fin 4)) :=
  [swap 0 1 * swap 2 3,
   swap 0 2 * swap 1 3,
   swap 0 3 * swap 1 2]

lemma mem_cons_iff_three {α : Type*} {x a b c : α} {l : List α} :
    x ∈ [a, b, c] ++ l ↔ x = a ∨ x = b ∨ x = c ∨ x ∈ l := by
  simp only [List.mem_cons, List.cons_append, List.mem_append]

lemma eq_empty_iff_forall_not_mem {α : Type*} {s : Finset α} :
    s = ∅ ↔ ∀ x, x ∉ s := by
  rw [Finset.ext_iff]
  simp only [Finset.not_mem_empty, iff_false]

lemma mem_doubleTranspositions_iff {σ : Perm (Fin 4)} :
    σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ := by
  constructor
  · intro h
    simp [doubleTranspositions] at h
    rcases h with rfl | rfl | rfl
    · exact ⟨0, 1, 2, 3, by decide, by decide, by decide, rfl⟩
    · exact ⟨0, 2, 1, 3, by decide, by decide, by decide, rfl⟩
    · exact ⟨0, 3, 1, 2, by decide, by decide, by decide, rfl⟩

    intro h
    rcases h with ⟨a, b, c, d, hab, hcd, hdisj, rfl⟩

    have distinct : ∀ x ∈ ({a, b} : Finset (Fin 4)), ∀ y ∈ ({c, d} : Finset (Fin 4)), x ≠ y := by
      intro x hx y hy
      rw [Finset.disjoint_iff_inter_eq_empty, eq_empty_iff_forall_not_mem] at hdisj

      exact hdisj ⟨x, hx, hy⟩
    fin_cases a <;> fin_cases b <;> fin_cases c <;> fin_cases d <;>
    try { simp [distinct, hab, hcd] at * } <;>
    simp [doubleTranspositions, mem_cons_iff_three, *]

The whole code is here. I want to prove σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ, and in it I need two lemmas to prove lemma mem_doubleTranspositions_iff

[Nick_adfor]

Robin Arnez said:

You have an iff (↔) not an implication! Putting iff_false in the simp before should do the trick

OK, thanks:

I fix it as

lemma eq_empty_iff_forall_not_mem {α : Type*} {s : Finset α} :
    s = ∅ ↔ ∀ x, x ∉ s := by
  rw [Finset.ext_iff]
  simp only [Finset.not_mem_empty, iff_false]

[Nick_adfor]

For the whole proof, the part

    have distinct : ∀ x ∈ ({a, b} : Finset (Fin 4)), ∀ y ∈ ({c, d} : Finset (Fin 4)), x ≠ y := by

      intro x hx y hy

      rw [Finset.disjoint_iff_inter_eq_empty, eq_empty_iff_forall_not_mem] at hdisj

      exact hdisj ⟨x, hx, hy⟩

    fin_cases a <;> fin_cases b <;> fin_cases c <;> fin_cases d <;>

    try { simp [distinct, hab, hcd] at * } <;>

    simp [doubleTranspositions, mem_cons_iff_three, *]

eq_empty_iff_forall_not_mem and mem_cons_iff_three should be my lemmas, but it does not work that well in the whole code.

[Robin Arnez]

You can use the decide +revert tactic for the last part:

  · intro h
    rcases h with ⟨a, b, c, d, hab, hcd, hdisj, rfl⟩
    decide +revert

[Sébastien Gouëzel]

Since the whole proof is about finite objects, you can also brute-force your statement by checking it for all these objects, as in

lemma mem_doubleTranspositions_iff {σ : Perm (Fin 4)} :
    σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ := by
  revert σ
  simp only [doubleTranspositions, IsDoubleTransposition]
  decide

[Nick_adfor]

Robin Arnez said:

You can use the decide +revert tactic for the last part:

  · intro h
    rcases h with ⟨a, b, c, d, hab, hcd, hdisj, rfl⟩
    decide +revert

Sébastien Gouëzel said:

Since the whole proof is about finite objects, you can also brute-force your statement by checking it for all these objects, as in

lemma mem_doubleTranspositions_iff {σ : Perm (Fin 4)} :
    σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ := by
  revert σ
  simp only [doubleTranspositions, IsDoubleTransposition]
  decide

Thanks for all! I do not know that lean can check the code for all the finite objects, I think that I may need to write by myself, which truely confused me.

[Nick_adfor]

What about the part as follows? I may think it can be shortened, too.

  · intro h
    simp [doubleTranspositions] at h
    rcases h with rfl | rfl | rfl
    · exact ⟨0, 1, 2, 3, by decide, by decide, by decide, rfl⟩
    · exact ⟨0, 2, 1, 3, by decide, by decide, by decide, rfl⟩
    · exact ⟨0, 3, 1, 2, by decide, by decide, by decide, rfl⟩

[Robin Arnez]

I mean, instead of intro; simp; rcases you can do rintro (_ | ⟨_, _ | ⟨_, _ | ⟨_, _ | _⟩⟩⟩) although I would need some time to explain why that works

[Nick_adfor]

Robin Arnez said:

I mean, instead of intro; simp; rcases you can do rintro (_ | ⟨_, _ | ⟨_, _ | ⟨_, _ | _⟩⟩⟩) although I would need some time to explain why that works

lemma mem_doubleTranspositions_iff {σ : Perm (Fin 4)} :
    σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ := by
  constructor
  · rintro (_ | ⟨_, _ | ⟨_, _ | ⟨_, _ | _⟩⟩⟩)
    repeat
      exact ⟨_, _, _, _, by decide, by decide, by decide, rfl⟩
  · intro h
    rcases h with ⟨a, b, c, d, hab, hcd, hdisj, rfl⟩
    decide +revert

So the lemma is now like this. It is totally a magic! But I also need some time to explain why that works. And I do want to ask how can you write such a brief code even you cannot explain why it works? It might be a unbelievable ability for me to learn.

[Sébastien Gouëzel]

As I wrote above, an even better (and shorter) proof is

lemma mem_doubleTranspositions_iff {σ : Perm (Fin 4)} :
    σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ := by
  revert σ
  simp only [doubleTranspositions, IsDoubleTransposition]
  decide

It says: expand the definition of doubleTranspositions and IsDoubleTransposition, and then check for each individual permutation that the result is true. Since there are finitely many permutations to check, it's fine.

[Sébastien Gouëzel]

Or the even shorter version

lemma mem_doubleTranspositions_iff {σ : Perm (Fin 4)} :
   σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ := by
  simp only [doubleTranspositions, IsDoubleTransposition]
  decide +revert

[Nick_adfor]

If I write

def allThreeCycles : List (Perm (Fin 4)) :=
  [swap 0 1 * swap 0 2,  -- (0 1 2)
   swap 0 2 * swap 0 1,  -- (0 2 1)
   swap 0 1 * swap 0 3,  -- (0 1 3)
   swap 0 3 * swap 0 1,  -- (0 3 1)
   swap 0 2 * swap 0 3,  -- (0 2 3)
   swap 0 3 * swap 0 2,  -- (0 3 2)
   swap 1 2 * swap 1 3,  -- (1 2 3)
   swap 1 3 * swap 1 2]  -- (1 3 2)
--lean does not have a good way to define a list of all 3-cycles, so I use swap products.

lemma mem_allThreeCycles_iff {σ : Perm (Fin 4)} :
    σ ∈ allThreeCycles ↔ σ.IsThreeCycle := by
  revert σ
  simp only [allThreeCycles, IsThreeCycle]
  decide

Then it cannot work. Why that? The tactic seems a failure for ThreeCycles.

[Nick_adfor]

Sébastien Gouëzel said:

Or the even shorter version

lemma mem_doubleTranspositions_iff {σ : Perm (Fin 4)} :
   σ ∈ doubleTranspositions ↔ IsDoubleTransposition σ := by
  simp only [doubleTranspositions, IsDoubleTransposition]
  decide +revert

I seem to know something. "decide + revert" means if it can decide, then decide, if cannot, then first revert, second decide. (I don't know if the explanation is right.)

[Nick_adfor]

lemma Equiv.Perm.IsThreeCycle.exists_swap_mul_swap {σ : Perm (Fin 4)}
    (h : σ.IsThreeCycle) :
    ∃ a b c : Fin 4, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ σ = swap a b * swap a c := by
  have : σ ∈ allThreeCycles := by sorry

I may seem to introduce a new lemma, and seems that it can "decie", too, but I do not know how to write this.