I’ve a relation C that takes three parameters. It represents an operation of my theory. So C(a, b, c) represents a = b @ c, however I didn’t (succeed to) define this operator in Coq, so I use only the relation C. I want this relation to be associative: (d @ e) @ f = d @ (e @ f). And I have to express it with C. I thought of two axioms, but I don’t know which one is best (if they’re are both correct).
Parameter Entity: Set.
Parameter C : Entity -> Entity -> Entity -> Prop.
Axiom asso1 : forall a c d e,
((exists b, C a b c /\ C b d e) <-> (exists f, C a d f /\ C f e c)).
Axiom asso2 : forall s t u a b c d,
(C a s t -> C b a u -> C d s c -> C c t u -> b = d).
What do you think about it?
Both axioms are equivalent if you also know that C is a functional relation (i.e., it represents a function): every input pair maps to a unique output.
(* A functional relation is one that is total and deterministic in the following sense: *)
Axiom total_C : forall a b, exists c, C c a b.
Axiom deterministic_C : forall a b c c', C c a b -> C c' a b -> c = c'.