Basic

Intro

Functional style and the sense of "functional" in "functional programming"

• Pure without side effects, then all we need to undersatand about it is how it maps inputs to outputs(compute a mathematical objects).
  • programs <-> mathematical objects
  • well behavior <-> correct proofs

Data and Functions

New Types from Old

Apart from enumerate types (their definitions explicitly enumerate a finite set of elements called constructors).cunstructors是构造元素(like word)，constructor expressions是构造表示(like sentence)，用来描述 constructor 到零个或者多个 constructor 或 constructor expressions 的映射。

Inductive 定义包含了一组 constructor expressions 并赋予名字。The definitions say which constructor expressions belong to the specific sets(like [rgb]).

• Start with an infinite set of constructors. (E.g. [red] [primary])
• Constructor expressions are formed by applying constructors to zero or more other constructors or constructor. (E.g. [red] that is zero [primary red] apply [primary] to another constructor [red] 1 param)

Inductive rgb : Type :=
  | red
  | green
  | blue.

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

Definition define functions just as we did for the enumerate types.

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

Modules

Aid in organizing large developments. Like name space. Definitions are referred to by names like [X.foo] instead of just [foo]. Limit the scope of definitions and reuse names.

Module Playground.
  Definition b : rgb := blue.
End Playground.

Definition b : bool := true.

Check Playground.b : rgb.
Check b : bool.

Tuples

Multiple parameters canbe used to create a tuple type.

Inductive bit : Type :=
  | B0
  | B1.

Inductive nybble : Type :=
  | bits (b0 b1 b2 b3 : bit).

Check (bits B1 B0 B1 B0)
    : nybble.

The [bits] constructor ([bits] is a constructor and bits ( have 4 bits) is a constructor is a constructor expression) acts as a wrapper for its contents.

match x withpattern-matching

Numbers

Neither base 10 or base 2. We wish here to choose a representation that makes proofs simpler (even simpler than binary), so we use base 1, namely unary.

To represent unary numbers with a Coq datatype, we use two constructors. Here is the complete datatype definition.

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

Unary here is like counting the infinite numbers, but give infinite (only two) constructors expressions or inductive rules to describe it, which makes proofs simpler.

We've done so far is just to define a representation of numbers: a way of writing them down. The names [O] and [S] are arnotrary without any special meaning. Actually we could write essentially the same definition this way:

Inductive nat' : Type :=
  | stop
  | tick (foo : nat').

[nat] compare to [rgb] and [color]（理解之前的rgb拆开的原因，这样控制 primary 生成的链有限）。

Coq provides a tiny bit of built-in magic for parsing and printing nat (unary base 1 <->decimal base 10):

• Ordinary decimal numerals canbe used as an alternative to the "unary" notation.
• Coq prints numbers in decimal form by default.

For convinience.

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

Definition minustwo (n : nat) : nat :=
  match n with
    | O => O
    | S O => O
    | S (S n') => n'
  end.

Compute (minustwo 4).
(* Equal to minustwo S(S(S(S(O)))) *)
Compute (minustwo (S(S(S(S O))))).
(* ===> 2 : nat *)

Pattern matching with recursion. Introoduced with the keyword [Fixpoint] instead of [Definition].

Proof by Simplification

The proofs of examples claimed before were always the same: use [simpl] [reflexivity] to check that both sides contain identical values.

[reflexivity] is more powerful than I have expected. It automatically perfoem some simplification.

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

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

• [Theorem] instead of [Example] (for style)
• [forall n:nat] talks all nat.
• [intros] from the quantifier in the goal to a context of current assumptions.

A tactics is a command that is used between [Proof] and [Qed] to guide the process.

Proof by Rewriting

Without universal claim about all nat, talk about a specialized property only holds when [n = m].

Theorem plus_id_example : forall n m:nat,
  n = m ->
  n + n = m + m.

After [intros] we get [n] [m] are arbitrary numbers. We can't just use simplification to prove (absolutely imposibble) but need to use the hypothesis.

Proof.
  (* move both quantifiers into the context: *)
  intros n m.
  (* move the hypothesis into the context: *)
  intros H.
  (* rewrite the goal using the hypothesis: *)
  rewrite -> H.
  reflexivity.  Qed.

With [rewrite <- / ->] tactics we can use previously proved theorems or hypothesis to rewrite our goal.

Proof by Case Analysis

Not everything can be proved by simple calculation and rewriting.

Block like this.

Theorem plus_1_neq_0_firsttry : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n.
  simpl.  (* does nothing! *)
Abort.

Reason: [n] and [n + 1] (Notation of plus n 1) lie on each side of [=?]. [equ] [plus] begins by performing match on first argument. Both unknown number [n]! Match fail.

The reason for this is that the definitions of both [eqb] and [+] begin by performing a [match] on their first argument. But here, the first argument to [+] is the unknown number [n] and the argument to [eqb] is the compound expression [n + 1]; neither can be simplified.

Tells Coq to consider seprately, the cases where [n = O] and where [n = S n'] is called destruct.

Exercise

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b c.
  destruct b eqn:Eb.
  {
    simpl.
    intros H.
    rewrite <- H.
    reflexivity.
  }
  {
    simpl.
    destruct c eqn:Ec.
    - simpl. reflexivity.
    - intros H. rewrite -> H. reflexivity.
  }
Qed.

If there are no constructor arguments that need names, we can just write [[]] to get the case analysis.

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

Fixpoints and Structural Recursion (Optional)

decreasing and structural recursion

Coq demands that some argument of every [Fixpoint] definition is "decreasing".

Tests

Not to intros. at the very begining.

All passed. 14/14.