CODEWITHSUNDEEP
coq
user251130
user251130

Reputation: 33

Making coercions explicit in assumptions in Coq

I do not really understand how to work with coercions in Coq. Example:

Inductive T1:=
   | P1: T1.
Inductive T2:=
   | T1_of: T1 -> T2.
Coercion T1_of: T1 >-> T2.
Variable S: Set.
Variable f: T2 -> Set.
Lemma L: f P1 -> True.
intro.

I get the following assumption:

H : f P1

I have two questions:

  1. Is it the case that the "real" type of H is "f (T1_of P1)" and "f P1" is just a nice printing for "f (T1_of P1)"?
  2. Is there a way to rewrite this assumption as
H : f (T1_of P1)

?

Upvotes: 0

Views: 117

Answers (1)

perthmad
perthmad

Reputation: 291

Indeed.

  1. Yes, this is just syntactic sugar, the underlying term is the one you mention.
  2. Use the Set Printing Coercions command or the option provided in your IDE.

Upvotes: 1

Related Questions