Proving if then else in Coq

Question

I'm new at Coq and I'm trying to prove something pretty basic

Lemma eq_if_eq : forall a1 a2, (if beq_nat a1 a2 then a2 else a1) = a1.

I struggled through a solution posted below, but I think there must be a better way. Ideally, I'd like to cleanly case on beq_nat a1 a2 while putting the case values in the list of hypothesis. Is there a tactic t such that using t (beq_nat a1 a2) yields two subcases, one where beq_nat a1 a2 = true and another where beq_nat a1 a2 = false? Obviously, induction is very close but it loses its history.

Here's the proof I struggled through:

Proof.
Hint Resolve beq_nat_refl.
Hint Resolve beq_nat_eq.
Hint Resolve beq_nat_true.
Hint Resolve beq_nat_false.
intros.
compare (beq_nat a1 a2) true.
intros. assert (a1 = a2). auto. 
replace (beq_nat a1 a2) with true. auto.
intros. assert (a1 <> a2). apply beq_nat_false.
apply not_true_is_false. auto.
assert (beq_nat a1 a2 = false). apply not_true_is_false. auto.
replace (beq_nat a1 a2) with false. auto.
Qed.

Answer 1

Generally for this kind of things, I use the eqn variant of destruct. It would look like this:

destruct (beq_nat a1 a2) as []_eqn. (* Coq <= 8.3 *)

destruct (beq_nat a1 a2) as []eqn:? (* Coq >= 8.4 *)

It will add the equality as a hypothesis. In the 8.4 variant, you can replace the question mark with a name to give to the hypothesis.

Answer 2

The tactic that does what you are asking for is case_eq. The following script proves the lemma in 8.4pl3:

intros.
case_eq (beq_nat a1 a2).
intuition.
apply beq_nat_true_iff in H.
intuition.
intuition.