1.定义函数

定义函数gtb，使得gtb n m 返回布尔值 true当且仅当 n > m。至少用两种方法定义这个函数。

（请用 【Example】 语句测试 n>m, n=m, n<m 三种情况下你定义的gtb函数(含两种方式)的输出）

方法一 根据先前定义的函数来定义

Coq代码

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 gtb(n m :nat):bool :=
 negb (leb n m).

Example test_gtb1: gtb 4 2 = true.
Proof. simpl. reflexivity. Qed.
Example test_gtb2: gtb 2 2 = false.
Proof. simpl. reflexivity. Qed.
Example test_gtb3: gtb 2 4 = false.
Proof. simpl. reflexivity. Qed.

Coq运行截图

方法二：设置新的 Fixpoint

Coq代码

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

Example test_gtb1: gtb 4 2 = true.
Proof. simpl. reflexivity. Qed.
Example test_gtb2: gtb 2 2 = false.
Proof. simpl. reflexivity. Qed.
Example test_gtb3: gtb 2 4 = false.
Proof. simpl. reflexivity. Qed.

Coq运行截图

2.证明性质

证明下面的性质。

Theorem gtb_test : forall n : nat, gtb (n+1) 0 = true.

Coq代码

Theorem gtb_test : forall n : nat, gtb (n+1) 0 = true.
Proof.
intros n.
destruct n as [| n'] eqn:E.
- reflexivity.
- reflexivity.

Coq运行截图

3.定义函数

（请用【Compute】语句使用你定义的F函数 分别计算出第【1、5、10】个斐波那契数以表明定义的正确性。 ）

Coq代码

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

Coq运行截图