These series of notes combined

- My notes on reading
Software Foundationand (if any) watching onCoq intensive.- Gotchas from my independent studies and discussion within
Prof.Fluet’s class.

The

`.v`

code is a gorgeous example ofliteral programmingand the compiled`.html`

website is full-fledged. So this note is intended to be NOT self-contained and only focus on things I found essential or interesting.

This note is intended to be very personal and potentially mix English with Chinese (You can Lol) So yeah. Don’t expect it to be well organized and well written. I posted it on blog mainly for my own references purpose.

The quotes could either come from the book or saying from someone (even including me).

## Data and Functions

### Custom Notation

1
2

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).

can go pretty far with unicode char…

making things *infix*

1
2
3
4
5
6
7
8
9

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.

why `40`

`50`

? Making sure there are still *rooms* for priority in between…

no known PL using real number for priority though

### Data Constructor with arguments

there are 2 ways to define them:

1
2
3
4
5

Inductive color : Type :=
| black
| white
| primary (p : rgb). (* ADT, need to name arg, useful in proof *)
| primary : rgb -> color. (* GADT style, dependent type *)

### Syntax for arguments having the same type

As a notational convenience, if two or more arguments have the same type, they can be written together

1
2

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

1
2

Fixpoint mult (n m : nat) : nat :=
Fixpoint plus (n : nat) (m : nat) : nat :=

`Fixpoint`

and Structrual Recursion

This requirement is a fundamental feature of Coq’s design: In particular, it guarantees that every function that can be defined in Coq will terminate on all inputs.

However, Coq’s “decreasing analysis” is not very sophisticated. E.g.

1
2
3
4
5
6

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

will result in a error that basically complains *“this structure is not shrinking”*.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

Error:
Recursive definition of evenb is ill-formed.
evenb : nat -> bool
n : nat
n0 : nat
n1 : nat
Recursive call to evenb has principal argument equal to
"Nat.pred (Nat.pred n)" instead of one of the following variables: "n0" "n1".
Recursive definition is:
"fun n : nat =>
match n with
| 0 => true
| 1 => false
| S (S _) => evenb (Nat.pred (Nat.pred n))
end".

N.B. the `n0`

and `n1`

are sub-terms of `n`

where `n = S (S _)`

.

So we have to make the sub-structure explicit to indicate the structure is obviously shrinking:

1
2
3
4
5
6

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

Now Coq will know this `Fixpoint`

is performing a structural recursion over the 1st recursion and it guarantees to be terminated since the structure is decreasing:

1
2

evenb is defined
evenb is recursively defined (decreasing on 1st argument)

## Proof by Case Analysis

1
2
3
4
5
6

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

`simpl.`

does nothing since both `+`

and `=?`

have 2 cases.

so we have to `destruct`

`n`

as 2 cases: nullary `O`

and unary `S n'`

.

1

intros n. destruct n as [ (* O *) | (* S *) n'] eqn:E.

- the
*intro pattern*`as [ |n']`

name new bindings. `eqn:E`

annonate the destructed`eqn`

(equation?) as`E`

in the premises of proofs. It could be elided if not explicitly used, but useful to keep for the sake of documentation as well.

1
2
3
4
5
6
7
8
9
10
11
12
13
14

subgoal 1
n : nat
E : n = 0 (* case 1, n is [O] a.k.a. [0] *)
============================
(0 + 1 =? 0) = false
subgoal 2
n, n' : nat
E : n = S n' (* case 2, n is [S n'] *)
============================
(S n' + 1 =? 0) = false

If there is no need to specify any names, we could omit `as`

clause or simply write `as [|]`

or `as []`

.
In fact. Any `as`

clause could be ommited and Coq will fill in random var name auto-magically.

### A small caveat on `intro`

1

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

By doing this, name `y`

is shadowed. It’d usually better to use, say `y'`

for this purpose.

`Qed`

standing for Latin words *“Quod Erat Demonstrandum”*…meaning “that which was to be demonstrated”.