Zulip Chat Archive

Stream: lean4

Topic: issues extracting proofs


Arien Malec (Oct 03 2022 at 17:17):

Working through TPIL4, and where I was able to extract proofs to subproofs for the props chapter, I'm having typing issues for the quantifiers chapter.

here's a super simple example:

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

theorem all_and_separable_quantifiers: ( x, p x  q x)  ( x, p x)  ( x, q x) :=
  fun (h:  x, p x  q x) =>
    have hp: ( x, p x) := fun y => (h y).left
    have hq: ( x, q x) := fun y => (h y).right
    hp,hq

example : ( x, p x  q x)  ( x, p x)  ( x, q x) :=
  Iff.intro (fun h => all_and_separable_quantifiers h)
    -- (fun (h: ∀ x, p x ∧ q x) =>
    --   have hp: (∀ x, p x) := fun y => (h y).left
    --   have hq: (∀ x, q x) := fun y => (h y).right
    --   ⟨hp,hq⟩
    -- )
    (fun (h: ( x, p x)  ( x, q x)) =>
      fun y => show p y  q y from And.intro (h.left y) (h.right y))

the typing issue is:

application type mismatch
  all_and_separable_quantifiers h
argument
  h
has type
   (x : α), p x  q x : Prop
but is expected to have type
  Type : Type 1

If I pointsfree the subproof call, I get instead

application type mismatch
  Iff.intro all_and_separable_quantifiers
argument
  all_and_separable_quantifiers
has type
   (α : Type) (p q : α  Prop), ( (x : α), p x  q x)  ( (x : α), p x)   (x : α), q x : Prop
but is expected to have type
  ( (x : α), p x  q x)  ( (x : α), p x)   (x : α), q x : Prop

lean4 seems to be interpreting the types in the variable statement differently between thoerem and example or is there some obvious typo I'm missing?

Rish Vaishnav (Oct 03 2022 at 17:23):

Your variables (α : Type) (p q : α → Prop) are not implicit, so all_and_separable_quantifiers expects them to be explicitly given as your first arguments. Try:

variable {α : Type} {p q : α  Prop}

Arien Malec (Oct 03 2022 at 17:27):

Thanks -- I see now I previously explicitly declared implicit parameters in my code for the props chapter.


Last updated: Dec 20 2023 at 11:08 UTC