error when using theorem/lemma instead of def

Stream: new members

[Mikołaj Gradowski]

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]

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

[Patrick Massot]

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]

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]

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

[Bhavik Mehta]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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