combining noting of me reading, mtf lectures and (possible) coq intensive watching Only noting interesting things. The
.vcode and book can be seen as literal 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”
