Stream: Coq users

Topic: Non-unfolding of coercions definitionally equal to id

view this post on Zulip Martin C (Sep 26 2023 at 19:15):


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.
    rewrite H.

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

Thank you

view this post on Zulip 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 (, so that Type_ T' and coercion are only propositionally equal respectively to T / id.

view this post on Zulip Martin C (Sep 26 2023 at 20:00):

Didn't know about sealing, many thanks!

Last updated: Jun 13 2024 at 19:02 UTC