在本章中，我们将更认真地研究如何使用Coq来研究其他东西。我们的案例研究是一种简单的命令式编程语言Imp，它体现了传统主流语言（如C和Java）的一个微小核心片段。这是一个用Imp编写的熟悉的数学函数。

Z := X;
       Y := 1;
       while ~(Z = 0) do
         Y := Y * Z;
         Z := Z - 1
       end

我们在这里集中定义Imp的语法和语义；《编程语言基础》（软件基础，第2卷）的后面几章发展了程序等价理论，并介绍了霍尔逻辑，这是一种广泛用于推理命令式程序的逻辑。

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From Coq Require Import Bool.Bool.
From Coq Require Import Init.Nat.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat. Import Nat.
From Coq Require Import Lia.
From Coq Require Import Lists.List. Import ListNotations.
From Coq Require Import Strings.String.
From LF Require Import Maps.

Arithmetic and Boolean Expressions

我们将分三部分介绍Imp：首先是算术和布尔表达式的核心语言，然后是这些表达式的变量扩展，最后是命令语言，包括赋值、条件、排序和循环。

Syntax 语法

Module AExp.

这两个定义指定算术和布尔表达式的抽象语法。

Inductive aexp : Type

Inductive aexp : Type :=
  | ANum (n : nat)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Inductive bexp : Type

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

在本章中，我们将主要从程序员实际编写到这些抽象语法树的具体语法中省略翻译——例如，将字符串“1+2×3”转换为AST的过程

APlus (ANum 1) (AMult (ANum 2) (ANum 3)).

可选章节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更为非正式——例如，它给出了一些关于表达式表面语法的建议（比如加法操作是用中缀编写的），而未指定词法分析和解析的其他方面（比如+、-、和×、使用paren对子表达式进行分组等）。需要一些额外的信息——以及人类的智慧——才能将这个描述转化为一个正式的定义，例如，用于实现一个编译器。

Coq版本始终忽略所有这些信息，只关注抽象语法。

• 相反，BNF版本更轻，更容易阅读。它的非正式性使它变得灵活，这在黑板上讨论这样的情况下是一个很大的优势，在这种情况下，传达总体想法比精确地确定每个细节更重要。

事实上，有几十种类似BNF的符号，人们可以在它们之间自由切换，通常不用费心说他们使用的是哪种BNF，因为没有必要这样做：一个粗略的非正式理解才是最重要的。

对这两种符号都很熟悉是件好事：用于人与人之间交流的非正式符号和用于执行实现和证明的正式符号。

Evaluation

对算术表达式求值产生一个数字。

Fixpoint aeval (a : aexp) : nat

Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n => n
  | APlus  a1 a2 => (aeval a1) + (aeval a2)
  | AMinus a1 a2 => (aeval a1) - (aeval a2)
  | AMult  a1 a2 => (aeval a1) * (aeval a2)
  end.

Example test_aeval1

Example test_aeval1:
  aeval (APlus (ANum 2) (ANum 2)) = 4.
Proof. reflexivity. Qed.

类似地，对布尔表达式求值会生成布尔表达式。

Fixpoint beval (b : bexp) : bool

Fixpoint beval (b : bexp) : bool :=
  match b 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.

Optimization

我们还没有定义太多，但我们已经可以从定义中获得一些里程。假设我们定义了一个函数，它接受一个算术表达式并稍微简化它，将每次出现的0+e（即（APlus（ANum 0）e）都更改为e。

Fixpoint optimize_0plus (a:aexp) : aexp

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.

为了确保我们的优化做了正确的事情，我们可以在一些示例上测试它，看看输出是否正常。

Example test_optimize_0plus

Example test_optimize_0plus:
  optimize_0plus (APlus (ANum 2)
                        (APlus (ANum 0)
                               (APlus (ANum 0) (ANum 1))))
  = APlus (ANum 2) (ANum 1).
Proof. reflexivity. Qed.

但是如果我们想确保优化是正确的——也就是说，对优化表达式求值会得到与原始表达式相同的结果——我们应该证明它。

Theorem optimize_0plus_sound

Theorem optimize_0plus_sound: forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros a. induction a.
  - (* ANum *) reflexivity.
  - (* APlus *) destruct a1 eqn:Ea1.
    + (* a1 = ANum n *) destruct n eqn:En.
      * (* n = 0 *)  simpl. apply IHa2.
      * (* n <> 0 *) simpl. rewrite IHa2. reflexivity.
    + (* a1 = APlus a1_1 a1_2 *)
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.
    + (* a1 = AMinus a1_1 a1_2 *)
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.
    + (* a1 = AMult a1_1 a1_2 *)
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.
  - (* AMinus *)
    simpl. rewrite IHa1. rewrite IHa2. reflexivity.
  - (* AMult *)
    simpl. rewrite IHa1. rewrite IHa2. reflexivity.  Qed.