diff --git a/content/blog/induction-ints-coercing-nats-lean4.md b/content/blog/induction-ints-coercing-nats-lean4.md new file mode 100644 index 0000000..0634edc --- /dev/null +++ b/content/blog/induction-ints-coercing-nats-lean4.md @@ -0,0 +1,123 @@ +--- +title: "Coercing Ints to Nats for Induction in Lean 4" +date: 2024-03-27T21:51:02-04:00 +draft: false +tags: ["Formal Methods"] +math: true +medium_enabled: false +--- + +Warning: This post is what happens when I solve a problem that's already solved within Mathlib. I find it interesting enough to share though. Hopefully this will inspire techniques to use within your own proofs. + +--- + +Before getting into how to do induction on integers through nat coercion, let's discuss the proper way of solving this problem using `mathlib`. + +Let $x$ be an integer greater than some integer $m$. Show that $x$ satisfies some property. For example, prove $x > -5 \rightarrow x > -10$. + +Okay, I hear you, `linarith` can do this for us. Let's pretend that doesn't exist for now and show how we can go about solving this using `mathlib`. + +```lean4 +example (x : ℤ): x > -5 → x > -10 := by + -- Int.le_induction expects something of the form m ≤ x → ... + show -4 ≤ x → x > -10 + + -- Int.le_induction doesn't let you specify the + -- motive so you need to make it easy for it to induce + let P : ℤ → Prop := fun x => x > -10 + + -- Base Case + have H_base : P (-4) := by decide + + -- Inductive case + have H_ind : ∀ (n : ℤ), -4 ≤ n → P n → P (n + 1) := by + intro (n : ℤ) + intro (HH1 : -4 ≤ n) + intro (HH2 : n > -10) + show n + 1 > -10 + exact lt_add_of_lt_of_pos HH2 (show 0 < 1 by decide) + + -- Use the induction principle + exact show (-4 ≤ x → x > -10) from Int.le_induction H_base H_ind x +``` + +`Int.le_induction` is a nice and clean solution which I highly recommend you use. It makes sense too, prove that the property works for the lower bound and then prove the induction case holds. + +Now what if for some reason you couldn't rely `Int.le_induction` and you wanted to find another way to go about this? This is where coercion comes in. + +Starting from the beginning of the proof, this time let's introduce the hypothesis. + +```lean +intro (H : x > -5) +``` + +Now we want to create a natural number which we'll perform induction over. Similar to the mathlib proof, we want to start with the lower bound as the base case. Therefore, make it so when $x$ is the lower bound our new natural number variable $n$ is 0. + +```lean4 +let n : ℕ := Int.toNat (x + 5) +``` + +Our goal `x > -10` is still written in terms of the original variable $x$. To rewrite this, we'll need to prove the following relationship: + +```lean4 +have H1 : x = n - 5 := by + -- We should start off by saying this relationship + -- holds for the integer version of n + let nz : ℤ := x + 5 + have H1_1 : x = nz - 5 := eq_sub_of_add_eq (show nz = x + 5 by rfl) + suffices nz - 5 = n - 5 by rewrite [H1_1]; assumption + + -- Through congruence closure we can ignore the (- 5) + suffices nz = n by + let Minus5 : ℤ → ℤ := fun x => x - 5 + show Minus5 nz = Minus5 n + exact congrArg Minus5 this + + -- An integer coercion is only equal to a nat + -- if the integer was 0 or positive to begin with + have H1_2 : nz ≥ 0 := by + have H : nz - 5 > 0 - 5 := by rewrite [<- H1_1]; assumption + have H1 : nz - 5 ≥ 0 - 5 := Int.le_of_lt H + exact (Int.add_le_add_iff_right (-5)).mp H1 + + exact show nz = n from (Int.toNat_of_nonneg H1_2).symm +``` + +With $x$ written in terms of $n$, we can now rewrite our goal using our natural number. + +```lean4 +suffices n - 5 > (-10: ℤ) by rewrite [H1]; assumption +``` + +Here's the rest of the induction. Of course like before, I avoid the use of `linarith` so I wouldn't be cheating ;) + +```lean4 +have H_base : 0 - 5 > -10 := by decide + +have H_ind : ∀ n : ℕ, n - 5 > (-10 : ℤ) → (n + 1) - 5 > (-10: ℤ) := by + intro n + intro (IH : n - 5 > (-10 : ℤ)) + have IH : (-10: ℤ) < n - 5 := IH + show (-10: ℤ) < n + 1 - 5 + + have IH_2 : n + 1 - (5: ℤ) = n + (-5 : ℤ) + 1 := by calc + n + 1 - (5: ℤ) = n + 1 + (-5 : ℤ) := rfl + _ = n + (1 + (-5: ℤ)) := Int.add_assoc (↑n) 1 (-5) + _ = n + ((-5 : ℤ) + 1) := rfl + _ = n + (-5 : ℤ) + 1 := (Int.add_assoc (↑n) (-5) 1).symm + _ = n - (5: ℤ) + 1 := rfl + + suffices -10 < n - (5: ℤ) + 1 by rewrite [IH_2]; assumption + + exact lt_add_of_lt_of_pos IH (show 0 < 1 by decide) + +exact show n - 5 > (-10: ℤ) from Nat.recOn + (motive := fun x: ℕ => x - (5 : ℤ) > (-10: ℤ)) + n + H_base + H_ind +``` + +This version is slightly longer than the `Int.le_induction` version as we had to carry forward the `- 5` portion of the equations. While it might not make sense in the integer case to perform this coercion, I'm hopeful that I can use a technique similar to this on other inductive types in the future. + +Let me know if you end up using this or if you have any other cool induction techniques in your tool belt. Until next time.