この章では、学習のためにCoqを使う方法に焦点を当てます。 ここで学ぶ対象は、Imp と呼ばれる単純な命令型プログラミング言語です。 Imp は C や Java のような標準的に広く使われている言語の中心部分の機能だけを取り出したものです。 下の例は、おなじみの数学的関数を Imp で書いたものです。

       Z ::= X;;  
       Y ::= 1;;  
       WHILE ~(Z = 0) DO  
         Y ::= Y * Z;;  
         Z ::= Z - 1  
       END  

この章ではImpの構文(syntax)と意味(semantics)の定義方法について学びます。 「プログラミング言語の基礎(Programming Language Foundations)」（ソフトウェアの基礎(Software Foundations)、第二巻）の章では、プログラムの同値性(program equivalence)の理論を構築し、命令型プログラムについての推論のための論理として一番知られているホーア論理(Hoare Logic)を導入します。

算術式とブール式

Impを三つの部分に分けて示します： 最初に算術式(arithmetic expressions)とブール式(boolean expressions)、次にこれらの式に変数(variables)を加えたもの、 そして最後に代入(assignment)、条件分岐(conditions)、コマンド合成(sequencing)、ループ(loops)を持つコマンド(commands)の言語です。

構文

次の2つの定義は、算術式とブール式の抽象構文(abstract syntax)を定めます。

この章では、プログラマが実際に書く具象構文から抽象構文木への変換はほとんど省略します。 例えば、文字列"1 + 2 * 3"をAST（Abstract Syntax Tree, 抽象構文木）
      APlus (ANum 1) (AMult (ANum 2) (ANum 3))

にする変換のことです。 この変換に使う単純な字句解析器と構文解析器をオプションの章ImpParserで実装します。 この章を理解するのにImpParser章の理解は必要ではありませんが、もしこれらの技術について（例えばコンパイラの講義などで）触れたことがないならば、ざっと見てみるのも良いでしょう。

比較のため、同じ抽象構文を定義する慣習的なBNF(Backus-Naur Form)文法を以下に示します:

    a ::= nat 
        | a + a 
        | a - a 
        | a * a 
 
    b ::= true 
        | false 
        | a = a 
        | a <= a 
        | ~ b 
        | b && b 

上述のCoq版と比較して...

• BNFはより非形式的です。 例えば、BNFは式の表面的な構文についていくらかの情報（可算は中置記号+を使って記述される、など）を与えていますが、字句解析と構文解析の他の面（+、-、*の優先順位、括弧による部分式のくくりだし、など）は定めないままになっています。 コンパイラを実装するときなどは、この記述を形式的定義にするために、追加の情報（および人間の知性）が必要でしょう。
  Coq版はこれらの情報を整合的に省略し、抽象構文だけに集中します。
• 逆に、BNF版はより軽くて、読むのがより簡単です。 非形式的であることで柔軟性を持っているので、黒板を使って議論する場面などでは特段に有効です。 そういう場面では、細部をいちいち正確に確定させていくことより、全体的アイデアを伝えることが重要だからです。
  実際、BNFのような記法は山ほどあり、人は皆、それらの間を自由に行き来しますし、通常はそれらのうちのどのBNFを使っているかを気にしません。 その必要がないからです。 おおざっぱな非形式的な理解だけが必要なのです。

両方の記法に通じているのは良いことです。 非形式的なものは人間とのコミュニケーションに、形式的なものは実装と証明に便利です。

評価

算術式を評価する(evaluating)と、式から1つの数を生成します。

同様に、ブール式を評価するとブール値になります。

最適化(Optimization)

ここまで定義したものはわずかですが、その定義から既にいくらかのものを得ることができます。 算術式をとって、それを少し簡単化する関数を定義するとします。 すべての 0 + e （つまりAPlus (ANum 0) e）を単にeにするものです。

この最適化が正しいことをすることを確認するために、 いくつかの例についてテストして出力がよさそうかを見てみることができます。

しかし、もし最適化が正しいことを確認したいならば、つまり、最適化した式がオリジナルの式と同じ評価結果を返すことを確認したいならば、証明すべきです。

Coq の自動化

前の証明の最後の繰り返しはちょっと面倒です。 証明対象の言語や最適化の健全性証明が今に比べて著しく複雑だったら、現実的な問題になるでしょう。 ここまで、Coq のタクティックのほんのひとつかみだけですべての証明をしてきていて、証明を自動的に構成する非常に強力な機構を完全に無視してきました。 このセクションではこれらの機構のいくつかを紹介します。 それ以上のものを、以降のいくつかの章で次第に見ることになるでしょう。 それらに慣れるには多少エネルギーが必要でしょう。 Coq の自動化は電動工具です。-- しかし自動化機構を使うことで、より複雑な定義や、より興味深い性質について、退屈で繰り返しの多いローレベルな詳細に飲み込まれることなく、作業をスケールアップできます。

