Stream: new members

Topic: I'm missing something basic about construction in theorems

Matt Pillsbury (Dec 04 2022 at 00:57):

I tripped over an error message as I've been working my way through the exercises in *Theorem Proving in Lean 4*. This simple attempt at a proof...

variable (α : Type) (p q : α → Prop)

example : (∀ x, p x) ∧ (∀ x, q x) → (∀ x, p x ∧ q x) :=
(fun ⟨hp, hq⟩ =>
fun x => (hp x) ∧ (hq x))


...gives me this error message that I'm very puzzled by:

application type mismatch
And (_ : p x)
argument
hp x
has type  p x : Prop
but is expected to have type  Prop : Type


However, this seemingly equivalent approach works:

#check And.intro -- And.intro : ?m.21 → ?m.22 → ?m.21 ∧ ?m.22

example : (∀ x, p x) ∧ (∀ x, q x) → (∀ x, p x ∧ q x) :=
(fun ⟨hp, hq⟩ =>
fun x => And.intro (hp x) (hq x))


Where is the difference in the two proofs that breaks the first one?

Kevin Buzzard (Dec 04 2022 at 01:00):

And.intro makes the term. (hp x) ∧ (hq x) is the type. You can't prove a theorem by stating the theorem.

Kevin Buzzard (Dec 04 2022 at 01:02):

In fact (hp x) ∧ (hq x) is just a mess. If P and Q have type Prop then P ∧ Q has type Prop and it's the theorem statement. hp x is a proof, so it has type P for some P of type Prop. You're confusing types and terms.

Kevin Buzzard (Dec 04 2022 at 01:03):

def foo := 2 + 2 = 5. Do you understand what that means and why it works? I ask because I was confused about this when I was a beginner. Another example is def f := Nat -> Nat.

Matt Pillsbury (Dec 04 2022 at 01:27):

I think I get it now, especially based on the last bit. I was confusing the type of And.intro with the term And.intro.

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC