The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Abhishek, Dear Coq Users,

 

I made some experiments around your suggestion. It goes fairly well, just at one point I got stuck. I have a type class Welldefined:

 

Class Welldefined {t : Type} (eq : relation t) (ord : relation t) :=

{

  welldefined :> Proper (eq==>eq==>iff) ord

}.

 

which I use in my order structures to express that lt and le are well defined with respect to eq. For rewriting under Welldefined, I need two proper instances, one for rewriting each argument:

 

Global Instance Proper_Welldefined1 {T : Type} (RR : relation (relation T)):

  Proper

    (pointwise_relation T (pointwise_relation T iff) ==> RR ==> Basics.flip Basics.impl)

    Welldefined.

 

Global Instance Proper_Welldefined2 {T : Type} (R : relation T):

  Proper

    (pointwise_relation T (pointwise_relation T iff) ==> Basics.flip Basics.impl)

    (Welldefined R).

 

The second one is easy, but the first one I find a bit hard to prove, because I need to show Welldefined R U from Welldefined S V. But I have the pointwise only between R and S. All I have for U and V is RR U V for some relation-relation RR.

 

The complete error message I get when I do a rewrite of the first argument of Welldefined is:

 

Error: setoid rewrite failed: Unable to satisfy the following constraints:

UNDEFINED EVARS:

?X195==[ |- relation (relation nat)] (internal placeholder) {?r}

?X196==[(do_subrelation:=do_subrelation)

          |- Proper (pointwise_relation nat (pointwise_relation nat iff) ==> ?X195 ==> Basics.flip Basics.impl)

               Welldefined] (internal placeholder) {?p}

?X197==[ |- ProperProxy ?X195 (fun x x0 : nat => (x <? x0) = true)] (internal placeholder) {?p0}

 

I would very much appreciate some help with this.

 

Best regards,

 

Michael

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928