website/content/blog/integer-sets-lean4.md

title	date	draft	tags	math	medium_enabled
Working with integer sets in Lean 4	2024-03-31T21:10:23-04:00	false	Formal Methods	true	false

Recently I was convinced by James Oswald to work with him on proving some lemmas about specific integer sets in Lean 4. Since we have different styles in going about Lean proofs, I present my version here.

We'll go over three proofs today:

• \\{x \mid x \in \mathbb{Z} \wedge x^2 = 9\\} = \\{-3, 3\\}
• \\{x \mid x \in \mathbb{Z} \wedge -4 \le n \wedge n \le 15 ∧ Even~n \\} = \\{-4, -2, 0, 2, 4, 6, 8, 10, 12, 14\\}
• \\{x \mid x \in \mathbb{Z} \wedge x^2 = 6\\} = \emptyset

Example 1

First, let's define our set A

def A : Set Int := {x : Int | x^2 = 9}

We want to prove the following lemma:

lemma instA : A = ({3, -3} : Finset ℤ)

Recall that for sets, A = S \iff A \subseteq S \wedge S \subseteq A.

Since we're given a specific Finset for S, it would be really nice if we can compute whether S is a subset of A. In fact we can, as long as we prove a couple theorems first.

instance (n: Int) : Decidable (n ∈ A) := by
  suffices Decidable (n^2 = 9) by
    rewrite [A, Set.mem_setOf_eq]
    assumption
  apply inferInstance

First as shown above, we need to decide whether an integer is in A. Given how A is defined, this is equivalent to seeing if n^2 = 9. Luckily for us, the core of Lean already has a decision procedure for this. We can have Lean apply the appropriate one by calling apply inferInstance.

With this, we can now use #eval to see if elements are in A or not.

#eval List.Forall (· ∈ A) [-3, 3]

To say that a finite set S is a subset of A, is to say that all the elements of S are in A. Using the last theorem, we can prove that checking subsets in this direction is decidable.

instance (S : Finset Int) : Decidable (↑S ⊆ A) := by
  rewrite [A]
  rewrite [Set.subset_def]
  show Decidable (∀ x ∈ S, x ∈ {x | x ^ 2 = 9})
  apply inferInstance

Keep in mind that at this point it's not necessarily decidable if A \subseteq S. This is because we haven't established if A is finite. However instead of trying to prove finiteness, let's skip to the main proof and show that A = \\{3, -3\\} classically.

lemma instA : A = ({3, -3} : Finset ℤ) := by
  let S : Finset ℤ := {3, -3}
  change (A = ↑S)

As stated before, set equality is making sure both are subsets of each other

suffices A ⊆ ↑S ∧ ↑S ⊆ A by
  rewrite [Set.Subset.antisymm_iff]
  assumption

Lets make use of our decidability proof to show S \subseteq A in one line!

have H2 : ↑S ⊆ A := by decide

For the other side,

have H1 : A ⊆ ↑S := by
  intro (n : ℤ)
  -- Goal is now (n ∈ A → n ∈ {3, -3})
  intro (H1_1: n ∈ A)

Let's change H1_1 to be in a form easier to work with

have H1_1 : n^2 = 9 := by
  rewrite [A, Set.mem_setOf_eq] at H1_1
  assumption

To show that n \in \\{3, -3\\}, then it's the same as saying that n = 3 or n = -3.

suffices n = 3 ∨ n = -3 by
  show n ∈ S
  rewrite [Finset.mem_insert, Finset.mem_singleton]
  assumption

We can show this using a theorem from mathlib!

exact eq_or_eq_neg_of_sq_eq_sq n 3 H1_1

(Quite the long name...)

Lastly, we combine the two subset proofs to show equality

exact And.intro H1 H2

All together the proof looks like:

