The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I'm wondering if there are definitions analagous to [Reflexive] and [Transitive] that are both universe polymorphic and work with the built-in tactics such as [reflexivity] and setoid rewriting. In particular, I note that when I use the basic definitions I get a universe constraint that I would like to avoid. For example,

Require Import Coq.Classes.RelationClasses.

Set Printing Universes.

Polymorphic Class ILogic (T : Type) : Type :=

{ lentails : T -> T -> Prop

; Refl_lentails : Reflexive lentails }.

Print ILogic.

(*

Polymorphic Record ILogic (T : Type@{Top.1}) : Type@{max(Set+1, Top.1)}

  := Build_ILogic

  { lentails : T -> T -> Prop;  Refl_lentails : Reflexive lentails }

(* Top.1 |= Top.1 <= Coq.Classes.RelationClasses.1

             *)

*)

The extra constraint [Top.1 <= Coq.Classes.RelationClasses.1] makes this definition less useful in my particular context. If I inline the definition of [Reflexive] then everything works out.

Polymorphic Class ILogic' (T : Type) : Type :=

{ lentails' : T -> T -> Prop

; Refl_lentails' :> forall a : T, lentails' a a }.

Print ILogic'.

(*

Polymorphic Record ILogic' (T : Type@{Top.12}) : Type@{max(Set+1, Top.12)}

  := Build_ILogic'

  { lentails' : T -> T -> Prop;  Refl_lentails' : forall a : T, lentails' a a }

(* Top.12 |=  *)

*)

However, with this definition, [reflexivity] does not work. I'm wondering if there already exists polymorphic instances of the basic classes, e.g. [Reflexive], [Transitive], [Proper], [Respectful], etc, or if there is some way to tell Coq to look for instances of a polymorphic version of these classes that I would define.

Thanks so much.

--

gregory malecha