Case analysis of equality

[radeusgd]

It often comes up in proofs that I have 2 values (for example nats) and the proof continues differently depending on whether they are equal or not.

One trick to deal with that is to use the following code (assume we have x y: nat):

remember (x =? y) as xeqy.
destruct xeqy.
* assert (x = y). apply beq_nat_true. auto.
  [part of proof with the H: x = y]
* assert (x <> y). apply beq_nat_false. auto.
  [part of proof with the H: x <> y]

This becomes tedious to write when there are multiple cases to analyse and can make proof less readable.

[radeusgd]

I wanted to create a tactic for this, but didn't know how to handle branching. So the first improvement was an assertEq that proved the equality (so that I didn't have to remember the names of the lemmas used).

Ltac assertEq H := assert H; ((try apply beq_nat_true); (try apply beq_nat_false)); auto.

Now the code looked like this:

remember (x =? y) as xeqy.
destruct xeqarg.
* assertEq (x = arg).
  [part of proof with the H: x = y]
* assertEq (x <> y).
  [part of proof with the H: x <> y]

This made the cases at least a bit shorter and clearer, but still required multiple boilerplate lines.

[radeusgd]

One approach is to use eq_nat_decide from Coq.Arith.EqNat.

Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}.

It can be applied as:

destruct (eq_nat_decide x y).
* apply eq_nat_eq in e.
  [part of proof with the H: x = y]
* [part of proof with the H: x <> y, but the assumption we actually get is H: ~ eq_nat x y]

So the assumption in second branch is not exactly as we wanted (it's equivalent but may be less comfortable in use).

[radeusgd]

The final solution was to write my own decidability function:

Definition decide (x y : label) : x = y \/ x <> y.
  remember (x =? y).
  destruct b.
  * left. apply beq_nat_true. intuition.
  * right. apply beq_nat_false. intuition.
Qed.

This allowed for exactly what I wanted:

destruct (dec x arg).
* [part of proof with the H: x = y]
* [part of proof with the H: x <> y]

It's just a single command and the added hypotheses are in the exact form that I wanted to have.