Stream: Coq users

Topic: simplification under binders


view this post on Zulip Lef Ioannidis (Oct 20 2021 at 02:18):

I am a bit confused with what the rules for simplification under binders are.
The following simplifies

Eval cbv in (fun (x: bool) => andb true true).

But not the following.

Eval cbv in (fun (x: bool) => (if x then fun x0 : bool => x0 else fun x0 : bool => negb x0) x).

Why is that? Is there a way to instruct Coq to simplify this to fun (x: bool) => if x then x else negb x with no additional lemmas (ex: functional extensionality).

view this post on Zulip Guillaume Melquiond (Oct 20 2021 at 06:01):

Your second term cannot be simplified, even if it was not under a binder. It is just not possible to extract something out of a match (or conversely to push something under a match). As for your original question, there is no specific restrictions for terms under binders; they are simplified the exact same way as other terms.

view this post on Zulip Lef Ioannidis (Oct 20 2021 at 16:02):

What does this mean with regards to strong normalization of Gallina? My guess is it's not strongly normalizing or maybe values include matches?

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 16:05):

Nothing, Coq is strongly normalizing (at least the ideal underlying system, so barring bugs). I think that what you're looking for is canonicity.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 16:05):

Canonicity tells you that a closed boolean indeed reduces to a boolean. But obviously as you observed it's not true when you go under a context.

view this post on Zulip Pierre-Marie Pédrot (Oct 20 2021 at 16:07):

More interestingly, the proof of SN precisely handles open terms in a principled way, i.e. under a context a normal term is either an actual value or a neutral, i.e. a term blocked on a variable in head position (i.e. recursive application head / case scrutinee)

view this post on Zulip Lef Ioannidis (Oct 20 2021 at 21:35):

I see, thanks for that explanation of the SN proof and the difference between values and neutral terms, that's what I was missing.


Last updated: Mar 28 2024 at 21:01 UTC