lemma instA : A = ({3, -3} : Finset ℤ) := by
  let S : Finset ℤ := {3, -3}
  change (A = ↑S)

  suffices A ⊆ ↑S ∧ ↑S ⊆ A by
    rewrite [Set.Subset.antisymm_iff]
    assumption

  have H1 : A ⊆ ↑S := by
    intro (n : ℤ)
    -- Goal is now (n ∈ A → n ∈ {3, -3})
    intro (H1_1: n ∈ A)
    have H1_1 : n^2 = 9 := by
      rewrite [A, Set.mem_setOf_eq] at H1_1
      assumption

    suffices n = 3 ∨ n = -3 by
      show n ∈ S
      rewrite [Finset.mem_insert, Finset.mem_singleton]
      assumption

    exact eq_or_eq_neg_of_sq_eq_sq n 3 H1_1

  have H2 : ↑S ⊆ A := by decide

  exact And.intro H1 H2

Example 2

We got to cheat a little by applying a mathlib theorem in the last example. This one will require a little more technique. First, let's start by defining our set B.

def B : Set Int := {n | -4 ≤ n ∧ n ≤ 15 ∧ n % 2 = 0}

As before, we can show that set membership in B is decidable. We can make use of the fact that each condition within it is decidable through And.decidable.

instance (n : Int) : Decidable (n ∈ B) := by
  suffices Decidable (-4 ≤ n ∧ n ≤ 15 ∧ n % 2 = 0) by
    rewrite [B, Set.mem_setOf_eq]
    assumption

  exact And.decidable

Sanity check to see that everything works as expected.

#eval List.Forall (· ∈ B) [-4, -2, 0, 2, 4, 6, 8, 10, 12, 14]

We can also show that checking if a finset is a subset of B is decidable.

instance (S : Finset Int) : Decidable (↑S ⊆ B) := by
  suffices Decidable (∀ x ∈ S, -4 ≤ x ∧ x ≤ 15 ∧ x % 2 = 0) by
    rewrite [Set.subset_def, B]
    assumption
  apply inferInstance

The beginning of our proof stays the same

lemma instB : B = ({-4, -2, 0, 2, 4, 6, 8, 10, 12, 14} : Finset Int) := by
  let S : Finset Int := {-4, -2, 0, 2, 4, 6, 8, 10, 12, 14}
  change (B = ↑S)

  -- To show equality, we need to show that
  -- each is a subset of each other
  suffices ((B ⊆ ↑S) ∧ (↑S ⊆ B)) by
    rewrite [Set.Subset.antisymm_iff]
    assumption
 
  have H2 : ↑S ⊆ B := by decide

For the other direction we want to show that is n meets the condition to be in B, then it must be in S.

have H1 : B ⊆ ↑S := by
  intro (n : ℤ)
  intro (H : n ∈ B)

  have H1 : -4 ≤ n ∧ n ≤ 15 ∧ n % 2 = 0 := by
    rewrite [B] at H; assumption
  clear H

  show n ∈ S

Since S is a finset, we can say that n must be equal to one of the elements of S.

repeat rewrite [Finset.mem_insert]
rewrite [Finset.mem_singleton]

At this point, the problem is integer arithmetic and we can call the omega tactic to finish the subproof.

omega

With both sides subset proven, we use and introduction to prove the goal

exact show ((B ⊆ ↑S) ∧ (↑S ⊆ B)) from And.intro H1 H2

The full proof is below.

lemma instB : B = ({-4, -2, 0, 2, 4, 6, 8, 10, 12, 14} : Finset Int) := by
  let S : Finset Int := {-4, -2, 0, 2, 4, 6, 8, 10, 12, 14}
  change (B = ↑S)

  -- To show equality, we need to show that
  -- each is a subset of each other
  suffices ((B ⊆ ↑S) ∧ (↑S ⊆ B)) by
    rewrite [Set.Subset.antisymm_iff]
    assumption

  have H1 : B ⊆ ↑S := by
    intro (n : ℤ)
    intro (H : n ∈ B)

    have H1 : -4 ≤ n ∧ n ≤ 15 ∧ n % 2 = 0 := by
      rewrite [B] at H; assumption
    clear H

    show n ∈ S
    repeat rewrite [Finset.mem_insert]
    rewrite [Finset.mem_singleton]
    omega

  have H2 : ↑S ⊆ B := by decide

  exact show ((B ⊆ ↑S) ∧ (↑S ⊆ B)) from And.intro H1 H2

