## Stream: Coq users

### Topic: Non-unfolding of coercions definitionally equal to id

#### Martin C (Sep 26 2023 at 19:15):

Hello,

Is there a way for Coq not to reduce / unfold coercion applications which are equivalent to the identity function?

Let me try to give an example (there might be a simpler/more minimal example). Consider the code below:

``````Section Test.
Variable T : Type.

Structure AugmentedT := {
Type_ :> Type;
coercion : Type_ -> T
}.

Coercion coercion : Type_ >-> T.

Definition T' :=
{| Type_ := T; coercion := @id _ |}.

Definition T'' :=
{| Type_ := T * T; coercion := fst |}.

Variable f : T -> unit.

Set Printing All.
Check (fun x : T' => f x).
(*
fun x : Type_ T' => f x
: forall _ : Type_ T', unit
*)

Check (fun x : T'' => f x).
(*
fun x : Type_ T'' => f (coercion T'' x)
: forall _ : Type_ T'', unit
*)
``````

What I am looking for is a way for the first Check statement to behave like the second one, i.e. to also be `fun x : Type_ T' => f (coercion T' x)`.

Why would I want this? Say I have a generic fact on all `AugmentedT`, then I could also use it in the `T'` case (not possible at the moment):

``````  Variable H : forall (U : AugmentedT) (x : U), f x = tt.

Theorem tstT'' (x : T'') :
f x = tt.
Proof.
rewrite H.
reflexivity.
Qed.

Theorem tstT' (x : T') :
f x = tt.
Proof.
Fail rewrite H.
(* The command has indeed failed with message:
Found no subterm matching "f ?M161" in the current goal. *)
End Test.
``````

Thank you

#### Paolo Giarrusso (Sep 26 2023 at 19:49):

as a side note, fact `H T'` would be applicable here — at least `apply (H T')` would work.
But for your original question, one way is to use sealing (https://github.com/LPCIC/coq-elpi/tree/master/apps/locker), so that `Type_ T'` and coercion are only propositionally equal respectively to T / id.

#### Martin C (Sep 26 2023 at 20:00):

Didn't know about sealing, many thanks!

Last updated: Jun 13 2024 at 19:02 UTC