but is expected to have type Prop : Type error

Stream: new members

[Arien Malec]

I'm working through the Theorem Proving book, and trying to prove associativity of and.

I've got

lemma and_assoc_right (p q r : Prop) : (p ∧ q) ∧ r → p ∧ (q ∧ r) :=
  assume hpqr: (p ∧ q) ∧ r,
  show p ∧ (q ∧ r), from and.intro hpqr.left.left (and.intro hpqr.left.right hpqr.right)

which typechecks just fine, but when I try to use it I get a strange error:

example (p q r : Prop) : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
  iff.intro
  ( assume h: (p ∧ q) ∧ r,
    show p ∧ (q ∧ r), from and_assoc_right h)
-- etc

type mismatch at application
  and_assoc_right h
term
  h
has type
  (p ∧ q) ∧ r : Prop
but is expected to have type
  Prop : Type

& I'm not sure what Lean is trying to tell me.

[Kyle Miller]

The first three arguments to and_assoc_right are p, q, and r themselves. To use it as written, you can write and_assoc_right _ _ _ h, where the underscores tell Lean to figure out p, q, and r from context.

[Kyle Miller]

If you alter and_assoc_right to have {p q r : Prop} in curly braces, then your example should work. This causes Lean to always try to figure out p, q, and r from context.

[Kyle Miller]

The type mismatch error you are seeing is from the fact that you are supplying h for p, but p is supposed to be a Prop.

[Arien Malec]

Ah -- mentally I think I'm I'm passing in one conjunction and getting back another, but I could partially apply…? something?

[Arien Malec]

I guess I'm passing in some types and a compound with those types? Or?? My mental model doesn't match dependent typing well.

[Arien Malec]

Reading again, I have an actual Prop and Lean wants me to pass a type....

[Kyle Miller]

and_assoc_right takes four explicit arguments: the three before the colon and a proof of (p ∧ q) ∧ r

[Kyle Miller]

The error message that it is expecting a Prop : Type is admittedly confusing, but it's meant to give you more information. It's just wanting a Prop for the first argument (and Prop has type Type). It is similar to how it is reporting that h has type (p ∧ q) ∧ r (and (p ∧ q) ∧ r has type Prop).

[Kyle Miller]

My curly brace suggestion has the effect of making the first three arguments be implicit arguments. That way when you supply h it goes toward the explicit argument corresponding to (p ∧ q) ∧ r.