8

Coq リファレンス マニュアル (8.5p1) から、私の印象はrevertの逆ですが、ある程度introはそうです。generalizeたとえば、revert以下generalize dependentは同じようです。

Goal forall x y: nat, 1 + x = 2 + y -> 1 + x + 5 = 7 + y.
intros x y. revert x y.
intros x y. generalize dependent y. generalize dependent x.

generalizeより強力なのはそれだけですかrevert？

また、ドキュメントは次のことを説明するのに少し循環的ですgeneralize:

この戦術は、あらゆる目標に適用されます。ある用語に関して結論を​​一般化します。

generalizeラムダ計算の抽象化演算子に似ていますか?

4

2 に答える 2

7

はい、generalizeより強力です。revertでシミュレートすることによりrevert、少なくとも同じ力があることを実証しましたgeneralize。--識別子に対してのみ、generalizeどの用語に対しても機能することに注意してください。revert

たとえばrevert、マニュアルの例を実行することはできません:

  x, y : nat
  ============================
  0 <= x + y + y

Coq < generalize (x + y + y).
1 subgoal

  x, y : nat
  ============================
  forall n : nat, 0 <= n

定義の「循環性」に関しては、実際の説明は例のすぐ下にあります。

ゴールがGであり、 ゴール内のtのサブタームである場合、はゴールをに置き換えます。Tgeneralize tforall x:T, G0G0Gtx

基本的に、これはgeneralize目標を でラップしforall、一部の用語を新しい変数 ( ) に置き換えますx。

もちろん、generalize使用後に虚偽のステートメントが証明される可能性があるため、いくつかの考慮と注意を払って使用する必要があります。

Goal forall x y, x > 0 -> 0 < x + y + y.
  intros x y H.
  generalize dependent (x + y + y).

(* results in this proof state: *)
  x, y : nat
  H : x > 0
  ============================
   forall n : nat, 0 < n
于 2016-06-28T06:53:41.797 に答える
1

私が思い出す限りでは、revertは の単純な形式でありgeneralize、通常は初心者にとって使いやすいものです。これは の反対ですintro。のフレーバーを使用するとgeneralize、さらに多くのことができます (特に、用語と型の間の依存関係で)。

于 2016-06-28T06:52:45.327 に答える