The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 30/01/15 21:01, Eric Mullen wrote:
> If you wanted to give a 10 minute demo to show off how cool Coq was, what
> example would you use?

Below is an example that I used several times with professional
engineers.  It consists in proving the correctness of a simple
arithmetic circuit (ripple-carry adder).  It assumes the audience
knows a bit about computer arithmetic and circuits.  You can get some
pretty interesting questions from the audience, e.g. "but can I make
sure my two input numbers have the same number of bits?" (dependent
types here we come!).

More advanced examples that I sometimes use:
- The Majority algorithm of Boyer and Moore
(http://www.cs.utexas.edu/users/moore/best-ideas/mjrty/index.html)
- Compilation of arithmetic expressions to a stack machine.

- Xavier Leroy

--------------------------------------------------

(** Tutorial 1: adder circuits. *)

Require Import Bool.   (** The library for booleans *)
Require Import List.   (** The library for lists *)
Require Import ZArith. (** The library for integer arithmetic (type Z) *)
Open Scope Z_scope.    (** Using the notations for type Z *)

(** The boolean equations for a full adder circuit:
      - 3 inputs: two bits A, B and a carry in
      - 2 outputs: one bit and a carry out.
*)

Definition adder_sum (A B Cin: bool) : bool :=
  xorb (xorb A B) Cin.

Definition adder_carry_out (A B Cin: bool) : bool :=
  orb (andb (xorb A B) Cin) (andb A B).

Definition adder (A B Cin: bool) : bool * bool :=
  (adder_sum A B Cin, adder_carry_out A B Cin).

(** The integer denoted by a single bit A. *)

Definition val_bit (A: bool) : Z :=
  if A then 1 else 0.

(** Checking that the full adder does compute the sum of its 3 inputs. *)

Theorem adder_correct:
  forall A B Cin,
  val_bit (adder_sum A B Cin) + val_bit (adder_carry_out A B Cin) * 2
  = val_bit A + val_bit B + val_bit Cin.
Proof.
  destruct A; destruct B; destruct Cin; auto.
Qed.

(** Composing full adders to sum vectors of bits. *)

Fixpoint ripple_carry_adder (A B: list bool) (Cin: bool) : list bool :=
  match A, B with
  | A1 :: A', B1 :: B' =>
      adder_sum A1 B1 Cin ::
      ripple_carry_adder A' B' (adder_carry_out A1 B1 Cin)
  | _, _ =>
      Cin :: nil
  end.

(** The integer denoted by a vector of bits A.
    Least-significant bit comes first. *)

Fixpoint val_bits (A: list bool) : Z :=
  match A with
  | nil => 0
  | A1 :: A' => val_bit A1 + val_bits A' * 2
  end.

(** Checking that the ripple carry adder does compute the sum of its inputs. 
*)

Theorem ripple_carry_adder_correct:
  forall A B Cin,
  length A = length B ->
  val_bits (ripple_carry_adder A B Cin) =
  val_bits A + val_bits B + val_bit Cin.
Proof.
  induction A; destruct B; simpl; intros.
- (* A and B are nil: base case *)
  omega.
- (* A is nil, B is not: contradicts the hypothesis on lengths *)
  exfalso. omega.
- (* B is nil, A is not: contradiction *)
  exfalso. omega.
- (* A and B are not nil: inductive case *)
  rewrite IHA.
  specialize (adder_correct a b Cin); intros.
  omega.
  omega.
Qed.

(*Print ripple_carry_adder_correct.*)