coq - 我如何推广 iff 的 Coq 证明？

Question

我必须做出的一种常见证明是这样的

Lemma my_lemma : forall y, (forall x x', Q x x' y) -> (forall x x', P x y <-> P x' y).
Proof.
  intros y Q_y.
  split.
  + <some proof using Q>
  + <the same proof using Q, but x and x' are swapped>

其中 Q 本身就是某种 iff 形谓词。

我的问题是，P x y -> P x' y 和 P x' y -> P x y 的证明通常基本相同，唯一的区别是其中 x 和 x' 的角色在它们之间交换。我可以要求 Coq 将目标转化为

forall x x', P x y -> P x' y

然后推广到 iff 情况，这样我就不需要在证明中重复自己了？

我浏览了标准库、策略索引和一些 SO 问题，但没有告诉我如何做到这一点。

Answer 1

这是一个自定义策略:

Ltac sufficient_if :=
  match goal with
  | [ |- forall (x : ?t) (x' : ?t'), ?T <-> ?U ] =>    (* If the goal looks like an equivalence (T <-> U) (hoping that T and U are sufficiently similar)... *)
    assert (HHH : forall (x : t) (x' : t'), T -> U);   (* Change the goal to (T -> U) *)
      [ | split; apply HHH ]                           (* And prove the two directions of the old goal  *)
  end.

Parameter Q : nat -> nat -> nat -> Prop.
Parameter P : nat -> nat -> Prop.
Lemma my_lemma : forall y, (forall x x', Q x x' y) -> (forall x x', P x y <-> P x' y).
Proof.
  intros y Q_y.
  sufficient_if.