Software Foundations: Rocq, Hoare Logic and IMP

Basic: Functional Programming in Rocq#

简单介绍了一下 Rocq 是什么（之前是 Coq，然后好像什么名字不太优雅就改了）。

枚举类型：

Inductive day : Type :=
| monday
| ...
| sunday.

这里的每一个东西被称为一个构造子（constructor）。

然后定义对应函数：

Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| ...
| sunday => monday
end.

Rocq 的函数调用基于空格，这和 haskell 一样。

优先级：空格优先级高，即 f a+b 表示的是 (f a) + b。

声明定理：Theorem，Lemma，Example 等。然后使用 tactic 证明，最简单的是 simpl 化简，reflexivity 在等式两边相等时结束证明（其实他也会先做一下 simpl）。

定义函数时可以使用 if then else，例如：

Definition andb' (b1:bool) (b2:bool) : bool :=
if b1 then b2
else false.

Check 可以用于检查类型，例如：

Check true : bool.

定义函数时 match 可以用于模式匹配，例如：

Definition monochrome (c : color) : bool :=
match c with
| black => true
| white => true
| primary p => false
end.

定义自然数：使用 Piano Axioms：

Inductive nat : Type :=
| O
| S (n : nat).

定义递归函数需要使用 Fixpoint 而非 Definition。

然后还讲了三个证明 tatic：rewrite，intros 和 destruct。

rewrite 用于把一个等式左边的东西全部换成右边（或反之）。

intros 将全称量词引入假设区。

destruct 将一个变量按照归纳定义进行分解，然后分别证明。具体写法是（比如对一个 nat 分解）：