Example 3

Finally let's define our last set.

def C : Set Int := {n | n^2 = 6}

We're aiming to show that C is equivalent to the empty set. Therefore, we don't have a need to show decidability for membership or finite subsets. We can't make use of the mathlib theorem from Example 1, so how will we go about proving this?

Analyzing the last example more carefully, we had upper and lower bounds to work with. We can similarly identify these bounds for this example.

Let's define the integer squared to be the upper bound.

lemma IntPow2GeSelf (H : (a : Int)^2 = z) : a ≤ z := by
  have H1 : a ≤ a ^ 2 := Int.le_self_sq a
  rewrite [H] at H1
  assumption

For the lower bound, take its negation.

lemma NegIntPow2LeSelf (H : (a : Int)^2 = z) : a ≥ -z := by

To prove the lower bound, split up between positives and negatives using the law of excluded middle

have H1 : a ≥ 0 ∨ a < 0 := le_or_lt 0 a

For a positive a, we can rely on the linarith tactic

have H_LEFT : a ≥ 0 → a ≥ -z := by
  have HL1 : a ≤ z := IntPow2GeSelf H
  intro (HL2 : a ≥ 0)
  linarith

For a negative a, we need to prove it by induction

have H_RIGHT : a < 0 → a ≥ -z := by
  intro (HR1: a < 0)
  have HR1 : a ≤ -1 := Int.le_sub_one_iff.mpr HR1
  revert HR1

  suffices a ≤ -1 → a ≥ -(a^2) by
    rewrite [<- H]; assumption

  let P : ℤ → Prop := fun x => x ≥ -(x^2)

  have H_base : P (-1) := by decide

  have H_ind : ∀ (n : ℤ), n ≤ -1 → P n → P (n - 1) := by
    intro (n : ℤ)
    intro (H21 : n ≤ -1)
    intro (H22 : P n)
    simp_all
    linarith

  exact Int.le_induction_down H_base H_ind a

We have shown that this lower bound holds for both positive and negative a, therefore we can show that it holds for all a.

exact Or.elim H1 H_LEFT H_RIGHT

All together the lower bound proof is the following

lemma NegIntPow2LeSelf (H : (a : Int)^2 = z) : a ≥ -z := by
  have H1 : a ≥ 0 ∨ a < 0 := by omega

  have H_LEFT : a ≥ 0 → a ≥ -z := by
    have HL1 : a ≤ z := IntPow2GeSelf H
    intro (HL2 : a ≥ 0)
    linarith

  have H_RIGHT : a < 0 → a ≥ -z := by
    intro (HR1: a < 0)
    have HR1 : a ≤ -1 := Int.le_sub_one_iff.mpr HR1
    revert HR1

    suffices a ≤ -1 → a ≥ -(a^2) by
      rewrite [<- H]; assumption

    let P : ℤ → Prop := fun x => x ≥ -(x^2)

    have H_base : P (-1) := by decide

    have H_ind : ∀ (n : ℤ), n ≤ -1 → P n → P (n - 1) := by
      intro (n : ℤ)
      intro (H21 : n ≤ -1)
      intro (H22 : P n)
      simp_all
      linarith

    exact Int.le_induction_down H_base H_ind a


  exact Or.elim H1 H_LEFT H_RIGHT

With our lower and upper bounds in place, we can look at the original problem. That is, we want to prove that C = \emptyset. We'll start the same proof like before.

example : C = (∅ : Set Int) := by
  suffices C ⊆ ∅ ∧ ∅ ⊆ C by
    rewrite [Set.Subset.antisymm_iff]
    assumption
  have H2 : ∅ ⊆ C := Set.empty_subset C

