These series of notes combined
- My notes on reading Software Foundation and (if any) watching on Coq intensive.
- Gotchas from my independent studies and discussion within Prof.Fluet’s class.
.vcode is a gorgeous example of literal programming and the compiled
.htmlwebsite 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
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.
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".
n1 are sub-terms of
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
=? have 2 cases.
so we have to
n as 2 cases: nullary
O and unary
1 intros n. destruct n as [ (* O *) | (* S *) n'] eqn:E.
- the intro pattern
as [ |n']name new bindings.
eqn:Eannonate the destructed
Ein 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 + 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
In fact. Any
as clause could be ommited and Coq will fill in random var name auto-magically.
A small caveat on
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.
standing for Latin words “Quod Erat Demonstrandum”…meaning “that which was to be demonstrated”.