软件基础：形式验证

10 collapsed lines
1
(*
2
这段Coq代码定义了一个新的归纳类型（Inductive Type），名为 day。
3
可以这样理解：
4
Inductive day : Type: 这部分声明了我们要创建一个名为 day 的新类型。Inductive 关键字表示这个类型是通过列举其所有可能的构造函数（constructor）来定义的。: Type 表示 day 本身是一个类型。
5
:=: 这是定义操作符，意思是“被定义为”。
6
| monday | tuesday ... | sunday: 这一长串由 | 分隔的列表是 day 类型的构造函数。每一个构造函数都是 day 类型的一个唯一、离散的值。
7
简单来说，这段代码是在创建一个枚举类型，就像在其他编程语言中一样。 它创建了一个名为 day 的新类型，这个类型的变量只能取 monday, tuesday, wednesday, thursday, friday, saturday, sunday 这七个值中的一个。
8
*)
9

10

11
Inductive day : Type :=
12
| monday
13
| tuesday
14
| wednesday
15
| thursday
16
| friday
17
| saturday
18
| sunday.
19

12 collapsed lines
20
(*
21
match d with ... end:
22

23
这是一个模式匹配表达式，是Coq（以及许多函数式编程语言）中非常核心和强大的功能。
24
它的作用是检查变量 d 的具体值，并根据不同的值执行不同的代码分支。
25
你可以把它看作是其他语言中 switch-case 语句的更强大版本。
26
| monday => tuesday:
27

28
这是一个匹配分支。| 分隔了不同的情况。
29
它表示：“如果 d 的值是 monday，
30
那么 => 整个表达式的结果就是 tuesday”。
31
*)
32
Definition next_weekday (d : day) : day :=
33
match d with
34
| monday => tuesday
35
| tuesday => wednesday
36
| wednesday => thursday
37
| thursday => friday
38
| friday => monday
39
| saturday => monday
40
| sunday => monday
41
end.
42

43
(* 测试：计算 next_weekday friday 的结果（应返回 monday） *)
44
Compute (next_weekday friday).  (* 输出：monday : day *)
45

46
(*
47
   定义一个测试用例命题：
48
   "连续两次对 saturday 调用 next_weekday 的结果应等于 tuesday"
49
   解释：
50
   1. 第一次 next_weekday saturday → monday
51
   2. 第二次 next_weekday monday → tuesday
52
*)
53
Example test_next_weekday:
54
  (next_weekday (next_weekday saturday)) = tuesday.
55

56
(* 证明过程：
57
   - simpl：化简表达式（计算具体值）
58
   - reflexivity：检查等式两边是否相同
59
   - Qed：完成证明
60
*)
61
Proof.
62
  simpl.       (* 展开计算：next_weekday saturday → monday
63
                       然后 next_weekday monday → tuesday *)
64
  reflexivity. (* 验证 tuesday = tuesday *)
65
Qed.
66

67
(* 检查 test_next_weekday 的类型，确认它是一个已被证明的命题 *)
68
Check test_next_weekday.  (* 输出：test_next_weekday : ... = tuesday *)

Definition nandb (b1:bool) (b2:bool) : bool :=
(*一开始不知道match可以匹配两个参数*)
  match b1, b2 with
  | true, true => false
  | _, _       => true
  end.

Example test_nandb1: (nandb true false) = true.
Proof. reflexivity. Qed.

Example test_nandb2: (nandb false false) = true.
Proof. reflexivity. Qed.

Example test_nandb3: (nandb false true) = true.
Proof. reflexivity. Qed.

Example test_nandb4: (nandb true true) = false.
Proof. reflexivity. Qed.

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
match b1,b2,b3 with
| true,true,true => true
| _,_,_ => false
end.

