Associativity of Elvis operator

I had written a piece of code in the format a ?: (b ?: c) and I was wondering if I could omit the brackets. That’s right, we need to figure if this operator is associative.

That is, we need to see if we can show that (a ?: b) ?: c = a ?: (b ?: c).

The definition of it is:
a ?: b = a (if a is not empty)
a ?: b = b (otherwise)

So that means we can consider these cases:

Suppose a is empty.
Now we are left with b ?: c = b ?: c, which is true by reflexivity.
Suppose a is not empty.
Then, (a ?: b) evaluates to a, so we have a ?: c on the LHS, and thus a ?: c = a ?: (b ?: c).

Since a is not empty, and by definition of this operator, we have that a = a, which is true by reflexivity.

Bonus: here’s the same proof in Coq:

(* Definition of data type for empty and value one *)
Inductive value {a : Type} : Type :=
  | Value : a -> value
  | Empty : value.

(* Definition of Elvis operator *)
Definition elvis {x : Type} (x1 : @value x) (x2 : @value x) : (@value x) :=
  match x1 with
  | Empty => x2
  | Value _ => x1
  end.

(* Fancy notation for Elvis operator *)
Notation "x ?: y" := (elvis x y) (at level 50).

Theorem elvis_assoc : forall (X : Type) (x1 : @value X) (x2 : @value X) (x3 : @value X),
  x1 ?: (x2 ?: x3) = (x1 ?: x2) ?: x3.
Proof.
  intros X x1 x2 x3.
  case x1.
  - (* x1 is not empty *) simpl. reflexivity.
  - (* x1 is empty     *) simpl. reflexivity.
Qed.

Now that both considered cases are true, we’ve shown that ?: is associative and you can skip any brackets in your code 🙂