## (Dis)advantages of using Abstract Data Types in Proof Assistants

This blog post explains the advantages and disadvantages of using Abstract Data Types (ADTs, see TaPL Chapter 24) in a Proof Assistant. On the plus side, ADTs promote data representation independence, code reuse, and clean code extraction; but they also do not support fix/match syntax, have to expose derived operations, and prohibit computational reasoning.

### Represenation Independence

(*
Fixpoint add (n m : nat) : nat :=
match n with
| 0 => m
| S n' => S (add n' m)
end
*)

This implementation is unsatisfactory, as it exposes the data representation details of the nat datatype. For example, this implementation of add will not work with a more space efficient binary representation of natural numbers.

The standard solution to this problem is to hide the data representation using an ADT. ADTs can be implemented using either Modules (see), Sigma/Existential Types (see TaPL Chapter 24), Records (see), or Type Classes (see). In this blog post, we choose to implement ADTs in the Coq Proof Assistants using Type Classes.

Our ADT for natural numbers NatADT consists of: a type Nat whose representation is hidden, operations on the type (zero, succ, natRect), and equations that describe the operation’s behavior (natRectZero, natRectSucc).

The operation natRect is the eliminator for natural numbers. The equations describe the computational behavior of natRect.

Nat : Type;
zero : Nat;
succ : Nat -> Nat;
natRect : forall P, P zero -> (forall n, P n -> P (succ n)) -> forall n, P n;
natRectZero : forall P z s, natRect P z s zero = z;
natRectSucc : forall P z s n, natRect P z s (succ n) = s n (natRect P z s n)
}.

Given this ADT, we can now implement an add function that is independent of any particular implementation of the natural numbers (hurray).

Unfortunately, this also means that we have to implement the code in terms of the eliminator, and cannot use fix/match syntax (sigh). However, getting around this syntactic restriction would be trivial for eliminator based languages like Lean.

Definition add {NatADT} (n m:Nat) : Nat :=
natRect _ m (fun _ rec => succ rec) n.

### Code Reuse

We can instantiate the ADT using Coq’s standard library natural numbers, …

Instance natNat : NatADT := {|
Nat := nat;
zero := 0;
succ := S;
natRect := nat_rect
|}.
Proof.
- reflexivity.
- reflexivity.
Defined.

We can even prove that our implementation of add is equivalent to the standard library operation Nat.add (+).

induction n; cbn in *; congruence.
Qed.

We can also instantiate the ADT using Coq’s binary natural numbers N, …

Require Import NArith.

Open Scope N.

Instance NNat : NatADT := {|
Nat := N;
zero := N.zero;
succ := N.succ;
natRect := N.peano_rect
|}.
Proof.
- apply N.peano_rect_base.
- apply N.peano_rect_succ.
Defined.

ADTs thus enable code reuse, because a function has to only be implemented once for an ADT, instead of every single instatiation of the ADT.

While this instantiation of add is exponentially more space efficient than the instantiation with natNat, the computation still requires time exponential in the number of n’s bits.

The problem of ADTs is that they hide implementation details, and thus deny opportunities for optimization. To overcome this problem, ADT implementers have to guess and expose all the operations that some future instatiation of the ADT can implement more efficiently (even if they can be implemented less efficiently using other operations of the ADT). The result is an ADT that is hard to understand (because the essential operations are swamped by derived operations) and inefficient (because some optimization opportunity will inevitably be lost for lack of precognition).

ADTs are also useful for extraction. We can instantiate an ADT using opaque terms that will be implemented on extraction.

Parameter HsNat : Type.
Parameter hsZero : HsNat.
Parameter hsSucc : HsNat -> HsNat.
Parameter hsNatRect : forall P, P hsZero -> (forall n, P n -> P (hsSucc n)) -> forall n, P n.
Axiom hsNatRectZero : forall P z s, hsNatRect P z s hsZero = z.
Axiom hsNatRectSucc : forall P z s n, hsNatRect P z s (hsSucc n) = s n (hsNatRect P z s n).

Extract Constant HsNat => "Prelude.Integer".
Extract Constant hsZero => "0".
Extract Constant hsSucc => "Prelude.succ".
Extract Constant hsNatRect => "(\z s -> let f n = if n Prelude.== 0
then z
else s (Prelude.pred n)
(f (Prelude.pred n)) in f)".

Instance HsNatNat : NatADT := {|
Nat := HsNat;
zero := hsZero;
succ := hsSucc;
natRect := hsNatRect
|}.
Proof.
- apply hsNatRectZero.
- apply hsNatRectSucc.
Defined.

Definition hsAdd : HsNat := @add HsNatNat (hsSucc (hsSucc hsZero)) (hsSucc hsZero).

This approach clearly documents all the terms that have to be implemented by extraction (Parameter) and the assumptions about their behavior (Axiom), and is thus cleaner than the common alternative of syntactically replacing arbitrary Coq terms and data types:

Extract Inductive nat => "Prelude.Integer" ["0" "Prelude.succ"]
"(\z s n -> if n Prelude.== 0
then z ()
else s (Prelude.pred n))".

Definition hsAddNat : nat := 2 + 1.

There is another major downside to using ADTs — they severely impact theorem proving. Consider the following proof that 0 + n = n + 0 using Coq’s standard library natural numbers. After the induction, the proof is almost automatic due to Coq’s ability to computationally simplify (cbn) the goal.

Open Scope nat.

Lemma natAddZero (n : nat) : 0 + n = n + 0.
induction n as [|n' IHn'].
- reflexivity.
- cbn in IHn'.         (* A *)
rewrite IHn' at 1.   (* B *)
cbn.                 (* C *)
reflexivity.
Qed.

Compare this to the proof which uses the ADT, where we have to perform equational reasoning instead of computational reasoning. This is extremely burdensome, especially for more complicated proofs.

refine (natRect (fun n => add zero n = add n zero) _ (fun n' IHn' => _) n).
- reflexivity.
- unfold add in IHn'.             (* A *)
rewrite natRectZero in IHn'.    (* A *)
rewrite IHn' at 1.              (* B *)
rewrite natRectSucc.            (* C *)
rewrite natRectZero.            (* C *)
reflexivity.
Qed.