decide for small finite sets and lists

Stream: new members

[Hugh]

lemma powerset_cases {x : ℕ} {n₁ n₂ n₃ : ℕ}
  (h1 : n₁ = 1) (h2 : n₂ = 2) (h3 : n₃ = 3)
  : ({n₁, n₂, n₃} : Finset ℕ).powerset =
  {{}, {n₁}, {n₂}, {n₃}, {n₁, n₂}, {n₂, n₃}, {n₃, n₁}, {n₁, n₂, n₃}} := by
  subst n₁ n₂ n₃
  decide

I'm trying to understand why decide doesn't work here with variables instead of literals (commenting out the subst line breaks). In general I want to understand how to solve this and other goals of the form {x, y} ⊆ {x, y, z}, [n₁, n₂, n₃] ∈ [n₁, n₂, n₃].permutations, and

lemma list_exists (l : List ℕ) (hl : l.length = 3)
  : ∃ x ∈ l, ∃ y ∈ l, ∃ z ∈ l, x ≠ y ∧ y ≠ z ∧ z ≠ x := by

I have a long proof by cases which involves 8 goals and manually choosing the correct or each time (is there a better way to do this too? i.e. avoiding long chains of right; right; ... left?), I've also tried fin_cases and hammer but couldn't get either to work.
My best guess is there is a combination of Finset.insert/Finset.mem lemmas to give to simp_all, but I couldn't find them.

[Weiyi Wang]

For why decide doesn't work for variables here, my guess is it can't handle the possibility of n_1 = n_2

[Aaron Liu]

import Mathlib

lemma list_not_necessarily_exists : ¬∀ (l : List ℕ) (hl : l.length = 3),
    ∃ x ∈ l, ∃ y ∈ l, ∃ z ∈ l, x ≠ y ∧ y ≠ z ∧ z ≠ x := by
  intro h
  specialize h [0, 0, 0] rfl
  simp at h

[Hugh]

Aaron Liu said:

import Mathlib

lemma list_not_necessarily_exists : ¬∀ (l : List ℕ) (hl : l.length = 3),
    ∃ x ∈ l, ∃ y ∈ l, ∃ z ∈ l, x ≠ y ∧ y ≠ z ∧ z ≠ x := by
  intro h
  specialize h [0, 0, 0] rfl
  simp at h

Oops, I conflated lists with sets here, there shouldn't be any x /= y
Really I just want to pattern match a list of len 3 with three new variables

[Aaron Liu]

The reason decide doesn't work with variables is that it's not designed to

[Aaron Liu]

You can clean up the free variables into bound variables with decide +revert, but then it won't be able to infer a Decidable instance.

[Hugh]

Aaron Liu said:

You can clean up the free variables into bound variables with decide +revert, but then it won't be able to infer a Decidable instance.

yeah this was one of the things I tried, I also tried to manually prove the instance but couldn't

[Aaron Liu]

Hugh said:

Really I just want to pattern match a list of len 3 with three new variables

You should have just said so!

import Mathlib

lemma List.eta_of_length_eq_three {α : Type*} {l : List α} (hl : l.length = 3) :
    l = [l[0], l[1], l[2]] :=
  match l with
  | [_, _, _] => rfl

[Hugh]

Weiyi Wang said:

For why decide doesn't work for variables here, my guess is it can't handle the possibility of n_1 = n_2

Tried adding hypotheses that none are equal to each other, but it looks like @Aaron Liu is right that decide is not meant for variables

[Hugh]

Aaron Liu said:

Hugh said:

Really I just want to pattern match a list of len 3 with three new variables

You should have just said so!

import Mathlib

lemma List.eta_of_length_eq_three {α : Type*} {l : List α} (hl : l.length = 3) :
    l = [l[0], l[1], l[2]] :=
  match l with
  | [_, _, _] => rfl

Is there a way to do this for sets?

[Aaron Liu]

Hugh said:

Is there a way to do this for sets?

Can you give a #mwe?

[Hugh]

Aaron Liu said:

Hugh said:

Is there a way to do this for sets?

Can you give a #mwe?

Sure!

import Mathlib
lemma Set.eta_of_length_eq_three {s : Finset ℕ} (hs : s.card = 3)
  : ∃ x ∈ s, ∃ y ∈ s, ∃ z ∈ s, x ≠ y ∧ y ≠ z ∧ z ≠ x := by
  sorry

[Aaron Liu]

Funny thing, I noticed the name Set.eta_of_length_eq_three doesn't follow the naming convention, so I renamed it to Finset.card_eq_three, and I got hit with

'Finset.card_eq_three' has already been declared

docs#Finset.card_eq_three

[Hugh]

Aaron Liu said:

Funny thing, I noticed the name Set.eta_of_length_eq_three doesn't follow the naming convention, so I renamed it to Finset.card_eq_three, and I got hit with

