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. *)
Admitted.
End Test.
```

Thank you

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.

Didn't know about sealing, many thanks!

Last updated: Jun 13 2024 at 19:02 UTC