Boolean function example in Coq, taken from Boolean section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html

booleans.v

(* taken from https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Inductive bool : Type :=
  | true  : bool
  | false : bool.

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

Example test_negb_true : (negb true) = false.
Proof. simpl. reflexivity. Qed.

Example test_negb_false : (negb false) = true.
Proof. simpl. reflexivity. Qed.

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

Example test_andb_true_true : (andb true true) = true.
Proof. simpl. reflexivity. Qed.

Example test_andb_true_false : (andb true false) = false.
Proof. simpl. reflexivity. Qed.

Example tet_andb_false_true : (andb false true) = false.
Proof. simpl. reflexivity. Qed.

Example test_andb_false_false : (andb false false) = false.
Proof. simpl. reflexivity. Qed.

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

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

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

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

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

Infix "&&" := andb.
Infix "||" := orb.

Example test_andb_infix : true && true && false = false.
Proof. simpl. reflexivity. Qed.

Example test_orb_infix : false || false || true = true.
Proof. simpl. reflexivity. Qed.

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

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

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

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

Example test_nandb_true_true : (nandb true true) = false.
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_andb3_true_true_true : (andb3 true true true) = true.
Proof. simpl. reflexivity. Qed.

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

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

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