why show..from ?

Stream: new members

[E F Vincent]

Hi all - just starting so pardon the dumb question...

why would one choose to use show .. from syntax in the following example, when the most desugared version seems more straightforward and less like macro magic? Is the show..from syntax supposed to be more readable?

/-- `show .. from`  syntax for Or elimination -/
def ex1 (hPQ : p ∨ q) : q ∨ p :=
  Or.elim hPQ
    (λ (hP : p) => show q ∨ p from Or.intro_right q hP)
    (λ (hQ : q) => show q ∨ p from Or.intro_left  p hQ)

/-- desugars to `have` syntax -/
def ex2 (hPQ : p ∨ q) : q ∨ p :=
  Or.elim hPQ
    (λ (hP : p) => have hQP : q ∨ p := Or.intro_right q hP; hQP)
    (λ (hQ : q) => have hQP : q ∨ p := Or.intro_left  p hQ; hQP)

/-- which further desugars to a straight forward anon fn -/
def ex3 (hPQ : p ∨ q) : q ∨ p :=
  Or.elim hPQ
    (λ (hP : p) => Or.intro_right q hP)
    (λ (hQ : q) => Or.intro_left  p hQ)

[Kevin Buzzard]

Yes!

[Kevin Buzzard]

Why are you writing this code anyway? docs4#Or.symm is presumably already in core lean 4 and I would imagine that the proof is as minimal as possible. So probably you're writing it for teaching purposes, because you don't need to prove it again. So the form of the proof will depend on what you are trying to teach at that point.

[Kevin Buzzard]

Heh, the proof in core is great :-)

[E F Vincent]

The why - that's right I'm just trying to understand the purpose of show..from syntax, and there's little in the doc to explain why it exists, the proof is just an example. Also in VSCode one cannot navigate to the source code for show..from or from the having syntax, presumably because they're macros and go to definition function doesn't work on macros, so it's not easy to find the meaning. This file was the only mention I came across, and aside from pointing out how each syntax desugars, it doesn't really explain why it would exist.

[Martin Dvořák]

I suppose it exists because you might want to write something definitionally equivalent to the goal.

[Kevin Buzzard]

Yeah sometimes people use show to change the goal to something definitionally equal but syntactically different, so that a rewrite will work.

[E F Vincent]

got it ... perhaps the value will be more obvious as I experiment with less trivial examples - thanks for the feedback! :smile:

[Martin Dvořák]

This reminds me a question I wanted to ask but forgot (sorry for hijacking your thread): Does Lean 4 have an equivalent of Lean 3's change ... at ... ?

[Kevin Buzzard]

The last time someone asked this, the answer was revert h, change ... -> _, intro h. Sounds like a nice exercise for someone wanting to learn how to write tactics, if it's not done already

[Jireh Loreaux]

Martin Dvořák said:

This reminds me a question I wanted to ask but forgot (sorry for hijacking your thread): Does Lean 4 have an equivalent of Lean 3's change ... at ... ?

No, this still needs to be implemented I'm fairly sure.