软件理论基础与实践
持续更新中......
一. Coq函数式编程
程序语言：
命令式语言：直接描述底层机器应该执行的动作
函数式语言：
𝜆演算：计算的本质是函数调用
采用函数调用描述计算
逻辑式语言：
用户给出前提、结论和推导式
从 前提 推导 结论 的过程就构成了计算
Coq与Gallina：
Coq是一个交互式定理证明工具
Gallina是包含在Coq中的描述语言，是函数式编程语言、也用来描述定理和证明
枚举：
定义一个数据集合Type：
Inductive day : Type := | monday | tuesday | wednesday | thursday | friday | saturday | sunday.函数定义：
Definition next_weekday (d:day) : day := match d with | monday ⇒ tuesday | tuesday ⇒ wednesday | wednesday ⇒ thursday | thursday ⇒ friday | friday ⇒ monday | saturday ⇒ monday | sunday ⇒ monday end.检验：
compute指令：
Eval compute in (next_weekday friday).Eval compute in (next_weekday (next_weekday saturday)).f a表示把a作为参数传给f
空格左结合：f a b = (f a)b
空格的优先级大于其他操作
定理和证明：
Example test_next_weekday: (next_weekday (next_weekday saturday)) = tuesday. Proof. simpl. reflexivity. Qed.Example：声明定理
simpl：化简表达式
reflexivity：根据对称性证明
让 Coq 从 Definition 中'提取（Extract）' 出用其它更加常规的编程语言编写的程序 （如 OCaml、Scheme、Haskell 等）
布尔值：
Inductive bool : Type := | true | false.Definition orb (b1:bool) (b2:bool) : bool := match b1 with | true ⇒ true | false ⇒ b2 end.Notation：为既有的定义赋予新的符号记法，比如以下定义函数orb记法为 ||
Notation "x || y" := (orb x y).条件判断：
Definition orb' (b1:bool) (b2:bool) : bool := if b1 then true else b2.coq支持对任意表达式使用if
类型：
check true. 会返回true是bool类型
check true : bool. 会返回true是不是布尔类型，不是则报错
check negb : bool -> bool.
理解为nega类型是"给定一个 bool 类型的输入，该函数产生一个 bool 类型的输出"
又比如andb 的类型写作 bool → bool → bool，可以理解为 “给定两个 bool 类型的输入，该函数产生一个 bool 类型的输出。”
由旧类型构造新类型：
Inductive rgb : Type := | red | green | blue. Inductive color : Type := | black | white | primary (p : rgb).原子标识符，构造子Constructo：比如之前的true、monday
每个归纳定义的类型（如 day、bool、rgb、color 等） 都描述了一组由'构造子'构成的'构造子表达式' constructor expression。
若 p 是属于 rgb 的构造子表达式，则 primary p（读作“构造子 primary 应用于参数 p）是属于集合 color 的构造子表达式；且通过这些方式构造的构造子表达式'只属于'集合 rgb 和 color。
使用带参数的构造函数：
Definition isred (c : color) : bool := match c with | black ⇒ false | white ⇒ false | primary red ⇒ true | primary _ ⇒ false end.primary _ 是“构造子 primary 应用到除 red 之外的任何 rgb 构造子上”的简写形式
元组：
一个多参数的单构造子可以用来创建元组类型
Inductive bit : Type := | B0 | B1. Inductive nybble : Type := | bits (b0 b1 b2 b3 : bit).运用了包装作用，nybble是一个四比特元组
解包可以通过模式匹配实现：
Definition all_zero (nb : nybble) : bool := match nb with | (bits B0 B0 B0 B0) ⇒ true | (bits _ _ _ _) ⇒ false end.模块：类似于java里的包或c++里的namespace
如果我们将一组定义放在 Module X 和 End X 标记之间，那么在文件中的 End 之后，我们就可以通过像 X.foo 这样的名字来引用，而不必直接用 foo 了
数值：
之前定义的都是有限集合，定义自然数：
皮亚诺公理：
• 0是自然数
• 每个自然数有一个后继，后继也是自然数
• 0不是任何数的后继
• 如果x和y的后继相同，那么x和y相等
定义自然数：
Inductive nat : Type := | O | S (n : nat).0 被表示为 O, 1 则被表示为 S O, 2 则是 S (S O)，以此类推
前驱函数：
Definition pred (n : nat) : nat := match n with | O ⇒ O | S n' ⇒ n' end.Coq原生自然数类型：一进制：
Check (S (S (S (S O)))). (* ===> 4 : nat *)需要强调Coq并没有将自然数转换成计算机内部表示 并采用相应汇编指令来计算的过程，这个特性使得包含某些未知量时也能计算，在证明 时非常有用：比如
minustwo (S (S n)) = n定义递归函数：
Fixpoint evenb (n:nat) : bool := match n with | O ⇒ true | S O ⇒ false | S (S n') ⇒ evenb n' end.多参数也可以这样定义：
Fixpoint mult (n m : nat) : nat :=定义减法：
这里使用了并列匹配
Fixpoint minus (n m:nat) : nat := match n, m with | O , _ ⇒ O | S _ , O ⇒ n | S n', S m' ⇒ minus n' m' end.嵌套match：
Fixpoint eqb (n m : nat) : bool := match n with | O ⇒ match m with | O ⇒ true | S m' ⇒ false end | S n' ⇒ match m with | O ⇒ false | S m' ⇒ eqb n' m' end end.结构递归：递归调用的实参是原形参的子结构，一定终止
基于化简的证明：
Theorem plus_O_n' : ∀ n : nat, 0 + n = n. Proof. intros n. reflexivity. Qed.使用 simpl 来化简等式两边，然后用 reflexivity 来检查两边是否具有相同的值。
simpl 策略用于应用乘法的定义并简化等式，使得我们可以看到表达式的具体形式。
reflexivity 策略用于证明等式成立，当两边的表达式完全相同时
关键字 Example 和 Theorem（以及其它一些，包括 Lemma、Fact 和 Remark）都表示完全一样的东西
量词：使用intros n实现“'假设' 存在一个任意自然数 n...”（也可以用别的字母）
关键字 intros、simpl 和 reflexivity 都是'策略（Tactic）'的例子。 策略是一条可以用在 Proof（证明）和 Qed（证毕）之间的指令，它告诉 Coq 如何来检验我们所下的一些断言的正确性
基于改写的证明：
->蕴含
Theorem plus_id_example : ∀ n m:nat, n = m → n + n = m + m.我们需要在能够假定存在自然数 n 和 m 的基础上进行推理。 另外我们需要假定有前提 n = m。intros 策略用来将这三条前提从证明目标 移到当前上下文的假设中：
Proof. (* 将两个量词移到上下文中： *) intros n m. (* 将前提移到上下文中： *) intros H. (* 用前提改写目标： *) rewrite → H. reflexivity. Qed.第三行告诉 Coq 改写当前目标（n + n = m + m），把前提等式 H 的左边替换成右边。
rewrite 中的箭头与蕴含无关：它指示 Coq 从左往右地应用改写。 若要从右往左改写，可以使用 rewrite <-
例：
Theorem plus_id_exercise : forall n m o : nat, n = m -> m = o -> n + m = m + o. Proof. intros n m o H1 H2. (* 引入前提 *) rewrite -> H1. (* 使用等号的传递性，将 n 替换为 m *) rewrite <- H2. (* 使用等号的传递性，将 o 替换为 m *) reflexivity. (* 结论成立 *) Qed.
使用分类讨论来证明
Theorem plus_1_neq_0 : ∀ n : nat, (n + 1) =? 0 = false. Proof. intros n. destruct n as [| n'] eqn:E. - reflexivity. - reflexivity. Qed.destruct 策略会生成两个子目标
as [| n'] 这种标注被称为 '引入模式'。它告诉 Coq 应当在每个子目标中 使用什么样的变量名。总体而言，在方括号之间的是一个由 | 隔开的 '列表的列表'（译者注：list of lists）。在上面的例子中，第一个元素是 一个空列表，因为 O 构造子是一个空构造子（它没有任何参数）。 第二个元素提供了包含单个变量名 n' 的列表，因为 S 是一个单构造子。
作业难题
重写证明：
Theorem mult_n_1 : forall n : nat, n * 1 = n. Proof. intros n. rewrite <- mult_n_Sm. rewrite <- mult_n_O. reflexivity. Qed.对mult_n_Sm从右到左带入m=0
分类证明：遇到前提不对的情况下，用rewrite
Theorem andb_true_elim2 : forall b c : bool, andb b c = true -> c = true. Proof. intros b c H1. destruct b eqn:Eb. - destruct c eqn:Ec. + reflexivity. + rewrite <- H1. reflexivity. - destruct c eqn:Ec. + reflexivity. + rewrite <- H1. reflexivity.关于intros .
题目：
Theorem andb_eq_orb : forall (b c : bool), (andb b c = orb b c) -> b = c.如果是intro. simpl.只能对目标简化，不能简化到蕴含的前提，所以一开始不能将H intros
如果是intro b c.
simpl.之后：
再intros . (即intros H.)
最终答案：
Proof. intros b c. destruct b eqn:Eb. - destruct c eqn:Ec. + simpl. reflexivity. + simpl. intros. rewrite -> H. reflexivity. - destruct c eqn:Ec. + simpl. intros. rewrite -> H. reflexivity. + simpl. reflexivity. Qed.notice :
Example test_bin_incr1 : (incr (B Z)) = A (B Z). Proof. simpl. reflexivity. Qed. (* 函数是会自己调的，Theorem才需要rewrite *)