Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Heterogeneous relations in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Heterogeneous relations in Coq


chronological Thread 
  • From: Damien Pous <Damien.Pous AT inria.fr>
  • To: "Lucian M. Patcas" <lucian.patcas AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Heterogeneous relations in Coq
  • Date: Sat, 3 Dec 2011 18:14:40 +0100

You can have a look at the ATBR library we developed with Thomas:
http://sardes.inrialpes.fr/~braibant/atbr/

We handle heterogeneous relations as you define them, and it includes
a tactic for the Kleene algebra fragment.

I also have a rather large formalisation of left and right residuals,
including a tactic for residuated lattices (but nothing about
symmetric quotients).
It's not however not yet ready for a release. Please tell me if you
need such tools in a near future, I'll do my best to release something
asap.

Best,
Damien Pous


2011/12/3 Lucian M. Patcas 
<lucian.patcas AT gmail.com>:
> Hello,
>
> I wonder if someone can point me to existing formalizations, if any, of
> heterogeneous relations in Coq (that is, A -> B -> Prop where A B : Type).
> In particular, I'm interested in left and right residuals, and also in
> symmetric quotients. Most of the formalizations that I looked at in the
> Standard Library are about homogeneous relations (that is, A -> A - Prop).
> Any pointers are greatly appreciated.
>
> Thanks,
> Lucian
>
>



Archive powered by MhonArc 2.6.16.

Top of Page