4
$\begingroup$

Does Lean 4 have a good way of handling data type conversion (e.g. between the natural and real numbers)?

I am trying to solve the following property from the Mechanics of Proof book:

$\forall a \in Z, a ^ 2 - 5 * a + 5 ≤ -1 ↔ a = 2 ∨ a = 3$

In lean:

example {a : ℤ} : a ^ 2 - 5 * a + 5 ≤ -1 ↔ a = 2 ∨ a = 3 := by
  sorry

The arithmetic is simple enough if one views the number $a$ as a real or rational number, and that

$a ^ 2 - 5 * a + 5 = (a - 5/2) ^ 2 - 5/4$

Then, this translates to

$ (a - 5/2) ^ 2 \leq 1/4 $

or eventually to

$ 2 \leq a \leq 3$

If one views $a$ as integer again, $a = 2 \lor a = 3$ follows.

But how can I switch the context and use $a$ as an integer sometimes and sometimes as real numbers.

Directly using $a$ as a real number doesn't work. For example, I tried:

  have ha : a ^ 2 - 5 * a + 5 = (a - 5/2) ^ 2 - 5/4    := by ring

, and this gives an error:

ring failed, ring expressions not equal.

I then tried:

have ha : (a : ℝ) ^ 2 - 5 * a + 5 = (a - 5/2) ^ 2 - 5/4    := by ring

This seems to check. But the VSCode inforview shows the equation with an up-arrow prepended to the variable a.

ha : ↑a ^ 2 - 5 * ↑a + 5 = (↑a - 5 / 2) ^ 2 - 5 / 4

I am not sure what ↑a is, or how to use it in the proof that follows.

Hence, the question here.

In Lean 4, how can I convert between different number types during a proof?

Note:

I know that I can probably get away with a workaround by multiplication and bring everything back to integer:

  have ha : 4 * (a ^ 2 - 5 * a + 5 ) = (2 * a - 5) ^ 2 - 5    := by ring

But in general, there is no guarantee such tricks to bring things to integer would work. For example, what if the condition in question was:

a ^ 2 - 5 * a + 5 ≤ -0.9
$\endgroup$
2
  • $\begingroup$ I fixed my answer, including giving tactics for working with coercions. I think this should give you the information you need to work with your example and be a good resource to others. $\endgroup$
    – Jason Rute
    Commented Jun 23 at 19:53
  • $\begingroup$ Note that my answer may not be in the spirit of MiL. I haven't read the book, and I don't know the intended solution. $\endgroup$
    – Jason Rute
    Commented Jun 23 at 19:56

1 Answer 1

3
$\begingroup$

This is a reasonable approach. You prove this by "relaxing" a to be a real number, namely proving 2 <= (a : Real) <= 3 and then using that to deduce 2 <= (a : Int) <= 3. I'll let you handle how to prove 2 <= (a : Real) <= 3, but let's talk about converting between Int and Real, and more generally casting from one type to another.

Coercion basics

If a has type Int and you write a : Real, what you are telling Lean to do is coerce a from Int to Real. So a is replaced with ↑a. This uparrow symbol (written \u or \uparrow in the Lean vs code plugin) is shorthand for @Int.cast ℝ Real.instIntCast a. You can find this out by hovering over ↑a in the infoview. It also gives this helpful message:

↑x represents a coercion, which converts x of type α to type β, using typeclasses to resolve a suitable conversion function. You can often leave the off entirely, since coercion is triggered implicitly whenever there is a type error, but in ambiguous cases it can be useful to use to disambiguate between e.g. ↑x + ↑y and ↑(x + y).

As this message suggests, if Lean is expecting a real number, as in a < Real.pi, then a, ↑a, and (a : ℝ) are all the same.

#check ∀ a : ℤ, a < Real.pi        -- ∀ (a : ℤ), ↑a < Real.pi
#check ∀ a : ℤ, ↑a < Real.pi       -- ∀ (a : ℤ), ↑a < Real.pi
#check ∀ a : ℤ, (a : ℝ) < Real.pi  -- ∀ (a : ℤ), ↑a < Real.pi

One case where a alone wouldn't work is when the expression is valid as either an Int or a Real. In that case, you have to specify the coercion using (a : ℝ) in at least one place.

#check ∀ a : ℤ, ((a : ℝ) / 2) * 2 = a  -- ((a : ℝ) / 2) * 2 = a

It is not enough here to just use ↑a since Lean doesn't know what to coerce to. For example, this doesn't coerce at all:

#check ∀ a : ℤ, ↑a / 2 * 2 = a  -- ∀ (a : ℤ), a / 2 * 2 = a

