Software Foundations, Volume 1: Logical Foundations
title:: software foundations volume 1: logical foundations
origin:: https://softwarefoundations.cis.upenn.edu/lf-current/Preface.html
- #book
- ## preface
collapsed:: true
- ### overview
collapsed:: true
- 写健壮软件有多种方式
collapsed:: true
- managing software projects teams (e.g., extreme programming)
- design philosophies for libraries (e.g., model-view-controller, publish-subscribe, etc.)
- programming languages (e.g., object-oriented programming, aspect-oriented programming, functional programming, ...)
- mathematical techniques for specifying and reasoning about properties of software and tools for helping validate these properties
- SF这本书讲的是最后一种方式
- #### logic
collapsed:: true
- logic在CS里面应用比在数学里面应用更多.
- CS里面用的最多的是inductive proof
- #### proof assistants
collapsed:: true
- CS也有反向贡献logic
collapsed:: true
- Automated theorem provers.
collapsed:: true
- 给一堆proposition, 计算机计算出true或者false, 或者不停机
- 例如SMT, SAT, model checker
- Proof assistants
collapsed:: true
- 结合了人的指引和计算, interactive的辅助证明
- 这本书用的coq, coq的应用有
collapsed:: true
- as a platform for modeling programming languages
- as an environment for developing formally certified software
- as a realistic environment for functional programming with dependent types
- as a proof assistant for higher-order logic
- #### functional programming
- 最基础的信条是 "computation should be pure"
- 因为pure所以可以distribute或者parallel执行, 数据结构是immutable就可以随便copy
- 和logic的关系更密切. proofs are programs
- ### exercises
collapsed:: true
- 难度登记
- 1 star, 1-2分钟就能完成
- 2 star, 5-10分钟完成
- 3 star, 10-40分钟完成
- 45 star, 30分钟+完成
- ### resources
collapsed:: true
- #### sample exams
collapsed:: true
- https://www.seas.upenn.edu/~cis500/current/exams/index.html
- #### lecture videos
- https://deepspec.org/event/dsss17
- https://deepspec.org/event/dsss18/
-
- ## functional programming in coq(basic)
collapsed:: true
- ### introduction
collapsed:: true
- 如果一个function是pure的, 所有的信息就是怎么从input map到output
- 另一个functional的意思是function as first class value
- 还有一些其他的feature, 方便操作函数的
- adt
- pattern matching
- polymorphic type system
- 这章的前半部分讲怎么用gallina写程序. 后半部分一些基本tactics可以验证gallina程序
- ### data and functions
collapsed:: true
- #### enumerated types
- coq只提供了非常基础的type, 连list, map, set这类东西都是common library提供的, 并且是可以用户态自己构造出来的
- #### days of the week
- 定义类型
- ```coq
Inductive day : Type :=
| monday
| tuesday
| wednesday
| thursday
| friday
| saturday
| sunday.
```
- 定义函数
- ```coq
Definition next_weekday (d:day) : day :=
match d with
| monday ⇒ tuesday
| tuesday ⇒ wednesday
| wednesday ⇒ thursday
| thursday ⇒ friday
| friday ⇒ monday
| saturday ⇒ monday
| sunday ⇒ monday
end.
```
- 定义example
- ```coq
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
```
-
- #### homowork submission guidelines
- ### boolean
- boolean也是可以自己构造的
- ```coq
Inductive bool : Type :=
| true
| false.
```
- 自定义notation
- ```coq
Notation "x && y" := (andb x y).
```
- coq有自带的if then else. 是支持所有只有两个constructor的type的. 默认第一个是true, 第二个是false
- ```
Definition negb' (b:bool) : bool :=
if b then false
else true.
```
- ### types
- coq里面的每个expression都有个type, 可以用check来打印type
- ```coq
Check true.
```
- 可以判断是否符合type
- ```coq
Check true : bool.
```
- function type 用arrow来表示
- ```coq
Check negb : bool -> bool.
```
- ### new types from old
- type除了枚举所有inhabitant, 还可以加type参数
- ```coq
Inductive rgb : Type :=
| red
| green
| blue.
Inductive color : Type :=
| black
| white
| primary (p : rgb).
```
- 可以pattern match
- ```coq
Definition isred (c : color) : bool :=
match c with
| black ⇒ false
| white ⇒ false
| primary red ⇒ true
| primary _ ⇒ false
end.
```
- #### modules
- module是一个提供namespace的方法
- ```coq
Module Playground.
Definition b : rgb := blue.
End Playground.
Definition b : bool := true.
Check Playground.b : rgb.
Check b : bool.
```
- #### tuples
- 一个constructor加多个参数, 就是tuple
- ```coq
Inductive bit : Type :=
| B0
| B1.
Inductive nybble : Type :=
| bits (b0 b1 b2 b3 : bit).
Check (bits B1 B0 B1 B0)
: nybble.
```
- #### numbers
- ```coq
Module NatPlayground.
Inductive nat : Type :=
| O
| S (n : nat).
```
- constructor 有点像是function, 可以传参数进去, 但是他什么都没计算. 只是a way to write a thing
- 类似写111, 这就是个data, 不是computation
- 如果需要递归, 就要把definition换成fixpoint
- ```coq
Fixpoint even (n:nat): bool :=
match n with
| O => true
| S O => false
| S (S n') => even n'
end.
```
- 可以用逗号同时pattern match
- ```coq
Fixpoint minus (n m:nat) : nat :=
match n, m with
| O , _ ⇒ O
| S _ , O ⇒ n
| S n', S m' ⇒ minus n' m'
end.
```
- ### proof by simplification
collapsed:: true
- 之前写的example也是一种proof, proof的是单个案例
- ```coq
Theorem plus_0_n: forall n : nat, 0 + n = n.
Proof.
intros n. simpl. reflexivity. Qed.
```
- 对于coq来说, Example, Theorem, Lemma, Fact, Remark都是基本上一样的, 只是style的问题
- intros, simpl, reflexivity这些都是tatics
- ### proof by rewriting
collapsed:: true
- ```coq
Theorem plus_id_example : ∀ n m:nat,
n = m →
n + n = m + m.
Proof.
(* move both quantifiers into the context: *)
intros n m.
(* move the hypothesis into the context: *)
intros H.
(* rewrite the goal using the hypothesis: *)
rewrite → H.
reflexivity. Qed.
```
- check 后面跟一个proof的名字, 可以显示这个proof
- ```coq
Check mult_n_O.
(* ===> forall n : nat, 0 = n * 0 *)
Check mult_n_Sm.
(* ===> forall n m : nat, n * m + n = n * S m *)
```
-
- ### proof by case analysis
collapsed:: true
- 在destruct一个type的时候, 需要给一个[]
collapsed:: true
- 元素的个数由这个type有多少个constructor决定, 这里是两个
- 第一个是空, 因为O没有argument
- 第二个是n', 意思是会引入一个 S n'. S是有argument的
- eqn:E的意思是, 上面的那个假设, 取名字为E
collapsed:: true
- 在第一个subgoal里面, E就是 n = 0
- 在第二个subgoal里面, E就是 n = S n'
- ```coq
Theorem plus_1_neq_0 : ∀ n : nat,
(n + 1) =? 0 = false.
Proof.
intros n. destruct n as [| n'] eqn:E.
- reflexivity.
- reflexivity. Qed.
```
- #### more on notation (optional)
- #### fixpoints and structural recursion (optional)
- structural recursion的意思是recur的时候, 参数结构变小了
- coq规定所有Fixpoint在递归的时候, 必须有一个参数是变小的
- 为了停机
- ### more exercises
- ### testing your solutions
- ## Proof by induction (induction)
- ### separate compilation
collapsed:: true
- 跳过没看, 不重要. 下载了网上全套的代码, 然后跑起来了.
- 重点是在Basic.v里面先点compile buffer.
- 然后再去indection.v里面跑require
- ### proof by induction
- principle of induction over natural numbers
- if P(n) is some proposition involving a natural number n, and we want to show that P holds for all numbers n. we can
- show that P(0) holds.
- show that, for any n', if P(n') holds, then so does P(S n')
- conclude that P(n) holds for all n.
- coq里面有个induction n as [| n' IHn']
- |前面的第一个部分, n = 0, 没有参数, 所以不需要给名字
- 后面n'引入了 n = S (n')
- IHn' 引入了一个 Induction Hypothesis, P(n') holds
- ### proofs within proofs
- ### formal vs. informal proof
- ### more exercises
- ### nat to bin and back to nat
- ### bin to nat and back to bin (advanced)
- ## working with structured data (lists)
collapsed:: true
- ### pairs of numbers
- ### lists of numbers
- ### reasoning about lists
- #### induction on lists
- #### search
- #### list exercises, part1
- #### list exercises, part2
- ### options
- ### partial maps