The Coq mailing list

[Anders Lundstedt <anders AT anderslundstedt.se>]

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