The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Friday, January 30, 2015 03:05:51 PM Adam Chlipala wrote:
> A very different tack would be to show a highly automated proof of a
> moderately complex program, like some of the examples distributed with
> Bedrock <http://plv.csail.mit.edu/bedrock/>.
> 
> On 01/30/2015 03:01 PM, Eric Mullen wrote:
> > If you wanted to give a 10 minute demo to show off how cool Coq was,
> > what example would you use?
> > 
> > Specifically, if you were talking to a bunch of undergraduates in
> > Computer Science, and you had 10 minutes to convince them that Coq was
> > an awesome research tool, what would be your go to example?
> > 
> > Ideas so far have been:
> >  * Implementing slow and fast Fibonacci functions, and proving they
> > 
> > calculate the same thing
> > 
> >  * Proving that the identity function and the Fibonacci function are
> > 
> > both monotonic
> > 
> > I'm leaning towards the second due to its simplicity, but I would very
> > much appreciate small examples which illustrate how cool it is to
> > write code and prove properties about it.
> > 
> > Thanks much,
> > Eric Mullen

Or, along similar lines, you could go with a more mathematically oriented 
proof, like maybe this proof that binary addition of positive numbers is 
associative:

Inductive positive : Set :=
| pos_1
| pos_double (p : positive)
| pos_double_p1 (p : positive).

Delimit Scope positive_scope with positive.
Open Scope positive_scope.

Notation "1" := pos_1 : positive_scope.
Notation "p ~0" := (pos_double p) (left associativity, at level 6,
  format "p ~0")
  : positive_scope.
Notation "p ~1" := (pos_double_p1 p) (left associativity, at level 6,
  format "p ~1")
  : positive_scope.

Fixpoint Psucc (p : positive) : positive :=
match p with
| 1 => 1~0
| p'~0 => p'~1
| p'~1 => (Psucc p')~0
end.

Fixpoint Pplus (p q : positive) : positive :=
match p, q with
| 1, _ => Psucc q
| _, 1 => Psucc p
| p'~0, q'~0 => (Pplus p' q')~0
| p'~1, q'~0 => (Pplus p' q')~1
| p'~0, q'~1 => (Pplus p' q')~1
| p'~1, q'~1 => (Pplus_with_carry p' q')~0
end
with
Pplus_with_carry (p q : positive) : positive :=
match p, q with
| 1, _ => Psucc (Psucc q)
| _, 1 => Psucc (Psucc p)
| p'~0, q'~0 => (Pplus p' q')~1
| p'~1, q'~0 => (Pplus_with_carry p' q')~0
| p'~0, q'~1 => (Pplus_with_carry p' q')~0
| p'~1, q'~1 => (Pplus_with_carry p' q')~1
end.

Lemma Pplus_with_carry_eqn : forall p q : positive,
  Pplus_with_carry p q = Psucc (Pplus p q).
Proof.
induction p; destruct q; simpl; congruence.
Qed.

Lemma Pplus_succ_l : forall p q : positive,
  Pplus (Psucc p) q = Psucc (Pplus p q).
Proof.
induction p; destruct q; simpl;
repeat rewrite Pplus_with_carry_eqn; congruence.
Qed.

Lemma Pplus_1_r : forall p : positive, Pplus p 1 = Psucc p.
Proof.
destruct p; reflexivity.
Qed.

Lemma Pplus_succ_r : forall p q : positive,
  Pplus p (Psucc q) = Psucc (Pplus p q).
Proof.
induction p; destruct q; simpl;
repeat (rewrite Pplus_with_carry_eqn || rewrite Pplus_1_r);
congruence.
Qed.

Lemma Pplus_assoc : forall p q r : positive,
  Pplus p (Pplus q r) = Pplus (Pplus p q) r.
Proof.
induction p; destruct q, r; simpl;
repeat (rewrite Pplus_with_carry_eqn ||
        rewrite Pplus_succ_l || rewrite Pplus_succ_r ||
        rewrite Pplus_1_r); congruence.
Qed.

The neat thing here is that in the Pplus_assoc proof, there are 27 different 
cases to consider.  However, the proof script just says "by rewriting using 
the previous results, each of these 27 cases is easy to prove".

(OK, checking the original message again, I guess this example would possibly 
be more suitable for mathematics undergraduates than for CS undergraduates, 
though.)
-- 
Daniel Schepler