lean structure for a complicated (for me) logical proof

Stream: new members

[rzeta0]

As I learn lean I am doing exercises from Heather Macbeths course. The current one is the most complicated one that I have encountered.

The following is a recasting of the specifics into a more general question:

Given hypotheses:

$$h1 : (A \lor B) \\ h2 : (C \lor D)$$

We want to prove

$$(S \land T) \lor (U \land V)$$

My thoughts for casting this into Lean are:

• Since the proof goal is a disjunction, I only need to prove one of the two statements, let's choose left S \land T
• I use obtain to split h1 into A and B, and h2 into C and D
• I need to prove that all four possible combinations lead to the goal, that is : (A \land C), (A \land CD, (C \land C), (B \land D)

However, when I do this in Lean, it appears not to establish these 4 as goals to prove.

The following is a specific example:

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by

  left
  -- only prove a = 0 ∧ b = 0

  have ha := by
    calc
      a * (b - 1) = a * b - a := by ring
      _ = 0 := by addarith [h1]
  have hb := eq_zero_or_eq_zero_of_mul_eq_zero ha
  obtain hc | hd := hb
  -- hc: a = 0
  -- OR
  -- hd: b - 1 = 0

  have he := by
    calc
      b * (a - 1) = a * b - b := by ring
      _ = 0 := by addarith [h2]
  have hf := eq_zero_or_eq_zero_of_mul_eq_zero he
  obtain hg | hh := hf
  -- hg: b = 0
  -- OR
  -- hh: a - 1 = 0

The goals from the Infoview are:

3 goals
a b : ℝ
h1 : a * b = a
h2 : a * b = b
ha : a * (b - 1) = 0
hc : a = 0
he : b * (a - 1) = 0
hg : b = 0
⊢ a = 0 ∧ b = 0

a b : ℝ
h1 : a * b = a
h2 : a * b = b
ha : a * (b - 1) = 0
hc : a = 0
he : b * (a - 1) = 0
hh : a - 1 = 0
⊢ a = 0 ∧ b = 0

a b : ℝ
h1 : a * b = a
h2 : a * b = b
ha : a * (b - 1) = 0
hd : b - 1 = 0
⊢ a = 0 ∧ b = 0

I don't understand why:

• there are 3 goals, not 4
• why the combinations are not what I expected
• apparently contradictory hypotheses are listed eg hc: a=0 and hh: a-1 = 0

[Yakov Pechersky]

after your obtain hc | hd := hb line, since you didn't focus on a particular goal, the next lines automatically run only in the first created goal

[Yakov Pechersky]

so when you do obtain hg | hh := hf later, that is only in the hc context

[Yakov Pechersky]

It's also likely that taking left as your first step is premature.

[rzeta0]

Can I ask how a left can be too premature?

I ask because the answer will help my learning of how lean works - and should be used.

Logically I want to take the left. Procedurally I guess i can't take it too soon!

[Eric Paul]

I think it might be more clear what's happening if I rewrite your code using match.

The translation is
obtain ha | hb := something
is the same as

match something with
| .inl ha => stuff in this goal
| .inr hb => stuff in this goal

With this in mind, here is a rewritten version of what you have:

import Mathlib

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by

  left
  -- only prove a = 0 ∧ b = 0

  have ha := by
    calc
      a * (b - 1) = a * b - a := by ring
      _ = 0 := by addarith [h1]
  have hb := eq_zero_or_eq_zero_of_mul_eq_zero ha
  match hb with
  | .inl hc =>
    have he := by
      calc
        b * (a - 1) = a * b - b := by ring
        _ = 0 := by addarith [h2]
    have hf := eq_zero_or_eq_zero_of_mul_eq_zero he

    match hf with
    | .inl hg => sorry
    | .inr hh => sorry

  | .inr hd => sorry

Notice how when you are splitting up hf into hg and hh that that is only happening in the first branch of the original match and not in the second. That is why you end up with only three goals.

With regard to the left being premature:
You can write left whenever you want to, Lean allows it.
But it is worth noting that you can choose left within one goal and right within another and sometimes that is necessary. If you made the choice to go left before splitting into multiple goals, then each of the these goals must prove left as it has already been chosen. However, if you delay choosing left or right, then each goal can make its own choice.

For example, I'll write the same code I did above with match and have each branch of the match choose a different side. (I'm not claiming this is what you want to do, just showing an example.)

import Mathlib

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by

  have ha := by
    calc
      a * (b - 1) = a * b - a := by ring
      _ = 0 := by addarith [h1]
  have hb := eq_zero_or_eq_zero_of_mul_eq_zero ha
  match hb with
  | .inl hc =>
    left
    -- the goal in this branch is `a = 0 ∧ b = 0`
    have he := by
      calc
        b * (a - 1) = a * b - b := by ring
        _ = 0 := by addarith [h2]
    have hf := eq_zero_or_eq_zero_of_mul_eq_zero he

    match hf with
    | .inl hg => sorry
    | .inr hh => sorry

  | .inr hd =>
    right
    -- the goal in this branch is `a = 1 ∧ b = 1
    sorry

[rzeta0]

Using the replies that explain the "stack" in reply to my other question, I understand how lean wants me to prove the sub-goals a little better.

Initially I though the focussing dot was not that useful but it did help write the proof by filtering out the irrelevant "context" from the current sub-goal.

So here is my solution which seems to pass:

example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by

  have ha := by
    calc
      a * (b - 1) = a * b - a := by ring
      _ = 0 := by addarith [h1]
  have hb := eq_zero_or_eq_zero_of_mul_eq_zero ha

  obtain hc | hd := hb

  -- hc: a = 0
  · left
    constructor
    · apply hc
    · calc
      b = a * b := by rw [h2]
      _ = 0 * b := by rw [hc]
      _ = 0 := by ring

  -- hd: b - 1 = 0
  · right
    constructor
    · have he: b = 1 := by addarith [hd]
      have hf :=
        calc
          a * b = b := by rw [h2]
          _ = 1 * b := by ring
      cancel b at hf
    · addarith [hd]