Lef Ioannidis (Oct 20 2021 at 02:18): 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).
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.
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?
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.
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.
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)
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: Oct 03 2023 at 02:34 UTC