Stream: Coq users

Topic: Unfold Coercion


view this post on Zulip Fabian Kunze (Nov 06 2020 at 14:38):

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.

view this post on Zulip Enrico Tassi (Nov 06 2020 at 16:21):

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: Jan 29 2023 at 06:02 UTC