This Easter I set myself a little challenge to learn a little bit of Coq – enough to construct a proof of a simple but useful theorem in computer arithmetic. Long-time readers of this blog will know that this is not my first outing with dependent types, though I’ve never used them in anger. Four years ago – also during the Easter break! – I read Stump‘s book on Agda and spent some time playing with proofs and programming, as I documented here.
This blog post documents some of the interesting things in Coq I observed over the last few days. I’ve decided to write the majority of this post in Coq itself, below, before finishing off with some concluding remarks. In this way, anyone really interested can step through the definitions and proofs themselves.
Require Import Coq.Program.Equality.
Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Arith.Peano_dec.
Inductive bv : nat -> Set :=
| nilbv : bv 0
| consbv : forall n : nat, bool -> bv n -> bv (S n).
Definition hdi {n : nat} (xs : bv (S n)) :=
match xs with
| consbv _ head _ => head
end.
Definition tli {n : nat} (xs : bv (S n)) :=
match xs with
| consbv _ _ tail => tail
end.
Definition carryfunc (a : bool) (b: bool) (c: bool) : bool :=
orb (orb (andb a b) (andb a c)) (andb b c).
Definition sumfunc (a : bool) (b : bool) (c : bool) : bool :=
xorb (xorb a b) c.
Fixpoint rcai {n : nat} (x : bv n) (y : bv n) (cin : bool) : (bool * bv n) :=
match x in bv n return bv n -> ( bool * bv n ) with
| nilbv => fun _ => (cin, nilbv)
| consbv n1 xh xt => fun y1 =>
let (cout, sumout) := rcai xt (tli y1) (carryfunc cin xh (hdi y1)) in
(cout, consbv n1 (sumfunc cin xh (hdi y1)) sumout)
end y.
Definition moduloadder {n : nat} (x : bv n) (y : bv n) : (bv n) :=
snd (rcai x y false).
Infix “+” := moduloadder.
Fixpoint neg {n : nat} (x : bv n) : (bv n) :=
match x with
| nilbv => nilbv
| consbv n1 xh xt => consbv n1 (negb xh) (neg xt)
end.
Fixpoint bvzero {n : nat} : (bv n) :=
match n with
| O => nilbv
| (S n1) => consbv n1 false bvzero
end.
Definition bvone {n : nat} :=
consbv n true bvzero.
Definition addinv {n : nat} (x : bv (S n)) : (bv (S n)) :=
neg(x) + bvone.
Definition modulosub {n : nat} (x : bv (S n)) (y : bv (S n)) :=
x + (addinv y).
Infix “-” := modulosub.
Fixpoint ones {n : nat} : (bv n) :=
match n with
| O => nilbv
| S n1 => consbv n1 true ones
end.
Lemma invertzeros : forall {n : nat} (x : bv n),
x = bvzero -> neg x = ones.
Proof.
intros n x H.
induction n.
dependent destruction x.
auto.
dependent destruction x.
simpl.
f_equal.
simpl bvzero in H.
inversion H.
reflexivity.
simpl bvzero in H.
inversion H.
apply inj_pair2_eq_dec in H2.
2: apply eq_nat_dec.
apply IHn.
apply H2.
Qed.
Lemma rcai_zero: forall (n : nat) (x : bv n),
rcai x bvzero false = (false, x).
Proof.
intros n x.
induction n.
dependent destruction x.
auto.
dependent destruction x.
simpl bvzero.
simpl rcai.
destruct b.
unfold sumfunc. simpl.
unfold carryfunc. simpl.
destruct (rcai x bvzero false) eqn: H.
f_equal.
rewrite IHn in H.
inversion H.
reflexivity.
rewrite IHn in H.
inversion H.
f_equal.
unfold sumfunc. simpl.
unfold carryfunc. simpl.
destruct (rcai x bvzero false) eqn: H.
f_equal.
rewrite IHn in H.
inversion H.
reflexivity.
rewrite IHn in H.
inversion H.
f_equal.
Qed.
Lemma allones: forall {n : nat}, @addinv n bvone = ones.
Proof.
intros n.
induction n.
auto.
simpl.
unfold bvone.
unfold addinv.
simpl.
unfold bvone.
unfold “+”.
simpl.
unfold carryfunc.
simpl.
unfold sumfunc.
simpl.
destruct (rcai (neg bvzero) bvzero false) eqn: H.
simpl.
f_equal.
f_equal.
rewrite rcai_zero in H.
inversion H.
apply invertzeros.
reflexivity.
Qed.
Lemma increment_with_carry : forall (n : nat) (x : bv (S n)),
x + bvone = snd (rcai x bvzero true).
Proof.
intros n x.
dependent destruction x.
simpl bvzero.
simpl rcai.
unfold bvone.
unfold “+”.
simpl rcai.
destruct b.
unfold carryfunc.
simpl.
unfold sumfunc.
simpl.
reflexivity.
unfold carryfunc.
simpl.
unfold sumfunc.
simpl.
reflexivity.
Qed.
Lemma rcai_ones_cin_identity : forall (n : nat) (x : bv n),
snd (rcai x ones true) = x.
Proof.
intros n x.
induction n.
dependent destruction x.
simpl.
reflexivity.
dependent destruction x.
simpl ones.
simpl rcai.
destruct b.
unfold carryfunc.
unfold sumfunc.
simpl.
destruct (rcai x ones true) eqn: H.
simpl.
f_equal.
apply (f_equal snd) in H.
simpl in H.
rewrite IHn in H.
auto.
unfold carryfunc.
unfold sumfunc.
simpl.
destruct (rcai x ones true) eqn: H.
simpl.
f_equal.
apply (f_equal snd) in H.
simpl in H.
rewrite IHn in H.
auto.
Qed.
Lemma main_helper : forall (n : nat) (x : bv (S n)),
neg (x + ones) = neg x + bvone.
Proof.
intros n x.
induction n.
dependent destruction x.
destruct b.
dependent destruction x.
auto.
dependent destruction x.
auto.
dependent destruction x.
simpl.
unfold bvone.
unfold “+”.
simpl rcai.
destruct b.
unfold carryfunc.
unfold sumfunc.
simpl.
rewrite rcai_zero.
destruct (rcai x (consbv n true ones) true) eqn: H.
simpl neg.
simpl snd.
f_equal.
f_equal.
apply (f_equal snd) in H.
simpl snd in H.
rewrite rcai_ones_cin_identity in H.
auto.
unfold carryfunc.
unfold sumfunc.
simpl.
destruct (rcai (neg x) (consbv n false bvzero)) eqn: H.
apply (f_equal snd) in H.
simpl snd in H.
rewrite <- increment_with_carry in H.
simpl snd.
destruct (rcai x (consbv n true ones) false) eqn: H1.
simpl snd.
simpl neg.
f_equal.
apply (f_equal snd) in H1.
simpl snd in H1.
rewrite <- H1.
rewrite <- H.
apply IHn.
Qed.
Theorem main_theorem: forall (n : nat) (x : bv (S n)),
neg x + bvone = neg (x – bvone).
Proof.
intros n x.
unfold “-“.
rewrite allones.
rewrite <- main_helper.
reflexivity.
Qed.
Some Lessons
So what have I learned from this experience, beyond a little bit of Coq? Firstly, it was fun. It was a nice way to spend a couple of days of my Easter holiday. I am not sure I would want to do it under time pressure, though, as it was also frustrating at times. If I ever wanted to use Coq in anger for my work, I would want to take a couple of months – or more – to really spend time with it.
On the positive side, Coq really forced me to think about foundations. What do I actually mean when I write
? Should I be thinking in
, in
, or in digits, and when? How should bitvector arithmetic behave on zero-sized bitvectors? (Oh, and I certainly did not expect to be digging out a proof of decidability of natural equality from Coq’s standard library to prove this theorem!) The negative side is the same: Coq really forced me to think about foundations. And I remain to be convinced that I want to do that when I’m not on Easter holiday and in a philosophical mood.
I loved the type system and the expression of theorems. I’m luke warm about the proof process. At least the way I wrote the proofs – which was probably intolerably amateur – it felt like someone could come along and change the tactics at some point and my proof would be broken. Maybe this is not true, but this is what it felt like. This was a different feeling to that I remember when playing with Agda four years ago, which felt like everything needed to be explicit but somehow felt more nailed down and permanent. In Agda, the proofs are written in the same language as the types and I enjoyed that, too. Both languages are based on dependent types, and so as – I understand – is Lean. My colleague Kevin Buzzard is a strong advocate of Lean. Perhaps that’s one for another Easter holiday!
Thinking about this proof from a hardware perspective – designing efficient bit-parallel arithmetic hardware – it is clear that we do not need to have proved the theorem for all n. Each bit slice occupies silicon area, and as this is a finite resource, it would be sufficient to have one proof for each feasible value of n. Of course, this makes things much easier to prove, even if it comes with much more baggage. I can fire up an SMT solver and prove the theorem completely automatically for a specific value of n. As an example, if you paste the code below into the Z3 prover (hosted at rise4fun), the solver will report unsat, i.e. there is provably no satisfying value of the variable x violating the theorem for n = 4.
(declare-fun x () (_ BitVec 4))
(assert (not (= (bvadd (bvneg x) #x1) (bvneg (bvadd x #xF)))))
(check-sat)
(exit)
There are pluses and minuses to this. On the plus side, the SMT query is fast and automatic. On the minus side, in addition to only being valid for n = 4, it gives me – and perhaps some future AI – none of the intuition as to why this theorem holds. When I read mathematics, the proofs are not incidental, they are core to the understanding of what I’m reading.
Will this also be true for future AI-driven EDA tools?
Notes
In case this is useful to anyone (or to me in the future): I got syntax highlighting playing well for Coq with WordPress.com by using coqdoc to generate HTML and CSS, then hacking at the CSS so that it didn’t affect the rest of my WordPress theme, pasting it into the WordPress.com CSS customiser, and putting the generated HTML in a WordPress.com HTML block. Take care to avoid the CSS class .comment, used by coqdoc for code comments but also used by WordPress for blog post comment formatting!
Thanks again to Yann Herklotz for help understanding let bindings in Coq.