destruct n as [| n'] eqn:E

括号内传分解后的变量名，E 表示分解得到的等式。

Induction: Proof by Induction#

结构归纳法：对于任意递归定义的类型，证明 P 对该类型的每一个构造子都成立（如果构造子接受该类型的参数，则假设 P 对参数成立）。

数学归纳法即位结构归纳法在 nat 上的特例。

在 rocq 中的 tactic 为 induction，写法例如：

induction n as [| n' IHn'].

归纳假设成立的命题就是上面的 IHn'。

然后是一个 tactic：replace 用于引入等价子定理，可以把证明中的一个部分 replace 了，然后分别证明 replace 的正确性和 replace 后的命题。

Lists: Working with Structured Data#

先定义了 pair 非常平凡，随之定义了 fst 和 snd 两个函数。

然后定义 list（其实是 natlist，这里还没讲到多态）：

Inductive natlist : Type :=
| nil
| cons (n : nat) (l : natlist).

和一些对应的基础函数 repeat，length，app（拼接），hd， tl（这里的 tail 指的是去掉开头一个之后剩下的序列），rev。以及一些对应的平凡的定理，基本直接 induction 就能证。

然后还定义了一种类型 option，类似于 haskell 中的 Maybe：

Inductive natoption : Type :=
| Some (n : nat)
| None. 

Poly: Polymorphism and Higher-Order Functions#

这节讲的是 Parametric Polymorphism，就是让一个类型 / 函数对多种类型适用，即面向对象的泛型。

然后把上一节的 natlist 拿过来重新定义成 list：

Inductive list (X:Type) : Type :=
| nil
| cons (x : X) (l : list X).

同理也可以定义多态函数，就是多传一个 Type 进去。

然后还讲了隐式参数，换成 {X:Type} 大括号即可，感觉这一块应该不重要。

同理可以把之前定义的 pair 和 option 也拿过来重新定义成多态的。

高阶函数：函数也可以作为参数传递。这在 Haskell 里面已经讲了很多了，Rocq 中写法也是类似的。特别的是匿名函数的写法 (fun n => n * n)。

用高阶函数可以定义 map，fold 等，这和 haskell 中都是一致的。

还有一部分是 lambda 演算（后面还会讲），三条语法和两条语义：

t ::=
      x        variable
      \x. t   abstraction
      t t      application

Alpha-Renaming：绑定的变量可以随意改名，(\x. x) (\x. x) = (\y. y) (\z. z)。

Beta-Reduction：函数调用，(\x. t12) t2 = [x |-> t2] t12。

lambda 演算实现递归可以使用 Y Combinator：

Y = \f. (\x. f (x x)) (\x. f (x x))

展开后发现 Y f = f (Y f)，然后就可以递归了。例如写阶乘：

g = \f. \n. if eq n c0
            then c1
            else times n (f (pred n))
fac = Y g

Tactics: More Tactics#

讲了一堆证明的 tactic。

apply：直接应用假设完成推导，或者应用形如 P -> Q 的假设把结论从 Q 变成 P。

注意 apply 会自动替换假设里面的全称量词，无法匹配的可以用 apply ... with ... 来指定。

同时 apply 也可以作用到假设上，写法为 apply ... in ...：

(** H : P -> Q
    H1 : P **)
apply H in H1.
(** H : P -> Q
    H1 : Q **)

symmetry：交换目标等式的左右两边。

transitivity：传递性，transitivity o 可以把目标的 a = b 拆成 a = o 和 o = b 分别证明。

injection：利用归纳定义类型的 injection（同一个构造子传入不同参数时构造的值不同）和 disjointness（不同构造子构造的值不同）的特点，来推导参数等价性。例如：

(** H : S n = S m **)
injection H as Hnm.
(** Hnm : n = m **)

同样也可以推导出多个等价性：

(** H : [n, m] = [o, o] **)
injection H as H1 H2.
(** H1 : n = o
    H2 : m = o **)

关于如何证明 injection：定义一个函数返回对应构造子即可。

discriminate：如果一个等式两边由不同构造子生成，则任意结论成立（爆炸原理）。

f_equal：可以在一个假设的两边同时作用一个函数，x = y -> f x = f y。

specialize：将假设中的全称量词替换为具体值。

generalize dependent：将假设区中的一个变量变成全称量词，重新放回结论中。在一些归纳的时候很有用。

unfold：simpl 并不会展开所有东西，此时可以用 unfold 手动展开。

具体来说，simpl 只会在能展开 match 或 fixpoint 的时候进约简，例如：

Definition foo (x: nat) := 5.
Fact silly_fact_1 : forall m, foo m + 1 = foo (m + 1) + 1.
Fact silly_fact_1' : forall m, foo m = foo (m + 1).

由于 + 是 fixpoint 定义的，因此 silly_fact_1 会被 simpl 展开为 6 = 6，而 silly_fact_1' 则不会被展开。

Logic: Logic in Rocq#

形式系统包含四个部分：

• 字母表 Alphabet：一个符号的集合 $\Sigma$。
• 文法 Grammar：一组文法规则，定义 $\Sigma^*$ 的一个子集，为该形式系统中可以写的命题集合。
• 公理模式 Axiom Schemata：一组公理模板，定义命题集合的一个子集，代表为真的命题。
• 推导规则 Inference Rules：一组推导规则，用于推导出公理以外为真的命题。

文法包括：

• 一组非终结符，用大写字母表示，如 S, A, B。
• 一组终结符，用小写字母表示，如 a, b。
• 一个非终结符作为开始符号，用字母 S 表示。
• 一组产生式，表示把一个字符串中的左边部分替换成右边部分。

推导式写作：

P1, ..., Pn => P

或

P1 ... Pn
---------
    P

证明序列：给定一个前提集合和一组推导式集合 $I$。对于证明序列 P1, ..., Pn，需满足对于任意 $i$，Pi 是前提 或 存在推导式 Pi1, ..., Pik => Pi 其中 $i_1,\cdots,i_k < i$。

然后还有一些离散内容，但是感觉不是考试重点。

Rocq 中的命题：类型为 Prop，无论是否成立。

Rocq 中的谓词可以被视作返回 Prop 的函数。例如：

Check @eq : forall A : Type, A -> A -> Prop.

逻辑与：写作 /\，类型为：

Check and : Prop -> Prop -> Prop.

证明逻辑与：使用 conj 定理，或直接用 tactic split。

Lemma conj : forall A B : Prop, A -> B -> A /\ B.

假设中的逻辑与：使用 destruct 可以将其拆开。

逻辑或：写作 \/，类型为：

Check or : Prop -> Prop -> Prop.

证明逻辑或：使用 tactic left 或 right（Rocq 使用直觉主义逻辑，没有排中律）。

假设中的逻辑或：依旧使用 destruct 展开成两种情况分别证明。

逻辑非：写作 ~，类型为：

Check not : Prop -> Prop.
Definition not (P:Prop) := P -> False.

爆炸原理：tactic exfalso 可以直接将证明目标换成 False，原理是：

Theorem ex_falso_quodlibet : forall (P:Prop), False -> P.
Proof.
  intros P contra.
  destruct contra.
Qed.

可以直接 destruct 是因为 False 没有任何构造子。

与之相对的是 tactic I，可以直接证明 True：

Lemma True_is_true : True.
Proof. apply I. Qed.

蕴含关系 ->：

• 蕴含关系在目标中：Γ, P => Q，则 Γ => P -> Q，对应 intro。
• 蕴含关系在假设中：P, P -> Q => Q，对应 apply。

逻辑等价性 <->：其实就是用 and 定义的：

Definition iff (P Q : Prop) := (P -> Q) /\ (Q -> P).

全称量词 forall：

• 全称量词在目标中：P => forall x, P，对应 intro。
• 全称量词在假设中：forall x, P => P [x \ t]，对应 apply。

存在量词 exists：

• 存在量词在目标中：P [x \ t] => exists x, P，对应 exists。
• 存在量词在假设中：P -> Q => (exists x, P) -> Q，x 不是 Q 中的自由变量。在 tactic 中直接 destruct 就行。

然后是递归定义的命题和给定理传参数，这些是平凡的。

Rocq 中一个值只能属于一个类型，可以通过谓词来定义类型的子集，如偶数。

函数等价性：函数相等当且仅当所有输入输出对相等（外延性），即 functional extensionality：

Axiom functional_extensionality : forall {X Y: Type} {f g : X -> Y},
(forall (x:X), f x = g x) -> f = g.

逻辑式可以写作命题也可以写作布尔表达式。可以通过证明布尔表达式来帮助证明，称为 Proof by reflection。

排中律：P /\ ~P。直觉主义逻辑相比经典逻辑缺少排中律和一些其他的等价公理。

ProofObjects: The Curry-Howard Correspondence#

Curry-Howard Correspondence：将命题视为类型，证明视为值。

带参数的归纳类型定义：

Inductive nnlist : bool -> Type :=
| nnnil : nnlist false
| nncons {b:bool} (x : nat) (l : nnlist b) : nnlist true.

带参数的归纳命题定义：

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS (n : nat) (H : ev n) : ev (S (S n)).

例如此时需要证明 ev 4，用 tactic 写是：

Theorem ev_4 : ev 4.
Proof.
  apply ev_SS. Show Proof.
  (* (ev_SS 2 ?Goal) *)
  apply ev_SS. Show Proof.
  (* (ev_SS 2 (ev_SS 0 ?Goal)) *)
  apply ev_0. Show Proof.
  (* (ev_SS 2 (ev_SS 0 ev_0)) *)
Qed.

也可以直接写成定义：

Definition ev_4 := ev_SS 2 (ev_SS 0 ev_0).

后者即为 Proof Object。

再看 intros 实际做了什么：

Theorem ev_plus4 : forall n, ev n -> ev (4 + n).
Proof.
  intros n H.
  (* (fun (n : nat) (H : ev n) => ?Goal) *)
  apply ev_SS.
  apply ev_SS.
  apply H.
Qed.

中间 ?Goal 能访问到的参数即为所有可用的假设。上面这一段证明写成 Proof Object 为：

Definition ev_plus4' : forall n, ev n -> ev (4 + n) :=
fun (n : nat) => fun (H : ev n) => ev_SS (S (S n)) (ev_SS n H).

generalize dependent 对 proof object 的作用：

(* (fun n m : nat => ?Goal) *)
generalize dependent n.
(* (fun n m : nat => ?Goal n) *)

逻辑与的定义：

Inductive and (P Q : Prop) : Prop :=
| conj : P -> Q -> and P Q.

split 是指如果目标只有一个 constructor，则在 proof object 中生成该 constructor。其实等价于 apply constructor，因此可以写出下面的操作：

Lemma truth : True.
Proof. split. Qed.

这是因为 True 只有一个 constructor I。

split 最常见的是作用到逻辑与上：

(* (fun (A B : Porp) (HA : A) (HB : B) => ?Goal ) *)
split. Show Proof.
(* (fun (A B : Prop) (HA : A) (HB : B) => conj ?Goal ?Goal0) *)

destruct 的作用是根据参数的归纳定义生成 match，例如：

(* (fun (P Q : Prop) (HPQ : P /\ Q) => ?Goal) *)
destruct HPQ as [HP HQ]. Show Proof.
(* (fun (P Q : Prop) (HPQ : P /\ Q) => match HPQ with
| conj HP HQ => ?Goal
end) *)

reflexivity 等价于 apply eq_refl。对应的 proof object：

Definition four' : 2 + 2 = 1 + 3 :=
  eq_refl 4.

然后 eq 的构造子只有一个：

Inductive eq {X:Type} (x:X) : X -> Prop :=
| eq_refl : eq x x.

这也意味着我们可以用 destruct 来代替 rewrite。

False 的定义没有 constructor，这也意味着不可能构造出 False：

Inductive False : Prop := .

因此条件中如果包含 False 那么可以直接写如下的 proof object：

Definition false_implies_zero_eq_one : False -> 0 = 1 :=
  fun contra => match contra with end.

逻辑或的定义：

Inductive or (P Q : Prop) : Prop :=
| or_introl : P -> or P Q
| or_intror : Q -> or P Q.

left 和 right 分别表示使用两个 constructor。

存在量词的定义：

Inductive ex {A : Type} (P : A -> Prop) : Prop :=
| ex_intro : forall x : A, P x -> ex P.

写一个 proof object 就类似这样：

Definition some_nat_is_even' : exists n, ev n :=
  ex_intro ev 0 ev_0.

逻辑非的定义：

Definition not (P:Prop) := P -> False.

总结一下，除了 forall 和 ->，其他的逻辑运算符都适用 inductive 或普通 definition。

• 当 inductive definition 出现在前提中，用 destruct 分解；
• 当 inductive definition 出现在目标中，apply constructor。

直接用 constructor i 这个 tactic 可以直接调用第 $i$ 个构造子。

injection 的作用时生成从复杂结构到简单结构的函数，并调用 f_equal。例如：

Definition S_injective'' : forall (n m : nat),
  S n = S m -> n = m :=
  fun (n m : nat) (H : S n = S m) =>
    f_equal (fun e : nat => match e with
      | 0 => n
      | S n0 => n0
    end) H.

IndPorp: Inductively Defined Propositions#

remember 在 proof object 上的做法是添加一个 let ... in。

inversion 策略：针对递归定义的命题，将每个 constructor 分别生成一个 goal，然后对比 constructor 产生的 index 和被分解的假设，如果矛盾则自动删除。所以 inversion 可以代替 discriminate，因为分解出 eq_refl 发现两边不相等直接删除。

IndPrinciples: Induction Principles#

结构归纳法定理：Rocq 会对每个递归定义的类型生成对应的结构归纳法定理。

例如对于 nat 类型：

Inductive nat : Type :=
| O
| S (n : nat).

其对应的结构归纳法定理即为：

Check nat_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> P (S n)) ->
    forall n : nat, P n.

