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

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

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

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

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

Automatically choose an assumption from local context

coq

coq-tactic