接受任意数量量词的 Ltac 策略

Question

我正在尝试编写一个——我的第一个——Coq 策略。 它应该将

forall x y z ..., A <-> B

分成两个：

forall x y z ..., A -> B

和

forall x y z ..., B -> A

.

这是我的第一次尝试：

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.

它只适用于固定数量的量词（在本例中只有 2 个），但我想扩展它以接受它们的任意列表。

我怎样才能做到这一点？

Answer 1

由于 Adam Chlipala，这个答案使用了一个技巧（仅限专家😊）。 如果不清楚，请不要犹豫，要求更多解释。

Ltac

不允许放在活页夹下面，但你可以通过 折叠量词。 让我们采用

forall x y, x + y = 0

，这是一个嵌套的通用量化。 你可以把它折叠成

forall p, fst p + snd p = 0

，这是一个简单的量化。如果你可以任意折叠和展开嵌套量化，你就完成了：你折叠，执行你的转换然后展开。

这是解决问题的代码

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

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

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

Ltac mk_right f :=
   match f with
    | fun x : ?T => ?A <-> ?B => constr:(fun 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 v3' := (eval simpl in v3) in
         let v4 := mk_right v1 in
         let v5 := unfold_forall v4 in 
         let v5' := (eval simpl in v5) in
         assert v3' by apply H;
         assert v5' by apply H

 end.

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