CODEWITHSUNDEEP
coqltac
radrow
radrow

Reputation: 7139

How to create a custom Ltac to recursively destruct conjunctions?

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?

Upvotes: 0

Views: 259

Answers (2)

M Soegtrop
M Soegtrop

Reputation: 1448

Adding on the answer of abc, here is a variant which names the hypothesis after the variables - which is a bit intricate because you have to distinguish the case if it is variable or a complex term and in Ltac1 one can't do this inside of the let (afaik)

Ltac smart_destruct H
  := match type of H with
     | ?l /\ ?r =>
       tryif is_var l then (
         let HL := fresh "H" l in
         tryif is_var r then (
           let HR := fresh "H" r in
           destruct H as [HL HR]; smart_destruct HL; smart_destruct HR
         )
         else (
           destruct H as [HL ?HtmpR]; smart_destruct HL; smart_destruct HtmpR
         )
       ) else (
         tryif is_var r then (
           let HR := fresh "H" r in
           destruct H as [?HtmpL HR]; smart_destruct HtmpL; smart_destruct HR
         )
         else (
           destruct H as [?HtmpL ?HtmpR]; smart_destruct HtmpL; smart_destruct HtmpR
         )
       )
     | _ => idtac
     end.

Upvotes: 1

abc
abc

Reputation: 61

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.

Upvotes: 1

Related Questions