Coq Reference

January 23, 2021

Learn x in y style

(* This is a comment *)

(* Inductive type, enumerated finite *)
(* Each item called a constructor *)
Inductive day : Type :=
  | monday
  | tuesday. 
(* lots of periods needed, most things need an 'end' *)

(* This is a function type, has a match structure *)
(* Note that pattern matching happens in order *)
Definition next_weekday (d:day) : day :=
  match d with
  | monday => tuesday
  | tuesday => monday
end.

(* This runs a function *)
Compute (next_weekday monday). 
(* Output should be tuesday: day*)

(* Example is an assertion/unit test (silent success) *)
Example test_next_weekday:
  (next_weekday (next_weekday tuesday)) = tuesday.
(* This runs the unit test, only throws if error happens. One per Example *)
(* simpl = simplification *)
(* reflexivity = check equality *)
Proof. simpl. reflexivity. Qed.

Inductive bool : Type :=
  | true
  | false.

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

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

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

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

(* Notation multi-args *)
(* (n m : nat ) is the same as (n: nat) (m: nat) *)
(* can also match two expressions with comma *)
(* match n, m with *)

(* Writing aliases *)
Notation "x || y" := (orb x y).
(* Using above alias *)
Example test_orb5: false || true || false = true.
Proof. simpl. reflexivity. Qed.

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

Example test_nandb1: (nandb true false) = true.
Proof. simpl. reflexivity. Qed.

Example test_nandb2: (nandb true true) = false.
Proof. simpl. reflexivity. Qed.

Example test_nandb3: (nandb false false) = true.
Proof. simpl. reflexivity. Qed.

Example test_nandb4: (nandb false true) = true.
Proof. simpl. reflexivity. Qed.

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

Example test_andb31: (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.

Example test_andb32: (andb3 true true false) = false.
Proof. simpl. reflexivity. Qed.
(* Prints out the type *)
Check true. 
(* should give bool *)
Check nandb.
(* bool -> bool -> bool *)

(* Type within type *)

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


(* Takes an argument *)
Inductive color: Type :=
  | black
  | white
  | primary (p: rgb).

(* primary colors are only constructors that are members of both color and rgb type *)

(* _ is a wildcard, order matters so red first *)
Definition isred (c : color) : bool :=
  match c with
  | black => false
  | white => false
  | primary red => true
  | primary _ => false
end.

(* Module system means scope only within here *)
Module Playground.
  Definition b : rgb := blue.
End Playground.

Definition b: bool := true.
Check b.
Check Playground.b.

Module TuplePlayground.
Inductive bit : Type :=
  | B0
  | B1.

(* bits here acts as a constructor *)
Inductive nybble : Type :=
  | bits (b0 b1 b2 b3 : bit).

Check (bits B1 B0 B1 B0).
End TuplePlayground.

Module NatPlayground.
(* Example of an infinite type *)
(* O = 0, S O = 1, S (S O) = 2  This is actually what it represents *)
(* S is a constructor for successor, n is the input of nat *)
(* S is not a function! *)
Inductive nat : Type :=
  | O
  | S (n : nat).
End NatPlayground.

Module NatPlayground2.
(* Fixpoint if Definition has recursion *)
Fixpoint plus (n: nat) (m: nat) : nat :=
  match n with
    | O => m
    | S n' => S (plus n' m)
  end.

Compute (plus 3 2).
(* S (plus (S (S O)) (S (S O))) = 5*)
End NatPlayground2.