结构归纳法定理的证明是简单的：

Print nat_ind.
(*
 * nat_ind =
 * fun (P : nat -> Prop) (f : P 0)
 *   (f0 : forall n : nat, P n -> P (S n)) =>
 * fix F (n : nat) : P n :=
 *   match n with
 *   | 0 => f
 *   | S n0 => f0 n0 (F n0)
 *   end
 *)

更复杂一些的类型也都有对应的结构归纳法定理，例如对于二叉树：

Inductive tree (X:Type) : Type :=
| leaf (x : X)
| node (t1 t2 : tree X).

Check tree_ind :
  forall (X : Type) (P : tree X -> Prop),
  (forall x : X, P (leaf X x)) ->
  (forall t1 : tree X,
    P t1 -> forall t2 : tree X, P t2 -> P (node X t1 t2)) -> forall t : tree X, P t.

tactic 中的 induction 实际就是应用了结构归纳法定理，例如：

Theorem plus_n_O : forall n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn']. Show Proof.
  (* (fun n : nat =>
  nat_ind (fun n0 : nat => n0 = n0 + 0) ?Goal
    (fun (n' : nat) (IHn' : n' = n' + 0) => ?Goal0) n) *)

命题对应的结构归纳法定理：

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS (n : nat) (H : ev n) : ev (S (S n)).

Check ev_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, ev n -> P n -> P (S (S n))) ->
    forall n : nat, ev n -> P n.

关系对应的结构归纳法定理：

Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat)                : le n n
  | le_S (n m : nat) (H : le n m) : le n (S m).

Check le_ind : forall P : nat -> nat -> Prop,
  (forall n : nat, P n n) ->
  (forall n m : nat, le n m -> P n m -> P n (S m)) ->
    forall n n0 : nat, le n n0 -> P n n0.

如果把 le 的定义改一下，n 一开始就传进去，那么会变成：

Inductive le (n : nat) : nat -> Prop :=
  | le_n : n <= n
  | le_S : forall m : nat, n <= m -> n <= S m 

Check le_ind:
  forall (n : nat) (P : nat -> Prop),
    P n ->
    (forall m : nat, n <= m -> P m -> P (S m)) ->
    forall n0 : nat, n <= n0 -> P n0.

对于 eq，他对应的结构归纳法定理是：

Check eq_ind :
  forall (A: Type) (x:A) (P : A -> Prop),
    P x -> forall y : A, x=y -> P y.

因此可以用这种方法来实现 discriminate，形如：

Definition zero_not_one' : 0 <> 1 :=
  fun contra : 0 = 1 => eq_ind 0
    (fun e:nat => match e with
                  | 0 => True
                  | S _ => False
                  end) I 1 contra.

