proof - Coqでゴールを「S x = S y」から「x = y」に変える戦術は

Question

S x = S y目標をからに変更したいx = y。のようなものinversionですが、仮説ではなく目標のためです。

このような戦術は正当に思えます。なぜなら、x = yがあれば、単純に and を使用rewriteしreflexivityて目的を証明できるからです。

現在、私は常に新しいサブゴールを導入するために使用していることに気づきますが、複雑な表現である場合をassert (x = y)記述するのは面倒です。xy

score 7 · Accepted Answer

タクティックapply f_equal.は、任意のコンストラクターまたは関数に対して、必要なことを行います。

レマf_equalは、どの関数fに対しても常にを持っていることを示していますx = y -> f x = f y。f x = f yこれにより、目標をからに減らすことができますx = y。

Proposition myprop (x y: nat) (H : x = y) : S x = S y.
Proof.
  apply f_equal.  assumption.
Qed.

(このinjectionタクティックは、逆の含意を実装します — 一部の関数、特にコンストラクターに対しては、f x = f y -> x = y.)

score 1 · Accepted Answer

2 に答える 2