# ~/Blog

## Brandon Rozek

PhD Student @ RPI studying Automated Reasoning in AI and Linux Enthusiast.

# 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


(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
)


The last $n = 6$ is under a different name

rewrite [H1_4] at H1_1


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
)

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

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.

Was this useful? Feel free to share: Hacker News Reddit Twitter

Published a response to this? :