2

以下に、さらに 3 つのサブゴールがある証明を示します。証明は、ここで示されている単純な算術言語での最適化の正しさについてplus 0です。は「算術式」であり、「算術評価」です。optimize_0plusaexpaeval

3 subgoal
a1 : aexp
a2 : aexp
IHa1 : aeval (optimize_0plus a1) = aeval a1
IHa2 : aeval (optimize_0plus a2) = aeval a2
______________________________________(1/3)
aeval (optimize_0plus (APlus a1 a2)) = aeval (APlus a1 a2)

は次のoptimize_0plusとおりです。

Fixpoint optimize_0plus (a:aexp) : aexp :=
  match a with
  | ANum n =>
      ANum n
  | APlus (ANum 0) e2 =>
      optimize_0plus e2
  | APlus e1 e2 =>
      APlus (optimize_0plus e1) (optimize_0plus e2)
  | AMinus e1 e2 =>
      AMinus (optimize_0plus e1) (optimize_0plus e2)
  | AMult e1 e2 =>
      AMult (optimize_0plus e1) (optimize_0plus e2)
  end.

私の戦争計画はoptimize_0plus、現在のサブゴールの LHS に適用し、以下を取得することです。

aeval (APlus (optimize_0plus a1) (optimize_0plus a2)) = aeval (APlus a1 a2)

（しかし、Coqでこれを行う方法がわかりません）。

次に、 some を通じてsimpl、以下を取得します。

(aeval (optimize_0plus a1)) + (aeval (optimize_0plus a2)) = (aeval a1) + (aeval a2)

帰納法仮説を適用IHa1しIHa2、証明を完成させます。

私の質問は：

optimize_0plusCoq に の定義を1 回だけ適用し、それ以上もそれ以下も行わないようにするにはどうすればよいでしょうか?

私は試しましたが、それはあまりにも多くのことをしているように見えるsimpl optimize_0plus長いステートメントで何かを与えます. そして、補題を確立するために毎回タクティックmatchを使用するのは好きではありません。なぜなら、この計算は紙と鉛筆を使った正確な 1 ステップだからです。rewrite

ノート：

1.これは以前の質問 hereに関連していますが、使用に関する回答はここでは機能してsimpl XXXいないようです。これはより複雑なケースのようです。

2.元のウェブサイトは、機能する証拠を提供しています。a1しかし、そこにある証明は、用語などのケース分析を開始するため、必要以上に複雑であるように思われます.

  Case "APlus". destruct a1.
    SCase "a1 = ANum n". destruct n.
      SSCase "n = 0". simpl. apply IHa2.
      SSCase "n ≠ 0". simpl. rewrite IHa2. reflexivity.
    SCase "a1 = APlus a1_1 a1_2".
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.
    SCase "a1 = AMinus a1_1 a1_2".
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.
    SCase "a1 = AMult a1_1 a1_2".
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.

したがって、私の関心事は、この単純な定理を実際に証明することではなく、紙の上で行うように直感的に証明する方法です。

- アップデート -

@gallais のおかげで、元の計画は変更される可能性があるため正しくありません

aeval (optimize_0plus (APlus a1 a2))

に

aeval (APlus (optimize_0plus a1) (optimize_0plus a2))

a1でない場合のみANum 0。この0ケースはdestruct a1.、注 2 で引用したコースの Web サイトと同様に、個別に処理する必要があります。

ただし、以下にリストされている他のケースについても同じ質問があり、元の計画はうまくいくはずです。

5 subgoal
SCase := "a1 = APlus a1_1 a1_2" : String.string
Case := "APlus" : String.string
a1_1 : aexp
a1_2 : aexp
a2 : aexp
IHa1 : aeval (optimize_0plus (APlus a1_1 a1_2)) = aeval (APlus a1_1 a1_2)
IHa2 : aeval (optimize_0plus a2) = aeval a2
______________________________________(1/5)
aeval (optimize_0plus (APlus (APlus a1_1 a1_2) a2)) =
aeval (APlus (APlus a1_1 a1_2) a2)
...

______________________________________(5/5)
aeval (optimize_0plus (AMult a1 a2)) = aeval (AMult a1 a2)

betaこれらの 5 つのケースのそれぞれについて、 の 1 つの適用 (削減??) により、たとえば ( に対して)optimize_0plusを変更できるように思われます。AMinus

aeval (optimize_0plus (AMinus a1 a2))

に

aeval (AMinus (optimize_0plus a1) (optimize_0plus a2))

、 右？

もしそうなら、どうすればこのワンステップの削減を行うことができますか?

追記：やってみた

Eval cbv beta in (aeval (optimize_0plus (AMinus a1 a2))).

そして、私は証明でaeval (AMinus (optimize_0plus a1) (optimize_0plus a2))a を使いたいと思っても得られませんでした。Eval

4

3 に答える 3

1

Coqに必要なだけ多くの計算を行わせるのは必ずしも簡単ではないことに同意します。しかし、ここでは、あなたの言うことに反して、最初の書き換えは単なる計算ステップではありません。実際、 はoptimize_0plusその引数を 1 回破棄しますが、 の形式のものを見つけるとAPlus _ _、最初の新しい引数を破棄する必要があるため、ここではa1計算するために破棄する必要があります。

ただし、結果は依然として真であり、初期定理を証明するための便利なヘルパー レンマと見なすことができます。

Lemma optimize_0plus_aux : forall a1 a2,
  aeval (optimize_0plus (APlus a1 a2)) =
  aeval (APlus (optimize_0plus a1) (optimize_0plus a2)).
Proof.
Admitted.

ワンステップ計算に関するあなたの最初の質問に関して、私には 2 つの秘訣があります。

  • rewrite毎回使用したくないことはわかっていますが、私によると、方程式補題を持つことは、固定点を一度適用するための最良の方法です。通常、この補題は で自動的に作成できることに注意してくださいFunctional Scheme。ここ、

    Functional Scheme optimize_0plus_ind := Induction for optimize_0plus Sort Prop.

  • まれに、証明中に絶対に展開したくない関数があります。このような場合、 で定義を一時的に不透明にすることができますOpaque <function>。証明の最後に、 で再び透明にしTransparent <function>ます。しかし、私はそれが良いスタイルだとは思いませんし、使用することをお勧めしません.

于 2015-11-25T13:47:20.830 に答える
1

ここに 2 つの解決策があります。

  • 書き直し補題をまさにあなたが望むもので述べ、それを証明してからそれを使用してください。これは、非常に複雑な書き換えを行う必要がある場合に最適なソリューションですが、状況ごとに補題を記述する必要があるため、うまくスケーリングできません。たとえば、次のように述べることができます (そして を使って自明に証明できますsimpl):

      forall a1 a2, optimize_0plus (APlus a1 a2) = APlus (optimize_0plus a1) (optimize_0plus a2).

  • 私の記憶が正しければsimpl、他の人はバインダーの下に行かない. 戦術を使用して、pattern単純化したい部分を「抽出」して、式の一部のサブ用語でのみ実行することができますsimpl。ここで説明すると少し長くなるので、ドキュメントunfoldを読む必要があります。

  • replace編集：戦術について話すのを忘れていました。これはrewrite解決策のように機能しますが、サブゴールとして、補題をすぐに証明するように求めます。

于 2015-11-25T08:26:46.667 に答える