error in thinking -> unexpected token 'calc'; expected ':='

Stream: new members

[rzeta0]

The following is my attempt to complete an exercise from Heather MacBeth's course.

There are two errors which I don't understand, and these in turn will probably lead to misunderstandings about wiring lean proofs.

example {x : ℝ} (hx : x ^ 2 + 2 * x - 3 = 0) : x = -3 ∨ x = 1 := by
  have h1 := by
    calc
      (x + 3) * (x - 1) = x ^ 2 + 2 * x - 3 := by ring
      _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  obtain ha | hb := h2
  left
  calc
    x = - 3 := by addarith [ha]
  right  -- <- error here "unexpected token 'calc'; expected ':='Lean 4"
  calc -- <-- error here "unexpected token 'calc'; expected ':='Lean 4"
    x = 1 := by addarith [ha]

Here is my thinking (which may be in error):

• as per tutorial, the idea is to set up a product $(x+3)(x-1)=0$ in preparation to use the lemma eq_zero_or_eq_zero_of_mul_eq_zero
• we then use the lemma to give us a disjunction which is $(x + 3 = 0) ∨ (x - 1 = 0)$
• we use obtain to split this into 2 cases, so this becomes a proof by cases
• the goal at this point is also a disjunction, x = -3 ∨ x = 1
• because it is a disjunction we use left and right to indicate which part we want to prove
• and then do each using a simple calc

Clearly there is some error in my thinking above. I'd welcome guidance.

Note: addarith is Macbeth's version of linarith

[Kevin Buzzard]

You should use \.. You should never have more than one goal, it's bad style, confusing to read etc.

[rzeta0]

Thanks Kevin,

The \. was discussed in a previous chat I was in, but I couldn't find any "official" tutorial to understand (1) what it actually does, and (2) where to use it (before left, before calc?)

To be fair, someone did say the \. "focussed" the goal state by excluding other goals outside the current case, but this wasn't sufficient exposition for a beginner like me.

[rzeta0]

The following, which uses \., perhaps incorrectly, also gives the same error:

example {x : ℝ} (hx : x ^ 2 + 2 * x - 3 = 0) : x = -3 ∨ x = 1 := by
  have h1 := by
    calc
      (x + 3) * (x - 1) = x ^ 2 + 2 * x - 3 := by ring
      _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  obtain ha | hb := h2
  left
  · calc
    x = - 3 := by addarith [ha]
  right
  · calc
    x = 1 := by addarith [ha]

The following variant also gives the error:

example {x : ℝ} (hx : x ^ 2 + 2 * x - 3 = 0) : x = -3 ∨ x = 1 := by
  have h1 := by
    calc
      (x + 3) * (x - 1) = x ^ 2 + 2 * x - 3 := by ring
      _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  obtain ha | hb := h2
  · calc
      x = - 3 := by addarith [ha]
  · calc
      x = 1 := by addarith [ha]

[Edward van de Meent]

i think the main issue here is that single-line calc tactics have trouble being parsed as intended, and are typically unnecessary. with regards to \.: put the left and right after the \., not before.

[Edward van de Meent]

if you want to show the goal state in your code, rather use show x = -3, like so:

import Mathlib

example {x : ℝ} (hx : x ^ 2 + 2 * x - 3 = 0) : x = -3 ∨ x = 1 := by
  have h1 := by
    calc
      (x + 3) * (x - 1) = x ^ 2 + 2 * x - 3 := by ring
      _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  obtain ha | hb := h2
  · left
    show x = -3
    sorry --addarith [ha] (commented out for troubleshooting in live-lean)
  · right
    show x = 1
    sorry -- addarith [ha]

[rzeta0]

Hi Edward - thanks for the comments. I need to understand what you're suggesting better so I have some follow up questions:

• how should one do a "one-line" calc?
• where can I read more about '\.' so that I can understand why it needs to go before left' and right`?
• I still don't really understand what '\.` does.
• what does show do? I've never seen it before. The doc string doesn't have an explanation suitable for beginners, it talks about "unification".

[rzeta0]

This works - but I don't know why - questions above:

example {x : ℝ} (hx : x ^ 2 + 2 * x - 3 = 0) : x = -3 ∨ x = 1 := by
  have h1 := by
    calc
      (x + 3) * (x - 1) = x ^ 2 + 2 * x - 3 := by ring
      _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  obtain ha | hb := h2
  · left
    calc
      x = x + 3 - 3 :=  by ring
      _ = 0 - 3 := by rw [ha]
      _ = - 3 := by numbers
  · right
    calc
      x = x - 1 + 1 :=  by ring
      _ = 0 + 1 := by rw [hb]
      _ = 1 := by numbers

[Edward van de Meent]

• as far as i can tell, one shouldn't. putting something in a one-linecalc doesn't meaningfully change the goal; it only allows you to do two things: use defeq to reword the goal, and show the goal state in the code rather than just in the infoview. both of these things can be done using show
• \. is called a "focusing dot". it acts like a tactic combinator which only allows the following (indented) tactics to act on the primary goal (hence focusing), and is used for a kind of hygiene. it additionally visualises some of the structure of a proof. it doesn't need to go before left and right, but it's the obtain ha | hb line that produces multiple goals, so putting the focusing dots right after that line is the "most hygienic"

[Edward van de Meent]

show is a tactic that tries to rewrite the goal via definitions to the goal you're describing. the docs reference a feature that seems to be a TODO

[Edward van de Meent]

an example of its usage:

variable (m n : ℕ)

example (h : m + 1 ≤ n * 3): (m < n * 3) := by
  show m + 1 ≤ n * 3
  exact h

here we're using the fact that a < b is defined to be equal to a + 1 ≤ b