Refolding of definitions · Coq users

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.

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?

Stream: Coq users

Topic: Refolding of definitions

Meven Lennon-Bertrand (Feb 07 2023 at 15:00):