## Stream: Coq users

### Topic: simplification under binders

#### 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: Jun 16 2024 at 01:42 UTC