Issue with proof syntax

Stream: new members

[Mike]

I've been trying to work out an example in S05 Proving Facts about Algebraic Structures from Mathematics in Lean

Here's what I have:

import MIL.Common
import Mathlib.Topology.MetricSpace.Basic

variable {α : Type*} [Lattice α]
variable (a b c : α)

example (h : ∀ x y z : α, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by
  have h₁ : a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c := by
    calc
      a ⊓ (b ⊔ c) ≤ a ⊓ (a ⊓ b ⊔ c) := by
        apply le_inf
        . show a ⊓ (b ⊔ c) ≤ a
          apply inf_le_left
        . show a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ c
          calc
            a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c) := by
              apply le_inf
              . show a ⊓ (b ⊔ c) ≤ a ⊔ c
                calc
                  a ⊓ (b ⊔ c) ≤ a := by apply inf_le_left
                  _ ≤ a ⊔ c := by apply le_sup_left
              . show a ⊓ (b ⊔ c) ≤ b ⊔ c
                apply inf_le_right
            _ = (c ⊔ a) ⊓ (c ⊔ b) := by apply sup_comm
            _ = c ⊔ (a ⊓ b) := by rw [h]
            _ = a ⊓ b ⊔ c := by apply sup_comm
  have h₂ : a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c) := by
    apply sup_le
    . show a ⊓ b ≤ a ⊓ (b ⊔ c)
      apply le_inf
      . show a ⊓ b ≤ a
        apply inf_le_left
      . show a ⊓ b ≤ b ⊔ c
        calc
          a ⊓ b ≤ b := by apply inf_le_right
          _ ≤ b ⊔ c := by apply le_sup_left
    . show a ⊓ c ≤ a ⊓ (b ⊔ c)
      apply le_inf
      . show a ⊓ c ≤ a
        apply inf_le_left
      . show a ⊓ c ≤ b ⊔ c
        calc
          a ⊓ c ≤ c := by apply inf_le_right
          _ ≤ b ⊔ c := by apply le_sup_left
  apply le_antisymm
  . apply h₂
  . apply h₁

There don't seem to be any issues with the proofs of h₁ or h₂, but there probably is something wrong with them. The last three lines aren't highlighted and I get an error that h₁ is an unresolved goal.

[Patrick Massot]

I think the entire proof layout is broken and the Lean parser is completely confused (I am certainly confused when reading your code).

[Patrick Massot]

Do you think you ever finished the proof of h₁?

[Patrick Massot]

I recommend commenting out the whole "proof" of h₁, replace it with sorry, try to fix the rest of the proof and then come back to actually proving h₁.

[Mike]

@Patrick Massot You're right! The proof of h₁ wasn't finished. I got it to work by breaking it apart and moving h₁ and h₂ into their own lemmas. When I did that, the syntax highlighting started working correctly again. The proof was sort of on the right track, but it needed some work.

lemma lemma_h1 (a b c : α) (h : ∀ x y z : α, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c := by
  calc
    a ⊓ (b ⊔ c) ≤ a ⊓ (a ⊓ b ⊔ c) := by
      apply le_inf
      . show a ⊓ (b ⊔ c) ≤ a
        apply inf_le_left
      . show a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ c
        calc
          a ⊓ (b ⊔ c) ≤ (c ⊔ a) ⊓ (c ⊔ b) := by
            apply le_inf
            . show a ⊓ (b ⊔ c) ≤ c ⊔ a
              calc
                a ⊓ (b ⊔ c) ≤ a := by apply inf_le_left
                _ ≤ c ⊔ a := by apply le_sup_right
            . show a ⊓ (b ⊔ c) ≤ c ⊔ b
              calc
                a ⊓ (b ⊔ c) ≤ b ⊔ c := by apply inf_le_right
                _ = c ⊔ b := by apply sup_comm
          _ = c ⊔ (a ⊓ b) := by rw [←h]
          _ = a ⊓ b ⊔ c := by apply sup_comm
    _ = (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c) := by
      rw [absorb2]
    _ = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) := by rw [sup_comm]
    _ = a ⊓ b ⊔ a ⊓ c := by rw[h]

lemma lemma_h2 (a b c : α) : a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c) := by
  apply sup_le
  . show a ⊓ b ≤ a ⊓ (b ⊔ c)
    apply le_inf
    . show a ⊓ b ≤ a
      apply inf_le_left
    . show a ⊓ b ≤ b ⊔ c
      calc
        a ⊓ b ≤ b := by apply inf_le_right
        _ ≤ b ⊔ c := by apply le_sup_left
  . show a ⊓ c ≤ a ⊓ (b ⊔ c)
    apply le_inf
    . show a ⊓ c ≤ a
      apply inf_le_left
    . show a ⊓ c ≤ b ⊔ c
      calc
        a ⊓ c ≤ c := by apply inf_le_right
        _ ≤ b ⊔ c := by apply le_sup_right

example (h : ∀ x y z : α, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by
  apply le_antisymm
  . show a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
    apply lemma_h1
    . apply h
  . show a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c)
    apply lemma_h2

What was the most confusing earlier is that VS Code didn't show any issues with the proofs of either h₁ or h₂, so, it did look like it was finished. There weren't any syntax errors highlighted, and the "by" wasn't underlined in red (this also happens with Lean 4 Web). Lean Infoview didn't show any issues, either. Then what I was doing with them was really simple, so it seemed like it should have worked.

The solution provided is:

example (h : ∀ x y z : α, x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c := by
  rw [h, @sup_comm _ _ (a ⊓ b), absorb2, @sup_comm _ _ (a ⊓ b), h, ← inf_assoc, @sup_comm _ _ c a,
    absorb1, sup_comm]

but it's too compact. It's way above my Lean4 fluency level.

[Ruben Van de Velde]

Are you aware that you can move your cursor through the rw call to see the intermediate states?

[Mike]

@Ruben Van de Velde Thanks! That helps!

[Patrick Massot]

Mike, a very important difference between your proof and the solution is that the solution is chaining equalities, it features no inequalities. So you could try to rewrite it as a single calc command, without inequality.

[Mike]

@Patrick Massot You're right that the proof I gave is really sub-optimal! I mostly just care about figuring out how to make the syntax work...

Here's a really simple example of something that's giving me problems:

import Mathlib.Topology.MetricSpace.Basic

variable {R : Type*} [StrictOrderedRing R]
variable (a b c : R)

lemma small_lemma : b*c + -a*c = b*c - a*c := by
  sorry

It seems like it should work with something like rw [sub_eq_add_neg], but I cannot get it to recognize the grouping b*c and a*c. Looking at the solution to the examples, I know I don't need to use small_lemma, but I still would like to know how to get something simple like that to work.

[Ruben Van de Velde]

Your lemma has (-a) * c, not -(a * c), so you need to deal with that first

[Ruben Van de Velde]

import Mathlib.Topology.MetricSpace.Basic

variable {R : Type*} [StrictOrderedRing R]
variable (a b c : R)

lemma small_lemma : b*c + -a*c = b*c - a*c := by
  rw [neg_mul]
  rw [sub_eq_add_neg]

[Mike]

@Ruben Van de Velde Thank you!!

[Kevin Buzzard]

You can see where the brackets are in your code by hovering over operators in the infoview