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

帰納仮説が 1 つしかない場合は、次の Ltac を使用して解決できます (マニュアルの第 9 章を参照)。

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

?c、などの疑問符?stで始まる変数がパターン マッチング メタ変数である場合、コンマは仮説を区切り、回転式改札口記号 ( |-) は仮説とゴールを区切ります。ここで、に適用できる帰納仮説IHと互換性のある仮説を探します。部品は確実に互換性があります。HIHH?c / ?stIHH

帰納仮説が 2 つあるサブゴールは、同様に解くことができます。

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.
于 2017-05-29T07:40:20.220 に答える