coq - 自动从本地上下文中选择一个假设

Question

我有一个证明脚本，其中有一个部分看起来像这样:

  - destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence.
  - destruct (IHx1 _ _ H6). congruence.
  - destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence.
  - destruct (IHx1 _ _ H6). congruence.
  - destruct (IHx  _ _ H2). congruence.
  - destruct (IHx  _ _ H5). congruence.
  - destruct (IHx  _ _ H2). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H7). congruence.
  - destruct (IHx  _ _ H4). congruence.
  - destruct (IHx1 _ _ H8). congruence.
  - destruct (IHx1 _ _ H5). subst. destruct (IHx2 _ _ H9).

它似乎是使用 ; 干净地解决问题的候选者，不幸的是，假设无处不在。如何将各种子证明折叠在一起？

Answer 1

我们只有一个归纳假设的情况可以使用以下 Ltac 解决(参见手册，chapter 9):

match goal with
  IH : forall st2 s2, ?c / ?st \\ s2 / st2 -> _,
  H : ?c / ?st \\ _ / _
  |- _ => now destruct (IH  _ _ H)
end

变量以问号为前缀，例如?c、?st等是模式匹配元变量，逗号分隔假设，十字转门符号(|-)分隔假设目标。在这里，我们正在寻找归纳假设 IH 和兼容假设 H，以便我们可以将 IH 应用于 H。 ?c/?st 部分确保 IH 和 H 兼容。

具有两个归纳假设的子目标可以类似地解决:

match goal with
  IH1 : forall st2 s2, ?c1 / ?st \\ s2 / st2 -> _,
  IH2 : forall st2 s2, ?c2 / _ \\ s2 / st2 -> _,
  H1 : ?c1 / ?st \\ _ / ?st'',
  H2 : ?c2 / ?st'' \\ _ / st2
  |- _ => now destruct (IH1  _ _ H1); subst; destruct (IH2 _ _ H2)
end

当然，如果你愿意，你可以将名称绑定(bind)到那些自定义战术上，对它们使用战术等等:

Ltac solve1 :=
  try match goal with
        IH : forall st2 s2, ?c / ?st || s2 / st2 -> _,
        H : ?c / ?st || _ / _
        |- _ => now destruct (IH  _ _ H)
      end.