Is there a way to tell coq to always "substitute in" the argument of a certain coercion at the time the coercion is inserted?
Lets say I have the following definitions:
Definition SpecV n := Vector.t (RegSpec) n.
Definition Spec n :Type := list Prop * SpecV n.
I would like to "default" the first component of Spec to [].
Currently, I do as follows:
Definition coerceSpec {sig n} V : Spec sig n := ([],V).
Coercion coerceSpec : SpecV >-> Spec.
But to have clearer Lemmas and "normal forms" for my lemmas, I would that V : Spec _ _
is syntactically exactly ([],V)
after pretyping.
I don't think it is possible to automatically unfold a coercion.
An hack that comes to mind:
Notation clean t := (ltac:(let t1 := eval simpl in t in exact t1)).
Lemma test : clean ( 0 + 0 = 0 ).
1 subgoal
============================
0 = 0
Last updated: Oct 13 2024 at 01:02 UTC