Conversely, Lean seems to apply ↑a as far inside as possible. So sometimes one needs to explicitly use to specify where the conversion should be.

#check ∀ a : ℤ, ((a + a) : ℝ) = (a : ℝ) + (a : ℝ)
-- ∀ (a : ℤ), ↑a + ↑a = ↑a + ↑a
#check ∀ a : ℤ, (↑(a + a) : ℝ) = a + a
-- ∀ (a : ℤ), ↑(a + a) = ↑a + ↑a

Coersion can change the truth value of a theorem

The reason that

have ha : a ^ 2 - 5 * a + 5 = (a - 5/2) ^ 2 - 5/4    := by ring

failed, is that the theorem is false (and ring tells you this), because for the integers, 5/4 = 1 and 5/2 = 2.

#eval (5: ℤ ) / 4  -- 1
#eval (5: ℤ ) / 2  -- 2

(This is similar to say 5 // 4 and 5 // 2 in python if you are familiar with integer division in typical programming languages.)

So this brings us to an important point. Just because you prove a theorem for (a : ℝ) doesn't mean it still holds for a.

How to go back and forth between coercions?

It shouldn't be hard for you to prove 2 <= (a : Real) and (a : Real) <= 3, but that isn't your goal. You want 2 <= a and a <= 3 (which since a is an integer implies that a = 2 or a = 3).

This is a common case in coercions. While it isn't true in general that any theorem of (a : Real) is a theorem of a, it is true that many functions and relations are -invariant (meaning R_ℤ a b ↔ R_ℝ ↑a ↑b) and other functions are -equivariant (meaning ↑(f_ℤ a b) = f_ℝ ↑a ↑b).

These theorems should be readily available in Mathlib, but instead of looking them up, there are tactics to help.

norm_cast normalizes coercions (removing them if possible).

example (a : ℤ) (h : a < 9) : (a : ℝ) < 10 := by
  norm_cast -- normalizes coercions (removing them if possible) in goal
  /-
  a : ℤ
  h : a < 9
  ⊢ a < 10
  -/
  linarith [h]

example (a : ℤ) (h : (a : ℝ) < 9) : a < 10 := by
  norm_cast at h  -- normalizes coersions (removing them if possible) in the hypotheses `h`
  /-
  a : ℤ
  h : a < 9
  ⊢ a < 10
  -/
  linarith [h]

push_cast pushes coercions inward (again removing them if possible).

example (a b : ℤ) (h : a + b < 9) : ↑ (a + b) < 10 := by
  push_cast  -- pushes coercions inward (removing them if possible) in the goal
  /-
  a b : ℤ
  h : a + b < 9
  ⊢ a + b < 10
  -/
  linarith [h]

example (a b : ℤ) (h : ↑ (a + b) < 9) : a + b < 10 := by
  push_cast at h  -- pushes coercions inward (removing them if possible) in the hypothesis
  /-
  a b : ℤ
  h : a + b < 9
  ⊢ a + b < 10
  -/
  linarith [h]

exact_mod_cast and apply_mod_cast are versions of exact and apply which also normalizes coercions.

example (a : ℤ) (h : a < 10) : (a : ℝ) < 10 := by
  exact_mod_cast h  -- like `exact` but normalizes coercions first

example (a : ℤ) (h : (a : ℝ) < 10) : a < 10 := by
  exact_mod_cast h  -- like `exact` but normalizes coercions first

example (a : ℤ) (h : (a : ℝ) < 10) : a < 10 := by
  apply_mod_cast h -- like `apply` but normalizes coercions first

rify converts goals on , , , etc. to ℝ. There is also qify for rationals and zify for integers. The zify, qify, rify tactics require Mathlib, while the other ..._cast tactics are available in base Lean.

example (a : ℤ) (h : (a : ℝ) < 9) : a < 10 := by
  rify -- converts goal to reals (use `zify` for ℤ and `qify` for ℚ)
  /-
  a : ℤ
  h : ↑a < 9
  ⊢ ↑a < 10
  -/
  linarith [h]

example (a : ℤ) (h : (a : ℝ) < 10) : a < 10 := by
  rify [h]  -- `rify` using `h` as a simp lemma

Other coercions

There are a lot of coercions in Lean. They come up in natural settings where one wants to interpret one type as another because of some canonical embedding (usually a homomorphism).

There are coercions from ℕ to ℚ to ℝ to ℂ; coercions to and from Nat and Fin n; coercions from fields to rings to groups (the forgetful functor); coercions from ℕ to rings, and many more.

New coercions have to be registered so Lean knows about them. For more information see Coercions using Type Classes in Theorem Proving in Lean 4.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.