タクティカル(Tacticals)

タクティカル(tactical)は Coq の用語で、他のタクティックを引数に取るタクティックのことです。 「高階タクティック(higher-order tactics)」と言っても良いでしょう。

tryタクティカル

Tがタクティックのとき、タクティック try T はTと同様ですが、Tが失敗するときtry T は（失敗する代わりに）成功として何もしない点が違います。

There is no real reason to use try in completely manual proofs like these, but it is very useful for doing automated proofs in conjunction with the ; tactical, which we show next.

;タクティカル（基本形）

一番よくある形として、; タクティカルは二つのタクティックを引数として取ります。 TとT'がタクティックのとき、T;T' はタクティックで、最初にTを行い、Tが生成した「サブゴールそれぞれ」にT'を行います。

例えば、次の簡単な補題を考えます:

上の証明を;タクティカルを使って簡単化できます。

tryと;の両方を使うと、ちょっと前に悩まされた証明の繰り返しを取り除くことができます。

Coqの専門家は、tryをinductionのようなタクティックと一緒に使うことで、多くの似たような「簡単な」場合を一度に処理します。 これは自然に非形式的な証明に対応します。 例えば、この定理の形式的な証明の構造にマッチする非形式的な証明は次の通りです: 「定理」: すべての算術式aについて
       aeval (optimize_0plus a) = aeval a

「証明」: aについての帰納法を使う。 ほとんどの場合は帰納仮定から直ちに得られる。 残るのは以下の場合である:

• あるnについて a = ANum n とする。示すべきことは次の通りである:
            aeval (optimize_0plus (ANum n)) = aeval (ANum n)
  これはoptimize_0plusの定義からすぐに得られる。
• あるa1とa2について a = APlus a1 a2 とする。 示すべきことは次の通りである:
            aeval (optimize_0plus (APlus a1 a2)) = aeval (APlus a1 a2)
  a1のとり得る形を考える。 そのほとんどの場合、optimize_0plusは部分式について単に自分自身を再帰的に呼び出し、a1と同じ形の新しい式を再構成する。 これらの場合、結果は帰納仮定からすぐに得られる。
  興味深い場合は、あるnについて a1 = ANum n であるときである。 このとき n = 0 ならば次が成立する:
            optimize_0plus (APlus a1 a2) = optimize_0plus a2
  そしてa2についての帰納仮定がまさに求めるものである。 一方、あるn'について n = S n' ならば、optimize_0plusはやはり自分自身を再帰的に呼び出し、結果は帰納仮定から得られる。 ☐

しかし、この証明はさらに改良できます。 最初の場合（a = ANum n のとき）はかなり自明です。 帰納仮定からすぐに得られるとわざわざ言う必要もないくらい自明でしょう。 それなのに完全に記述しています。 これを消して、単に最初に 「ほとんどの場合、すぐに、あるいは帰納仮定から直接得られる。興味深いのはAPlusの場合だけである...」 と言った方がより良く、より明快でしょう。 同じ改良を形式的な証明にも行うことができます。 以下のようになります:

The ; Tactical (General Form)

The ; tactical also has a more general form than the simple T;T' we've seen above. If T, T1, ..., Tn are tactics, then T; T1 | T2 | ... | Tn is a tactic that first performs T and then performs T1 on the first subgoal generated by T, performs T2 on the second subgoal, etc. So T;T' is just special notation for the case when all of the Ti's are the same tactic; i.e., T;T' is shorthand for: T; T' | T' | ... | T'

The repeat Tactical

The repeat tactical takes another tactic and keeps applying this tactic until it fails. Here is an example showing that 10 is in a long list using repeat.

The tactic repeat T never fails: if the tactic T doesn't apply to the original goal, then repeat still succeeds without changing the original goal (i.e., it repeats zero times).

The tactic repeat T also does not have any upper bound on the number of times it applies T. If T is a tactic that always succeeds, then repeat T will loop forever (e.g., repeat simpl loops, since simpl always succeeds). While evaluation in Coq's term language, Gallina, is guaranteed to terminate, tactic evaluation is not! This does not affect Coq's logical consistency, however, since the job of repeat and other tactics is to guide Coq in constructing proofs; if the construction process diverges (i.e., it does not terminate), this simply means that we have failed to construct a proof, not that we have constructed a wrong one.