'Finset.card_eq_three' has already been declared

docs#Finset.card_eq_three

thanks

[Hugh]

In case anyone else has a similar problem, I eventually got it to work with the help of two reflexively equal lemmas:

import Mathlib

lemma powerset_singleton {n : ℕ}
  : ({n} : Finset ℕ).powerset = {∅, {n}}
  := by rfl

lemma singleton_insert_eq_union {n : ℕ} (s : Finset (Finset ℕ))
  : insert ({n} : Finset ℕ) s = ({{n}} : Finset (Finset ℕ)) ∪ s
  := by rfl

lemma powerset_cases {n₁ n₂ n₃ : ℕ}
  : ({n₁, n₂, n₃} : Finset ℕ).powerset =
  {{}, {n₁}, {n₂}, {n₃}, {n₁, n₂}, {n₂, n₃}, {n₁, n₃}, {n₁, n₂, n₃}} := by
  simp_all [Finset.powerset_insert, Finset.insert_comm, powerset_singleton, <- singleton_insert_eq_union]
  congr!

I understand why Mathlib wouldn't want to have lemmas that can be proven by rfl, but it seems like these would be pretty handy?

[Kenny Lau]

Hugh said:

I understand why Mathlib wouldn't want to have lemmas that can be proven by rfl

That is not true

[Kenny Lau]

I think you weren't very clear on what the goal was.

[Hugh]

Kenny Lau said:

I think you weren't very clear on what the goal was.

oh, I just wanted to learn how to work with small finite sets/lists, like computing a powerset, or like {x, y} ⊆ {x, y, z}, [n₁, n₂, n₃] ∈ [n₁, n₂, n₃].permutations

[Hugh]

after reading Finset.card_eq_three I'm pretty sure there isn't a general way though.

[Kenny Lau]

@Hugh one at a time, don't overwhelm yourself (and me),

import Mathlib

@[simp] lemma powerset_singleton {n : ℕ} : ({n} : Finset ℕ).powerset = {∅, {n}} := rfl

--lemma singleton_insert_eq_union {n : ℕ} (s : Finset (Finset ℕ)) :
--    insert ({n} : Finset ℕ) s = ({{n}} : Finset (Finset ℕ)) ∪ s :=
--  Finset.insert_eq _ _

lemma powerset_cases {n₁ n₂ n₃ : ℕ} : ({n₁, n₂, n₃} : Finset ℕ).powerset =
    {{}, {n₁}, {n₂}, {n₃}, {n₁, n₂}, {n₂, n₃}, {n₁, n₃}, {n₁, n₂, n₃}} := by
  simp [Finset.powerset_insert, ← Finset.insert_eq, Finset.insert_comm]

lemma foo1 {x y z : ℕ} : ({x, y} : Finset ℕ) ⊆ {x, y, z} := by
  intro s; aesop

lemma foo2 {n₁ n₂ n₃ : ℕ} : [n₁, n₂, n₃] ∈ [n₁, n₂, n₃].permutations := by
  simp

I agree that the simp lemmas above seem to be missing, but it's essentially by simp

[Kenny Lau]

the "general" way depends on what you want to do

[Kenny Lau]

I think that in general if you really want to use the power of decide, you need to first bring it to finite types

[Hugh]

Kenny Lau said:

the "general" way depends on what you want to do

thanks!

[Kenny Lau]

btw please note the spacing conventions, which I've corrected in my code

[Kenny Lau]

for example, decide can solve:

import Mathlib

lemma foo3 : (Finset.univ : Finset (Finset (Fin 3))) =
    {{}, {0}, {1}, {2}, {0, 1}, {0, 2}, {1, 2}, {1, 2, 3}} := by
  decide

[Hugh]

I was a bit lazy with foo2, in the general case its something like:

import Mathlib
lemma foo2 {n₁ n₂ n₃ : ℕ} : [n₂, n₁, n₃] ∈ [n₁, n₂, n₃].permutations := by
  simp

which simp doesn't close. Still very helpful though and much appreciated!

[Kenny Lau]

@Hugh yeah it seems like some simp lemmas are missing for it to work.

[Kenny Lau]

import Mathlib

lemma foo1 {n₁ n₂ n₃ : ℕ} : [n₂, n₁, n₃] ∈ [n₁, n₂, n₃].permutations := by
  simp [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.cons_swap]

lemma foo2 {a b c d e f : ℕ} : [b, d, a, e, f, c] ∈ [c, e, d, a, f, b].permutations := by
  simp [← Multiset.coe_eq_coe, ← Multiset.cons_coe, Multiset.cons_swap, ← Multiset.cons_zero]

[Kenny Lau]

@Hugh when you include code, please include the import Mathlib so that the code can compile on its own.

[Hugh]

Kenny Lau said:

Hugh when you include code, please include the import Mathlib so that the code can compile on its own.

will do!