# Working with integer sets in Lean 4

Published on

12 minute reading time

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
```

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.