練習問題: ★★★, standard (optimize_0plus_b_sound)

optimize_0plusの変換がaexpの値を変えないことから、bexpの値を変えずに、bexpに現れるaexpをすべて変換するためにoptimize_0plusが適用できるべきでしょう。 bexpについてこの変換をする関数を記述しなさい。 そして、それが健全であることを証明しなさい。 ここまで見てきたタクティカルを使って証明を可能な限りエレガントにしなさい。

☐

練習問題: ★★★★, standard, optional (optimize)

設計練習: 定義したoptimize_0plus関数で実装された最適化は、算術式やブール式に対して考えられるいろいろな最適化の単なる1つに過ぎません。 より洗練された最適化関数を記述し、その正しさを証明しなさい。 （本当に簡単な最適化を作って証明し、それを少しずつ面白いものに仕立て上げていくと良いでしょう。）

新しいタクティック記法を定義する

Coqはまた、タクティックスクリプトを「プログラミングする」いろいろな方法も提供します。

• Tactic Notation コマンドは、「略記法タクティック("shorthand tactics")」を定義する簡単な方法を提供します。 「略記法タクティック」は、呼ばれると、いろいろなタクティックを一度に適用します。
• より洗練されたプログラミングのために、CoqはLtacと呼ばれる小さな組込みの言語と、証明の状態を調べたり変更したりするためのLtacのプリミティブを提供します。 その詳細はここで説明するにはちょっと複雑過ぎます（しかも、LtacはCoqの設計の一番美しくない部分だというのが共通見解です!）。 しかし、詳細はリファレンスマニュアルにありますし、Coqの標準ライブラリには、読者が参考にできるLtacの定義のたくさんの例があります。
• Coqの内部構造のより深いレベルにアクセスする新しいタクティックを作ることができるOCaml API も存在します。 しかしこれは、普通のCoqユーザにとっては、苦労が報われることはほとんどありません。

Tactic Notation 機構は取り組むのに一番簡単で、多くの目的に十分なパワーを発揮します。 例を挙げます。

これは1つのタクティックcを引数としてとるsimpl_and_tryという新しいタクティカルを定義しています。 simpl_and_try c はタクティック simpl; try c と同値です。 例えば、証明内で"simpl_and_try reflexivity."と書くことは「simpl; try reflexivity.」と書くことと同じでしょう。

omegaタクティック

omegaタクティックは「プレスバーガー算術」(Presburger arithmetic、「プレスブルガー算術」とも)と呼ばれる一階述語論理のサブセットの決定手続き(decision procedure)を実装します。 William Pugh が発明したOmegaアルゴリズム Pugh 1991 （Bib.v 参照）に基いています。 ゴールが以下の要素から構成された全称限量された論理式とします。以下の要素とは:

• 数値定数、加算（+とS）、減算（-とpred）、定数の乗算（これがプレスバーガー算術である条件です）、
• 等式（=と<>）および不等式（<=）、
• 論理演算子/\, \/, ~, ->

です。 このとき、omegaを呼ぶと、ゴールを解くか、失敗によりそのゴールが偽であることを表すか、いずれかになります。 （ただしゴールが上記の形「ではない」場合にもomegaは失敗します。）

(Note the From Coq Require Import omega.Omega. at the top of the file.)

便利なタクティックをさらにいくつか

最後に、役に立ちそうないろいろなタクティックをいくつか紹介します。

• clear H: 仮定Hをコンテキストから消去します。
• subst x: 変数xについて、コンテキストから仮定 x = e または e = x を発見し、xをコンテキストおよび現在のゴールのすべての場所でeに置き換え、この仮定を消去します。
• subst: x = e および e = x の形（xは変数）のすべての仮定を置換します。
• rename... into...: 証明コンテキストの仮定の名前を変更します。 例えば、コンテキストがxという名前の変数を含んでいるとき、rename x into y は、すべてのxの出現をyに変えます。
• assumption: ゴールにちょうどマッチする仮定Hをコンテキストから探そうとします。 発見されたときは apply H と同様に振る舞います。
• contradiction: Falseと同値の仮定Hをコンテキストから探そうとします。 発見されたときはゴールを解きます。
• constructor: 現在のゴールを解くのに使えるコンストラクタcを（現在の環境のInductiveによる定義から）探そうとします。 発見されたときは apply c と同様に振る舞います。

進むにしたがって、これら全てについてたくさんの例を見ることになります。

関係としての評価

