Zulip Chat Archive

Stream: new members

Topic: Type checking a higher order definition


view this post on Zulip Ken Roe (Jul 12 2018 at 00:39):

Can someone fix the following definition so that it can be type checked:

def absAll {t : Type} : (t    Prop)  (  Prop) :=
    (λ (st : t    Prop), ( (q:t), (st q))).

view this post on Zulip Simon Hudon (Jul 12 2018 at 00:45):

What happens if you write this:

def absAll {t : Type} : (t    Prop)  (  Prop) :=
    (λ (st : t    Prop) (i : ), ( (q:t), (st q i))).

view this post on Zulip Ken Roe (Jul 12 2018 at 01:29):

It works--maybe I should file a bug report.

view this post on Zulip Simon Hudon (Jul 12 2018 at 01:30):

That's not a bug, you made a mistake

view this post on Zulip Simon Hudon (Jul 12 2018 at 01:31):

The term of the definition has to be a function that takes two parameters (st : t → ℕ → Prop and i : ℕ) and returns a Prop (∀ (q:t), (st q i))

view this post on Zulip Simon Hudon (Jul 12 2018 at 01:32):

You wrote st q which has type ℕ -> Prop. But the body of a must be a Prop

view this post on Zulip Simon Hudon (Jul 12 2018 at 01:36):

I encourage you to use typed holes (i.e. _) to explore what are the types expected from you. For instance, look at what Lean tells you when you write the following in your definition:

  • (λ (st : t → ℕ → Prop), _)
  • (λ (st : t → ℕ → Prop) (i : ℕ), _)
  • (λ (st : t → ℕ → Prop) (i : ℕ), (∀ (q:t), _))

view this post on Zulip Simon Hudon (Jul 12 2018 at 01:47):

I'm not sure what you're going for but you may prefer this definition:

def absAll {t : Type} (st : t    Prop) (i : ) : Prop :=
 (q:t), (st q i)

It is clearer and its equations are nicer too

view this post on Zulip Kevin Buzzard (Jul 12 2018 at 07:21):

What does "its equations are nicer" mean in this context?

Edit: I think I've answered my own question using #print prefix absAll. I am surprised! I knew that if you defined a fancy inductive type you got a bunch of generated equations, but I don't think I'd internalised that this was happening for just some random definition of a function.

Simon's version gives

absAll : Π {t : Type}, (t → ℕ → Prop) → ℕ → Prop
absAll.equations._eqn_1 : ∀ {t : Type} (st : t → ℕ → Prop) (i : ℕ), absAll st i = ∀ (q : t), st q i

I guess my revised question is why this equation is there at all! It just seems to be the definition of absAll.

view this post on Zulip Sean Leather (Jul 12 2018 at 07:32):

I guess my revised question is why this equation is there at all! It just seems to be the definition of absAll.

If you use simp [absAll], I believe it uses that equation in the simplifier.

view this post on Zulip Kevin Buzzard (Jul 12 2018 at 07:34):

Aah that would make sense. I don't use simp like this usually -- I am only just beginning to get the hang of what simp does, and now I tend to only feed it equalities (I used to feed it arbitrary strings of symbols which I hoped made sense :-) )


Last updated: May 15 2021 at 00:39 UTC