The Coq mailing list

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

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