3

我有一个证明脚本，其部分如下所示：

  - 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).

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

4

1 回答 1

2

我们只有一个归纳假设的情况可以使用以下 Ltac 来解决（参见手册，第 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

当然，如果您愿意，可以将名称绑定到这些自定义策略，使用 tactical 与它们等等：

Ltac solve1 :=
  try match goal with
        IH : forall st2 s2, ?c / ?st || s2 / st2 -> _,
        H : ?c / ?st || _ / _
        |- _ => now destruct (IH  _ _ H)
      end.
于 2017-05-29T07:40:20.220 回答