coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
>
>
- [Coq-Club] Heterogeneous relations in Coq, Lucian M. Patcas
- Re: [Coq-Club] Heterogeneous relations in Coq, Damien Pous
Archive powered by MhonArc 2.6.16.