Converting applicative proofs to tactical proofs

Stream: new members

[Lars Ericson]

In the Classical Logic section of Theorem Proving in Lean 4 there is an exercise "show that em can be proved from dne". @Jason Rute provides several proof versions on Proof Assistant's Stack Exchange and from these, @ZHAO Jiecheng rewrote the proof as a one-liner as follows:

theorem dne_implies_em (dne : {p : Prop} -> (¬¬p -> p)): p ∨ ¬p :=
  dne (fun (h : ¬(p ∨ ¬p)) => h (Or.inr (fun hp: p => h (Or.inl hp))))

#check dne_implies_em -- dne_implies_em {p : Prop} (dne : ∀ {p : Prop}, ¬¬p → p) : p ∨ ¬p

The one-liner is beautifully compact but hard to read. I broke it down into its components as follows:

variable (dne : {p : Prop} -> (¬¬p -> p))

variable (p : Prop)

variable (hp : p)

variable (h : ¬(p ∨ ¬p))

#check h (Or.inl hp) -- h (Or.inl hp) : False

#check Or.inr fun hp: p => h (Or.inl hp) -- Or.inr fun hp => h (Or.inl hp) : ?m.107 ∨ (p → False)

#check h -- h : ¬(p ∨ ¬p)

#check (Or.inr fun hp: p => h (Or.inl hp)) -- Or.inr fun hp => h (Or.inl hp) : ?m.144 ∨ (p → False)

#check h (Or.inr fun hp: p => h (Or.inl hp)) -- h (Or.inr fun hp => h (Or.inl hp)) : False

def term := fun (h : ¬(p ∨ ¬p)) =>
    h (
      Or.inr (
        fun hp: p => h (Or.inl hp)
      )
    )
#check term -- term (p : Prop) (h : ¬(p ∨ ¬p)) : False

#check term p -- term p : ¬(p ∨ ¬p) → False

#check dne (term p) -- dne (term p) : p ∨ ¬p

From Lean 3 exercises I find I am more comfortable with verbose tactic-mode proofs than with dense λ-style proofs (what is the adverb for these?). I'm not sure how to translate these separately #checked bits into a tactic-style proof. I hope to learn about that in a later section.

[Kyle Miller]

Term proofs can generally be turned into a sequence of intro and apply/exact/refine.

theorem dne_implies_em {p : Prop} (dne : {p : Prop} -> (¬¬p -> p)) : p ∨ ¬p := by
  apply dne
  intro h
  apply h
  apply Or.inr
  intro hp
  apply h
  apply Or.inl
  exact hp

[Lars Ericson]

Thanks @Kyle Miller. I was also looking for inspiration in the ProofWiki version. I wonder if MathLib obsoletes ProofWiki, except that the ProofWiki version pretty-prints (manually) into a possibly easier to comprehend series of steps:
image.png
Another idea would be to write a pretty-printer for Lean functional proofs that produces something like the ProofWiki tableau method table.

[Kyle Miller]

Try the #explode command

[Lars Ericson]

Thanks @Kyle Miller. What do I need to import to get this to work in Lean 4 playground? It says "expected token" in

theorem dne_implies_em (dne : {p : Prop} -> (¬¬p -> p)): p ∨ ¬p :=
  dne (fun (h : ¬(p ∨ ¬p)) => h (Or.inr (fun hp: p => h (Or.inl hp))))

#check dne_implies_em -- dne_implies_em {p : Prop} (dne : ∀ {p : Prop}, ¬¬p → p) : p ∨ ¬p

#explode dne_implies_em -- expected token

Also the #check is blue undersquiggled but the #explode is black with a red caret.
image.png

[Kyle Miller]

import Mathlib.Tactic.Common might be sufficient

[Kyle Miller]

import Mathlib.Tactic.Explode imports just that command

[Lars Ericson]

Thanks @Kyle Miller the second one works. Importing Common doesn't import Explode.