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.
* A first datapath identity
* George A. Constantinides, 2/4/21
*
* This is an attempt to learn some basic Coq by proving a standard identity used in computer arithmetic,
* namely \bar{x} + 1 = \bar{x – 1}.
*
* This identity is useful because it allows Boolean operations to move through arithmetic operations.
*
* The code is for learning and teaching purposes only. It is not intended to be an efficient or elegant
* approach, nor is it intended to make best use of existing Coq libraries. On the contrary, I have often used
* many steps when one would do, so we can step through execution and see how it works.
*)
Require Import Coq.Program.Equality.
Require Import Coq.Logic.Eqdep_dec.
Require Import Coq.Arith.Peano_dec.
(* Create my own bitvector type. It has a length, passed as a nat, and consists of bools. *)
Inductive bv : nat -> Set :=
| nilbv : bv 0
| consbv : forall n : nat, bool -> bv n -> bv (S n).
(* Head and tail of a bitvector, with implicit length arguments *)
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.
(* The basic carry and sum functions of a Boolean full adder *)
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.
(*
* A ripple carry adder, with implicit length argument
* Note that this definition makes use of a trick known as the ‘convoy pattern’ [1]
* to get the dependent typing to work in a match clause. We use a ‘return’ clause
* to make the type of the match result be a function which is then applied to the unmatched
* argument. In this way the type system can understand that x and y have the same dependent type.
* Note also the use of Fixpoint for a recursive definition.
*)
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) (* an empty adder passes its carry in to its carry out *)
| 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.
(* We define addition modulo 2^n by throwing away the carry out, using snd, and then define an infix operator *)
Definition moduloadder {n : nat} (x : bv n) (y : bv n) : (bv n) :=
snd (rcai x y false).
Infix “+” := moduloadder.
(* Bitwise negation of a word *)
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.
(* The word-level constant zero made of n zeros *)
Fixpoint bvzero {n : nat} : (bv n) :=
match n with
| O => nilbv
| (S n1) => consbv n1 false bvzero
end.
(* The word-level constant one with n leading zeros *)
Definition bvone {n : nat} :=
consbv n true bvzero.
(* Additive inverse of a word, defined as ‘negate all the bits and add one’ *)
Definition addinv {n : nat} (x : bv (S n)) : (bv (S n)) :=
neg(x) + bvone.
(* Subtraction modulo 2^n is defined as addition with the additive inverse and given its own infix operator *)
Definition modulosub {n : nat} (x : bv (S n)) (y : bv (S n)) :=
x + (addinv y).
Infix “-” := modulosub.
(* a bit vector of just ones *)
Fixpoint ones {n : nat} : (bv n) :=
match n with
| O => nilbv
| S n1 => consbv n1 true ones
end.
(* OK, now we have some definitions, let’s prove some theorems! *)
(* Our first lemma (‘Lemma’ versus ‘Theorem’ has no language significance in Coq) says that inverting a
* bitvector of ones gives us a bitvector of zeros.
* There’s a couple of interesting points to note even in this simple proof by induction:
* 1. I had to use ‘dependent destruction’,
* which is defined in the Coq.Program.Equality library, to get the destruction of variable x to take into account
* the length of the bitvector.
* 2. The second use of inversion here didn’t get me what I wanted / expected, again due to dependent typing, for
* reasons I found explained in [2]. The solution was to use a theorem inj_pair_eq_dec, defined in
* Coq.Logic.Eqdep_dec. This left me needing to prove that equality on the naturals is decidable. Thankfully,
* Coq.Arith.Peano_dec has done that.
*)
Lemma invertzeros : forall {n : nat} (x : bv n),
x = bvzero -> neg x = ones.
Proof.
intros n x H.
induction n.
dependent destruction x.
auto. (* base case proved *)
dependent destruction x.
simpl.
f_equal.
simpl bvzero in H.
inversion H.
reflexivity.
simpl bvzero in H.
inversion H. (* inversion with dependent type starts here… *)
apply inj_pair2_eq_dec in H2. (* goes via this theorem *)
2: apply eq_nat_dec. (* and completes via a proof of decidability of equality *)
apply IHn.
apply H2.
Qed.
(*
* The next lemma says that if you fix one input to a ripple carry adder to zero and feed in the carry-in as zero
* too, then the carry out will not be asserted and the sum will just equal the fixed input.
* I proved this by induction, reasoning by case on the possible Boolean values of the LSB.
* The wrinkle to notice here is that I didn’t know how to deal with a ‘let’ clause, but thanks to Yann Herklotz
* (https://yannherklotz.com) who came to my aid by explaining that a ‘let’ is syntactic sugar for a match.
*)
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. (* base case proved *)
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. (* The trick Yann taught me *)
f_equal.
rewrite IHn in H.
inversion H.
reflexivity.
rewrite IHn in H.
inversion H.
f_equal.
Qed.
(*
* The next lemma proves that -1 is a vector of ones
* One thing to note here is that I needed to explicitly supply the implicit argument n to addinv using @.
*)
Lemma allones: forall {n : nat}, @addinv n bvone = ones.
Proof.
intros n.
induction n.
auto. (* base case proved *)
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.
(*
* This lemma captures the fact that one way you can add one to a bitvector using a ripple carry adder is
* to add zero and assert the carry in port.
*)
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.
(* first peel off the LSB from the two operands *)
simpl bvzero.
simpl rcai.
unfold bvone.
unfold “+”.
simpl rcai.
(* now case split by the LSB of x to show the same thing *)
destruct b.
unfold carryfunc.
simpl.
unfold sumfunc.
simpl.
reflexivity.
unfold carryfunc.
simpl.
unfold sumfunc.
simpl.
reflexivity.
Qed.
(* This lemma says that if you add a vector of ones to a value x using a ripple carry adder, while asserting the
* carry in port, then the sum result will just be x. Of course this is because -1 + 1 = 0, though I didn’t prove
* it that way.
* A neat trick I found to use in this proof is to use the tactic ‘apply (f_equal snd)’ on one of the hypotheses
* in order to isolate the sum component in the tuple produced by the ripple carry function rcai.
*)
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.
(* case analysis *)
destruct b.
unfold carryfunc.
unfold sumfunc.
simpl.
destruct (rcai x ones true) eqn: H.
simpl.
f_equal.
apply (f_equal snd) in H. (* a neat trick *)
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.
(*
* This lemma is actually the main content of what we’re trying to prove, just not wrapped up in
* very readable form yet.
* Note the use of ‘rewrite <-‘ to use an existing lemma to rewrite a term from the RHS of the equality
* in the lemma to the LHS. Without the ‘<-‘ it would do it the other way round.
*)
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. (* base case proved *)
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.
(*
* References
* [1] http://adam.chlipala.net/cpdt/html/MoreDep.html
* [2] https://stackoverflow.com/questions/24720137/inversion-produces-unexpected-existt-in-coq
*)
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 
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.
Thinking 