The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 22 juil. 2013, at 09:31, Michiel Helvensteijn 
<mhelvens AT gmail.com>
 wrote:
> 
>>> Furthermore, it seems to break other things, like the `elements`
>>> coercion I asked for with `:>`:
>>> 
>>> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>>> Goal forall x y: E, (In _ elements x) -> x ≺ y. (* works fine *)
>>> Goal forall x y: E, (In _ dm x) -> x ≺ y. (* error *)
>>> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
>>> 
>>> If I use a Record instead of a Class, the coercion works as expected,
>>> but then the implicit argument inference for ≺ doesn't work. Can I
>>> somehow have my cake and eat it too?
>> 
>> :> in a Class declaration does not declare a coercion (as documented in the
>> reference manual) but an instance. You can certainly make elements a 
>> coercion
>> afterwards using the [Coercion] command.
> 
> That doesn't seem to work either:
> 
> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> Definition ESet := Ensemble E.
> 
> Class DM := {
>  elements : ESet;
>  order    : relation E
> }.
> 
> Arguments elements : clear implicits.
> 
> Coercion elements: DM >-> ESet.
> 
> Parameter dm: DM.
> 
> Goal forall x, (In _ (elements dm) x). (* works fine *)
> Goal forall x, (In _ dm x). (* error *)
> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> 
> Bug?
> 
> To ask an unrelated question: Why can't I use `Ensemble E` directly in
> the Coercion declaration? Apparently it requires a single identifier.

Hi, 
  
  It's not unrelated, you can write Ensemble in the coercion declaration but
not applied, the coercion just needs the head constant. Then [In _ dm x] 
checks.

---
Class DM := {
 elements : Ensemble E;
 order    : relation E
}.

Arguments elements : clear implicits.

Coercion elements: DM >-> Ensemble.

Parameter dm: DM.

Goal forall x, (In _ (elements dm) x). (* works fine *)
Goal forall x, (In _ dm x). (* error *)
---

-- Matthieu