Coq学习——《Software-Foundation》Volume1.3-Lists

Lists

Pair of numbers

nat pair and its notation. Be care for to the format to match

1
2
3
4
Inductive natprod : Type :=
| pair (n1 n2 : nat).

Notation "( x , y )" := (pair x y).

Note that pattern-matching on a pair (with parentheses: [(x, y)]) is not to be confused with the "multiple pattern" syntax (with no parentheses: [x, y]) that we have seen previously.

We also use [destruct] to construct the pair.

1
2
3
4
5
6
7
8
9
10
11
12
13
Theorem surjective_pairing' : forall (n m : nat),
  (n,m) = (fst (n,m), snd (n,m)).
Proof.
  reflexivity. Qed.

(** But [reflexivity] is not enough if we state the lemma in a more
    natural way: *)

Theorem surjective_pairing_stuck : forall (p : natprod),
  p = (fst p, snd p).
Proof.
  simpl. (* Doesn't reduce anything! *)
Abort.

Lists of Numbers

Similar to OCaml "List" including the notation.

1
2
3
4
5
6
7
8
9
10
11
(** For example, here is a three-element list: *)

Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

Definition mylist := cons 1 (cons 2 (cons 3 nil)).
Notation "x :: l" := (cons x l)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

[++] as (which even has a prettied version) is a notation of "(app x y)"

Advanced exercise (alternate)

1
2
3
4
5
6
7
8
9
10
11
12
13
Fixpoint alternate (l1 l2 : natlist) : natlist :=
  (* This solution cannot guess decreasing argument of fix *)
  (* match l1 with *)
  (* | [] => l2 *)
  (* | h :: m => h :: alternate l2 m *)

  (* Another solution Give defination by proof *)
  match l1, l2 with
  | [] , [] => []
  | [] , l2 =>  l2
  | l1 , [] => l1
  | h1::t1 , h2::t2 => h1::h2::(alternate t1 t2)
  end.

根据 mentor，处理这种 Fixpoint 找不到，Coq 自己很憨憨的问题，后面会有 Definition by proof 来解决。

[induction] 策略根据外层 match 来尝试。师兄指导下迷迷糊糊写了 add_inc_count 的证明。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Require Import Omega.
Theorem add_inc_count : forall bg : bag  ,forall num:nat,
      count num (num::bg) = (count num  bg) + 1.
Proof.
  Search "eqb".
  Print eqb_refl.
  Print count.
  Print bag.
  intros. destruct bg.
  - simpl. rewrite <- eqb_refl. reflexivity.
  - assert (n=num\/  n <> num).
    omega.
    destruct H.
    rewrite H.
    simpl. rewrite <- eqb_refl. simpl. omega.
    simpl. rewrite <- eqb_refl.
    intuition.
    Show Proof.
 Qed.

有时间再做修改吧。

Reasoning About Lists.

Consider whether match the param can be sustituted into the definition.

The easiest situation as app's def is:

1
2
3
4
5
6
7
app =
fix app (l1 l2 : natlist) {struct l1} : natlist :=
  match l1 with
  | [ ] => l2
  | h :: t => h :: app t l2
  end
     : natlist -> natlist -> natlist
1
2
3
Theorem nil_app : forall l : natlist,
  [] ++ l = l.
Proof. reflexivity. Qed.

Sometimes helpful to perform case analysis.

1
2
3
4
5
6
7
8
Theorem tl_length_pred : forall l:natlist,
  pred (length l) = length (tl l).
Proof.
  intros l. destruct l as [| n l'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons n l' *)
    reflexivity.  Qed.

Induction on Lists

Just like Induction on nat is usually from O, Lists usually from nil.

What if you forget the theorem name but only knows its basic form.

Use Search

1
2
3
4
5
6
7
8
9
10
11
12
13
Search rev.

(** Or say you've forgotten the name of the theorem showing that plus
    is commutative.  You can use a pattern to search for all theorems
    involving the equality of two additions. *)

Search (_ + _ = _ + _).

(** You'll see a lot of results there, nearly all of them from the
    standard library.  To restrict the results, you can search inside
    a particular module: *)

Search (_ + _ = _ + _) inside Induction.

More useful param with search pattern.

1
Search (?x + ?y = ?y + ?x).

List Exercises

Refer to my github repo.

Like plus_n_Sm , lemma leb_n_Sn might be helpful in the next exercise.

Leave the bag_count_sum (3 stars) and rev_injective (4 stars).

About if else, we could use [destruct] tactics to analysis different cases like this.

1
2
3
4
5
6
7
8
9
10
11
12
13
Theorem bag_count_sum : forall(b1 b2: bag) (n : nat),
    count n (sum b1 b2) = (count n b1) + (count n b2).
Proof.
  intros.
  induction b1.
  - simpl. reflexivity.
  - simpl. rewrite -> IHb1.
    (* use case_eqn or destruct *)
    destruct (n0 =? n) as []eqn:?.
    (* case_eq (n0 =? n). *)
    + simpl. reflexivity.
    + reflexivity. 
Qed.

Paritial Maps

How data structures can be defined in Coq.