「SF-LC」1 Basics

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.

The .v code is a gorgeous example of literal programming and the compiled .html website 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

Custom Notation

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).

can go pretty far with unicode char…

making things infix

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 though

Data Constructor with arguments

there are 2 ways to define them:

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

Inductive nybble : Type :=
  | bits (b0 b1 b2 b3 : bit).

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.

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

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

N.B. the n0 and n1 are sub-terms of n where n = S (S _).

So we have to make the sub-structure explicit to indicate the structure is obviously shrinking:

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:

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

Proof by Case Analysis

Theorem plus_1_neq_0_firsttry : ∀n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n.
  simpl. (* does nothing! *)
Abort.

simpl. does nothing since both + and =? have 2 cases.

so we have to destruct n as 2 cases: nullary O and unary S n'.

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

• the intro pattern as [ |n'] name new bindings.
• eqn:E annonate the destructed eqn (equation?) as E in the premises of proofs. It could be elided if not explicitly used, but useful to keep for the sake of documentation as well.

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 simply write as [|] or as []. In fact. Any as clause could be ommited and Coq will fill in random var name auto-magically.

A small caveat on intro

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.

Qed

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

• Next
  「SF-LC」2 Induction