The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Maybe [reflexivity] doesn't support CRelationClasses?  You can do

Ltac reflexivity :=

  first [ Coq.Init.Notations.reflexivity

        | intros; exact (@Coq.Classes.CRelationClasses.reflexivity _ _ _ _) ]

  || Coq.Init.Notations.reflexivity.

to work around this.  (The "|| Coq.Init.Notations.reflexivity" is just to get back the error messages of [reflexivity].)

On Wed, Dec 23, 2015 at 2:16 PM, Gregory Malecha <gmalecha AT gmail.com> wrote:

It looks like I spoke a bit too soon. What do I need to include in order to make it work with [reflexivity]?

Require Import Setoid.

Require Import Coq.Classes.CRelationClasses.

Set Printing Universes.

Polymorphic Class ILogic@{U X} (T : Type@{U}) : Type :=

{ lentails : T -> T -> Prop

; Refl_lentails :> Reflexive@{U X} lentails }.

Existing Instance Refl_lentails.

Print ILogic.

Section foo.

  Universe U T.

  Variable T : Type@{T}.

  Variable ILT : ILogic@{T U} T.

  Existing Instance ILT.

  Goal forall x : T, lentails x x.

        intros.

        reflexivity.

  (* Error: Tactic failure:  The relation lentails@{T

U} is not a declared reflexive relation. Maybe you need to require the Setoid library.

   *)

  eapply Refl_lentails. (* WORKS *)

Is this a bug with [eauto] and universe polymorphic lemmas?

On Wed, Dec 23, 2015 at 11:09 AM, Gregory Malecha <gmalecha AT gmail.com> wrote:

Yup. I believe that is what I'm looking for. Unfortunately, the online documentation does not show universes, so it pretty much looks the same as RelationClasses. ;-)

Thanks.

On Wed, Dec 23, 2015 at 10:52 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

I think you are looking for Coq.Classes.CRelationClasses.

On Wed, Dec 23, 2015 at 12:50 PM, Gregory Malecha <gmalecha AT gmail.com> wrote:

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

--

gregory malecha

--

gregory malecha