The Mechanics of Proof, Exercise 2.1.9.3

Stream: general

[Full name or 名前]

Hello!

I'm following "The Mechanics of Proof" book and am stuck at Exercise 2.1.9.3.

I came up with the following solution:

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
  have h3 : x * y > 0 := by addarith [h]
  cancel x at h3
  calc
    y = y / 1       := by ring
    _ = y / (x * y) := by rw [h]
    _ = 1 / x       := by ring
    _ ≤ 1 / 1       := by rel [h2]
    _ ≤ 1           := by numbers

Yet it fails on _ = 1 / x := by ring step:

▶ 1 goal
x y : ℚ
h : x * y = 1
h2 : x ≥ 1
h3 : 0 < y
⊢ y / (x * y) = 1 / x

▶ 95:27-95:31: error:
ring failed, ring expressions not equal
x y : ℚ
h : x * y = 1
h2 : x ≥ 1
h3 : 0 < y
⊢ y * y⁻¹ * x⁻¹ = x⁻¹

Is there any other tactic than ring which could allow me to cancel a positive variable divided by itself?

P.S. I'm using Lean v4.2.0 and Mathlib4 v4.2.0 (according to lake-manifest.json).

[Full name or 名前]

cc @Heather Macbeth

[Ruben Van de Velde]

Maybe field_simp?

[Kevin Buzzard]

Division and inverses are not axioms of a ring, so one should not expect ring to know things like $y\times y^{-1}=1$ for nonzero $y$.

[Full name or 名前]

Neither do this work:

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by
  have h3 : x * y > 0 := by addarith [h]
  cancel x at h3
  have h4 :=
    calc
      x * y = 1 := by rw[h]
      _ = 1 * 1 := by numbers
      _ ≤ 1 * x := by rel [h2]
  cancel x at h4 -- application type mismatch nonneg_of_mul_nonneg_left ...

application type mismatch
  nonneg_of_mul_nonneg_left h4
argument
  h4
has type
  x * y ≤ 1 * x : Prop
but is expected to have type
  0 ≤ ?m.113395 * x : Prop

[Ruben Van de Velde]

You've got x on the left and then on the right

[Full name or 名前]

Yeah, but how can I cancel them out? :thinking:

[Ruben Van de Velde]

I mean, you have $xy = 1x$ rather than $xy = x1$

[Full name or 名前]

Interesting... Now it compiles, but I get this error:

(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

[Full name or 名前]

The code is:

example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by -- (deterministic) timeout ...
  have h3 : x * y > 0 := by addarith [h]
  cancel x at h3
  have h4 :=
    calc
      x * y = 1 := by rw[h]
      _ = 1 * 1 := by numbers
      _ ≤ x * 1 := by rel [h2]
  cancel x at h4

[Heather Macbeth]

Strangely enough a colleague reported this exact example to me yesterday, as well. I think it's a reducibility setting -- but I also think the best fix will be a complete reimplementation (to mathlib standards of robustness) of this tactic, at which point I will also PR it to mathlib. Some previous discussion:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20The.20mechanics.20of.20proof.3A.20cancel.20tactic.20on.20a.5E2.20.3F/near/401470618

[Heather Macbeth]

In the short term: try the following endgame, which doesn't involve your last cancel step:
$y = 1\cdot y \le x y = 1$