We start the other direction the same as well.

have H1 : C ⊆ ∅ := by
  intro (n : ℤ)
  intro (H1_1 : n ∈ C)
  have H1_1 : n^2 = 6 := by
    rewrite [C, Set.mem_setOf_eq] at H1_1
    assumption

Now bring in our bounds

have H1_2 : n ≤ 6 := by apply IntPow2GeSelf H1_1
have H2_3 : n ≥ -6 := by apply NegIntPow2LeSelf H1_1

We can use omega to show that if the integer is within these bounds then n must equal one of the integers.

have H1_4 :  n ∈ ({-6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6} : Finset ℤ) := by
  repeat rewrite [Finset.mem_insert]
  rewrite [Finset.mem_singleton]
  omega

Turn this set into a disjunction

-- Make H1_4 a disjunction (n = -6 ∨ ... ∨ n = 6)
repeat rewrite [Finset.mem_insert] at H1_4
rewrite [Finset.mem_singleton] at H1_4

Trying to show that n is within the empty set is the same as trying to prove a contradiction

show False

So let's go through each disjunct in H1_4 and show that we derive a contradiction.

repeat (
  cases' H1_4 with H1_4H H1_4
  -- Plug in n = ?? to n^2 = 6
  rewrite [H1_4H] at H1_1
  contradiction
)

The last n = 6 is under a different name

rewrite [H1_4] at H1_1
contradiction

We can finally put it all together with and introduction

exact show C ⊆ ∅ ∧ ∅ ⊆ C from And.intro H1 H2

All together it's the following:

example : C = (∅ : Set Int) := by

  suffices C ⊆ ∅ ∧ ∅ ⊆ C by
    rewrite [Set.Subset.antisymm_iff]
    assumption

  have H1 : C ⊆ ∅ := by
    intro (n : ℤ)
    intro (H1_1 : n ∈ C)
    have H1_1 : n^2 = 6 := by
      rewrite [C, Set.mem_setOf_eq] at H1_1
      assumption

    show False

    have H1_2 : n ≤ 6 := by apply IntPow2GeSelf H1_1
    have H2_3 : n ≥ -6 := by apply NegIntPow2LeSelf H1_1


    have H1_4 :  n ∈ ({-6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6} : Finset ℤ) := by
      repeat rewrite [Finset.mem_insert]
      rewrite [Finset.mem_singleton]
      omega

    -- Make H3 a disjunction (n = -6 ∨ ... ∨ n = 6)
    repeat rewrite [Finset.mem_insert] at H1_4
    rewrite [Finset.mem_singleton] at H1_4

    -- Try each one, plug in n = a into n^2 = 6 and show it doesn't work
    repeat (
      cases' H1_4 with H1_4H H1_4
      rewrite [H1_4H] at H1_1
      contradiction
    )

    -- Last n = 6 has a different name
    rewrite [H1_4] at H1_1
    contradiction


  have H2 : ∅ ⊆ C := Set.empty_subset C

  exact show C ⊆ ∅ ∧ ∅ ⊆ C from And.intro H1 H2

Conclusion

We gave three examples on working with finite integer sets. The two key lessons from this post are:

1. If the set is equal to a non-empty finite set, then try to prove decidability of membership and if a finset is a subset of it.

If you're looking at a set of integers and this set is constructed with conditions that are mostly built-in (such as the < relation), then this is hopefully not too difficult. Unfold the definitions of your set using rewrite and have Lean auto-infer which decidability instance to call using apply inferInstance

2. Try to establish a lower and upper bound for the elements of your set.

This gives the omega tactic something additional to work with. In the second example, omega was able to close out the goal completely given the linear inequalities presented. In our last example, we only used omega to construct a finite set of possible integers.

If you develop any other general techniques for dealing with integer sets let me know. Otherwise, feel free to get in touch with any questions you have.