如何编写支持任意数量量词的Coq Ltac iff拆分策略？

你需要将形如forall x y z ..., A <-> B的命题拆分为两个蕴含命题forall x y z ..., A -> B和forall x y z ..., B -> A，原策略仅支持固定数量的量词，以下是两种可行解决方案：

方法一：递归匹配处理量词 #

通过递归Ltac逐个消解forall量词，直到定位到核心的<->命题：

Ltac iff_split H :=
  match type of H with
  | forall x, ?T =>
      let H_temp := fresh H in
      pose H as H_temp;
      clear H;
      intros x;
      iff_split H_temp;
      generalize x;
      intros x;
      rename (H_temp_r) into (H_r);
      rename (H_temp_l) into (H_l);
      clear H_temp
  | ?A <-> ?B =>
      let H_r := fresh H "r" in
      let H_l := fresh H "l" in
      assert (H_r : A -> B) by (apply H);
      assert (H_l : B -> A) by (apply H);
      clear H
  end.

工作逻辑 #

1. 匹配到forall x, T时，先临时保存原假设，进入量词作用域后递归处理剩余命题；
2. 递归完成后重新引入量词，并重命名生成的蕴含假设；
3. 匹配到A <-> B时，直接生成两个方向的蕴含假设并清除原假设。

方法二：利用标准库函数简化实现 #

借助Coq标准库自带的proj1和proj2函数（分别对应<->的前向/后向蕴含），无需递归即可处理任意数量量词：

Ltac iff_split H :=
  let prop_type := type of H in
  let forward_type := eval cbv beta in (fun p => proj1 p) prop_type in
  let backward_type := eval cbv beta in (fun p => proj2 p) prop_type in
  let H_r := fresh H "r" in
  let H_l := fresh H "l" in
  assert (H_r : forward_type) by (apply proj1, H);
  assert (H_l : backward_type) by (apply proj2, H);
  clear H.

工作逻辑 #

1. proj1的类型为forall A B, (A <-> B) -> (A -> B)，它会自动对forall量词做类型提升，作用在forall x y ..., A <-> B上时，会直接得到forall x y ..., A -> B；
2. 通过eval cbv beta计算出对应的蕴含命题类型，再用assert生成新假设；
3. proj2对应后向蕴含B -> A，逻辑与proj1完全一致。

测试示例 #

Lemma test_iff : forall a b c, (a + b = c) <-> (c - b = a).
Proof.
  intros.
  iff_split H.
  (* 此时会生成H_r : forall a b c, (a + b = c) -> (c - b = a)
     和H_l : forall a b c, (c - b = a) -> (a + b = c) *)
Abort.

内容的提问来源于stack exchange，提问作者Jay Lee