I quite often have to deal with complex conjunctions such as (Q /\ W) /\ (E /\ R). I am quite sick of destructing them manually and guessing how to arrange square brackets so I don't accidentally remove some important chunk. I would like to therefore write a custom Ltac that would nicely break such monsters down, exactly what repeat split does to the goal:
Theorem test : forall {Q W E R : Prop}, (Q /\ W) /\ (E /\ R) -> True.
Proof.
intros Q W E R.
intro H.
smart_destruct H.
(*
HQ : Q
HW : W
HE : E
HR : R
------------------
True
*)
Admitted.
What I have so far is
Ltac smart_destruct H
:= match H with
| _ /\ _ => destruct H as [?L ?R]; smart_destruct L; smart_destruct R
| _ => H
end.
But it does not work because
Error: Expression does not evaluate to a tactic.
If there exists a tactic that does exactly what I am trying to craft, then I would be happy to know, but most importantly I would like to know to write a custom Ltac for that. What am I doing wrong?
The error you are getting is telling you that a branch in your tactic doesn't return a tactic. In this case, it is the second branch in the match
| _ => H
Your tactic shouldn't return a hypothesis but instructions on how to manipulate the goal. So what you want here is to return the idtac tactic which is a tactic that does nothing to the goal.
The second problem with the tactic is that you match on the hypothesis rather than the type of the hypothesis. The tactic below should do what you want.
Ltac smart_destruct H :=
match type of H with
| _ /\ _ =>
let L := fresh "L" in
let R := fresh "R" in
destruct H as [L R]; smart_destruct L; smart_destruct R
| _ => idtac
end.