aevalとbevalをFixpointによって定義された関数として示しました。 評価について考える別の方法は、それを式と値との間の関係(relation)と見ることです。 この方法は、多くの場合Fixpointを用いたものより柔軟です。 この考えに立つと、算術式についてCoqのInductiveによる以下の定義が自然に出てきます...

Instead, we've chosen to leave the hypotheses anonymous, just giving their types. This style gives us less control over the names that Coq chooses during proofs involving aevalR, but it makes the definition itself quite a bit lighter.

aevalRの中置記法を定義するのと便利です。 算術式eが値nに評価されることを e \\ n と書きます。

実際は、CoqにはaevalR自身の定義中でこの記法を使う方法があります。 これにより、e \\ n の形の主張を含む証明で、aevalR e nという形の定義に戻らなければならない状況にならずに済みます。 このためには、最初に記法を「予約」し、それから定義と、記法が何を意味するかの宣言とを一緒に行います。

Inference Rule Notation

In informal discussions, it is convenient to write the rules for aevalR and similar relations in the more readable graphical form of inference rules, where the premises above the line justify the conclusion below the line (we have already seen them in the IndProp chapter). For example, the constructor E_APlus... | E_APlus : forall (e1 e2: aexp) (n1 n2: nat), aevalR e1 n1 -> aevalR e2 n2 -> aevalR (APlus e1 e2) (n1 + n2) ...would be written like this as an inference rule: e1 \\ n1 e2 \\ n2

---

(E_APlus) APlus e1 e2 \\ n1+n2 Formally, there is nothing deep about inference rules: they are just implications. You can read the rule name on the right as the name of the constructor and read each of the linebreaks between the premises above the line (as well as the line itself) as ->. All the variables mentioned in the rule (e1, n1, etc.) are implicitly bound by universal quantifiers at the beginning. (Such variables are often called metavariables to distinguish them from the variables of the language we are defining. At the moment, our arithmetic expressions don't include variables, but we'll soon be adding them.) The whole collection of rules is understood as being wrapped in an Inductive declaration. In informal prose, this is either elided or else indicated by saying something like "Let aevalR be the smallest relation closed under the following rules...". For example, \\ is the smallest relation closed under these rules:

---

(E_ANum) ANum n \\ n e1 \\ n1 e2 \\ n2

---

(E_APlus) APlus e1 e2 \\ n1+n2 e1 \\ n1 e2 \\ n2

---

(E_AMinus) AMinus e1 e2 \\ n1-n2 e1 \\ n1 e2 \\ n2

---

(E_AMult) AMult e1 e2 \\ n1*n2

Exercise: 1 star, standard, optional (beval_rules)

Here, again, is the Coq definition of the beval function: Fixpoint beval (e : bexp) : bool := match e with | BTrue => true | BFalse => false | BEq a1 a2 => (aeval a1) =? (aeval a2) | BLe a1 a2 => (aeval a1) <=? (aeval a2) | BNot b1 => negb (beval b1) | BAnd b1 b2 => andb (beval b1) (beval b2) end. Write out a corresponding definition of boolean evaluation as a relation (in inference rule notation).

☐

Equivalence of the Definitions

評価の、関係による定義と関数による定義が一致することを証明するのは簡単です。

さらにタクティカルを使うことで証明をより短くできます。

練習問題: ★★★, standard (bevalR)

関係bevalRをaevalRと同じスタイルで記述し、それがbevalと同値であることを証明しなさい。

☐

Computational vs. Relational Definitions

算術式とブール式の評価の定義について、関数を使うか関係を使うかはほとんど趣味の問題です。 どちらでも問題ありません。 しかしながら、評価の定義として、関係による定義が関数による定義よりはるかに望ましい状況があります。

For example, suppose that we wanted to extend the arithmetic operations with division:

Extending the definition of aeval to handle this new operation would not be straightforward (what should we return as the result of ADiv (ANum 5) (ANum 0)?). But extending aevalR is straightforward.

