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).
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.
What does this mean with regards to strong normalization of Gallina? My guess is it's not strongly normalizing or maybe values include matches?
Nothing, Coq is strongly normalizing (at least the ideal underlying system, so barring bugs). I think that what you're looking for is canonicity.
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.
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)
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: Feb 04 2023 at 21:02 UTC