Example test_andb31: (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb32: (andb3 false true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb33: (andb3 true false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb34: (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed.

Require Import Coq.Arith.Arith.

Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (plus n' m)
  end.

Module NatPlayground2.
Fixpoint mult (n m : nat) : nat :=
  match n with
  | O => O
  | S n' => plus m (mult n' m)  (* 正确的递归乘法 *)
  end.
Example test_mult1: (mult 3 3) = 9.
Proof. simpl. reflexivity. Qed.

Fixpoint factorial ( n : nat) : nat :=
match n with
 | O => 1
 | S n' => mult n (factorial n')
 end.
Example test_factorial1: (factorial 3) = 6.
Proof. simpl. reflexivity. Qed.
Example test_factorial2: (factorial 5) = (mult 10 12).
Proof. simpl. reflexivity. Qed.

(* 导入标准库（确保 eqb 和 leb 已定义） *)
Require Import Coq.Arith.Arith.

(* 方案1：直接模式匹配 leb 和 eqb 的结果 *)
Definition ltb_v1 (n m : nat) : bool :=
  match (n <=? m), (n =? m) with
  | true, false => true   (* n ≤ m 且 n ≠ m 时返回 true *)
  | _, _        => false  (* 其他情况返回 false *)
  end.

(* 方案2：嵌套 if 表达式 *)
Definition ltb_v2 (n m : nat) : bool :=
  if (n <=? m) then       (* 先检查 n ≤ m *)
    if (n =? m) then      (* 再检查是否不等于 *)
      false               (* n = m 时返回 false *)
    else true             (* n < m 时返回 true *)
  else false.             (* n > m 时返回 false *)

(* 方案3：独立递归实现（不依赖 leb/eqb） *)
Fixpoint ltb_v3 (n m : nat) : bool :=
  match n, m with
  | O,   S _  => true     (* 0 < 任何正数 *)
  | S n', S m' => ltb_v3 n' m'  (* 递归比较前驱 *)
  | _,    _    => false   (* 其他情况（包括 n=O,m=O 和 n>S _,m=O） *)
  end.

(* 方案4：利用 leb 的否定（最简洁数学定义） *)
Definition ltb_v4 (n m : nat) : bool :=
  negb (m <=? n).  (* n < m 当且仅当 ¬(m ≤ n) *)

(* 为所有方案声明统一的中缀记法 *)
Notation "x <? y" := (ltb_v1 x y) (at level 70).  (* 可替换为 v2/v3/v4 *)

(* ===================== 测试用例 ===================== *)
Section Tests.
(* 测试用例验证所有方案等价 *)
Example test_all1: ltb_v1 2 2 = false /\ ltb_v2 2 2 = false /\
                 ltb_v3 2 2 = false /\ ltb_v4 2 2 = false.
Proof. simpl; auto. Qed.

Example test_all2: ltb_v1 2 4 = true /\ ltb_v2 2 4 = true /\
                 ltb_v3 2 4 = true /\ ltb_v4 2 4 = true.
Proof. simpl; auto. Qed.

Example test_all3: ltb_v1 4 2 = false /\ ltb_v2 4 2 = false /\
                 ltb_v3 4 2 = false /\ ltb_v4 4 2 = false.
Proof. simpl; auto. Qed.

(* 边界测试：0 的比较 *)
Example test_zero: ltb_v1 0 0 = false /\ ltb_v3 0 1 = true.
Proof. simpl; auto. Qed.
End Tests.

(* 方案选择建议 *)
(*
1. 需要清晰逻辑：选择 v1 或 v2
2. 需要独立实现：选择 v3
3. 需要数学简洁性：选择 v4
4. 实际开发推荐直接使用标准库的 Nat.ltb
*)

Theorem andb_true_elim2 : forall b c : bool,
andb b c = true -> c = true.
Proof.
  intros b c H.              (* 引入假设 H: andb b c = true *)
  destruct b eqn:Eb.         (* 分情况讨论b *)
  - (* b = true *)
    simpl in H.              (* H变为 c = true *)
    apply H.                 (* 直接使用假设 *)
  - (* b = false *)
    simpl in H.              (* H变为 false = true *)
    discriminate H.          (* 排除不可能情况 *)
Qed.

Theorem andb_true_elim2 : ∀ b c, andb b c = true → c = true.
Proof.
  intros b c H.
  destruct b eqn:Eb.
  - (* b = true *)
    simpl in H.      (* H : c = true *)
    rewrite H.       (* 目标从 c=true 变为 true=true *)
    reflexivity.     (* 验证 *)
  - (* b = false *)
    simpl in H.      (* H : false = true *)
    discriminate H.
Qed.