CODEWITHSUNDEEP
prooftheorem-provinglean
Bobjoesmith
Bobjoesmith

Reputation: 121

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!

Upvotes: 2

Views: 2512

Answers (2)

Mario Carneiro
Mario Carneiro

Reputation: 1703

"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.

Upvotes: 3

Christopher Hughes
Christopher Hughes

Reputation: 1129

There is no such type called Proof. The docs mention it as an example of how Lean could have been implemented, but go on to explain why it was not implemented like that.

Upvotes: 5

Related Questions