Zulip Chat Archive

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


Last updated: Dec 20 2023 at 11:08 UTC