CODEWITHSUNDEEP
coqcoercionsubtype
jaam
jaam

Reputation: 980

Coq: coercion/subtyping between complex expressions

I've got an impression that it's impossible in Coq. For example

Parameter Arg: Type.
Parameter F X XP: Arg.
Parameter S P I PLS PI: Arg -> Type.
Parameter tree car: P X.
Parameter mary john: PLS XP.
Parameter c: PLS XP -> P XP.
Coercion c: PLS XP >-> P XP. (*Syntax error: '>->' expected after [vernac:class_rawexpr] (in [vernac:gallina_ext]).*)

So not only must the types of the expressions next to >-> be Set, Type or Prop, the expressions themselves must also be syntactically elementary ("rawexpressions" in Gallina?)? How to bypass this; can I form a coercion between complex expression? Is there another way to define a subtype in Coq, one which would work w/ complex expressions? Can I do better than

Let nui := PLS XP.
Let hui := P XP.
Parameter c: nui -> hui.
Coercion c: nui >-> hui.
Parameter st: P XP -> Type.
Check st (c mary). (*st mary : Type*)
Check st mary. (*Error: The term "mary" has type "PLS XP" while it is expected to have type "P XP".*)

Upvotes: 1

Views: 984

Answers (2)

jaam
jaam

Reputation: 980

After trying this, that and whatnot, the solution was surprisingly easy. There were two steps my question was missing:

  1. You can coerce functions towards one another, i.e. Coercion c: PLS >-> P works
  2. To avoid breaking the "uniform inheritance condition", you must define the function you want to make into a coercion in its general ("forall") form

In sum:

Parameter Arg: Type.
Parameter F X XP: Arg.
Parameter S P I PLS PI: Arg -> Type.
Parameter tree car: P X.
Parameter mary john: PLS XP.
Parameter c: forall x:Arg, PLS x -> P x.
Coercion c: PLS >-> P.
Check mary:P XP.

Upvotes: 1

ejgallego
ejgallego

Reputation: 6852

IMVHO, the setup of the problem is looking very complicated; I am not sure this modeling method will be effective (in the sense of efficient).

If you really want to go that route, note that Coercions have very particular rules; if you want to use them you'll have to get familiar with chapter 18 of the manual. In particular, I think that parameters cannot be made a source class so you will have to add some wrapping:

Parameter Arg: Type.
Parameter F X XP: Arg.
Parameter S P I PLS PI: Arg -> Type.
Parameter tree car: P X.
Parameter mary john: PLS XP.
Parameter c: PLS XP -> P XP.

Inductive p_wrap := p_wrap_C : PLS XP -> p_wrap.
Coercion u_cast x := match x with | p_wrap_C u => u   end.
Coercion c_cast x := match x with | p_wrap_C u => c u end.

Parameter st: P XP -> Type.
Definition Mary := p_wrap_C mary.
Check st (c Mary).
Check st Mary.

YMMV. Note that the general subType class in ssreflect doc may provide some help on how to make a generic coercion framework.

Upvotes: 1

Related Questions