Or suppose that we want to extend the arithmetic operations by a nondeterministic number generator any that, when evaluated, may yield any number. (Note that this is not the same as making a probabilistic choice among all possible numbers -- we're not specifying any particular probability distribution for the results, just saying what results are possible.)

Again, extending aeval would be tricky, since now evaluation is not a deterministic function from expressions to numbers, but extending aevalR is no problem...

At this point you maybe wondering: which style should I use by default? In the examples we've just seen, relational definitions turned out to be more useful than functional ones. For situations like these, where the thing being defined is not easy to express as a function, or indeed where it is not a function, there is no real choice. But what about when both styles are workable? One point in favor of relational definitions is that they can be more elegant and easier to understand. Another is that Coq automatically generates nice inversion and induction principles from Inductive definitions. On the other hand, functional definitions can often be more convenient:

• Functions are by definition deterministic and defined on all arguments; for a relation we have to show these properties explicitly if we need them.
• With functions we can also take advantage of Coq's computation mechanism to simplify expressions during proofs.

Furthermore, functions can be directly "extracted" from Gallina to executable code in OCaml or Haskell. Ultimately, the choice often comes down to either the specifics of a particular situation or simply a question of taste. Indeed, in large Coq developments it is common to see a definition given in both functional and relational styles, plus a lemma stating that the two coincide, allowing further proofs to switch from one point of view to the other at will.

変数を持つ式

Impの定義に戻りましょう。 次にしなければならないことは、算術式とブール式に変数を拡張することです。 話を単純にするため、すべての変数はグローバルで、数値だけを持つとしましょう。

状態

Since we'll want to look variables up to find out their current values, we'll reuse maps from the Maps chapter, and strings will be used to represent variables in Imp. A machine state (or just state) represents the current values of all variables at some point in the execution of a program.

簡単にするため、どのようなプログラムも有限個の変数しか使いませんが、状態はすべての変数について定義されているものとします。 状態はメモリ中に格納されている全ての情報を持ちます。 Imp で書かれたプログラムでは全ての変数が自然数だけを格納することから、状態を文字列から nat への写像で表現できます。 このとき状態の初期値は0ということにしておきます。 複雑なプログラミング言語では、状態はより複雑な構造となるでしょう。

構文

前に定義した算術式に、単にもう1つコンストラクタを追加することで変数を追加できます:

Defining a few variable names as notational shorthands will make examples easier to read:

（プログラム変数のこの慣習（X, Y, Z）は、大文字は型を表すのに使うという使用法と衝突します。 Impを構成していく章では多相性を多用はしないので、このことが混乱を招くことはないはずです。）

bexpの定義は（新しいaexpを使うこと以外）変わっていません:

Notations

To make Imp programs easier to read and write, we introduce some notations and implicit coercions. You do not need to understand exactly what these declarations do. Briefly, though, the Coercion declaration in Coq stipulates that a function (or constructor) can be implicitly used by the type system to coerce a value of the input type to a value of the output type. For instance, the coercion declaration for AId allows us to use plain strings when an aexp is expected; the string will implicitly be wrapped with AId. The notations below are declared in specific notation scopes, in order to avoid conflicts with other interpretations of the same symbols. Again, it is not necessary to understand the details, but it is important to recognize that we are defining new intepretations for some familiar operators like +, -, *, =., [<=], etc.

One downside of these coercions is that they can make it a little harder for humans to calculate the types of expressions. If you get confused, try doing Set Printing Coercions to see exactly what is going on.

評価

算術とブールの評価器は、状態を引数に追加するという自明な方法で変数を扱うように拡張できます:

We specialize our notation for total maps to the specific case of states, i.e. using (_ !-> 0) as empty state.

Now we can add a notation for a "singleton state" with just one variable bound to a value.

コマンド

さて、Imp コマンド（「文(statement)」と呼ばれることもあります）の構文と挙動を定義する準備が出来ました。

構文

非形式的には、コマンド c は以下の BNF で表現されます。

     c ::= SKIP | x ::= a | c ;; c | TEST b THEN c ELSE c FI 
         | WHILE b DO c END 

（すこし不格好な具象構文を使っていますが、これはImpの構文をCoqのNotationの機能を使って記述するためです。 特に、TESTは標準ライブラリのifやIFとの衝突を避けてのものです。） 例えば、Imp における階乗の計算は以下のようになります。

     Z ::= X;; 
     Y ::= 1;; 
     WHILE ~(Z = 0) DO 
       Y ::= Y * Z;; 
       Z ::= Z - 1 
     END 

このコマンドが終わったとき、変数 Y は変数 X の初期値の階乗を持つでしょう。

以下に、コマンドの抽象構文の形式的定義を示します。

式と同様、Impプログラムを読み書きしやすくするために、いくつかの Notation 宣言が使えます。

例えば先の階乗関数を Coq での形式的な定義として記述し直すと、以下のようになります。

Desugaring notations

Coq offers a rich set of features to manage the increasing complexity of the objects we work with, such as coercions and notations. However, their heavy usage can make for quite overwhelming syntax. It is often instructive to "turn off" those features to get a more elementary picture of things, using the following commands:

• Unset Printing Notations (undo with Set Printing Notations)
• Set Printing Coercions (undo with Unset Printing Coercions)
• Set Printing All (undo with Unset Printing All)

These commands can also be used in the middle of a proof, to elaborate the current goal and context.

The Locate command

Finding notations

When faced with unknown notation, use Locate with a string containing one of its symbols to see its possible interpretations.

Finding identifiers

When used with an identifier, the command Locate prints the full path to every value in scope with the same name. This is useful to troubleshoot problems due to variable shadowing.

他の例

代入:

ループ

無限ループ:

コマンドの評価

次に、Imp のコマンドの実行が何を意味するかを定義する必要があります。 WHILE ループが終了しなくても良くするため、評価関数の定義を少し変わった形にしています ...

関数としての評価（失敗版）

以下は WHILE 以外のコマンドの評価関数を定義しようとした、最初の試みです。 The following declaration is needed to be able to use the notations in match patterns.

In a traditional functional programming language like OCaml or Haskell we could add the WHILE case as follows: Fixpoint ceval_fun (st : state) (c : com) : state := match c with ... | WHILE b DO c END => if (beval st b) then ceval_fun st (c ;; WHILE b DO c END) else st end. Coq doesn't accept such a definition ("Error: Cannot guess decreasing argument of fix") because the function we want to define is not guaranteed to terminate. Indeed, it doesn't always terminate: for example, the full version of the ceval_fun function applied to the loop program above would never terminate. Since Coq is not just a functional programming language but also a consistent logic, any potentially non-terminating function needs to be rejected. Here is an (invalid!) program showing what would go wrong if Coq allowed non-terminating recursive functions: Fixpoint loop_false (n : nat) : False := loop_false n. That is, propositions like False would become provable (loop_false 0 would be a proof of False), which would be a disaster for Coq's logical consistency. Thus, because it doesn't terminate on all inputs, of ceval_fun cannot be written in Coq -- at least not without additional tricks and workarounds (see chapter ImpCEvalFun if you're curious about what those might be).

関係としての評価

改善策はこうです。 ceval を関数ではなく関係(relation) として定義します。 つまり、上の aevalR と bevalR と同様に Type ではなく Prop で定義するのです。

これは重要な変更です。 厄介な回避策から解放されるばかりでなく、定義での柔軟性も与えてくれます。 例えば、もし言語にanyのような並行性の要素を導入したら、評価の定義を非決定的に書きたくなるでしょう。 つまり、それは全域でないだけでなく、そもそも関数ですらないかも知れないのです！

ceavl 関係に対する表記として st =[ c ]=> st' を使います。 st =[ c ]=> st' と書いたら、プログラム c を初期状態 st で評価すると、その結果は最終状態 st' になる、ということを意味します。 これは「c は状態 st を st' にする」と読みます。

操作的意味論

評価の推論規則を読みやすく非形式的に書くと、以下のようになります。

                           -----------------                            (E_Skip) 
                           st =[ SKIP ]=> st 
 
                           aeval st a1 = n 
                   --------------------------------                     (E_Ass) 
                   st =[ x := a1 ]=> (x !-> n ; st) 
 
                           st  =[ c1 ]=> st' 
                           st' =[ c2 ]=> st'' 
                         ---------------------                            (E_Seq) 
                         st =[ c1;;c2 ]=> st'' 
 
                          beval st b1 = true 
                           st =[ c1 ]=> st' 
                ---------------------------------------                (E_IfTrue) 
                st =[ TEST b1 THEN c1 ELSE c2 FI ]=> st' 
 
                         beval st b1 = false 
                           st =[ c2 ]=> st' 
                ---------------------------------------               (E_IfFalse) 
                st =[ TEST b1 THEN c1 ELSE c2 FI ]=> st' 
 
                         beval st b = false 
                    -----------------------------                  (E_WhileFalse) 
                    st =[ WHILE b DO c END ]=> st 
 
                          beval st b = true 
                           st =[ c ]=> st' 
                  st' =[ WHILE b DO c END ]=> st'' 
                  --------------------------------                  (E_WhileTrue) 
                  st  =[ WHILE b DO c END ]=> st'' 

以下に形式的な定義を挙げます。 上の推論規則とどのように対応するか、確認しておきましょう。

評価を関数ではなく関係として定義することのコストは、あるプログラムを実行した結果がとある状態になる、というのを Coq の計算機構にやってもらう代わりに、その「証明」を構築する必要がある、ということです。

練習問題: ★★, standard (ceval_example2)

☐

Exercise: 3 stars, standard, optional (pup_to_n)

Write an Imp program that sums the numbers from 1 to X (inclusive: 1 + 2 + ... + X) in the variable Y. Prove that this program executes as intended for X = 2 (this is trickier than you might expect).

☐

評価の決定性

評価の定義を計算的なものから関係的なものに変更するのはとても良いことです。 というのも、評価が全関数でなければならないという不自然な要求から解放されるからです。 しかしこの変更は新たな疑問を生みます。 2つ目の評価の定義は本当に部分関数なのか？ それとも、同じ状態 st から始めて、あるコマンド c を違った方法で評価し、2つの異なる出力状態 st' と st'' に至るのが可能なのか？ というものです。 実際には、こうなることはありません。 評価関係 ceval は確かに部分関数です。

Imp プログラムに関する推論

「プログラミング言語の基礎」では、Imp におけるプログラムの推論手法としてより強力で系統だったテクニックに触れていきます。 しかし、そのままの定義を用いてもある程度は推論できます。 いくつかの例を見ていきましょう。

Inverting Heval essentially forces Coq to expand one step of the ceval computation -- in this case revealing that st' must be st extended with the new value of X, since plus2 is an assignment.

練習問題: ★★★, standard, recommended (XtimesYinZ_spec)

XtimesYinZ の仕様を書いて証明しなさい。

☐

練習問題: ★★★, standard, recommended (loop_never_stops)

Proceed by induction on the assumed derivation showing that loopdef terminates. Most of the cases are immediately contradictory (and so can be solved in one step with discriminate).

☐

練習問題: ★★★, standard (no_whiles_eqv)

以下の関数を考える。

この性質はプログラムが while ループを含まない場合 true を返します。 Inductive を使って c が while ループのないプログラムのとき、かつそのときに限り no_whilesR c が証明可能となる性質 no_whilesR を書きなさい。 さらに、それが no_whiles と等価であることを示しなさい。

☐

練習問題: ★★★★, standard (no_whiles_terminating)

while ループを含まない Imp プログラムは必ず停止します。 この性質を定理 no_whiles_terminating として記述し、証明しなさい。 no_whiles と no_whilesR のどちらでも好きなほうを使いなさい。

☐

追加の練習問題

練習問題: ★★★, standard (stack_compiler)

古い HP の電卓、Forth や Postscript などのプログラミング言語、および Java Virtual Machine などの抽象機械はすべて、「スタック(stack)」を使って算術式を評価します。 例えば、

      (2*3)+(3*(4-2)) 

という式は

      2 3 * 3 4 2 - * + 

と記述され、以下のように実行されるでしょう: （処理されるプログラムを右に、スタックの状態を左に書いています。）

      [ ]           |    2 3 * 3 4 2 - * + 
      [2]           |    3 * 3 4 2 - * + 
      [3, 2]        |    * 3 4 2 - * + 
      [6]           |    3 4 2 - * + 
      [3, 6]        |    4 2 - * + 
      [4, 3, 6]     |    2 - * + 
      [2, 4, 3, 6]  |    - * + 
      [2, 3, 6]     |    * + 
      [6, 6]        |    + 
      [12]          | 

この練習問題の目標は、aexp をスタック機械の命令列に変換する小さなコンパイラを書き、その正当性を証明することです。 スタック言語の命令セットは、以下の命令から構成されます:

• SPush n: 数 n をスタックにプッシュする。
• SLoad X: ストアから識別子 X に対応する値を読み込み、スタックにプッシュする。
• SPlus: スタックの先頭の 2 つの数をポップし、それらを足して、 結果をスタックにプッシュする。
• SMinus: 上と同様。ただし引く。
• SMult: 上と同様。ただし掛ける。

スタック言語のプログラムを評価するための関数を書きなさい。 関数は入力として、状態、数のリストで表現されたスタック（スタックの先頭要素はリストの先頭）、および命令のリストで表現されたプログラムを受け取り、受け取ったプログラムの実行後のスタックを返す。 下にある例で、その関数のテストをしなさい。 上の仕様では、スタックが 2 つ未満の要素しか含まずに SPlus や SMinus、SMult 命令に至った場合を明示していないままなことに注意しましょう。 我々のコンパイラはそのような不正な形式のプログラムは生成しないので、ある意味でこれは私たちがすることと無関係です。

次に、aexp をスタック機械のプログラムにコンパイルする関数を書きなさい。 このプログラムを実行した後の状態は、単に式の評価結果をスタックに積んだのと同じでなければなりません。

After you've defined s_compile, prove the following to test that it works.

☐

練習問題: ★★★★, advanced (stack_compiler_correct)

一つ前の練習問題で実装したコンパイラの正当性を証明します。 スタックに二つ未満しか要素がない状態で SPlus や SMinus 、 SMult 命令が来たときの仕様が規定されていないことを思い出してください。 （正当性を簡単に示すために、戻って定義を書き換えた方が良いと気づくこともあるでしょう！） 以下の定理を証明しなさい。 まずは使える帰納法の仮定を得るため、より一般的な補題を述べる必要があるでしょう。 主定理は補題の系として得られます。

☐

Exercise: 3 stars, standard, optional (short_circuit)

Most modern programming languages use a "short-circuit" evaluation rule for boolean and: to evaluate BAnd b1 b2, first evaluate b1. If it evaluates to false, then the entire BAnd expression evaluates to false immediately, without evaluating b2. Otherwise, b2 is evaluated to determine the result of the BAnd expression. Write an alternate version of beval that performs short-circuit evaluation of BAnd in this manner, and prove that it is equivalent to beval. (N.b. This is only true because expression evaluation in Imp is rather simple. In a bigger language where evaluating an expression might diverge, the short-circuiting BAnd would not be equivalent to the original, since it would make more programs terminate.)

Exercise: 4 stars, advanced (break_imp)

Imperative languages like C and Java often include a break or similar statement for interrupting the execution of loops. In this exercise we consider how to add break to Imp. First, we need to enrich the language of commands with an additional case.

Next, we need to define the behavior of BREAK. Informally, whenever BREAK is executed in a sequence of commands, it stops the execution of that sequence and signals that the innermost enclosing loop should terminate. (If there aren't any enclosing loops, then the whole program simply terminates.) The final state should be the same as the one in which the BREAK statement was executed. One important point is what to do when there are multiple loops enclosing a given BREAK. In those cases, BREAK should only terminate the innermost loop. Thus, after executing the following... X ::= 0;; Y ::= 1;; WHILE ~(0 = Y) DO WHILE true DO BREAK END;; X ::= 1;; Y ::= Y - 1 END ... the value of X should be 1, and not 0. One way of expressing this behavior is to add another parameter to the evaluation relation that specifies whether evaluation of a command executes a BREAK statement:

Intuitively, st =[ c ]=> st' / s means that, if c is started in state st, then it terminates in state st' and either signals that the innermost surrounding loop (or the whole program) should exit immediately (s = SBreak) or that execution should continue normally (s = SContinue). The definition of the "st =[ c ]=> st' / s" relation is very similar to the one we gave above for the regular evaluation relation (st =[ c ]=> st') -- we just need to handle the termination signals appropriately:

• If the command is SKIP, then the state doesn't change and execution of any enclosing loop can continue normally.
• If the command is BREAK, the state stays unchanged but we signal a SBreak.
• If the command is an assignment, then we update the binding for that variable in the state accordingly and signal that execution can continue normally.
• If the command is of the form TEST b THEN c1 ELSE c2 FI, then the state is updated as in the original semantics of Imp, except that we also propagate the signal from the execution of whichever branch was taken.
• If the command is a sequence c1 ;; c2, we first execute c1. If this yields a SBreak, we skip the execution of c2 and propagate the SBreak signal to the surrounding context; the resulting state is the same as the one obtained by executing c1 alone. Otherwise, we execute c2 on the state obtained after executing c1, and propagate the signal generated there.
• Finally, for a loop of the form WHILE b DO c END, the semantics is almost the same as before. The only difference is that, when b evaluates to true, we execute c and check the signal that it raises. If that signal is SContinue, then the execution proceeds as in the original semantics. Otherwise, we stop the execution of the loop, and the resulting state is the same as the one resulting from the execution of the current iteration. In either case, since BREAK only terminates the innermost loop, WHILE signals SContinue.

Based on the above description, complete the definition of the ceval relation.

Now prove the following properties of your definition of ceval:

☐

Exercise: 3 stars, advanced, optional (while_break_true)

☐

Exercise: 4 stars, advanced, optional (ceval_deterministic)

☐

Exercise: 4 stars, standard, optional (add_for_loop)

Add C-style for loops to the language of commands, update the ceval definition to define the semantics of for loops, and add cases for for loops as needed so that all the proofs in this file are accepted by Coq. A for loop should be parameterized by (a) a statement executed initially, (b) a test that is run on each iteration of the loop to determine whether the loop should continue, (c) a statement executed at the end of each loop iteration, and (d) a statement that makes up the body of the loop. (You don't need to worry about making up a concrete Notation for for loops, but feel free to play with this too if you like.)