From 01a28e2a4a54b66ecba994742434ea29737dfaa4 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 31 Mar 2024 21:14:12 -0400 Subject: [PATCH] New post --- content/blog/integer-sets-lean4.md | 515 +++++++++++++++++++++++++++++ 1 file changed, 515 insertions(+) create mode 100644 content/blog/integer-sets-lean4.md diff --git a/content/blog/integer-sets-lean4.md b/content/blog/integer-sets-lean4.md new file mode 100644 index 0000000..19b91f9 --- /dev/null +++ b/content/blog/integer-sets-lean4.md @@ -0,0 +1,515 @@ +--- +title: "Working with integer sets in Lean 4" +date: 2024-03-31T21:10:23-04:00 +draft: false +tags: ["Formal Methods"] +math: true +medium_enabled: false +--- + +Recently I was convinced by [James Oswald](https://jamesoswald.dev/) 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$ + +```lean4 +def A : Set Int := {x : Int | x^2 = 9} +``` + +We want to prove the following lemma: + +```lean4 +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. + +```lean4 +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. + +```lean4 +#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. + +```lean4 +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. + +```lean4 +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 + +```lean4 +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! + +```lean4 +have H2 : ↑S ⊆ A := by decide +``` + +For the other side, + +```lean4 +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 + +```lean4 +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$. + +```lean4 +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! + +```lean4 +exact eq_or_eq_neg_of_sq_eq_sq n 3 H1_1 +``` + +[(Quite the long name...)](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GroupPower/Ring.html#eq_or_eq_neg_of_sq_eq_sq) + +Lastly, we combine the two subset proofs to show equality + +```lean4 +exact And.intro H1 H2 +``` + +All together the proof looks like: + +```lean4 +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$. + +```lean4 +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`. + +```lean4 +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. + +```lean4 +#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. + +```lean4 +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 + +```lean4 +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$. + +```lean4 +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$. + +```lean4 +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. + +```lean4 +omega +``` + +With both sides subset proven, we use and introduction to prove the goal + +```lean4 +exact show ((B ⊆ ↑S) ∧ (↑S ⊆ B)) from And.intro H1 H2 +``` + +The full proof is below. + +```lean4 +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. + +```lean4 +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. + +```lean4 +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. + +```lean4 +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 + +```lean4 +have H1 : a ≥ 0 ∨ a < 0 := le_or_lt 0 a +``` + +For a positive $a$, we can rely on the `linarith` tactic + +```lean4 +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 + +```lean4 +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$. + +```lean4 +exact Or.elim H1 H_LEFT H_RIGHT +``` + +All together the lower bound proof is the following + +```lean4 +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. + +```lean4 +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. + +```lean4 +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 + +```lean4 +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. + +```lean4 +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 + +```lean4 +-- 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 + +```lean4 +show False +``` + +So let's go through each disjunct in `H1_4` and show that we derive a contradiction. + +```lean4 +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 + +```lean4 +rewrite [H1_4] at H1_1 +contradiction +``` + +We can finally put it all together with and introduction + +```lean4 +exact show C ⊆ ∅ ∧ ∅ ⊆ C from And.intro H1 H2 +``` + +All together it's the following: + +```lean4 +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. +