basic inctive logic relation list inp会有

一、basic

1.1 数据与函数

枚举类型

Inductive 定义一个数据集合

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Definition 可以写一些操作函数

Definition next_weekday (d:day) : day :=
  match d with
  | monday ⇒ tuesday
  | tuesday ⇒ wednesday
  | wednesday ⇒ thursday
  | thursday ⇒ friday
  | friday ⇒ monday
  | saturday ⇒ monday
  | sunday ⇒ monday
  end.

在 Coq 中检验的方式一共有三种：

第一，用 Compute 指令来计算包含 next_weekday 的复合表达式

Compute (next_weekday friday).
Compute (next_weekday (next_weekday saturday)).

第二，将期望的结果写成 Coq 的示例

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.

Proof. simpl. reflexivity.  Qed.

这段代码基本上可以读作“若等式两边的求值结果相同，该断言即可得证”

第三，我们可以让 Coq 从 Definition 中提取出用其它更加常规的编程语言编写的程序

布尔值

Inductive bool : Type :=
  | true
  | false.

布尔值的函数可按照同样的方式来定义

Definition negb (b:bool) : bool :=
  match b with
  | true ⇒ false
  | false ⇒ true
  end.

Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true ⇒ b2
  | false ⇒ false
  end.

Definition orb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true ⇒ true
  | false ⇒ b2
  end.

以下四个单元测试演示了多参数应用的语法

Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed

Notation 能为既有的定义赋予新的中缀记法

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.

类型

Check 指令会让 Coq 显示一个表达式的类型

Check true.
(* ===> true : bool *)

像 negb 这样的函数本身也有类型，被称为函数类型，用带箭头的类型表示

Check negb
    : bool → bool.
Check andb
    : bool → bool → bool.

由旧类型构造新类型

我们之前定义的枚举类型，每个元素都只是无参数构造子

下面的类型定义，会让其中一个构造子接受一个参数

Inductive rgb : Type :=
  | red
  | green
  | blue.
Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

最后一行表示若 p 是属于 rgb 的构造子表达式，则 primary p（构造子 primary 应用于参数 p）是属于集合 color 的构造子表达式

定义一个关于color的函数

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

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).
  
Check (bits B1 B0 B1 B0)
    : nybble.

Definition all_zero (nb : nybble) : bool :=
  match nb with
    | (bits B0 B0 B0 B0) ⇒ true
    | (bits _ _ _ _) ⇒ false
  end.

数值

我们把这个部分放在一个模块中，这样我们自己对自然数的定义就不会干扰标准库中的自然数

Module NatPlayground.

大写字母O表示零，当S构造函数应用于自然数n的表示时，结果是n+1，其中S代表后继（successor），可被放在一个自然数之前产生另一个自然数

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

0 → O，1 → S O，2 → S(S O)，3 → S(S(S O))，以此类推

定义自然数的前趋函数

Definition pred (n : nat) : nat :=
  match n with
    | O ⇒ O
    | S n' ⇒ n'
  end.

定义自然数减法函数

