CODEWITHSUNDEEP
coq
Lepticed
Lepticed

Reputation: 381

Best way to make a relation associative in Coq

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?

Upvotes: 1

Views: 66

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33399

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'.

Upvotes: 2

Related Questions