How to convert proofs of classical logic into proof terms?

Question

I saw from various tutorials that many proofs in lean 4 can be given using tactics or using proof terms (or a mixture of both). This makes sense to me given the constructive view of proofs as inductive data structures.

However, I cannot figure out how to convert proof tactics involving classical logic into proof terms. This includes by_cases and certain tactics about negation (by_contra, contrapose). For example, below is a proof about contrapose:

 example (P Q : Prop) (h : ¬P → ¬Q) : Q → P := by
  intro hq
  by_cases hp : P
  · exact hp
  · have := h hp
    contradiction

My question is:

How can I convert a proof with such tactics into a pure proof term (i.e. without entering the tactical mode or using the by)?

example (P Q : Prop) (h : ¬P → ¬Q) : Q → P := _

Note: the above proof may not be optimal. It's just something I came up with as an example. There is also another proof, but it requires mathlib:

import Mathlib.Data.Real.Basic
example (P Q : Prop) (h : ¬P → ¬Q) : Q → P := by
  contrapose! h
  apply and_comm.mp
  exact h

Answer 1

You can write show_term before the by to see a term mode proof. In this case it gives

 example (P Q : Prop) (h : ¬P → ¬Q) : Q → P := fun hq ↦
   if hp : P then hp
   else
     let_fun this := h hp;
     absurd hq this

that fails with "failed to synthesize Decidable P" (this is maybe a bug in show_term). Anyway, I guess that by_cases is using Clasical.em. If you start with

example (P Q : Prop) (h : ¬P → ¬Q) : Q → P := by
  intro hq
  cases Classical.em P with
  | inl H => exact H
  | inr H =>
    exfalso
    exact h H hq

you get

example (P Q : Prop) (h : ¬P → ¬Q) : Q → P := fun hq ↦
  Or.casesOn (motive := fun t ↦ Classical.em P = t → P) (Classical.em P) (fun H h ↦ H)
    (fun H h_1 ↦ False.elim (h H hq)) (Eq.refl (Classical.em P))

that works. You can golf it if you want

example (P Q : Prop) (h : ¬P → ¬Q) : Q → P := fun hq ↦
  Or.casesOn (Classical.em P) (fun H _ ↦ H)
    (fun H _ ↦ False.elim (h H hq)) (Classical.em P)