Ltac tactic that accepts an arbitrary number of quantifiers

Question

I'm trying to write a--my first--Coq tactic. It should split forall x y z ..., A <-> B into two: forall x y z ..., A -> B and forall x y z ..., B -> A.

This is my first attempt:

Ltac iff_split H :=
  match type of H with
  | forall x y, ?A <-> ?B =>
    let Hr := fresh H "r" in
    let Hl := fresh H "l" in
    assert (Hr : forall x y, A -> B) by (apply H);
    assert (Hl : forall x y, B -> A) by (apply H);
    clear H
  end.

It works only for a fixed number of quantifiers (in this case just 2), but I want to extend it to accept an arbitrary list of them.

How can I achieve this?

Answer 1

This answer uses a trick (for expert only ) due to Adam Chlipala. Don't hesitate to ask for more explanation if something is unclear.

Ltac does not allow to go under binder but you can trick it by folding the quantifiers. Let us take forall x y, x + y = 0 that is a nested universal quantification. You can fold it in into forall p, fst p + snd p = 0 that is a simple quantification. If you can arbitrary fold and unfold nested quantifications, you are done: you fold, perform your transformation then unfold.

Here is the code that does the trick

Ltac fold_forall f :=
  let rec loop F := 
    match F with
      | forall x y, @?body x y => 
          let v := (eval cbv beta in (forall t, body (fst t) (snd t))) in
          loop v 
      |  _ => F
    end 
  in  loop (forall _ : unit, f).

Ltac unfold_forall f :=
  let rec loop F := 
    match F with
      | forall t : _ * _, @?body t =>
         let v := (eval cbv beta in (forall x y, (body (x, y)))) in
         loop v
      |  _ => match eval simpl in F with
              | _ -> ?G => G 
              end
    end 
  in loop f.

Ltac mk_left f :=
   match f with
    | forall x : ?T, ?A <-> ?B => constr:(forall x : T, A -> B)
   end.

Ltac mk_right f :=
   match f with
    | forall x : ?T, ?A <-> ?B => constr:(forall x : T, B -> A)
   end.

Ltac my_tac  H := 
 match type of H with
 | ?v => let v1 := fold_forall v in 
         let v2 := mk_left v1 in
         let v3 := unfold_forall v2 in
         let v4 := mk_right v1 in
         let v5 := unfold_forall v4 in 
         assert v3 by apply H;
         assert v5 by apply H
 end.

Goal (forall x y z : nat, (x = z) <-> (z = y)) -> False.
intros H.
my_tac H.