7

coq では、補題または仮説を現在の目標の部分式に適用することは何とか可能ですか? たとえば、この例で 3 と 4 を交換するために、プラスが可換であるという事実を適用したいと思います。

Require Import Coq.Arith.Plus.

Inductive foobar : nat -> Prop :=
 | foob : forall n:nat, foobar n.

Goal foob (3 + 4) = foob (4 + 3).
Proof.
apply plus_comm. (* or maybe rewrite plus_comm *)

与えます：

Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with
"foob (3 + 4) = foob (4 + 3)".

plus_comm を適用するこの目標の正確な場所を coq に伝えるにはどうすればよいですか?

4

2 に答える 2

5

戦術の使用はsimpl機能しますが、理由rewrite plus_commや機能しないことを私に聞かないでくださいrewrite (plus_comm 3 4)。apply方程式ではなく含意のためです。

于 2012-11-30T13:57:18.173 に答える