## Stream: new members

### Topic: error when using theorem/lemma instead of def

#### Mikołaj Gradowski (Dec 18 2019 at 17:48):

Hello, I have a problem with the following snippet of code:

axiom a1  : Π { p q   : Prop },  p → (q → p)
axiom a2  : Π { p q r : Prop }, (p → (q → r)) → ((p → q) → (p → r))
axiom a3  : Π { p q   : Prop }, (p → q) → (¬q → ¬p)
axiom a4  : Π { p     : Prop },  ¬¬p → p
axiom a5  : Π { p     : Prop },  p → ¬¬p
axiom a6  : Π { p q   : Prop },  p ∧ q → p
axiom a7  : Π { p q   : Prop },  p ∧ q → q
axiom a8  : Π { p q r : Prop }, (p → q) → ((p → r) → (p → q ∧ r))
axiom a9  : Π { p q   : Prop },  p → p ∨ q
axiom a10 : Π { p q   : Prop },  q → p ∨ q
axiom a11 : Π { p q r : Prop }, (p → r) → ((q → r) → (p ∨ q → r))
axiom a12 : Π { p q   : Prop }, (p ↔ q) → (p → q)
axiom a13 : Π { p q   : Prop }, (p ↔ q) → (q → p)
axiom a14 : Π { p q   : Prop }, (p → q) → (q → p) → (p ↔ q)

def l1 { p q r : Prop} :=
@a1 ((p → (q → r)) → ((p → q) -> (p → r))) -- sub p
(q → r)                                -- sub q

def l2 { p q r : Prop} :=
l1 (@a2 p q r) -- MP

def l3 { p q r : Prop} :=
@a1
(q → r) -- sub p
p       -- sub q

def l4 { p q r : Prop} :=
@a2
(q → r)             -- sub p
(p → (q → r))       -- sub q
((p → q) → (p → r)) -- sub r

def l5 { p q r : Prop} :=
l4 (@l2 p q r) -- MP

def e1  { p q r : Prop} : (q -> r) -> ((p -> q) -> (p -> r)) :=
l5 (@l3 p q r) -- MP


I need to prove some theorems for my logic assignment using the Hilbert system above. The code works normally as it is, but when I change the defs to lemmas and theorems, Lean says that it cannot infer the type of the theorem/lemma, even though there is clearly enough information to do so, which deeply puzzles me.

I would be very grateful for an explanation and any general suggestions regarding my code, since I'm only making my baby steps with Lean.

Thanks!

#### Patrick Massot (Dec 18 2019 at 17:51):

I don't think you can have lemmas without explicitly giving the statement. At least that would look very weird

#### Patrick Massot (Dec 18 2019 at 17:53):

Since you are redoing such basic logic, it's probably dangerous to use the built in logic connectors. You could very well end up implicitly using what you are meant to prove.

#### Kevin Buzzard (Dec 18 2019 at 17:53):

If the definitions are compiling fine, then use #check to see the types of the lemmas and then when you switch to lemma/theorem, explicitly put the type in. I guess in theory Lean should be able to work out the type from the proof but on the other hand it's not something I've seen before.

#### Patrick Massot (Dec 18 2019 at 17:53):

You also have weird choices of implicit arguments if you need to use @ evreywhere.

#### Bhavik Mehta (Dec 18 2019 at 17:54):

Even if Lean could work out the type, it's still good practice to give the types of the things you've proved: it makes it easier to see what lemmas we've proved when reading code

#### Rob Lewis (Dec 18 2019 at 17:55):

I don't think you can have lemmas without explicitly giving the statement. At least that would look very weird

You can't, for more technical reasons than just "looking weird." Lean processes lemmas in parallel. Lemma b may reference lemma a, but get type checked before. This is fine, as long as it knows the type of a, since proofs are irrelevant. But if you don't give the type of a, it would have to process a first.

#### Kevin Buzzard (Dec 18 2019 at 17:55):

If you are trying to develop a theory of -> from first principles then you could use a different arrow to the one Lean already uses -- e.g. the one coming from \hom (assuming you're not going to be importing any category theory libraries...)

#### Mikołaj Gradowski (Dec 18 2019 at 17:57):

Wow, I didn't expect such quick and insightful feedback. It all seems reasonable to me now. Thanks for all the answers!

#### Kevin Buzzard (Dec 18 2019 at 17:58):

What Patrick is saying with the implicits is that if you write axiom a1 : Π ( p q : Prop ), p → (q → p) with ( not { then you don't have to use @ later on.

#### Mikołaj Gradowski (Dec 18 2019 at 17:59):

But then I'll have to explicitly instantiate each axiom every time, right?

#### Kevin Buzzard (Dec 18 2019 at 18:11):

I don't really know what that means (sorry, I'm a mathematician). All I know is that if you change { to ( then you don't have to write @. People tend not to use axioms in Lean. You could just be proving all of these things

Last updated: Dec 20 2023 at 11:08 UTC