I want to prove the following theorem on two pairs of type TR:
Definition s:= nat.
Definition d:= nat.
Definition c:= nat.
Definition p:= nat.
Inductive rt: Set :=
|al : rt
|bl : rt.
Definition TR: Set :=
rt* s*d* c* p.
Implicit Types m n : TR.
Theorem eq_TR_dec : forall n m, {n = m} + {n <> m}.
For now, the proof of this theorem begins by intros n. destruct n. destruct m. But I cannot figure out the best tactic to prove this theorem. Any idea how should I prove this theorem? Thank you
As mentionned in the comments, you can use decide equality which basically solve these goals (check the documentation here to learn more).
In this case, just apply it as many times as needed and it works :
Theorem eq_TR_dec : forall n m, {n = m} + {n <> m}.
Proof.
decide equality.
- decide equality.
- decide equality.
* decide equality.
* decide equality.
+ decide equality.
+ {
decide equality.
- decide equality.
- decide equality.
}
Qed.
or more simply using the repeat tactic (as also mentionned in eponier's comment), which basically applies (reccursively in the subgoal generated) the tactic you give it until it fails:
Theorem eq_TR_dec : forall n m, {n = m} + {n <> m}.
Proof.
repeat decide equality.
Qed.
As we saw in the first case, here you only need to solve apply decide equality enough times, so repeat is particularly efficient !