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
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 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
1 2 Fixpoint mult (n m : nat) : nat := Fixpoint plus (n : nat) (m : nat) : nat :=
n m having type
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".
n1 are sub-terms of
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)
1 (n + 1) =? 0 = false
can not be
simpl. since both
n which has 2 cases.
1 intros n. destruct n as [ (* O *) | (* S *) n'] eqn:E.
so we have to
n as 2 cases, nullary
O and unary
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 + 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
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
1 intros x y. destruct y as [|y] eqn:E.
standing for Latin words “Quod Erat Demonstrandum”… meaning “that which was to be demonstrated”