Search code examples
prooftheorem-provinglean

Lean 4 'unknown identifier Proof'

I have been experiencing an issue when using Lean 4.

I ran into it while working my way through the docs, in the Propositions and Proofs section. Under Propositions as Types, the docs introduce the Proof Type:

We could then introduce, for each element p : Prop, another type Proof p, for the type of proofs of p.

Below, it shows a code snippet checking for the type of Proof, which returns Proof : Prop → Type:

#check Proof   -- Proof : Prop → Type

When I try running this snippet, I get the following error:

example.lean:3:7: error: unknown identifier 'Proof'

implying that lean can not find the Proof type. This is my problem, how do I get Lean to recognize Proof?

Thanks!

Solution

  • "Theorem Proving in Lean 4" is still under construction (indeed lean 4 itself is still changing rapidly), so you will probably find many issues in it. In this case, however, I believe the issue is that it is speaking hypothetically about one way things could be set up that is not in fact the way it is done in lean.

    Here's one way to make those code blocks actually compile:

    namespace TPIL

axiom Prop' : Type
axiom And : Prop' → Prop' → Prop'
axiom Or : Prop' → Prop' → Prop'
axiom Not : Prop' → Prop'
axiom Implies : Prop' → Prop' → Prop'
axiom Proof : Prop' → Type

variable (p q r : Prop')
#check And p q                      -- Prop'
#check Or (And p q) r               -- Prop'
#check Implies (And p q) (And q p)  -- Prop'

#check Proof   -- Proof : Prop' → Type

axiom and_comm (p q : Prop') : Proof (Implies (And p q) (And q p))

variable (p q : Prop')
#check and_comm p q     -- Proof (Implies (And p q) (And q p))

axiom modus_ponens : (p q : Prop') → Proof (Implies p q) →  Proof p → Proof q

axiom implies_intro : (p q : Prop') → (Proof p → Proof q) → Proof (Implies p q)

    You have to use Prop' or «Prop» since Prop is a keyword, though.