Simplification tactics like `cbn`

and `simpl`

are doing some smart "refolding" of fixpoints. They are also able to refold other definitions, which is very handy to preserve notations attached to generic typeclass-based constants when simplifying goals. Sadly, it seems that `constructor`

and `econstructor`

do not have the same behaviour, which means that notations are lost without explicit refolding, see for instance the following example. Has anyone ever hit a similar issue? How did you solve it?

```
Inductive expr : Set :=
| var : nat -> expr
| constr : expr -> expr -> expr
| bad : expr.
Inductive wf_expr : expr -> Type :=
| wf_var n : wf_expr (var n)
| wf_constr e e' : wf_expr e -> wf_expr e' -> wf_expr (constr e e').
Class Wf := wf : expr -> Set.
Notation "[ |- e ]" := (wf e) (at level 0, e at level 50).
#[export] Instance Wf_expr : Wf := wf_expr.
Class Ren (X : Type) (Y Z : Type) := ren : X -> Y -> Z.
Notation "e ⟨ xi ⟩" := (ren xi e) (at level 7, left associativity, format "e ⟨ xi ⟩").
Fixpoint ren_expr (f : nat -> nat) (e : expr) {struct e} : expr :=
match e with
| var n => var (f n)
| constr e e' => constr (ren_expr f e) (ren_expr f e')
| bad => bad
end.
#[export] Instance Ren_expr : Ren (nat -> nat) expr expr := ren_expr.
Lemma wf_ren (σ : nat -> nat) (e : expr) :
[|- e] -> [|- e⟨σ⟩].
Proof.
induction 1.
all: cbn. (*cbn seems to be doing smart refolding*)
- now constructor.
- (* the notation is lost in the induction hypothesis *)
constructor. (* and constructor does not preserve it either *)
all: change wf_expr with wf in *.
all: assumption.
Qed.
```

I currently patch this by defining a tactic like the following:

```
Ltac refold := change wf_expr with wf in * ; change ren_expr with ren in *.
```

to be called whenever I have lost notations. I can also use it to define a custom induction principle, which gives induction steps with the correct notations in the hypothesis. This still has two problems. First, I need to invoke the refolding tactic quite often, which I feel is somewhat ugly and unprincipled. I guess here I could simply redefine `constructor`

to systematically call refolding… But more annoying, I would like to extend `refold`

on the fly: anytime I declare a new instance, I also want to add it to the refolding at that point. Is there a way to achieve this?

Last updated: Oct 04 2023 at 23:01 UTC