如何无需提前引入变量匹配Coq中的蕴含式？

需要编写一个Coq Tactic，用于检查目标是否为带任意数量全称量词的蕴含式，要求无需提前引入变量，像forall A B C D, (A/\B)->(C\/D)这类多变量的形式也能被正确判定为有效形式。但编写的代码执行报错，代码如下：

Ltac is_implication term :=
  match term with
  | ?A -> ?B => idtac term "is an implication"
  | _ => idtac term "is not an implication"; fail 1
  end.


Ltac universal_implication :=
  match goal with
  | [ |- forall _ , ?G]=>is_implication G
  | _=>idtac "Goal is not an universally quantified implication";fail 1
end.


Lemma toto: forall A B:Prop ,A->B.
universal_implication.

(*returns "Goal is not an universally quantified implication
Tactic failure".*)

问题原因 #

原universal_implication只匹配了单层全称量词的情况，但目标中的forall A B:Prop, A->B包含两层全称量词，导致匹配逻辑无法覆盖，直接进入了失败分支。

修正方案 #

通过递归处理所有全称量词，直到剥离完所有forall绑定后，再检查剩余部分是否为蕴含式：

Ltac is_implication term :=
  match term with
  | ?A -> ?B => idtac term "is an implication"
  | _ => idtac term "is not an implication"; fail 1
  end.

Ltac universal_implication :=
  match goal with
  | [ |- forall _ , ?G] => universal_implication  (* 递归剥离所有全称量词 *)
  | [ |- ?G] => is_implication G                  (* 剥离完成后检查是否为蕴含式 *)
  | _ => idtac "Goal is not an universally quantified implication"; fail 1
  end.

测试验证 #

测试原Lemma toto：

Lemma toto: forall A B:Prop ,A->B.
universal_implication.
(* 输出：(A -> B) is an implication *)

测试多变量场景：

Lemma test: forall A B C D:Prop, (A/\B)->(C\/D).
universal_implication.
(* 输出：((A /\ B) -> (C \/ D)) is an implication *)

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