同样也可以用 eq_ind 来实现 rewrite：

Definition plus_id_example' : forall n m:nat,
  n=m -> n+n=m+m :=
    fun (n m : nat) (H : n=m) =>
    eq_ind n (fun (m:nat) => n+n=m+m) eq_refl m H.

Maps: Total and Partial Maps#

重新定义了一下 map。还是用函数的形式定义 string -> A。

total_map：需要指定初始值（所有 undefined 的元全部定义为这个值）。

partial_map：加上了 Option，没有的返回 None。

Imp: Simple Imperative Programs#

本节开始将定义一个命令式程序设计语言 IMP。

先定义两种类型 aexp 和 bexp 的表达式：

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

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

然后容易按照规则把语义建模成函数 aeval 和 beval：

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

Fixpoint beval (st : state) (b : bexp) : bool :=
  match b with
  | BTrue => true
  | BFalse => false
  | BEq a1 a2 => (aeval st a1) =? (aeval st a2)
  | BNeq a1 a2 => negb ((aeval st a1) =? (aeval st a2))
  | BLe a1 a2 => (aeval st a1) <=? (aeval st a2)
  | BGt a1 a2 => negb ((aeval st a1) <=? (aeval st a2))
  | BNot b1 => negb (beval st b1)
  | BAnd b1 b2 => andb (beval st b1) (beval st b2)
  end.

语义也可以被建模成关系 aexp -> nat -> Prop（为了写得简单一些，把 AId 给暂时略去了）：

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum (n : nat) :
    aevalR (ANum n) n
  | E_APlus (e1 e2 : aexp) (n1 n2 : nat) :
    aevalR e1 n1 ->
    aevalR e2 n2 ->
    aevalR (APlus e1 e2) (n1 + n2)
  | E_AMinus (e1 e2 : aexp) (n1 n2 : nat) :
    aevalR e1 n1 ->
    aevalR e2 n2 ->
    aevalR (AMinus e1 e2) (n1 - n2)
  | E_AMult (e1 e2 : aexp) (n1 n2 : nat) :
    aevalR e1 n1 ->
    aevalR e2 n2 ->
    aevalR (AMult e1 e2) (n1 * n2).

然后一直写 aevalR 太麻烦了，用 Notation 写成 ==> 的样子：

Inductive aevalR : aexp -> nat -> Prop :=
  | E_ANum (n : nat) :
    (ANum n) ==> n
  | E_APlus (e1 e2 : aexp) (n1 n2 : nat) :
    (e1 ==> n1) -> (e2 ==> n2) -> (APlus e1 e2) ==> (n1 + n2)
  | E_AMinus (e1 e2 : aexp) (n1 n2 : nat) :
    (e1 ==> n1) -> (e2 ==> n2) -> (AMinus e1 e2) ==> (n1 - n2)
  | E_AMult (e1 e2 : aexp) (n1 n2 : nat) :
    (e1 ==> n1) -> (e2 ==> n2) -> (AMult e1 e2) ==> (n1 * n2)
  | E_ADiv (a1 a2 : aexp) (n1 n2 n3 : nat) :
    (a1 ==> n1) -> (a2 ==> n2) -> (n2 > 0) ->
    (mult n2 n3 = n1) -> (ADiv a1 a2) ==> n3

函数和关系两种建模方式是等价的。

再定义 IMP 的顶层语法：

c := skip
  | x := a
  | c ; c
  | if b then c else c end
  | while b do c end

在 Rocq 里面定义为 com：

Inductive com : Type :=
  | CSkip
  | CAss (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com).

然后定义了 IMP 命令的七条语义规则：

------------------- (E_Skip)
 st =[ skip ]=> st

         aeval st a = n
-------------------------------- (E_Asgn)
 st =[ x := a ]=> (x !-> n; st)

    st =[ c1 ]=> st'
   st' =[ c2 ]=> st''
------------------------ (E_Seq)
 st =[ c1 ; c2 ]=> st''

         beval st b = true
         st =[ c1 ]=> st'
------------------------------------ (E_IfTrue)
 st =[ if b then c1 else c2 ]=> st'

         beval st b = false
          st =[ c2 ]=> st'
------------------------------------ (E_IfTrue)
 st =[ if b then c1 else c2 ]=> 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''

把这些规则建模成关系，很容易能写到 Rocq 中去。

Auto: More Automation#

显然就是一个自动化证明策略。auto 可以自动搜索一系列由 intro 和 apply 组成的证明。

然后有些 apply 的时候一个变量不能自动推导，可以用 eapply，对应到 auto 上可以用 eauto。

似乎没有别的知识点了。

Equiv: Program Equivalence#

可以按照如下规则定义行为等价性：

Definition aequiv (a1 a2 : aexp) : Prop :=
  forall (st : state),
    aeval st a1 = aeval st a2.

Definition bequiv (b1 b2 : bexp) : Prop :=
  forall (st : state),
    beval st b1 = beval st b2.

