How can I reduce repetition without using tactics yet

Stream: new members

[Code Apprentice]

Hello Lean4 Community,

I'm a relative new comer with a background as a Software Engineer and strong undergraduate Mathematics. I'm intrigued by Lean to combine these two disciplines to formalize mathematics in a programming language. I'm working through the Theorem Proving in Lean 4 tutorial and am doing the exercises in Chapter 3 to prove several fundamental properties of boolean and first-order logic. I feel like my proofs are overly verbose even without using tactics. Can I get some feedback how to improve these? Keep in mind I'm only using the most basic syntax from Lean 4. I have read a very little bit about tactics, but I'm not using them yet as I want to learn the fundamentals. Also, I'm not using Mathlib yet, either. Thanks in advance for your advice.

-- associativity of ∧
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  Iff.intro
    (fun h : (p ∧ q) ∧ r =>
     have hp : p := And.left (And.left h)
     have hq : q := And.right (And.left h)
     have hr : r := And.right h
     show p ∧ (q ∧ r) from
     (And.intro hp (And.intro hq hr)))
    (fun h : p ∧ (q ∧ r) =>
     have hp : p := And.left h
     have hq : q := And.left (And.right h)
     have hr : r := And.right (And.right h)
     show (p ∧ q) ∧ r from
     (And.intro (And.intro hp hq) hr))

[Snir Broshi]

Welcome! :wave:

I'm intrigued by Lean to combine these two disciplines to formalize mathematics in a programming language

It's worth noting that Lean isn't the only theorem-prover that does this, see e.g. Rocq

As for verbosity, I think removing the type hints and the intermediate haves and using dot notation will get you very far.

1. Removing type hints:

-- associativity of ∧
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  Iff.intro
    (fun h =>
     have hp := And.left (And.left h)
     have hq := And.right (And.left h)
     have hr := And.right h
     (And.intro hp (And.intro hq hr)))
    (fun h =>
     have hp := And.left h
     have hq := And.left (And.right h)
     have hr := And.right (And.right h)
     (And.intro (And.intro hp hq) hr))

2. Using dot notation:

-- associativity of ∧
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  Iff.intro
    (fun h =>
     have hp := h.left.left
     have hq := h.left.right
     have hr := h.right
     (And.intro hp (And.intro hq hr)))
    (fun h =>
     have hp := h.left
     have hq := h.right.left
     have hr := h.right.right
     (And.intro (And.intro hp hq) hr))

3. Using angle brackets for constructors:

-- associativity of ∧
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  ⟨fun h =>
    have hp := h.left.left
    have hq := h.left.right
    have hr := h.right
    ⟨hp, ⟨hq, hr⟩⟩,
  fun h =>
    have hp := h.left
    have hq := h.right.left
    have hr := h.right.right
    ⟨⟨hp, hq⟩, hr⟩⟩

4. No intermediate haves:

example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  ⟨fun h => ⟨h.left.left, ⟨h.left.right, h.right⟩⟩,
  fun h => ⟨⟨h.left, h.right.left⟩, h.right.right⟩⟩

5. Going further, you can also destructure the hypothesis when defining the function:

-- associativity of ∧
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  ⟨fun ⟨⟨hp, hq⟩, hr⟩ => ⟨hp, ⟨hq, hr⟩⟩,
  fun ⟨hp, ⟨hq, hr⟩⟩ => ⟨⟨hp, hq⟩, hr⟩⟩

6. And the constructor syntax automatically nests things for you as long as they're to the right, so ⟩⟩ can usually be removed:

-- associativity of ∧
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  ⟨fun ⟨⟨hp, hq⟩, hr⟩ => ⟨hp, hq, hr⟩,
  fun ⟨hp, hq, hr⟩ => ⟨⟨hp, hq⟩, hr⟩⟩

[Snir Broshi]

btw to write angle-brackets use \< and \>, or \<> to get both at once

[Code Apprentice]

@Snir Broshi thanks for the response. I'll take a look at these suggestions when I have some time a little later. I think the destructuring syntax is the main thing I'm missing. Makes things nice and succinct.

[Chris Bailey]

The answer above is very good, but just for fun:

example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  ⟨fun ⟨⟨_, _⟩, _⟩ => ⟨‹_›,‹_›,‹_›⟩,
  fun ⟨_, _, _⟩ => ⟨⟨‹_›, ‹_›⟩, ‹_›⟩⟩

[Code Apprentice]

@Chris Bailey What is the <_>s? First of all, is that regular angle brackets rather than \< and \>? And what does it mean? Is this only used in the constructor syntax but not in the destructure syntax?

[Ilmārs Cīrulis]

image.png

[Ilmārs Cīrulis]

TIL, all thanks to Chris Bailey.

[Code Apprentice]

@Snir Broshi @Chris Bailey @Ilmārs Cīrulis Thanks everyone for the help. I completed the exercises for Chapter 3!

In case you are interested, they are here: https://github.com/codeguru42/lean4-tutorial/blob/main/Tutorial/Chapter3.lean.