combining noting of

me reading,mtf lecturesand (possible)coq intensive watchingOnly notinginterestingthings. The`.v`

code and book can be seen asliteral programming

## 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 tho

## 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, little dependent type *)

## Notation for arguments with 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).

meaning are having type `bit`

.

1
2

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

meaning both `n m`

having type `nat`

.

## Terminated Fixpoint

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 kinda “non-shrinking” error:

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".

the `n0`

and `n1`

are sub-terms of `n`

where `n = S (S _)`

.

So we have to be explicit on sub-structure to indicate it’s 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.

Coq will know what is decreasing:

1
2

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

## Case Analysis

1

(n + 1) =? 0 = false

can not be `simpl.`

since both `+`

and `=?`

involve `n`

which has 2 cases.

1

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

so we have to `destruct`

`n`

as 2 cases, nullary `O`

and unary `S n'`

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

give argument names.

`eqn:E`

annonate the destructed `eqn`

(equation?) as `E`

in the premises.
could be elided if not explicitly used, 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 written `as [|]`

or `as []`

.
In fact. Any `as`

clause could be ommited and Coq will fill in random var name automagically.

## More on Intro Pattern

A Bad example, which reuses name `y`

…

1

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

`Qed`

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