Definition cequiv (c1 c2 : com) : Prop :=
  forall (st st' : state),
    (st =[ c1 ]=> st') <-> (st =[ c2 ]=> st’).

Definition refines (c1 c2 : com) : Prop :=
  forall (st st' : state),
    (st =[ c1 ]=> st') -> (st =[ c2 ]=> st').

容易证明行为等价是等价关系，也是一个同余关系（子部件等价，则两者等价）。这些证明是平凡的。

然后讲了常量传播以及证明其正确性。但是注意下面的命题并不一定成立：

Definition subst_equiv_property := forall x1 x2 a1 a2,
  cequiv <{ x1 := a1; x2 := a2 }>
    <{ x1 := a1; x2 := subst_aexp x1 a1 a2 }>.

反例：

X = X + 1; Y = X
X = X + 1; Y = X + 1

Hoare: Hoare Logic#

霍尔逻辑用霍尔三元组来描述程序的性质，以及给出一套推导霍尔三元组的规则。

霍尔三元组：形如 {前条件} 语句 {后条件}，表示满足前条件的状态经过中间的语句后，得到的状态一定满足后条件。

霍尔逻辑的六条规则：

------------------ (Skip)
 { P } skip { P }


---------------------------- (Assign)
 { P [a / x] } x := a { P }

    { P } c1 { R }
    { R } c2 { Q }
--------------------- (Seq)
 { P } c1 ; c2 { Q }

       { P /\ b } c1 { Q }
      { P /\ ~ b } c2 { Q }
---------------------------------- (If)
 { P } if b then c1 else c2 { Q }

   |= (P => P')
 { P' } c { Q' }
   |= (Q' => Q)
----------------- (Consequence)
  { P } c { Q }

         { P /\ b } c { P }
------------------------------------- (While)
 { P } while b do c end { P /\ ~ b }

霍尔逻辑具有正确性（按照霍尔逻辑推导出来的三元组在 IMP 语义下都是正确的）和完整性（所有在 IMP 语义下正确的 Hoare 三元组都可以按照上面规则推导出来）。

在 Rocq 中，将 state 定义为 total_map nat，将断言定义为关于状态的谓词 Assertion := state -> Prop。

将合法的 hoare 三元组按照如下规则定义：

Definition valid_hoare_triple
  (P : Assertion) (c : com) (Q : Assertion) : Prop :=
  forall st st',
    st =[ c ]=> st' ->
    P st ->
    Q st'.

然后可以用 Notation 写成 {{P}} c {{Q}} 的形式。容易把上面的所有推导规则写成 Rocq 中的定理并证明。

上面定义的 Hoare 逻辑其实是部分正确性的，即不保证程序是终止的，若程序不终止则允许有任何后条件。

扩展为完全正确性的方法：给 While 加一个势能。

装饰程序：直接把条件用 {{ ... }} 然后写进程序，比较容易看。

循环不变式：足够弱（能被前条件推出），足够强（能推出后条件），能保持（每一次循环过程都保持）。找循环不变式没有形式化方法，只能凭感觉。

最弱前条件：称 {P} 为 c {Q} 的最弱前条件，若：

• {P} c {Q}；
• forall P'. {P'} c {Q} => P' -> P。

最强后条件：称 {Q} 为 {P} c 的最强后条件，若：

• {P} c {Q}；
• forall Q'. {P} c {Q'} => Q -> Q'。

关于计算最弱前条件（wp）：

wp(skip, Q) = Q
wp(x := a, Q) = Q [a / x]
wp(c1; c2, Q) = wp(c1, wp(c2, Q))
wp(if b then c1 else c2, Q) = (b -> wp(c1, Q)) /\ (~b -> wp(c2, Q))

关于循环的最弱前条件，需要引入存在量词：

wp(while b do c, Q) = exists i \in Nat, L_i (Q)
  where
    L_0 (Q) = false
    L_(i+1) (Q) = (~b => Q) /\ (b => wp(c, L_i (Q)))

计算最强后条件也是类似的，有区别的在于 Assign：

sp(P, x := a) = exists n. x = [a / x] /\ P [n / x]

sp 比 wp 的约束条件更复杂，因此实际使用更少。

HoareAsLogic: Hoare Logic as a Logic#

可以吧 Hoare 逻辑建模成可推导三元组：

Inductive derivable : Assertion -> com -> Assertion -> Type

然后证明了 Hoare Logic 的正确性和完备性。

注意 Hoare Logic 是不可判定的，因为停机问题等价于判定 {True} c {False} 是否成立。

SmallStep: Small-Step Operational Semantics#

前面写的语义都是大步法，直接给出运算后的结果。如果需要定义程序单步执行的过程，则需要使用小步法语义。

先看一个小型语言：

Inductive tm : Type :=
  | C : nat -> tm       (* Constant *)
  | P : tm -> tm -> tm. (* Plus *)

可以定义正常结束状态，不能继续往下执行：

Inductive value : tm -> Prop :=
  | v_C : forall n, value (C n).

定义小步法语义为：

-------------------------------- (ST_PlusConstConst)
 P (C n1) (C n2) -> C (n1 + n2)

      t1 -> t1'
--------------------- (ST_Plus1)
 P t1 t2 -> P t1' t2

      value v1
      t2 -> t2'
--------------------- (ST_Plus2)
 P v1 t2 -> P v1 t2'

然后可以证明确定性，即一个状态进行一次小步计算得到的状态是确定的。

随后定义了多步约简关系：

Inductive multi {X : Type} (R : relation X) : relation X :=
  | multi_refl : forall (x : X), multi R x x
  | multi_step : forall (x y z : X),
                  R x y ->
                  multi R y z ->
                  multi R x z.

可以证明大步法和小步法是等价的，即：

Theorem eval__multistep : forall t n,
  t ==> n -> t -->* C n.

比较有意思的是如果再定义一个并行运算，这样就不能用大步法来定义了，只能使用小步法。但注意加上并行运算后不再具有确定性。

Types: Type Systems#

类型系统是一种用来自动和高效证明程序没有某类错误的语法手段。

定义值：

Inductive bvalue : tm -> Prop :=
  | bv_true : bvalue <{ true }>
  | bv_false : bvalue <{ false }>.

Inductive nvalue : tm -> Prop :=
  | nv_0 : nvalue <{ 0 }>
  | nv_succ : forall t, nvalue t -> nvalue <{ succ t }>.

Definition value (t : tm) := bvalue t \/ nvalue t.

定义小步法语义：

------------------------------- (ST_IfTrue)
 if true then t1 else t2 -> t1


-------------------------------- (ST_IfFalse)
 if false then t1 else t2 -> t2

                    t1 -> t1'
------------------------------------------------- (ST_If)
 if t1 then t2 else t3 -> if t1' then t2 else t3

      t1 -> t1'
--------------------- (ST_Succ)
 succ t1 -> succ t1'


------------ (ST_Pred0)
 pred 0 = 0


     nvalue v
------------------- (ST_PredSucc)
 pred (succ v) = v

      t1 -> t1'
--------------------- (ST_Pred)
 pred t1 -> pred t1'


------------------ (ST_IsZero0)
 iszero 0 -> true

         nvalue v
-------------------------- (ST_IsZeroSucc)
 iszero (succ v) -> false

        t1 -> t1'
------------------------- (ST_IsZero)
 iszero t1 -> iszero t1'

定义了上面这个语义之后有些项不一定能够被约简到值，比如 succ true。因此我们定义了类型系统：

Inductive ty : Type :=
  | Bool : ty
  | Nat : ty.

类型关系如下：

------------------ (T_True)
 |- true \in Bool


------------------- (T_False)
 |- false \in Bool


-------------- (T_0)
 |- 0 \in Nat

   |- t1 \in Nat
-------------------- (T_Pred)
 |- pred t1 \in Nat

   |- t1 \in Nat
-------------------- (T_Succ)
 |- succ t1 \in Nat

     |- t1 \in Nat
----------------------- (T_IsZero)
 |- iszero t1 \in Bool

 |- t1 \in Bool  |- t2 \in T  |- t3 \in T
------------------------------------------ (T_If)
      |- if t1 then t2 else t3 \in T

然后比较重要的内容是进展性和保持性：

• 进展性 Progress：类型正确的项如果不是值，那么一定能约简；
• 保持性 Preservation：项往下约简之后能保持相同类型。

Theorem progress : forall t T,
  <{ |-- t \in T }> ->
  value t \/ exists t', t --> t'.

Theorem preservation : forall t t' T,
  <{ |-- t \in T }> ->
  t --> t' ->
  <{ |-- t' \in T }>.

这两个属性保证了项不会卡住，一定能约简到一个值。

但是没有卡住的项不一定具有正确的类型，比如 if false then 0 else true。

STLC: The Simply Typed Lambda-Calculus#

考虑描述 lambda 演算。先来定义 lambda 演算的语法和类型：

t ::= x                     (variable)
    | \x:T,t                (abstraction)
    | t1 t2                 (application)
    | true                  (constant true)
    | false                 (constant false)
    | if t1 then t2 else t3 (conditional)

T ::= Bool
    | T -> T

在 STLC 中，将 true，false 和所有的 lambda 抽象定义为值：

Inductive value : tm -> Prop :=
  | v_abs : forall x T2 t1,
      value <{\x:T2, t1}>
  | v_true :
      value <{true}>
  | v_false :
      value <{false}>.

然后可以定义 STLC 的小步法操作语义：

            value v2
--------------------------------- (ST_AppAbs)
 (\x:T2, t1) v2 -> [x |-> v2] t1

    t1 -> t1'
----------------- (ST_App1)
 t1 t2 -> t1' t2

    value v1
    t2 -> t2'
----------------- (ST_App2)
 v1 t2 -> v1 t2'


------------------------------- (ST_IfTrue)
 if true then t1 else t2 -> t1


-------------------------------- (ST_IfFalse)
 if false then t1 else t2 -> t2

                    t1 -> t1'
------------------------------------------------- (ST_If)
 if t1 then t2 else t3 -> if t1' then t2 else t3

注意不能添加下面这个小步规则：

       t1 -> t1'
-----------------------
 \x:T, t1 -> \x:T, t1'

否则会出现下面这个约简：

   \y:Bool, ((\x:Bool, (\y:Bool x)) y)
-> \y:Bool, (\y:Bool y)

但正确的应该是约简为 \y:Bool, (\z:Bool y)。

然后尝试在 STLC 中引入类型系统。STLC 中包含变量，因此需要引入变量的类型，因此加入上下文 Gamma，表示从变量名到类型的映射。Gamma |-- t \in T 表示在上下文 Gamma 下，t 变量具有 T 类型。

从而可以定义类型的推导规则：

    Gamma x = T1
-------------------- (T_Var)
 Gamma |-- x \in T1

  x |-> T2; Gamma |-- t1 \in T1
---------------------------------- (T_Abs)
 Gamma |-- \x:T2, t1 \in T2 -> T1

 Gamma |-- t1 \in T2 -> T1
    Gamma |-- t2 \in T2
--------------------------- (T_App)
  Gamma |-- t1 t2 \in T1


------------------------- (T_True)
 Gamma |-- true \in Bool


-------------------------- (T_False)
 Gamma |-- false \in Bool

         Gamma |-- t1 \in Bool
 Gamma |-- t2 \in T  Gamma |-- t3 \in T
---------------------------------------- (T_If)
  Gamma |-- if t1 then t2 else t3 \in T

STLCProp: Properties of STLC#

证明了 STLC 上类型系统的 Progress 和 Preservation。

同时还证明了类型系统正确性：

Definition stuck (t:tm) : Prop :=
  (normal_form step) t /\ ~ value t.

Corollary soundness : forall t t' T,
  empty |-- t \in T ->
  t -->* t' ->
  ~(stuck t').

以及类型的唯一性：

Theorem unique_types : forall Gamma e T T',
  Gamma |-- e \in T ->
  Gamma |-- e \in T' ->
  T = T'.

MoreSTLC: More on the Simply Typed Lambda-Calculus#

尝试在 STLC 中加入更多的语言成分。

Nat：和 Type 一节的定义相同。

Let：在 terms 中加入 let x = t in t。

小步法约简规则：

               t1 -> t1'
--------------------------------------- (ST_Let1)
 let x = t1 in t2 -> let x = t1' in t2

            value v1
---------------------------------- (ST_LetValue)
 let x = v1 in t2 -> [x := v1] t2

类型规则：

        Gamma |-- t1 \in T1
   x |-> T1; Gamma |-- t2 \in T2
----------------------------------- (T_Let)
 Gamma |-- let x = t1 in t2 \in T2

Unit：直接写作 unit，是值，就是滚木，比如没有返回值的命令可以返回 unit。命令序列 t1; t2 等价于 (\x:Unit, t2) t1。

类型规则：

------------------------- (T_Unit)
 Gamme |-- unit \in Unit

Pair：term 包含 (t1, t2)，t0.fst 和 t0.snd。其中 (v1, v2) 是值。

小步法约简规则：

       t1 -> t1'
----------------------- (ST_Pair1)
 (t1, t2) -> (t1', t2)

       value v1
       t2 -> t2'
----------------------- (ST_Pair2)
 (v1, t2) -> (v1, t2')

    t0 -> t0'
------------------- (ST_Fst1)
 t0.fst -> t0'.fst


-------------------- (ST_FstPair)
 (v1, v2).fst -> v1

    t0 -> t0'
------------------- (ST_Snd1)
 t0.snd -> t0'.snd


-------------------- (ST_SndPair)
 (v1, v2).snd -> v2

类型规则：

      Gamma |-- t1 \in T1
      Gamma |-- t2 \in T2
-------------------------------- (T_Pair)
 Gamma |-- (t1, t2) \in T1 * T2

 Gamma |-- t0 \in T1 * T2
-------------------------- (T_Fst)
 Gamma |-- t0.fst \in T1

 Gamma |-- t0 \in T1 * T2
-------------------------- (T_Snd)
 Gamma |-- t0.snd \in T2

Records：term 包含 {i1 = t1, ..., in = tn} 和 t.i。其中 {i1 = v1, ..., in = vn} 是值。

小步法约简规则：

                  ti -> ti'
-------------------------------------------- (ST_Rcd)
   {i1 -> v1, ..., im = vm, tn = ti, ...}
 -> {i1 -> v1, ..., im = vm, tn = ti', ...}

   t0 -> t0'
--------------- (ST_Proj1)
 t0.i -> t0'.i


---------------------------- (ST_ProjRcd)
 {..., i = vi, ...}.i -> vi

类型规则：

       Gamma |-- t1 \in T1  ...  Gamma |-- tn \in Tn
----------------------------------------------------------- (T_Rcd)
 Gamma |-- {i1 = t1, ..., in = tn} \in {i1:T1, ..., In:Tn}

 Gamma |-- t0 \in {..., i:Ti, ...}
----------------------------------- (T_Proj)
       Gamma |-- t0.i \in Ti

Sum：term 包含 inl T2 t1，inr T1 t2 和 case t0 of inl x1 => t1 | inr x2 => t2。其中值有 inl T2 v1 和 inr T1 v2。这里需要传另一个的类型，是因为这样能直接推出 Sum 的类型。

小步法约简规则：

        t1 -> t1'
------------------------ (ST_Inl)
 inl T2 t1 -> inl T2 t1'

        t2 -> t2'
------------------------ (ST_Inr)
 inr T1 t2 -> inr T1 t2'

                  t0 -> t0'
-------------------------------------------- (ST_Case)
   case t0 of inl x1 => t1 | inr x2 => t2
 -> case t0' of inl x1 => t1 | inr x2 => t2


------------------------------------------------- (ST_CaseInl)
 case (inl T2 v1) of inl x1 => t1 | inr x2 => t2
             -> [x1 := v1] t1


------------------------------------------------- (ST_CaseInr)
 case (inr T1 v2) of inl x1 => t1 | inr x2 => t2
             -> [x2 := v2] t2

类型规则：

      Gamma |-- t1 \in T1
--------------------------------- (T_Inl)
 Gamma |-- inl T2 t1 \in T1 + T2

      Gamma |-- t2 \in T2
--------------------------------- (T_Inr)
 Gamma |-- inr T1 t2 \in T1 + T2

                Gamma |-- t0 \in T1 + T2
             x1 |-> T1; Gamma |-- t1 \in T3
             x2 |-> T2; Gamma |-- t2 \in T3
--------------------------------------------------------- (T_Case)
 Gamme |-- case t0 of inl x1 => t1 | inr x2 => t2 \in T3

List：term 包含 nil T，t1 :: t2 和 case t1 of nil => t2 | xh :: xt => t3。其中值包含 nil T 和 v1 :: v2。

小步法约简规则：

       t1 -> t1'
----------------------- (ST_Cons1)
 t1 :: t2 -> t1' :: t2

       t2 -> t2'
----------------------- (ST_Cons2)
 v1 :: t2 -> v1 :: t2'

                 t1 -> t1'
------------------------------------------- (ST_Lcase1)
   case t1 of nil => t2 | xh :: xt => t3
 -> case t1' of nil => t2 | xh :: xt => t3


------------------------------------------------- (ST_LcaseNil)
 case nil T1 of nil => t2 | xh :: xt => t3 -> t2


----------------------------------------------- (ST_LcaseCons)
 case (vh :: vt) of nil => t2 | xh :: xt => t3
          -> [xh := vh] [xt := vt] t3

类型规则：

------------------------------ (T_Nil)
 Gamma |-- nil T1 \in List T1

      Gamma |-- t1 \in T1
    Gamma |-- t2 \in List T1
-------------------------------- (T_Cons)
 Gamma |-- t1 :: t2 \in List T1

               Gamma |-- t1 \in List T1
                 Gamma |-- t2 \in T2
    (xh |-> t1; xt |-> List t1; Gamma) |-- t3 \in T2
-------------------------------------------------------- (T_Lcase)
 Gamma |-- case t1 of nil => t2 | xh :: xt => t3 \in T2

fix：用于递归。term 是 fix t1。

小步法约简规则：

     t1 -> t1'
------------------- (ST_Fix1)
 fix t1 -> fix t1'


------------------------------------------------- (ST_FixAbs)
 fix (\xf:T1. t1) -> [xf := fix (\xf:T1. t1)] t1

类型规则：

 Gamma |-- t1 \in T1 -> T1
--------------------------- (T_Fix)
  Gamma |-- fix t1 \in T1

然后可以证明 progress 和 preservation 在扩展后仍然成立。

TypeChecking: A Typechecker for STLC#

写了一个类型检查函数，并证明其正确性。

然后由于每次都要分 Some 和 None 讨论太麻烦了，就定义了一点好看的语法。没有实质内容。

References: Typing Mutable References#

给 STLC 添加了引用和赋值。

分配一块内存：

let a = ref 5 in

读取一块内存：

!a

改写一块内存：

a := 6

可以用引用来实现模拟封装：

let newcounter = \_:Unit.
  let c = ref 0 in
  let incc = \_:Unit, (c := succ (!c); !c) in
  let decc = \_:Unit, (c := pred (!c); !c) in
  {i=incc, d=decc} 

也可以用引用来保存函数，例如：

newarray = \_:Unit. ref (\n:Nat.0)
lookup = \a:NatArray, \n:Nat. (!a) n
update = \a:NatArray, \m:Nat, \v:Nat,
  let oldf = !a in
  a := (\n:Nat. if equal m n then v else oldf n);

定义类型和项：

T ::= Nat
    | Unit
    | T -> T
    | Ref T

t ::= ...
    | ref t   (allocation)
    | !t      (dereference)
    | t := t  (assignment)
    | l       (location)

现在值的定义是：

Inductive value : tm -> Prop :=
  | v_abs : forall x T2 t1,
    value <{\x:T2, t1}>
  | v_nat : forall n : nat ,
    value <{ n }>
  | v_unit :
    value <{ unit }>
  | v_loc : forall l,
    value <{ loc l }>.

然后为了定义这个包含引用的语言的操作语义，首先需要定义内存空间：

Definition store := list tm.

接下来就可以定义小步法操作语义了（这里的 st 表示内存空间）：

     t1 / st -> t1' / st'
------------------------------ (ST_Ref)
 ref t1 / st -> ref t1' / st'

-------------------------------- (ST_RefValue)
 ref v / st -> loc |st| / st, v

  t1 / st -> t1' / st'
------------------------ (ST_Deref)
 !t1 / st -> !t1' / st'

             l < |st|
----------------------------------- (ST_DerefLoc)
 !(loc l) / st -> lookup l st / st

       t1 / st -> t1' / st'
---------------------------------- (ST_Assign1)
 t1 := t2 / st -> t1' := t2 / st'

       t2 / st -> t2' / st'
---------------------------------- (ST_Assign2)
 v1 := t2 / st -> v1 := t2' / st'

               l < |st|
--------------------------------------- (ST_Assign)
 loc l := v / st -> unit / [l := v] st

                 value v2
------------------------------------------ (ST_AppAbs)
 (\x:T2, t1) v2 / st -> [x := v2] t1 / st

    t1 / st -> t1' / st'
---------------------------- (ST_App1)
 t1 t2 / st -> t1' t2 / st'

         value v1
    t2 / st -> t2' / st'
---------------------------- (ST_App2)
 v1 t2 / st -> v1 t2' / st'

然后为了类型推导，还需要再记录一个用于存储每个位置类型的 ST。类型规则：

                l < |ST|
----------------------------------------- (T_Loc)
 Gamma; ST |-- loc l : Ref (lookup l ST)

     Gamma; ST |-- t1 : T1
------------------------------- (T_Ref)
 Gamma; ST |-- ref t1 : Ref T1

 Gamma; ST |-- t1 : Ref T1
--------------------------- (T_Deref)
  Gamma; ST |-- !t1 : T1

  Gamma; ST |-- t1 : Ref T2
    Gamma; ST |-- t2 : T2
------------------------------- (T_Assign)
 Gamma; ST |-- t1 := t2 : Unit

然后有在包含引用的语言上特殊定义的 progress 和 preservation：

Definition store_well_typed (ST:store_ty) (st:store) :=
  length ST = length st /\
  (forall l, l < length st ->
    empty; ST |-- { store_lookup l st } \in {store_Tlookup l ST }).

Inductive extends : store_ty -> store_ty -> Prop :=
  | extends_nil : forall ST',
    extends ST' nil
  | extends_cons : forall x ST' ST,
    extends ST' ST ->
    extends (x::ST') (x::ST).

Theorem preservation : forall ST t t' T st st',
  empty ; ST |-- t \in T ->
  store_well_typed ST st ->
  t / st --> t' / st' ->
  exists ST',
    extends ST' ST /\
    empty ; ST' |-- t' \in T /\
    store_well_typed ST' st'.

Theorem progress : forall ST t T st,
  empty ; ST |-- t \in T ->
  store_well_typed ST st ->
  (value t \/ exists t' st', t / st --> t' / st').

引用还可以用于定义递归，例如下面的函数 r 会递归调用自己：

(\r:Ref (Unit -> Unit).
  r := (\x:Unit.(!r) unit); (!r))
(ref (\x:Unit.unit)) unit

模仿上面的形式可以写出阶乘函数：

(\r:Ref (Nat -> Nat).
  r := (\n:Nat. if iszero n then 1 else n * ((!r) (n - 1))); (!r))
  (ref (\n:Nat. 0))

Sub: Subtyping#

定义子类关系 S <: T 表示 S 是 T 的子类。

Liskov 替换原则：如果在使用 T 类型的值的场合，都可以替换成 S 类型的值，那么 S 就是 T 的子类。

使用子类关系定义 term 的类型，认为一个 term 具有他类型的所有父类的类型：

 Gamma |-- t1 \in T1  T1 <: T2
------------------------------- (T_Sub)
      Gamma |-- t1 \in T2

定义子类关系：

 S <: U  U <: T
---------------- (S_Trans)
     S <: T

-------- (S_Refl)
 T <: T

 S1 <: T1  S2 <: T2
-------------------- (S_Prod)
 S1 * S2 <: T1 * T2

        forall jk in j1 ... jn,
      exists ip in i1 ... im, s.t.
          jk = ip and Sp <: Tk
---------------------------------------- (S_Rcd)
 {i1:S1 ... im:Sm} <: {j1:T1 ... jn:Tn}

函数的子类关系：整体子类关系与输入类型的子类关系是相反的（称作逆变式 contravariance），输出是相同的（称作协变式 covariance）：

  T1 <: S1  S2 <: T2
---------------------- (S_Arrow)
 S1 -> S2 <: T1 -> T2

引用的子类关系：引用既可以作为输入类型也可以作为输出类型，因此引用既是逆变式也是协变式，即不变：

 S1 <: T1  T1 <: S1
-------------------- (S_Ref)
  Ref S1 <: Ref T1

再定义一个 Top 类型，让他作为最大的类型，即所有类型的父类：

---------- (S_Top)
 S <: Top

在加上 Subtyping 之后，就不能像原来的方式一样进行类型推导了。解决方法是只对每个项求最小类型，函数调用的时候检查形参和实参是否有子类关系。