6
$\begingroup$

Been trying to do this exercise from Section 3 of the tutorial for hours and I cannot get it to check. Here's my best attempt below (theorem dne provided by the book):

variable (p : Prop)

open Classical

theorem dne (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid : p ∨ ¬p :=
  dne (
    fun (h : ¬(p ∨ ¬p)) => 
    h (Or.intro_right (p) (step h))
  )

When I type-check my 'step' lemma, I get that it says "∀ (p : Prop), ¬(p ∨ ¬p) → ¬p". I thought that I can give 'step' something of type ¬(p ∨ ¬p) and it will return something of type ¬p, but when I check it on specific examples it doesn't do that.

I've tried a lot of other attempts but I don't get helpful feedback from the editor, so I'm not sure where it's going wrong (like below).

theorem excmid : p ∨ ¬p :=
  dne (
    fun (h : ¬ (p ∨ ¬p)) : False => 
    fun (h2 : p ∨ ¬p) : False =>
    have np : ¬p := fun (hp : p) => h2 (Or.intro_left (¬p) (hp))
    h h2 (Or.intro_right p np)
  )

Any help would be appreciated.

$\endgroup$
4
  • $\begingroup$ The first argument of your step is a prop p. The second argument is your h. Lean 4 has a fancy feature where you don’t have to make (p : Prop) explicit in the definition. $\endgroup$
    – Jason Rute
    Nov 19, 2022 at 3:47
  • $\begingroup$ I'm not sure I understand. Does that mean there's a hidden input to step that is being eaten at step h instead of the thing I intend? $\endgroup$
    – TFS19
    Nov 19, 2022 at 4:22
  • $\begingroup$ I don't know what your exercise actually was. But if it was to prove p ∨ ¬p in Lean, note, this is already there as em p, which you are using to prove dne. $\endgroup$
    – Jason Rute
    Nov 20, 2022 at 0:45
  • $\begingroup$ @JasonRute, the exercise is here: lean-lang.org/theorem_proving_in_lean4/… and the wording is "As an exercise, you might try proving the converse, that is, showing that em can be proved from dne." $\endgroup$ Dec 27, 2023 at 18:29

2 Answers 2

6
$\begingroup$

TLDR: Supply the argument p ∨ ¬ p to both dne and p to step, or use implicit arguments.


You are almost there!

The variable command

The variable (p : Prop) command can be a bit confusing. At first it looks like it is saying "for this whole section, just fix p to be a Prop", but the problem is what do you do with definitions and theorems which use this p? How do you use them inside this section (when variable (p : Prop) is in scope) and how do you use them outside this section (when variable (p : Prop) is no longer in scope!)? Lean simplifies this (compared to say Coq modules) and instead variable (p : Prop) actually just means "for this whole section, any theorem or definition which uses p gets (p : Prop) automatically added to its assumptions in the signature". When you use the theorem you have to supply a value for this p argument.

To make it more clear, here are four solutions (with an interlude on solving term proofs in Lean):

Solution 1

Instead of variable (p : Prop) we can just write (p : Prop) explicitly:

open Classical

theorem dne (p : Prop) (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (p : Prop) (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid (p : Prop) : p ∨ ¬p :=
  dne (p ∨ ¬p) (
    fun (h : ¬(p ∨ ¬p)) => 
    h (Or.intro_right (p) (step p h))
  )

Here we supply the proposition p ∨ ¬p to dne and p to step as the first argument.

Solution 2

In your MWE, we have variable (p : Prop). Nonetheless, we still have to explicitly supply that argument to both dne and step:

variable (p : Prop)

open Classical

theorem dne (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid : p ∨ ¬p :=
  dne (p ∨ ¬p) (
    fun (h : ¬(p ∨ ¬p)) => 
    h (Or.intro_right (p) (step p h))
  )

Lean errors

Note, if you don't supply the p argument to step, then Lean does give fairly helpful errors (but of course error messages can always be improved!).

application type mismatch
  step h
argument
  h
has type
  ¬(p ∨ ¬p) : Prop
but is expected to have type
  Prop : Type

This is saying that your first argument to step is wrong. You should be putting a Prop in the first argument slot, not a proof of ¬(p ∨ ¬p). When you print step, you get:

theorem step : ∀ (p : Prop), ¬(p ∨ ¬p) → ¬p :=
fun p h hp => h (Or.intro_left (¬p) hp)

You see the first argument comes from ∀ (p : Prop).

Using holes (_) to solve term proofs

Here is some advice to solving term proofs in Lean. The most helpful tool in making term proofs is holes, i.e. the underscore character. (Note, tactic proofs, which you will cover later are even easier!) You correctly noticed that your proof needs to start with dne. So we start with the template:

theorem exclmid : p ∨ ¬p :=
  dne _ _

Why two underscores? Zero, one, and three underscores give an error at dne, while two underscores only puts the error at the underscore, so we know that is the correct number of arguments to dne. Next, we hover over the two underscores. The first, says:

p: Prop
⊢ Prop

The second says:

p: Prop
⊢ ¬¬(p ∨ ¬p)

So the first must be a Prop and the second a proof of ¬¬(p ∨ ¬p). But these are not independent. The Prop in the first actually is linked to the proof in the second. So the only possible value for the first is p ∨ ¬p. Lean therefore automatically puts the p ∨ ¬p in for you when you do the first _.

A good way to solve a term proof is just to use this trick over and over again until you solved the theorem. So next you can start to fill the proof of ¬¬(p ∨ ¬p) in by replacing the second underscore with (fun h => _). Again, Lean will tell you both the type of h and the expected type of the new hole.

Solution 3: Implicit arguments

Notice that Lean is smart enough to know that the first argument to dne is p ∨ ¬p and to step is p. So one could have just written, say, step _ h in the examples above. Better however, would be to mark (p : Prop) as implicit in the theorems themselves. This can be done with either variable {p : Prop} or theorem step {p : Prop} (h : ¬(p ∨ ¬ p)) : ¬p. Now we don't have to supply that annoying first argument and the proof you wrote goes through as is!

variable {p : Prop}

open Classical

theorem dne (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid : p ∨ ¬p :=
  dne (
    fun (h : ¬(p ∨ ¬p)) => 
    h (Or.intro_right (p) (step h))
  )

Solution 4: Lean 4 magic

Finally, Lean 4 offers a bit of magic. If a variable like p in a definition or theorem, is just one symbol and its type (Prop in this case) can be inferred from the rest of the theorem, then it is automatically added as an implicit argument to the theorem signature. In this case {p : Prop} is added automatically to the theorem signature. That means all we have to do is take your MWE and remove the variable line!

open Classical

theorem dne (h : ¬¬p) : p :=
  Or.elim (em p)
  (fun (hp : p) => hp)
  (fun (hnp: ¬p) => absurd hnp h)

theorem step (h : ¬(p ∨ ¬ p)) : ¬p :=
  fun (hp : p) => h (Or.intro_left (¬p) (hp))

theorem exclmid : p ∨ ¬p :=
  dne (
    fun (h : ¬(p ∨ ¬p)) => 
    h (Or.intro_right (p) (step h))
  )

Magic!

$\endgroup$
2
  • $\begingroup$ Thanks! That was a lot of really useful information. One small correction I think is that in your first two solutions it should say dne (p ∨ ¬p) ( ... ) in theorem exclmid. Very nicely Lean figures that out itself in the implicit examples. Cheers! $\endgroup$
    – TFS19
    Nov 21, 2022 at 20:12
  • $\begingroup$ @TFS19 Thanks. (I thought I tested all this. :/) Fixed! $\endgroup$
    – Jason Rute
    Nov 21, 2022 at 23:02
2
$\begingroup$

Jason Rute's answer is really good. I rewrite it to make it more compact and clear.

  1. remove the open classical and theorem dne to avoid to prove an axiom.
  2. embed the next to rewrite the proof into an example.
example (dne : {p : Prop} -> (¬¬p -> p)): p ∨ ¬p :=
  dne (
    fun (h : ¬(p ∨ ¬p)) => 
    h (
      Or.inr (
        fun hp: p => h (Or.inl hp)
      )
    ) 
  )
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.