The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Indeed. And in fact, there is also the singleton monad, whose Kleisli category is the category of functional relations.

On 28 January 2014 01:48, Daniel Schepler <dschepler AT gmail.com> wrote:

Hmm, the logical monad I came up with for this situation actually looked something like:

Record SubSingleton (A:Type) : Type := {

  SS_has_value : A -> Prop;

  SS_uniqueness : uniqueness SS_has_value

}.

Definition SS_return {A:Type} (x:A) : SubSingleton A.

refine {| SS_has_value := eq x |}.

Proof.

congruence.

Defined.

Definition SS_bind {A:Type} (x0 : SubSingleton A)

  {B:Type} (f : A -> SubSingleton B) : SubSingleton B.

refine {| SS_has_value := fun y:B => exists x:A, SS_has_value _ x0 x /\

  SS_has_value _ (f x) y |}.

Proof.

intros y1 y2 [x1 [? ?]] [x2 [? ?]].

pose proof (SS_uniqueness _ _ _ _ H H1).

destruct H3.

exact (SS_uniqueness _ _ _ _ H0 H2).

Defined.

So R would be packaged as a function A -> A -> SubSingleton A.

-- 

Daniel Schepler

On Sun, Jan 26, 2014 at 10:00 PM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

There is a way in that fun A => A -> Prop is a monad. So, basically, the same trick we discussed last time with the option type [ https://sympa.inria.fr/sympa/arc/coq-club/2014-01/msg00171.html ] may apply.

Here the coercion from A to A->Prop (you would have to write a type synonym for the latter to use the coercion mechanism), the monadic unit, is

Definition singleton x := fun y => y=x.

And the binary monadic extension is

Definition extension2 f x y := exists a, exists b, x a -> x b -> f a b

If you are interested about this sort of things you should read up about monads (there are plenty of resources for Haskell). Also there is there cousin, applicative functors, which may be relevant to your needs.

On 26 January 2014 17:35, Anders Lundstedt <anders AT anderslundstedt.se> wrote:

Dear all,

I have a ternary relation R such that R a b c -> R a b d -> c = d. Is it possible to treat R notationally as a binary function? R is not decidable.

Parameter A : Set.

Parameter R : A -> A -> A -> Prop.

(* we may assume that R is functional *)

Axiom R_functional : forall a b c d, R a b c -> R a b d -> c = d.

(* 

   is it possible to create a functional notation a * ... * b = c, i.e. s.t.

     a * b = c <-> R a b c

     a * b * c = d <-> exists x, a * b = x /\ x * c = d

     a * b * c * d = e <-> exists x, a * b * c = x /\ x * d = e

     etc...

*)

Best regards,

Anders Lundstedt