Structured proofs?

Stream: new members

[jsodd]

I've been reading The Hitchhiker's Guide to Logical Verification and found a chapter on "structured proofs", but for some reason most of their code doesn't work for me. Is this something deprecated and we don't do this kind of forward proofs without entering tactic mode anymore or the things have new names now?

Here's an example from the book which doesn't work:

theorem And_swap (a b : Prop) :
  a ∧ b → b ∧ a :=
  assume hab : a ∧ b
  have ha : a :=
    And.left hab
  have hb : b :=
    And.right hab
  show b ∧ a from
    And.intro hb ha

Specifically, assume and show do not work here.

[Kyle Miller]

assume doesn't exist anymore, and I'm not sure it was replaced with anything.

You can instead write

theorem And_swap (a b : Prop) :
    a ∧ b → b ∧ a :=
  fun hab : a ∧ b =>
  have ha : a :=
    And.left hab
  have hb : b :=
    And.right hab
  show b ∧ a from
    And.intro hb ha

[Kyle Miller]

The tactic version is almost the same:

theorem And_swap (a b : Prop) :
    a ∧ b → b ∧ a := by
  intro (hab : a ∧ b)
  have ha : a :=
    And.left hab
  have hb : b :=
    And.right hab
  exact show b ∧ a from
    And.intro hb ha

(Not sure about exact show as a pattern, and I probably would write exact (And.intro hb ha : b ∧ a) if I really wanted to include the type)

[jsodd]

image.png
fix also doesn't seem to work

[Kyle Miller]

What it says about let being (fun x => ...) t is incorrect by the way

[jsodd]

So, is the notion of "structured proof" from this book in some sense deprecated?

[Kyle Miller]

let is one of the raw proof terms

[Kyle Miller]

I can't say, I'm not familiar with the book

[Kyle Miller]

But fix and assume do not exist in Lean 4. Potentially this part of the book came from Lean 3.

[Julian Berman]

Just to be sure, I haven't read the book (yet) -- but I know there are multiple versions I believe for each semester it's taught. Are you reading the 2024 version (which casually does seem to be using Lean 4)?

[Julian Berman]

It lives here I believe: https://github.com/blanchette/interactive_theorem_proving_2024/tree/main/lean

[jsodd]

It seems that I'm reading a 2023 version which I took from learning resources page on lean website and there already exists 2024.

[Kyle Miller]

I did some poking around, and you're supposed to be using the LoVe library. These structured proof syntaxes are defined here: https://github.com/blanchette/logical_verification_2023/blob/main/lean/LoVe/LoVelib.lean#L30-L36

[jsodd]

image.png
But it also has fix on the very first page of the chapter

[jsodd]

Kyle Miller said:

I did some poking around, and you're supposed to be using the LoVe library. These structured proof syntaxes are defined here: https://github.com/blanchette/logical_verification_2023/blob/main/lean/LoVe/LoVelib.lean#L30-L36

So it's not a feature of lean itself?

[Kyle Miller]

Correct

[Kyle Miller]

The book is expecting that you're following along with its library.

[Kyle Miller]

(It could be helpful if this chapter mentioned that these are custom.)

[jsodd]

Okay, it seems that I've missed this recommendation. I'm not going to invest time in learning things which are not lean mainstream (hardly makes sense for a novice), but the book itself seems quite good. Thanks for the help!

[jsodd]

Just out of curiosity, what is the lean way of proving this without tactics? Just the first step, not the entire proof. What should there be instead of assume hall : ...? I tried using fun as above, but it didn't do the trick.

theorem Forall.one_point {α : Type} (t : α) (P : α → Prop) :
  (∀x, x = t → P x) ↔ P t :=
  Iff.intro
    (assume hall : ∀x, x = t → P x
     show P t from
       by
         apply hall t
         rfl)
    (assume hp : P t
     fix x : α
     assume heq : x = t
     show P x from
       by
         rw [heq]
         exact hp)

[Kyle Miller]

(Submitted an issue for the book by the way here)

[Kyle Miller]

fun seems to work:

theorem Forall.one_point {α : Type} (t : α) (P : α → Prop) :
  (∀x, x = t → P x) ↔ P t :=
  Iff.intro
    (fun hall : ∀x, x = t → P x =>
     show P t from
       by
         apply hall t
         rfl)
    (fun hp : P t =>
     fun x : α =>
     fun heq : x = t =>
     show P x from
       by
         rw [heq]
         exact hp)

[jsodd]

Is there a lazy way to avoid rewriting ∀x, x = t → P x manually? Some ?h trick...

[Kyle Miller]

Yeah, just delete the : and the type

[jsodd]

(I'm trying to better understand how to manually destruct such expressions)

[Kyle Miller]

None of the type ascriptions are needed here, since they can all be derived from the expected type.

theorem Forall.one_point {α : Type} (t : α) (P : α → Prop) :
    (∀x, x = t → P x) ↔ P t :=
  Iff.intro
    (fun hall => by
      apply hall t
      rfl)
    (fun hp x heq => by
      rw [heq]
      exact hp)

[jsodd]

And is it possible to avoid by mode altogether?

[Kyle Miller]

Yeah, it's always possible. Tactics are a way to construct proof terms.

One trick is using by?, which pretty prints what the tactic mode constructed. You might have to fiddle with the result because pretty printing doesn't always round trip.

[Kyle Miller]

theorem Forall.one_point {α : Type} (t : α) (P : α → Prop) :
    (∀x, x = t → P x) ↔ P t :=
  Iff.intro
    (fun hall => hall t rfl)
    (fun hp _ heq => heq ▸ hp)

[Kyle Miller]

The triangle line is sort of cheating, since that's rw for terms.

One possible replacement for that is cast (congr_arg P heq.symm) hp. It's worth getting familiar with congr_arg/congr_fun/congr to some degree, to get a feel for how something like simp works.

[Kyle Miller]

You can also write the triangle as Eq.recOn heq.symm hp, which is also sort of cheating because it calculates the motive argument to Eq.recOn automatically using the "eliminator elaborator".

[Kyle Miller]

Here's the manual version: Eq.recOn (motive := fun x _ => P x) heq.symm hp

[Kyle Miller]

(It's nice having access to the rw tactic to not have to write things like that!)

[jsodd]

Wow, thank you! Understanding how patterns are built seems important. I'll read more about congruences.

[jsodd]

It seems that everything here including the "structured"/"forward" style of the proof can be done within tactic mode, so there's no practical need for this. Just interesting to understand

[Kyle Miller]

Mathlib tends to use term proofs for simple lemmas like this, but more compressed (we call it "golfing", but we're not trying to shave off every keystroke), mostly to say "there is nothing mathematically interesting here, no need to read this".

Here's how it would probably be written in this style:

theorem Forall.one_point {α : Type} (t : α) (P : α → Prop) :
    (∀x, x = t → P x) ↔ P t :=
  ⟨fun hall => hall t rfl, fun hp _ heq => heq ▸ hp⟩

It's worth knowing how basic tactics relate to basic terms so that you can "degolf" it if needed.

[Kyle Miller]

Oh, just found the mathlib version, you can confirm: docs#forall_eq