The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Fri, 4 Mar 2011 00:37:00 +0100,
Andrej Bauer 
<andrej.bauer AT andrej.com>
 a écrit :

> Is there a way to register an equivalence relation e : A -> A > Type
> with "Add (Parametric) Relation"?  Notice that it maps to Type, not
> Prop. I seem to remember reading something about this, but I cannot
> find it. I would like to use the rewriting mechanisms for such a
> relation. Changing it to Prop is not an option.
> 
> With kind regards,
> 
> Andrej

I am not used to coercions and parametric relations, but isn't there a
way for you to cast "e: A → A → Type" in "p: A → A → Prop" with a
"Inductive e_wrapper (a1 a2: A): Prop :=
 e_wrapper_intro: e a1 a2 → e_wrapper a1 a2."
and, register "e_wrapper" with "Add (Parametric) Relation" and
establish a coercion from "e" to "e_wrapper" with "e_wrapper_intro" by
something like that:

" Definition AAType := A -> A -> Type.
  Definition AAProp := A -> A -> Prop.
  Coercion e_wrapper_intro: AAType >-> AAProp.
"

I think it won't work, since it would be too easy (I don't think that
rewrite uses the Coercion mechanism to guess that from a "e a b" it
can get a "e_wrapper a b"), but maybe it may give some ideas.

I guess that using something like
"Ltac wrap :=
 match goal with
 | H: e ?a ?b |- _ => generalize (e_wrapper a b H); intro
 end.
" (but better written, so that "repeat wrap" won't loop) and call it
before rewrite is not an option either.