Confusion with metavariables in "Mathematics in Lean"

Stream: new members

[Anand Jain]

Hello, I am working through Mathematics in Lean and I'm proving min (min a b) c = min a (min b c) and min a b + c = min (a + c) (b + c) from section 2.4. Both of them apply le_trans in a way that is confusing to me. In the first example,

example : min (min a b) c = min a (min b c) := by
  apply le_antisymm
  · apply le_min

giving proof state:
2 goals
case a.h₁
a b c d : ℝ
⊢ min (min a b) c ≤ a
case a.h₂
a b c d : ℝ
⊢ min (min a b) c ≤ min b c

after the le_min the solution applies le_trans which rewrites to 3 goals

3 goals
case a.h₁.a
a b c d : ℝ
⊢ min (min a b) c ≤ ?a.h₁.b✝
case a.h₁.a
a b c d : ℝ
⊢ ?a.h₁.b✝ ≤ a
case a.h₁.b
a b c d : ℝ
⊢ ℝ

Just by pattern matching I can (sort of) see that ?a.h1.b+ is min a b but I don't really see how the proof state gives any indication of that.

The second example is similar except I __really__ can't parse out what the hole is. Here is the full proof solution that I'm walking through

example : min a b + c = min (a + c) (b + c) := by
  apply le_antisymm
  · apply aux
  have h : min (a + c) (b + c) = min (a + c) (b + c) - c + c := by rw [sub_add_cancel]
  rw [h]
  apply add_le_add_right
  rw [sub_eq_add_neg]
  apply le_trans
  apply aux
  rw [add_neg_cancel_right, add_neg_cancel_right]

After le_trans

3 goals
case a.bc.a
a b c d : ℝ
h : min (a + c) (b + c) = min (a + c) (b + c) - c + c
⊢ min (a + c) (b + c) + -c ≤ ?a.bc.b✝
case a.bc.a
a b c d : ℝ
h : min (a + c) (b + c) = min (a + c) (b + c) - c + c
⊢ ?a.bc.b✝ ≤ min a b
case a.bc.b
a b c d : ℝ
h : min (a + c) (b + c) = min (a + c) (b + c) - c + c
⊢ ℝ

The confusing lines for me is apply le_trans and apply aux where aux is theorem aux : min a b + c ≤ min (a + c) (b + c). What is ?a.bc.b✝? And how does apply aux resolve the goals to

1 goal
case a.bc.a
a b c d : ℝ
h : min (a + c) (b + c) = min (a + c) (b + c) - c + c
⊢ min (a + c + -c) (b + c + -c) ≤ min a b

Sorry for the long message! Any clarity on how this is working would be really helpful

[Ruben Van de Velde]

So what apply le_trans does is saying "there is some ?c such that a ≤ ?c and ?c ≤ b" and ?c becomes just another new subgoal (of type \R). If you then solve the subgoal a ≤ ?c in a way that shows what the ?c needs to be, lean automatically fills in that subgoal as well.

Does that help at all?

[Ruben Van de Velde]

Notably, when you apply aux, lean can match the LHS with the LHS of the goal, and in that way decide what the a, b, and c arguments to aux need to be. Then lean also knows what the RHS of aux is, and this is what it needs to fill in the ?c from le_trans

[Richard Copley]

Compare this sad story, in which we make a wrong move after the le_trans and end up with a goal that can't be proved:

example : min a b + c = min (a + c) (b + c) := by
  apply le_antisymm
  · apply aux
  have h : min (a + c) (b + c) = min (a + c) (b + c) - c + c := by rw [sub_add_cancel]
  rw [h]
  apply add_le_add_right
  rw [sub_eq_add_neg]
  apply le_trans
  . have : min (a + c) (b + c) + -c ≤ max (a + c) (b + c) + -c := by
      apply add_le_add_right
      apply min_le_max
    exact this
  -- ⊢ max (a + c) (b + c) + -c ≤ min a b
  sorry