Definition minustwo (n : nat) : nat :=
  match n with
    | O ⇒ O
    | S O ⇒ O
    | S (S n') ⇒ n'
  end.
Compute (minustwo 4).
(* ===> 2 : nat *)

End NatPlayground.

Coq 会默认将自然数打印为十进制形式

Check (S (S (S (S O)))).
(* ===> 4 : nat *)

递归

关键字 Fixpoint 可用于定义递归函数

比如判断自然数是否为偶数

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O ⇒ true
  | S O ⇒ false
  | S (S n') ⇒ evenb n'
  end.

判断自然数是否为奇数

Definition oddb (n:nat) : bool :=
  negb (evenb n).

Example test_oddb1: oddb 1 = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: oddb 4 = false.
Proof. simpl. reflexivity. Qed.

递归多参数函数

Module NatPlayground2.

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

两个自然数的乘法

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 minus (n m:nat) : nat :=
  match n, m with
  | O , _ ⇒ O
  | S _ , O ⇒ n
  | S n', S m' ⇒ minus n' m'
  end.
  
End NatPlayground2.

自然数的幂

Fixpoint exp (base power : nat) : nat :=
  match power with
    | O ⇒ S O
    | S p ⇒ mult base (exp base p)
  end.

比较两个自然数是否相等

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.

第一个参数是否小于等于第二个参数

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O ⇒ true
  | S n' ⇒
      match m with
      | O ⇒ false
      | S m' ⇒ leb n' m'
      end
  end.

第一个参数是否严格小于第二个参数

Definition ltb (n m:nat) : bool :=
  (negb(eqb n m)) && (leb n m)

为了方便我们引入notation来记这几个常用的函数

Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x - y" := (minus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x * y" := (mult x y)
                       (at level 40, left associativity)
                       : nat_scope.
Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.

1.2 基于化简的证明

simpl 化简等式两边

reflexivity 检查两边是否具有相同的值，会自动做一些化简

intros n 假设存在一个任意自然数 n，将量词从证明目标转移到当前假设的上下文中

Example 和 Theorem 表示完全一样的东西

策略是一条可以用在 Proof 和 Qed（证毕）之间的指令，告诉 Coq 如何来检验我们所下的断言的正确性

例如：

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. reflexivity.  Qed.

Theorem plus_1_l : forall n:nat, 1 + n = S n.
Proof.
  intros n. reflexivity. Qed.

Theorem mult_0_l : forall n:nat, 0 * n = 0.
Proof.
  intros n. reflexivity. Qed.

后缀 _l 读作“在左边”

1.3 基于改写的证明

intros 将前提从证明目标移到当前上下文的假设中

rewrite 用来告诉 Coq 执行这种替换的策略

Admitted 指令告诉 Coq 我们想要跳过此定理的证明

例子一：

Theorem plus_id_example : ∀ n m:nat,
  n = m →
  n + n = m + m.

该定理并未对自然数 n 和 m 所有可能的值做全称断言，而是讨论了仅当 n = m 时这一更加特定情况

Proof.
  (* 将两个量词移到上下文中： *)
  intros n m.
  (* 将前提移到上下文中,并将其命名为 H *)
  intros H.      
  (* 告诉 Coq 改写当前目标,把前提等式 H 的左边替换成右边 *)
  rewrite → H.    
  reflexivity. Qed.

→表示把左边替换成右边，←表示把右边替换成左边

便于理解，放个例子

引入前提 H : n = m

如果是 -> ，代表把式子里面的n都换成m

如果是 <-，表示把式子里的m都换成n，逆向替换

例子二：

Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
  intros n m o H H1.
  rewrite -> H.
  rewrite -> H1.
  reflexivity.
Qed.

为了便于理解，具体过程如下

引入前提

根据前提 H1：n = m

把式子中的n换成m

根据前提 H1：n = m

把式子中的m都换成o

Check 命令

可用来检查以前声明的引理和定理

Check mult_n_O.
(* ===> forall n : nat, 0 = n * 0  *)
Check mult_n_Sm.
(* ===> forall n m : nat, n * m + n = n * S m  *)

除了上下文中现有的假设外，还可以通过 rewrite 策略来运用前期证明过的定理

例子三

Theorem mult_n_0_m_0 : ∀ n m : nat,
  (n × 0) + (m × 0) = 0.
Proof.
  intros n m.
  rewrite <- mult_n_O.
  rewrite <- mult_n_O.
  reflexivity. Qed.

例子四

Theorem mult_n_1 : ∀ n : nat,
  n × 1 = n.
Proof.
  intros.
  rewrite <- mult_n_Sm.
  rewrite <- mult_n_O.
  reflexivity. Qed.

例子五

Theorem mult_0_plus : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros n m.
  rewrite -> plus_O_n.
  reflexivity.  Qed.

例子六

Theorem mult_S_1 : forall n m : nat,
  m = S n ->
  m * (1 + n) = m * m.
Proof.
  intros n m H.
  simpl.
  rewrite <- H.
  reflexivity.
Qed.

1.4 基于情况分析的证明

destruct 分别对 n = 0 和 n = S n’ 这两种情况进行分析的策略

例一

Theorem plus_1_neq_0 : forall n : nat,
  beq_nat (n + 1) 0 = false.
Proof.
  intros n. destruct n as [| n'].
  - reflexivity.
  - reflexivity.
Qed.

destruct 生成两个子目标，然后我们分别证明

as [| n’] 是介绍模式，指出变量，变量之间用|分开。第一个组件是空的，因为O的构造函数是空的，第二个组件n’，因为S是一元构造函数

eqn:E 注释告诉析构函数给这个方程命名E

— 符号 标明这两个生成的子目标所对应的证明部分

例二

证明布尔值的取反是对合（Involutive）的

Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Proof.
  intros b. destruct b.
  - reflexivity.
  - reflexivity.  Qed.

destruct 没有 as 子句，因为此处 destruct 生成的子分类均无需绑定任何变量

b分成了true和false两种情况讨论

例三

在一个子目标内调用 destruct，产生出更多的证明义务，使用不同的标号来标记目标的不同层级

Theorem andb_commutative : ∀ b c, andb b c = andb c b.
Proof.
  intros b c. destruct b
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
Qed.

具体过程如下：

引入变量b c

分别讨论b为true和b为false两种情况

在b为true的情况下，分别讨论c为true和c为false两种情况

除了 - 和 + 之外，还可以使用 × – ***，也可以用花括号将每个子证明目标括起来

Theorem andb_commutative' : ∀ b c, andb b c = andb c b.
Proof.
  intros b c. destruct b
  { destruct c
    { reflexivity. }
    { reflexivity. } }
  { destruct c
    { reflexivity. }
    { reflexivity. } }
Qed.

花括号还允许我们在一个证明中的多个层级下使用同一个标号

Theorem andb3_exchange :
  ∀ b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
  intros b c d. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
Qed.

最后说一种简便写法，很多证明在引入变量之后会立即对它进行情况分析：

intros x y. destruct y as [|y] eqn:E.

但可以通过使用介绍模式而不是变量名来对变量进行案例分析

Theorem plus_1_neq_0' : ∀ n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity. Qed.

如果没有需要命名的构造子参数，只需写上 [] 即可进行情况分析

Theorem andb_commutative'' :
  forall b c, andb b c = andb c b.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

练习一

Theorem zero_nbeq_plus_1 : forall n : nat,
  0 =? (n + 1) = false.
Proof.
  intros [| n'].
  -simpl. reflexivity.
  -simpl. reflexivity.
Qed.

熟练使用简化的引入写法

练习二

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros [] [].
  - reflexivity.
  - intro H.
    rewrite <- H.
    reflexivity.
  - reflexivity.
  - intro H.
    rewrite <- H.
    reflexivity.
Qed.

说明一下第二种情况和第四种情况的过程，之前一直无法理解

引入 false && false = true 的条件，想要证明的结论是 false = true

把条件中的true rewrite 为 false && false

1.5 递归函数Fixpoint

1.6 更多练习

练习一

证明以下关于布尔函数的定理

Theorem identity_fn_applied_twice :
  forall (f : bool -> bool),
  (forall (x : bool), f x = x) ->
  forall (b : bool), f (f b) = b.
Proof.
  intros f H b.
  rewrite -> H.
  rewrite -> H.
  reflexivity.
Qed.

练习二

Theorem negation_fn_applied_twice :
  forall (f : bool -> bool),
  (forall (x : bool), f x = negb x) ->
  forall (b : bool), f (f b) = b.
Proof.
  intros f H b.
  rewrite -> H.
  rewrite -> H.
  rewrite -> negb_involutive.
  reflexivity.
Qed.

其中
negb_involutive
     : forall b : bool, negb (negb b) = b

练习三

Theorem andb_eq_orb :
  forall (b c : bool),
  (andb b c = orb b c) ->
  b = c.
Proof.
  intros b c H.
  destruct b.
  - destruct c.
    + reflexivity.
    + simpl in H.
      rewrite -> H. reflexivity.
  - destruct c.
    + simpl in H.
      rewrite -> H. reflexivity.
    + reflexivity.
Qed.

二、归纳证明 induction

2.1 归纳证明

在开始之前把上一章所有的定义都导入进来

在 CoqIDE 中：Open Basics.v，complie → compile buffer → make makefile

然后 Open Induction.v

From LF Require Export Basics.

证明这种关于数字、列表等归纳定义的集合，我们通常需要一个更强大的推理原理：归纳

方法：通过应用 induction，把它分为两个子目标：

一个是我们必须证明 P(O) 成立
另一个是我们必须证明 P(n’) → P(S n’)

例题

例子一：

Theorem plus_n_O : forall n:nat, n = n + 0.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)    reflexivity.
  - (* n = S n' *) simpl. rewrite <- IHn'. reflexivity.  Qed.

具体过程如下：

通过induction as分成两种情况，用|隔开

在第一个子目标中n被0取代

在第二个目标中，n 被 S n’ 取代，IHn’ ：n’ = n’ + 0 是已知前提

待证目标变成了 (S n’) + 0 = S n’，它可被simpl化简为 S (n’ + 0) = S n’，而此结论可通过 IHn’ 得出

这里没太懂

改写

例子二

Theorem minus_diag : forall n,
  minus n n = 0.
Proof.
  intros n. induction n as [| n' IHn'].      // IHn' : n' - n' = 0
  - (* n = 0 *)
    simpl. reflexivity.
  - (* n = S n' *)            // S n' - S n' = 0
    simpl.                    // n' - n' = 0
    rewrite -> IHn'.          // 0 = 0
    reflexivity.  Qed.

这里没懂

好像知道了simpl的作用，可以把 S n’ 化成 n’，不知道为啥

练习

练习一

Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
  intros n.
  induction n as [|n' IHn].
  - reflexivity.
  - simpl. rewrite -> IHn. reflexivity. Qed.

好像知道了simpl的作用，可以把 S n’ 化成 n’，不知道为啥

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
  intros n m.
  induction n as [|n' IHn].
  - reflexivity.
  - simpl. rewrite -> IHn. reflexivity.
Qed.

好像知道了simpl的另一个作用，可以把 S n’ + m 化成 S (n’ + m)

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction n as [|n' IHn].   //  IHn : n' + m = m + n'
  - (* n = 0 *)
    simpl.
    rewrite <- plus_n_O.
    reflexivity.
  - (* n = S n' *)             //  S n' + m = m + S n'
    simpl.                     //  S (n' + m) = m + S n'
    rewrite -> IHn.            //  S (m + n') = m + S n'
    rewrite -> plus_n_Sm.      //  m + S n' = m + S n'
    reflexivity.
Qed.

其中
plus_n_O
     : forall n : nat, n = n + 0
     
plus_n_Sm
     : forall n m : nat, S (n + m) = n + S m

Theorem plus_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros n m p.
  induction n as [|n' IHn].                 // IHn : n' + (m + p) = n' + m + p
  - reflexivity.
  - (* n = S n' *)             //  S n' + (m + p) = S n' + m + p
    simpl.                     //  S (n' + (m + p)) = S (n' + m + p)
    rewrite -> IHn.            //  S (n' + m + p) = S (n' + m + p)
    reflexivity.
Qed.

练习二

前提

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

用归纳法证明

Lemma double_plus : forall n, double n = n + n .
Proof.
  intros n.
  induction n as [|n' IHn].      // double n' = n' + n'
  - (* n = 0 *)
    reflexivity.
  - (* n = S n' *)               // double (S n') = S n' + S n'
   simpl.                        // S (S (double n')) = S (n' + S n')
   rewrite -> IHn.               // S (S (n' + n')) = S (n' + S n')
   rewrite <- plus_n_Sm.         // S (S (n' + n')) = S (S (n' + n'))
   reflexivity.
Qed.


其中
     
plus_n_Sm
     : forall n m : nat, S (n + m) = n + S m

练习三

Check negb_involutive.
Theorem evenb_S : forall n : nat,
  evenb (S n) = negb (evenb n).
Proof.
  intros n.
  induction n as [|n' IHn].            //  IHn : evenb (S n') = negb (evenb n')
  - reflexivity.
  -                                    //  evenb (S (S n')) = negb (evenb (S n'))
    rewrite -> IHn.                    //  evenb (S (S n')) = negb (negb (evenb n'))
    rewrite -> negb_involutive.        //  evenb (S (S n')) = evenb n'
    reflexivity.
Qed.


其中
negb_involutive
     : forall b : bool, negb (negb b) = b

辨析

一直没懂什么时候用基于化简，什么时候用基于归纳

0在n左边的时候用化简，0在n右边的时候用归纳

0 + n = n ，n = 0 + n 用化简，n + 0 = n，n = n + 0用归纳

0 * n = 0 用化简，n * 0 = 0用归纳

因为 0 * n = 0 可以被simpl. 后者不行

前者 simpl 结果

后者 simpl 结果，没有变化，这只能用归纳了

2.2 证明里的证明

在 Coq 中，大的证明通常会被分为一系列定理，后面的定理引用之前的定理

例如，我们之前对 mult_0_plus 定理的证明引用了前一个名为 plus_O_n 的定理

Theorem mult_0_plus : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros n m.
  rewrite -> plus_O_n.
  reflexivity.  Qed.

而我们只需使用 assert 就能陈述并证明 plus_O_n，后面的大括号内容是证明过程

Theorem mult_0_plus' : forall n m : nat,
  (0 + n) * m = n * m.
Proof.
  intros n m.
  assert (H: 0 + n = n). { reflexivity. }
  rewrite -> H.
  reflexivity.  Qed.

另一个例子

为了在需要的地方使用我们的小定理，可以引入一个局部引理来陈述 n + m = m + n，之后用 plus_comm 证明它，并用它来进行期望的改写

Theorem plus_rearrange : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  assert (H: n + m = m + n).
  { rewrite -> plus_comm. reflexivity. }
  rewrite -> H. reflexivity.  Qed.

2.3 形式化证明

形式化证明和非形式化证明的对比

非形式化证明是算法，形式化证明是代码

一方面，“读者”可以是像 Coq 这样的程序，此时灌输的是 P 能够从一个确定的，由形式化逻辑规则组成的集合中机械地推导出来，而证明则是指导程序检验这一事实的方法。这种方法就是形式化证明

另一方面，读者也可以是人类，这种情况下证明可以用英语或其它自然语言写出，因此必然是非形式化的

由于我们在本课程中使用 Coq，因此会重度使用形式化证明

但这并不意味着我们可以完全忽略掉非形式化的证明过程！

2.4 更多练习

练习一

可以不用归纳

Theorem plus_swap : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  intros n m p.                            //  n + (m + p) = m + (n + p)
  rewrite -> plus_assoc.                   //  n + m + p = m + (n + p)
  assert (H: n + m = m + n).            
  { rewrite -> plus_comm.  reflexivity. }
  rewrite -> H.                            //  n + m + p = n + (m + p)
  rewrite -> plus_assoc.                   //  n + m + p = n + m + p
  reflexivity.
Qed.

plus_assoc
     : forall n m p : nat, n + (m + p) = n + m + p
     
plus_comm
     : forall n m : nat, n + m = m + n

复习一下如果用归纳做，好像不是同一道题

Theorem plus_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  intros n m p.
  induction n as [|n' IHn].                 // IHn : n' + (m + p) = n' + m + p
  - reflexivity.
  - (* n = S n' *)             //  S n' + (m + p) = S n' + m + p
    simpl.                     //  S (n' + (m + p)) = S (n' + m + p)
    rewrite -> IHn.            //  S (n' + m + p) = S (n' + m + p)
    reflexivity.
Qed.

练习二

Theorem mult_n_Sm: forall n m : nat,
  n * S m = n + n * m.
Proof.
  intros n m.
  induction n as [|n' IHn].           //  IHn : n' * S m = n' + n' * m
  - (* n = 0 *)
    reflexivity.
  - (* n = S n' *)                    //  S n' * S m = S n' + S n' * m
    simpl.                            //  S (m + (n' + n' * m)) = S (n' + (m + n' * m)) 
    rewrite -> IHn.                   //  S (n' + (m + n' * m)) = S (n' + (m + n' * m))
    rewrite plus_swap.
    reflexivity.
Qed.

练习三

Theorem mult_comm : forall m n : nat,
  m * n = n * m.
Proof.
  intros n m.
  induction n as [|n' IHn].
  - rewrite -> mult_0_l.
    rewrite <- mult_n_O.
    reflexivity.
  - simpl.
    rewrite -> IHn.
    rewrite -> mult_n_Sm.
    reflexivity.
Qed.

练习四

区分什么时候该用什么方法

(a) 它能否能只用化简和改写来证明

(b) 它还需要分类讨论（destruct）

Theorem leb_refl : forall n:nat,
  true = leb n n.
Proof.
  intros n.
  induction n as [|n' IHn].
  - (* n = 0 *)
    reflexivity.
  - simpl. rewrite <- IHn. reflexivity.
Qed.

Theorem zero_nbeq_S : forall n:nat,
  beq_nat 0 (S n) = false.
Proof.
  intros n.
  simpl.
  reflexivity.
Qed.

Theorem S_nbeq_0 : forall n:nat,
  beq_nat (S n) 0 = false.
Proof.
  reflexivity.
Qed.

Theorem plus_ble_compat_l : forall n m p : nat,
  leb n m = true -> leb (p + n) (p + m) = true.
Proof.
  intros n m p H.
  induction p as [|p' IHp].
  - simpl.
    rewrite -> H.
    reflexivity.
  - simpl.
    rewrite -> IHp.
    reflexivity.
Qed.

Theorem mult_1_l : forall n:nat, 1 * n = n.
Proof.
  intros n.
  simpl. rewrite <- plus_n_O. reflexivity.
Qed.

这里simpl又可以把 1 * n = n 改写为 n + 0 = n，真是搞不懂

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof.
  intros n m p.
  induction n as [|n' IHn].
  - reflexivity.
  - simpl.
    rewrite -> IHn.
    rewrite -> plus_assoc.
    reflexivity.
Qed.

原文链接：https://blog.csdn.net/Caiyii530/article/details/122053700

函数程序设计语言 functional programing by coqlde

文章目录

一、basic

1.1 数据与函数

枚举类型

布尔值

类型

由旧类型构造新类型

元组

数值

递归

1.2 基于化简的证明

1.3 基于改写的证明

1.4 基于情况分析的证明

1.5 递归函数Fixpoint

1.6 更多练习

二、归纳证明 induction

2.1 归纳证明

例题

练习

辨析

2.2 证明里的证明

2.3 形式化证明

2.4 更多练习