# 「软件基础 - LF」 1. Basics (FP in Coq)

Posted by Hux on January 1, 2019

combining noting of me reading, mtf lectures and (possible) coq intensive watching Only noting interesting things. The .v code 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 + 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” 