Basic Syntax

• Nothing but functions and their types are built-in in Coq; everything else is defined
• Inductive command is used for declaring data types

Comments

• Wrap comments inside (* ... *)
• can span multiple lines

(* single line *)

(* multi-line
   comment *)

Inductive

Use Inductive to declare a type:

Inductive bool := true | false.

It is actually one of the simplest possible inductive definitions, with only base cases, and no inductive cases. This declaration states explicitly that there are exactly two elements in type bool: the distinct constants true and false, called the constructors of type bool.

More interesting examples

Inductive rgb : Type :=
  | red
  | green
  | blue.

Case with arguments

Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

Inductive bit : Type :=
  | B0
  | B1.

(* this is a tuple of 4 bits *)
Inductive nybble : Type :=
  | bits (b0 b1 b2 b3 : bit).

Constructor expressions are formed by applying a constructor to zero or more other constructors or constructor expressions, e.g.

• primary red
• red primary
• red true
• primary (primary primary)

Natural Numbers

• formalized by a type called nat
• constant O (capital "o" letter) represents zero
• S represents the successor
• Using base 10 works also

base-10	nat
0	O
1	(S O)
2	S (S 0)
3	S (S (S 0))
4	S (S (S (S O)))

Representation of numbers

(* short version *)
Inductive nat := O | S (n : nat).

(* equivalent *)
Inductive nat : Type :=
  | O
  | S (n : nat).

Modules

• You can create modules for purposes of organization and name reuse
• Definitions within a module will be references as moduleName.identifier

Module Playground.
  Definition b : rgb := blue.
End Playground.

Definition b : bool := true.

Check Playground.b : rgb.
Check b : bool.

Defining Functions

• Use Definition to define functions.
• Coq will do type inference → can omit return type, but including it improves readability
• In pattern matching, can use e.g. _ as wildcard

Boolean AND

Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | false => false
  | true => b2
  end.

Or write using conditional statement - can write conditional over any inductively defined type with two constructors - will return true if value matches first constructor and false otherwise

Definition andb (b1 b2 : bool) : bool := if b1 then b2 else false.

NOT

Definition negb (b:bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

OR

Definition orb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => true
  | false => b2
  end.

NAND

Definition nandb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | false => true
  | true => negb(b2)
  end.

Can match with multiple args, nest matches, and group contiguous arguments of the same type:

(* _ is wildcard match pattern *)
Definition andb' (b1 b2 : bool) : bool :=
  match b1, b2 with
  | true, true => true
  | _, _ => false
  end.

(* nested example *)
Definition andb3 (b1 b2 b3:bool) : bool :=
  match b1 with
  | false => false
  | true => match b2 with
        | true => b3
        | false => false
        end
  end.

Function with natural numbers

Definition f (n : nat) : nat := n + 1.

Predecessor function using nat

Definition pred (n : nat) : nat :=
  match n with
    | O => O
    | S n' => n'
  end.

Definition minustwo (n : nat) : nat :=
  match n with
    | O => O
    | S O => O
    | S (S n') => n'
  end.

Compute and Example

• How to use functions:
  1. Compute evaluates function for given args and displays the output
  2. Example similar to a unit test; make an assertion about the expected output
  3. Extract a program in another language such as OCaml

Use Compute to call the function:

Compute f 3.
(* f 3 : nat = 4 : nat *)

Use Example to check function returns expected value

Example test_f: f 3 = 4.  (* make some assertion *)
Proof. simpl. reflexivity. Qed. (* verify that is holds *)

Testing the OR function

Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.

Function with two arguments

Definition g (n m : nat) : nat := n + m * 2.


Compute g 2 3.
(* g 3 : nat -> nat = 8 : nat *)

Function that calls another function exactly twice

Definition repeat_twice (g : nat -> nat) : nat -> nat :=
    (* g (g x) is application of function g to an expression (g x)
    (g x) is application of function g to x *)
    fun x => g (g x).

Compute repeat_twice f 2.
(* = 4 : nat *)

Type Information

Use About or Print to display information

About andb.

(* outputs:
andb is not universe polymorphic
andb is transparent
Expands to: Constant math.andb
*)

Print andb.

(* outputs:
andb = fun b1 b2 : bool => if b1 then b2 else false
: bool -> bool -> bool
*)

Check prints the type of an expression.

• If the expression after Check is followed by a colon and a type, Coq will verify that the type of the expression matches the given type and halt with an error if not.
• Function types use arrows

Check andb. 

(* andb : bool -> bool -> bool *)

Check andb true. 

(* andb true: bool -> bool *)

Check andb true true. 

(* andb true true : bool *)

Check (S (S (S (S O)))). 

(* = 4 : nat *)

Fixpoint

• use Fixpoint for recursive operations on natural numbers e.g. addition or subtraction of arbitrary numbers
• computation must be guaranteed to terminate (!) → Termination is obvious when the recursive calls happen only on "syntactically smaller arguments"

Addition

Fixpoint addn n m :=
    match n with
    | 0 => m
    | S p => S (addn p m)
    end.

Compute addn 3 4.
(* = 7 : nat*)

Subtraction

Fixpoint minus (n m:nat) : nat :=
  match n, m with
  | O , _ => O
  | S _ , O => n
  | S n', S m' => minus n' m'
  end.

Multiplication

Fixpoint mult (n m : nat) : nat :=
  match n with
    | O => O
    | S n' => plus m (mult n' m)
  end.

Power

Fixpoint exp (base power : nat) : nat :=
  match power with
    | O => S O
    | S p => mult base (exp base p)
  end.

Check if number is even

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => evenb n'
  end.

Determine if arguments are equal

Fixpoint eqn m n :=
  match m, n with
  | 0,0 => true
  | S p, S q => eqn p q
  | _,_ => false
  end.

Inequality n \(\leq\) m

Tests whether first argument is less than or equal to its second argument

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
  end.

Notation & Infix

• Use Notation or Infix to create custom symbolic notations
• Notation is used to
  1. declare various kinds of notations/alias
  2. to specify their associativity
  3. and their precedence to the parsing engine of Coq.
• makes code easier to read and write
• associativity is one of:
  • left associativity
  • right associativity
  • no associativity
• precedence levels
  • 0 to 100
  • lower level binds more than a higher level
• each notation symbol als has notation scope
  • Coq tries to guess the scope from context
  • or can be set explicitly
• Infix is a shorthand for declaring notations for infix symbols
  • can also include associativity, level, and scope name

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
Notation "m + n" := (addn m n) (at level 50, left associativity).
Notation "x == y" := (eqn x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70, no associativity) : nat_scope.


Infix "&&" := andb.
Infix "||" := orb.
Infix "/\" := and (at level 80, right associativity).

Locate & Search

• use Locate to lookup a definition
• use full expression — does not match substring

Locate "==" .
(* Notation "x == y" := (eqn x y) : nat_scope (default interpretation) *)`}

• use Search to lookup existing definitions
• supports wildcards
• also supports searching inside a module

Search rev.
Search (_ + _ = _ + _).
Search (_ + _ = _ + _) inside Induction.
Search (?x + ?y = ?y + ?x).

Options

• Use option when function may or may not return a value

Inductive natoption : Type :=
  | Some (n : nat)
  | None.

Example: eliminate option

Definition option_elim (d : nat) (o : natoption) : nat :=
match o with
  | Some n' => n'
  | None => d
end.

Polymorphic options

Inductive option (X:Type) : Type :=
  | Some (x : X)
  | None.
Arguments Some {X} _.
Arguments None {X}.