Proof Review: Basic theorem about ternary relations in Coq

Question

I'm proving a simple fact about ternary relations in Coq as an exercise.

I'm interested in ternary relations at the moment because they are a simple thing that can represent a finitary consequence relation, i.e. a consequence relation $\vdash : \mathsf{Set}[\mathsf{Wff}] \times \mathsf{Wff} \to 2$ with the property that $\Gamma \vdash \varphi$ implies that some finite $\Gamma_0 \subset \Gamma$ exists such that $\Gamma_0 \vdash \varphi$. For finitary consequence relations, I can always rework my system to only have binary inference rules (provided I have something that works like conjunction (I think)).

Anyway, I want to prove some basic facts about ternary relations first. I decided to formalize this in Coq in the simplest way possible, defining a new type $T * T * T \to 2$.

I'm curious how this can be done better. The proof script below is extremely naive. It makes no use of implicit arguments and CommutativeTernaryRelation and the like are encoded as propositions rather than as new types.

The way the proof itself is done is also bad; it does the one line per tactic thing and makes liberal use of assert where other tactics would probably be more idiomatic.

(* TernaryRelation is a relation between three elements of the same type.
   Represented here as a decidable procedure giving us back a boolean. *)
Definition TernaryRelation (T : Type) : Type := (T * T * T) -> bool.

(* A ternary relation is commutative if and only if Rabc holds iff Rbac holds. *) 
Definition CommutativeTernaryRelation (T: Type) (R: TernaryRelation T) : Prop :=
  forall a b c : T, R (a, b, c) = R (b, a, c).

(* A ternary relation R is cyclic if and only if the truth value of R is not changed by permuting its arguments with a permutation of positive sign *)
Definition CyclicTernaryRelation (T: Type) (R: TernaryRelation T) : Prop :=
  forall a b c : T, R (a, b, c) = R (b, c, a).

(* We want to show that cyclic and commutative ternary relations are invariant
under reversing the arguments too. *)
Theorem CommutativeAndCyclicImpliesReversible: forall T: Type, forall R: TernaryRelation T, CommutativeTernaryRelation T R /\ CyclicTernaryRelation T R -> (forall a b c : T, R (a, b, c) = R (c, b, a)).
Proof.
  intros.
  intuition.
  unfold CyclicTernaryRelation in H1.
  unfold CommutativeTernaryRelation in H0.
  assert (R (a, b, c) = R (b, a, c)).
  intuition.
  assert (R (b, a, c) = R (a, c, b)).
  intuition.
  assert (R (a, c, b) = R (b, c, a)).
  symmetry in H2.
  rewrite H2.
  symmetry in H.
  rewrite H.
  intuition.
  intuition.
  rewrite H.
  rewrite H2.
  rewrite H3.
  assert (R (b, c, a) = R (b, c, a)).
  tauto.
  intuition.
Qed.
```

Answer 1

I decided to formalize this in Coq in the simplest way possible, defining a new type $T * T * T \to 2$

In proof assistants and functional programming languages more generally, it's generally more idiomatic to use curried types. Here, that would mean defining TernaryRelation as $T \to T \to T \to 2$. Furthermore, consider whether you want your relations to be computable (landing in bool) or propositional (landing in Prop, as in Coq.Relations.Relation_Definitions.relation in the standard library).

The proof script below is extremely naive. [...] The way the proof itself is done is also bad; it does the one line per tactic thing and makes liberal use of assert where other tactics would probably be more idiomatic.

It's fairly informative as far as proofs go (though it's good practice to always name hypotheses when posing them, e.g., with assert, whenever you're going to use the hypothesis later by name), but if you want a more concise and automated proof, consider simply writing Proof. intuition congruence. Qed.. This says to use the algorithm behind tauto ("a decision procedure for intuitionistic propositional calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff [Dyc92]") while using congruence (a "standard Nelson and Oppen congruence closure algorithm, which is a decision procedure for ground equalities with uninterpreted symbols") at the leaves.

Answer 2

To permute abc to cba with the given primitives, a single rotation and a single transposition suffice.

Theorem CommutativeAndCyclicImpliesReversible: forall T: Type, forall R: TernaryRelation T, CommutativeTernaryRelation T R /\ CyclicTernaryRelation T R -> (forall a b c : T, R (a, b, c) = R (c, b, a)).
Proof.
  intros T R [comm cyc] a b c.
  unfold CommutativeTernaryRelation in comm.
  unfold CyclicTernaryRelation in cyc.
  rewrite cyc, comm. reflexivity.
Qed.

IMO unfold is generally a code smell. Here, using records (or classes) you can avoid having to name the corresponding hypotheses, instead fetching them indirectly via projections:

(* TernaryRelation is a relation between three elements of the same type.
   Represented here as a decidable procedure giving us back a boolean. *)
Definition TernaryRelation (T : Type) : Type := (T * T * T) -> bool.

(* A ternary relation is commutative if and only if Rabc holds iff Rbac holds. *) 
Record CommutativeTernaryRelation (T: Type) (R: TernaryRelation T) : Prop :=
  { comm : forall a b c : T, R (a, b, c) = R (b, a, c) }.

(* A ternary relation R is cyclic if and only if the truth value of R is not changed by permuting its arguments with a permutation of positive sign *)
Record CyclicTernaryRelation (T: Type) (R: TernaryRelation T) : Prop :=
  { cyc : forall a b c : T, R (a, b, c) = R (b, c, a) }.

(* We want to show that cyclic and commutative ternary relations are invariant
under reversing the arguments too. *)
Theorem CommutativeAndCyclicImpliesReversible: forall T: Type, forall R: TernaryRelation T, CommutativeTernaryRelation T R -> CyclicTernaryRelation T R -> (forall a b c : T, R (a, b, c) = R (c, b, a)).
Proof.
  intros T R ? ? a b c.
  rewrite cyc, comm; [ reflexivity | auto .. ].
Qed.

• Link to the relevant section in the Coq manual for the _ ; [ _ | _ ..] syntax