1

Coq で用語を並べ替える方法について一般的な質問があります。たとえば、用語がある場合m + p + n + p、人間は用語を次のようにすばやく再配置できますm + n + p + p(暗黙的に plus_comm と plus_assoc を使用します)。Coqでこれを効率的に行うにはどうすればよいでしょうか?

（ばかげた）例として、

Require Import Coq.Arith.Plus.
Require Import Coq.Setoids.Setoid.

Theorem plus_comm_test: forall n m p: nat,
  m + p + (n + p) = m + n + 2 * p.
Proof. intros. rewrite plus_assoc. simpl. rewrite <- plus_n_O.

今、私たちは持っています

1 subgoals
...
______________________________________(1/1)
m + p + n + p = m + n + (p + p)

私の質問は：

m + n + p + pLHS を効果的に書き換えるにはどうすればよいですか?

を使用しようとしましrewrite plus_comm at 2たが、エラーが発生します。Nothing to rewrite.単純に rewrite を使用plus_commすると、LHS が に変更されp + m + n + pます。

効果的な書き直しに関する提案も歓迎します。

ありがとう。

4

3 に答える 3

1

Arthur が言うようomegaに、十分でない場合もありますが、このような簡単な手順に使用することもあります。

Require Import Omega.
Theorem test: forall a b c:nat, a + b + 2 * c = c + b + a + c.
  intros.
  replace (c + b + a) with (a + b + c) by omega.
  replace (a + b + c + c) with (a + b + (c + c)) by omega.
  replace (c + c) with (2 * c) by omega.
  reflexivity.
Qed.

これはばかげた例です。一度にすべてを解決できたはずですが、少し助けがなければ到達できないomega関数内のものを書き直したい場合があります...omega

于 2015-10-07T16:09:57.560 に答える