Home Articles 2019/03/24

## Interpreting + Abstractly with Signs

Abstract interpretation is a technique for statically analyzing programs—analyzing them without executing them. The main idea is to translate the hard-to-analyze program on “concrete” data into easy-to-analyze computations on “abstract” data that contains the information you want to know about the program.

This article will talk about the set-of-signs abstract domain, abstractly interpreting addition with sets of signs, and proving the soundness of that interpretation using Coq. This is the first in a series of articles on abstract interpretation in Coq. We'll focus on the specific details of this interpretation and leave the general formulation of abstract interpretation for the future.

The Coq script can be found here if you'd like to follow along. I'm new to Coq, so this is intended as something of a beginner's tutorial. As such, a lot of the proofs are written out even when they could be solved with one of the more powerful automatic tactics. If you're curious about something or have advice about how I can better approach things, don't hesitate to let me know!

### The General Idea

The goal of abstract interpretation is to make static program analysis easier by interpreting a program on an "abstract domain" that captures whatever property you're trying to analyze. In this case, we're going to interpret programs on the integers in such a way that we can determine the sign (positive, negative, or zero) of the result without actually computing the result. More specifically, we're going to write an abstract version of addition, which could be combined with abstract versions of negation, multiplication, etc. and used to interpret more complex programs.

We'll be interpreting addition over sets of signs. Why? Consider what the result of `Pos ⊕ Neg` should be. Depending on the values of the numbers added, the result could be positive, negative, or zero! We solve this problem by operating on sets of signs instead: `{Pos} ⊕ {Neg} = {Neg, Zero, Pos}`.

We'll be relating sets of integers to sets of signs via an abstraction function `α : Set Int -> Set Sign`. In short, we do this so we can define a sound mapping from the concrete domain (sets of integers) to the abstract domain (sets of signs).

Finally, for our interpretation to be sound, we must prove that the abstract interpretation of addition is at worst more general than concretely interpreting addition and abstracting the results. In other words, for sets of integers `N` and `M`, `α (N + M) ⊆ (α N) ⊕ (α M)`.

Let's work a quick example. Say we want to determine the sign of `5 + (-5)`.

• Interpreting `+` concretely: `α {5 + (-5)} = α {0} = {Zero}`
• Interpreting `+` abstractly: `(α {5}) ⊕ (α {-5}) = {Pos} ⊕ {Neg} = {Neg, Zero, Pos}`
Since `{Zero} ⊆ {Neg, Zero, Pos}`, we say that this interpretation is sound.

To sum up: we need to define

• Signs and sets of signs,
• The abstract interpretation of addition, ⊕,
• Sets of integers, and
• A means of abstracting sets of integers to sets of signs, α.
We need to prove
• That α is a sound abstraction method and
• That ⊕ is a sound interpretation of addition.
So, let's get down to business!

### Signs and Sets of Signs

#### Signs

Our signs are just `Neg`, `Zero`, and `Pos`:

```Inductive sign: Type :=
Neg : sign
| Zero : sign
| Pos : sign
.
```

Since `sign` is very finite, we can use a finite set library to build the sets-of-signs type. I eventually want to explore extracting these definitions to Haskell, so I decided to use an “efficient” finite set library: `MSetList`. To use this library on `sign`, we need to define equality (`eq`) and an order (`compare`) for our type. Let's do that first and prove a couple theorems that will be handy later on.

For equality, we specialize Logic.eq for `sign`:

```Definition eq := (@eq sign).
```

For order, we define `compare` by case and use it to define a strict order `lt`.

```Definition compare l r: comparison :=
match l, r with
Neg, Neg => Eq
| Neg, _ => Lt
| Zero, Neg => Gt
| Zero, Zero => Eq
| Zero, Pos => Lt
| Pos, Pos => Eq
| Pos, _ => Gt
end.

Definition lt l r: Prop := (compare l r) = Lt.
```

Let's prove a couple lemmas about `compare`. First, we'll show that if `compare` thinks two elements are equal, they are:

```Lemma sign_compare_eq: forall x y, compare x y = Eq -> x = y.
```

We'll do this by cases and symbolically execute `compare`:

```case x, y; simpl compare;
```
```9 subgoals
______________________________________(1/9)
Eq = Eq -> Neg = Neg
______________________________________(2/9)
Lt = Eq -> Neg = Zero
______________________________________(3/9)
Lt = Eq -> Neg = Pos
______________________________________(4/9)
Gt = Eq -> Zero = Neg
______________________________________(5/9)
Eq = Eq -> Zero = Zero
______________________________________(6/9)
Lt = Eq -> Zero = Pos
______________________________________(7/9)
Gt = Eq -> Pos = Neg
______________________________________(8/9)
Gt = Eq -> Pos = Zero
______________________________________(9/9)
Eq = Eq -> Pos = Pos
```

Each goal is of two forms: either the hypothesis is false (e.g., `Lt = Eq`) or the conclusion is trivial (e.g., `Neg = Neg`). We assume the hypothesis and then either prove the conclusion (`reflexivity`) or show that the hypothesis is self-contradictory (`discriminate`):

```intros H; try reflexivity; try discriminate H.
```
```No more subgoals.
```

```Qed.
```

Next we'll show that `lt` and `compare` agree. This has two parts: one for when `compare x y` is `Lt`, and one for when it is `Gt`. The first part is straightforward since we have defined `lt` in terms of `compare`. All we have to do is replace `lt` with its definition (with `unfold`) and we get exactly what we're proving:

```Lemma sign_compare_lt: forall x y, compare x y = Lt -> lt x y.
intros.
unfold lt.
exact H.
Qed.
```

The second part is a mix of the first two. We expand `lt`, then do case analysis just as we did in `sign_compare_eq`:

```Lemma sign_compare_gt: forall x y, compare x y = Gt -> lt y x.
unfold lt.
case x, y; simpl compare; intros H; try reflexivity; try discriminate H.
Qed.
```

#### Sets of Signs

`MSetList` is a finite set implementation which uses a sorted list to store set elements. To use it, we need to provide it with equality and order definitions for the element type and proofs that those definitions have certain properties. Since our type uses `Logic.eq`, which uses Coq's Leibniz equality, we can use the `MakeWithLeibniz` module functor to construct an instance of `MSetList` for `sign`.

(This section draws heavy inspiration from these examples: 1, 2, 3, 4.)

To use this module functor, we need a module which meets the `OrderedTypeWithLeibniz` module type. Below is the definition of `OrderedTypeWithLeibniz` (fetched via `Print OrderedTypeWithLeibniz.`). First it defines `t`, the type of elements of the set. Then it asks for definitions of equality and order and proofs of their properties.

```Module Type OrderedTypeWithLeibniz.
Parameter t : Type.
Parameter eq : t -> t -> Prop.
Parameter eq_equiv : Equivalence eq.
Parameter lt : t -> t -> Prop.
Parameter lt_strorder : StrictOrder lt.
Parameter lt_compat : Proper (eq ==> eq ==> iff) lt.
Parameter compare : t -> t -> comparison.
Parameter compare_spec :
forall x y : t, CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).
Parameter eq_dec : forall x y : t, {eq x y} + {~ eq x y}.
Parameter eq_leibniz : forall x y : t, eq x y -> x = y.
End OrderedTypeWithLeibniz.
```

We'll make a module `SignOTWL` that has this type. We say what type the set elements are and what the equality relationship is. Then, we have to prove that `eq` is an equivalence relation:

```Module SignOTWL <: OrderedTypeWithLeibniz.
Definition t := sign.
Definition eq := eq.
Instance eq_equiv : Equivalence eq.
Proof.
split;
unfold Reflexive; unfold Symmetric; unfold Transitive.
```
```3 subgoals
______________________________________(1/3)
forall x : sign, eq x x
______________________________________(2/3)
forall x y : sign, eq x y -> eq y x
______________________________________(3/3)
forall x y z : sign, eq x y -> eq y z -> eq x z
```

The `reflexivity` tactic can prove `eq x x`, so all we need to do is use the hypotheses to rewrite the conclusion to that form:

```reflexivity.
intros.
rewrite H.
reflexivity.
intros.
rewrite H.
rewrite H0.
reflexivity.
Qed.
```

There's more to prove about equality, but we're going to define the order before that. First, we have to prove that it's strict:

```Definition lt := lt.
Instance lt_strorder: StrictOrder lt.
Proof.
split;
unfold Irreflexive; unfold Reflexive; unfold complement; unfold Transitive;
unfold lt; unfold Top.lt.
```
```2 subgoals
______________________________________(1/2)
forall x : sign, compare x x = Lt -> False
______________________________________(2/2)
forall x y z : sign,
compare x y = Lt
-> compare y z = Lt
-> compare x z = Lt
```

The first goal we prove by cases and symbolically computing `compare`:

```intros x.
case x; simpl compare;
```
```4 subgoals
x : sign
______________________________________(1/4)
Eq = Lt -> False
______________________________________(2/4)
Eq = Lt -> False
______________________________________(3/4)
Eq = Lt -> False
(...)
```

Each hypothesis is false, so we can `discriminate` them:

```intros H; discriminate H.
```
```1 subgoal
______________________________________(1/1)
forall x y z : sign,
compare x y = Lt
-> compare y z = Lt
-> compare x z = Lt
```

The last goal can also be done by cases:

```case x, y, z; simpl compare;
```
```27 subgoals
______________________________________(1/27)
Eq = Lt -> Eq = Lt -> Eq = Lt
(...)
______________________________________(4/27)
Lt = Lt -> Gt = Lt -> Eq = Lt
(...)
______________________________________(6/27)
Lt = Lt -> Lt = Lt -> Lt = Lt
(...)
```

The three (of 27!) subgoals above show the three general cases: either one of the hypotheses is false or the conclusion is true. Situations like this are where the `try` tactic really comes in handy. We'll use it to attempt to disprove either hypothesis or, failing that, prove the conclusion:

```intros H1 H2; try discriminate H1; try discriminate H2; try reflexivity.
Qed.
```

The next reqirement asks us to prove that, if `x = y` and `z = w`, then `lt x z` iff `lt y w`.

```Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
Proof.
split;
```
```2 subgoals
x, y : sign
H : eq x y
x0, y0 : sign
H0 : eq x0 y0
______________________________________(1/2)
lt x x0 -> lt y y0
______________________________________(2/2)
lt y y0 -> lt x x0
```

We can use equality (`H` and `H0`) to rewrite the goals until they're exactly the same:

```rewrite H; rewrite H0;
```
```2 subgoals
(...)
______________________________________(1/2)
lt y y0 -> lt y y0
______________________________________(2/2)
lt y y0 -> lt y y0
```

And that is exactly what we're trying to prove.

```intros Hlt; exact Hlt.
Qed.
```

Next we provide a comparison function (`compare`) and prove that it agrees with `eq` and `lt`. We already proved the lemmas needed to show this; this proof just takes apart `CompSpec` and applies them.

```Definition compare := compare.
Lemma compare_spec: forall x y, CompSpec eq lt x y (compare x y).
intros.
unfold CompSpec.
case_eq (compare x y);
constructor.
apply sign_compare_eq.
exact H.
apply sign_compare_lt.
exact H.
apply sign_compare_gt.
exact H.
Qed.
```

Finally, we have a couple more things to prove about equality. It has to be decidable—either `eq x y` or `~ eq x y`. Coq states this by using a dependent pair which (more or less) is either the value `left` or `right`, plus a proof that the value was chosen correctly. As usual, we'll prove it by cases:

```Lemma eq_dec: forall x y:sign, {eq x y} + {~ eq x y}.
case x, y;
```
```9 subgoals
______________________________________(1/9)
{eq Neg Neg} + {~ eq Neg Neg}
______________________________________(2/9)
{eq Neg Zero} + {~ eq Neg Zero}
(...)
```

To prove each subgoal, we need to state which side of the pair we want to prove using `left` or `right`, then prove it. When using `try` on these subgoals, it is important to use e.g., `try (left; reflexivity)` rather than `try left; try reflexivity`. `left` would succeed for every subgoal, leaving us with a bunch of impossible things to prove!

```try (left; reflexivity); try (right; discriminate).
Qed.
```

The one thing that remains is to show that our equality is a Leibniz equality. Because that's what `Logic.eq` is, the proof is rather straightforward:

```Lemma eq_leibniz: forall x y: sign, (eq x y) -> x = y.
intros.
exact H.
Qed.
End SignOTWL.
```

Now that we've satisfied `OrderedTypeWithLeibniz`, we can make the SignSet module! We'll also make modules with various facts and properties that will come up later in proofs.

```Module SignSet := MakeWithLeibniz SignOTWL.
Module SignSetFacts := MSetFacts.WFacts SignSet.
Module SignSetProps := MSetProperties.WProperties SignSet.

Definition signset := SignSet.t.
```

For convenience, let's define the set of all signs, `AllSigns`. While strictly not necessary, I wrote a function for turning a list into a set to make this a bit easier. (There's probably something that does this already in `MSetList`, but I couldn't find it.)

```Require Import List.

Fixpoint fromList l : SignSet.t :=
match l with
nil => SignSet.empty
| (h :: t) => SignSet.add h (fromList t)
end.
```

We can then make `AllSigns` and prove that it, in fact, contains all elements of `sign`:

```Definition AllSigns := fromList (Neg :: Zero :: Pos :: nil).

Lemma in_allsigns: forall x, SignSet.In x AllSigns.
intros.
unfold AllSigns; simpl.
case x; intuition.
Qed.
```

One last fact that will come in handy as soon as we start proving things about α: if we have a singleton set (i.e., something that looks like `{s}`), there is something in that set:

```Lemma exists_in_singleton: forall s,
exists t, SignSet.In t (SignSet.singleton s).
intros.
exists s.
```
```1 subgoal
s : SignSet.elt
______________________________________(1/1)
SignSet.In s (SignSet.singleton s)
```

Here we can make use of one of the facts or propositions we have about `SignSet`. A search for `SignSet.singleton` turns up

``````SignSetProps.Dec.F.singleton_2:
forall x y : SignSet.elt, eq x y -> SignSet.In y (SignSet.singleton x)``````

If we `apply` this to the goal, it will transform the goal into the left hand side of the implication, leaving us to prove `eq s s`:

```apply SignSetProps.Dec.F.singleton_2.
reflexivity.
Qed.
```

### Sets of Integers

Coq provides a library for working with integers, `ZArith`, which defines the `Z` type.

```Require Import ZArith.
Open Scope Z_scope.
```

Since we need to work with potentially infinite sets of integers, we'll have to use a different set formalism. I chose to use Ensembles, which model a set `P` as a proposition `P : elt -> Prop` which determines whether a given element is included in the set. Set unions, subset relations, &c. can all be written using logical connectives. For example, `P ⊆ Q` corresponds to `forall x, P x -> Q x`.

While the ensemble library defines aliases for these operations, I've just directly written the logical versions as it was easier to reason about. (The ensemble library could really do with a few nontrivial examples of writing functions with ensembles; perhaps I'm just thinking about sets like a computer scientist and not like a mathematician.)

```Require Import Ensembles.
```

Unfortunately ensembles don't work all that well with `MSets`, so some of the definitions end up coming out a bit clunky. Ideally I think I should have written the entire thing to use ensembles and then proved some sort of extension from the ensemble version to a finite-set version. Something to think about for the future, anyway.

### Abstracting Sets of Integers to Sets of Signs

Abstracting an integer to the smallest set of signs describing it is pretty straightforward:

```Definition sign_of (n:Z) : signset :=
match Z.compare n 0 with
Eq => SignSet.singleton Zero
| Lt => SignSet.singleton Neg
| Gt => SignSet.singleton Pos
end.
```

A sound mapping from sets of integers to sets of signs is a bidirectional relationship `α : Set Z -> signset`, `γ : signset -> Set Z`. We use this bidirectional relationship to prove that α doesn't "go wrong"—that it produces results which contain the correct sign.

```Definition alpha P s : Prop := exists n, P n /\ SignSet.In s (sign_of n).
Definition gamma P n : Prop := exists s, P s /\ SignSet.In s (sign_of n).
```

In other words, a sign is in `α P` if it matches the sign of an integer in `P`. Likewise, an integer is in `γ P` if its sign is in `P`.

For α and γ to be sound, they must be monotone—they must preserve the “subset” relationship. If `P ⊆ Q`, `(α P) ⊆ (α Q)` and `(γ P) ⊆ (γ Q)`. These proofs are rather dull.

```Lemma alpha_monotone: forall (P Q: Ensemble Z),
(forall n, P n -> Q n) -> (forall s, (alpha P) s -> (alpha Q) s).
intros P Q HPnQn.
unfold alpha.
intros s [n [HPn Hsalpha]].
```
```1 subgoal
P, Q : Ensemble Z
HPnQn : forall n : Z, P n -> Q n
s : SignSet.elt
n : Z
HPn : P n
Hsalpha : SignSet.In s (sign_of n)
______________________________________(1/1)
exists n0 : Z, Q n0 /\ SignSet.In s (sign_of n0)
```

We need to find an integer in the set `Q` whose sign is `s`. The integer `n` fits both of these requirements, since `P ⊆ Q` and `n` is in `P`:

```exists n.
split.
apply HPnQn in HPn.
exact HPn.
exact Hsalpha.
Qed.
```

As I said before, these proofs just put me to sleep, and Coq agrees: you can solve them with `auto`:

```Lemma gamma_monotone: forall (P Q : Ensemble sign),
(forall s, P s -> Q s) -> (forall n, (gamma P) n -> (gamma Q) n).
intros P Q HPsQs.
unfold gamma.
intros n [s [HPs Hsalpha]].
exists s.
auto.
Qed.
```

Finally, α and γ must live up to the following relationships:

1. `P ⊆ (γ (α P))` — “throwing away” information about P by “traveling through `signset`” produces at most a “more general” version of P.
2. `(α (γ P)) ⊆ P` — any information “gained” by traveling through `Z` produces at most a “more specific” version of P. (In this case, we actually get = instead of ⊆!)

We'll first show that α maps every nonempty integer set `P` to a nonempty sign set. We do this by cases on an integer in `P` and symbolically computing `sign_of` to show that it produces nonempty sets of signs:

```Lemma sign_in_alpha: forall n P, P n -> exists s, SignSet.In s (sign_of n).
intros.
unfold sign_of.
case_eq n; simpl; intros; apply exists_in_singleton.
Qed.
```

To prove (1), we start by computing the sign `s` of an integer `n` in the set `P`:

```Lemma gamma_alpha: forall (P: Ensemble Z) n, P n -> (gamma (alpha P)) n.
intros P n HPn.
unfold alpha; unfold gamma.
assert (HPn_has_sign := HPn).
apply sign_in_alpha in HPn_has_sign.
destruct HPn_has_sign as [s Hsalpha].
```
```1 subgoal
P : Ensemble Z
n : Z
HPn : P n
s : SignSet.elt
Hsalpha : SignSet.In s (sign_of n)
______________________________________(1/1)
exists s0 : SignSet.elt,
(exists n0 : Z, P n0 /\ SignSet.In s0 (sign_of n0)) /\
SignSet.In s0 (sign_of n)
```

What remains is to show that `s` is in `α P` and therefore that `n` is in `γ (α P)`. This amounts to stating that `s` and `n` meet the requirements for the `exists` clauses in α and γ:

```exists s.
split.
exists n.
split.
exact HPn.
exact Hsalpha.
exact Hsalpha.
Qed.
```

To prove (2), we first introduce and simplify the numerous assumptions we get:

```Lemma alpha_gamma: forall P s, (alpha (gamma P)) s -> P s.
intros P s.
unfold alpha; unfold gamma.
intros [n [[t [Htp Htalpha]] Hsalpha]].
```
```1 subgoal
P : SignSet.elt -> Prop
s : SignSet.elt
n : Z
t : SignSet.elt
Htp : P t
Htalpha : SignSet.In t (sign_of n)
Hsalpha : SignSet.In s (sign_of n)
______________________________________(1/1)
P s
```

The rest of the proof consists of tediously showing that `t = s` follows from `Htalpha` and `Hsalpha` by doing case analysis on `n` and symbolically computing `sign_of`:

```case_eq n;
intros; rename H into Hn;
rewrite Hn in Hsalpha; unfold sign_of in Hsalpha; simpl in Hsalpha;
rewrite Hn in Htalpha; unfold sign_of in Htalpha; simpl in Htalpha;
apply SignSetProps.Dec.F.singleton_1 in Hsalpha;
apply SignSetProps.Dec.F.singleton_1 in Htalpha;
rewrite <- Htalpha in Htp;
rewrite <- Hsalpha;
exact Htp.
Qed.
```

(Note that

``````SignSetProps.Dec.F.singleton_1:
forall x y : SignSet.elt, SignSet.In y (SignSet.singleton x) -> eq x y``````

is the converse of `SignSetProps.Dec.F.singleton_2`.)

Recall that α relates sets of integers to sets of signs; therefore, we need to “lift” addition to sets of integers. The sum of two sets of integers `P` and `Q` is a set where each element is the sum of an element of `P` and an element of `Q`:

```Definition set_plus P Q x : Prop := exists n m, P n /\ Q m /\ n + m = x.
```

We begin by defining the result of adding two signs together. For the most part the sign of the result is known exactly; however, the example in “The General Idea” illustrates a situation where the result could have any sign.

It is easiest to define `sign_plus` by exhaustively writing out the cases. (We could take advantage of commutativity to reduce the cases by half, but Coq requires that the recursion terminate and can't see that the operation is commutative. That can be solved by using “gas” or a measure of “decreasing”ness, but that makes the function more complex and less obviously correct.)

```Definition sign_plus (n: sign) (m: sign) : SignSet.t :=
match n, m with
Neg,  Neg  => SignSet.singleton Neg
| Neg,  Zero => SignSet.singleton Neg
| Neg,  Pos  => AllSigns
| Zero, Neg  => SignSet.singleton Neg
| Zero, Zero => SignSet.singleton Zero
| Zero, Pos  => SignSet.singleton Pos
| Pos,  Neg  => AllSigns
| Pos,  Zero => SignSet.singleton Pos
| Pos,  Pos  => SignSet.singleton Pos
end.
```

Since our implementation of α gives us an ensemble rather than a finite set, we'll write `signset_plus` to add two ensembles of signs together.

```Definition signset_plus P Q s : Prop := exists n m, P n /\ Q m /\ SignSet.In s (sign_plus n m).
```

### Proving The Signs Interpretation Sound

At last, we are ready to prove that `signs_plus` is a sound interpretation of integer addition. Recall that this means proving that, for sets of integers `P` and `Q`, `α (P + Q) ⊆ (α P) ⊕ (α Q)`.

```Lemma signset_plus_sound: forall s (P Q: Ensemble Z),
(alpha (set_plus P Q)) s -> (signset_plus (alpha P) (alpha Q)) s.
```

We start by naming our premises, then recovering the two integers `n` and `m` summed together by `set_plus`. We also show that `s` is the sign of `n + m`.

```intros s P Q.
unfold alpha; unfold signset_plus.
intros [x [Hsp Hsign_x]].
unfold set_plus in Hsp.
destruct Hsp as [n [m [HPn [HQm Hplus]]]].
rewrite <- Hplus in Hsign_x.
```
```1 subgoal
s : SignSet.elt
P, Q : Ensemble Z
x, n, m : Z
HPn : P n
HQm : Q m
Hplus : n + m = x
Hsign_x : SignSet.In s (sign_of (n + m))
______________________________________(1/1)
exists n0 m0 : sign,
(exists n1 : Z, P n1 /\ SignSet.In n0 (sign_of n1)) /\
(exists n1 : Z, Q n1 /\ SignSet.In m0 (sign_of n1)) /\
SignSet.In s (sign_plus n0 m0)
```

Next, we see that we need to conjure up two signs that, when added together, produce a set containing `s`. The signs of `n` and `m` should meet this requirement! We can use `sign_in_alpha` to compute those signs:

```assert (HPn_has_sign := HPn).
apply sign_in_alpha in HPn_has_sign.
destruct HPn_has_sign as [t HPn_has_sign].
exists t.

assert (HQm_has_sign := HQm).
apply sign_in_alpha in HQm_has_sign.
destruct HQm_has_sign as [u HQm_has_sign].
exists u.
```
```1 subgoal
s : SignSet.elt
P, Q : Ensemble Z
x, n, m : Z
HPn : P n
HQm : Q m
Hplus : n + m = x
Hsign_x : SignSet.In s (sign_of (n + m))
t : SignSet.elt
HPn_has_sign : SignSet.In t (sign_of n)
u : SignSet.elt
HQm_has_sign : SignSet.In u (sign_of m)
______________________________________(1/1)
(exists n0 : Z, P n0 /\ SignSet.In t (sign_of n0)) /\
(exists n0 : Z, Q n0 /\ SignSet.In u (sign_of n0)) /\
SignSet.In s (sign_plus t u)
```

Next, we need to show that we haven't just plucked `t` and `u` out of thin air: there need to be corresponding integers in `P` and `Q`. Since we got them from `n` and `m`, we can say just that:

```split.
exists n.
split.
exact HPn.
exact HPn_has_sign.

split.
exists m.
split.
exact HQm.
exact HQm_has_sign.
```
```1 subgoal
s : SignSet.elt
P, Q : Ensemble Z
x, n, m : Z
HPn : P n
HQm : Q m
Hplus : n + m = x
Hsign_x : SignSet.In s (sign_of (n + m))
t : SignSet.elt
HPn_has_sign : SignSet.In t (sign_of n)
u : SignSet.elt
HQm_has_sign : SignSet.In u (sign_of m)
______________________________________(1/1)
SignSet.In s (sign_plus t u)
```

Finally, we have to prove that `s` truly is a possible outcome of adding `t` to `u`. Attempting this by cases on `s`, `t`, and `u` is verbose, as it results in 14 cases where we have to derive `False` from the premises. It is easier to approach this as a more complex version of the proof of `alpha_gamma` and do case analysis on `n` and `m` instead. This way, we directly compute the possible values of `s`, `t`, and `u`, skipping impossible outcomes.

```case_eq m; case_eq n;
```
```9 subgoals
s : SignSet.elt
P, Q : Ensemble Z
x, n, m : Z
HPn : P n
HQm : Q m
Hplus : n + m = x
Hsign_x : SignSet.In s (sign_of (n + m))
t : SignSet.elt
HPn_has_sign : SignSet.In t (sign_of n)
u : SignSet.elt
HQm_has_sign : SignSet.In u (sign_of m)
______________________________________(1/9)
n = 0 -> m = 0 -> SignSet.In s (sign_plus t u)
(...)
______________________________________(6/9)
forall p : positive, n = Z.neg p
-> forall p0 : positive, m = Z.pos p0
-> SignSet.In s (sign_plus t u)
(...)
```

Each of these subgoals comes with two hypotheses (to be named `Hn` and `Hm`) determining the value of `n` and `m`. Since their values are fixed, we can compute the value of `t` and `u`:

```intros until 2; rename H into Hn; rename H0 into Hm;

rewrite Hn in HPn_has_sign;
unfold sign_of in HPn_has_sign;
simpl in HPn_has_sign;
apply SignSetProps.Dec.F.singleton_1 in HPn_has_sign;
apply SignSet.E.eq_leibniz in HPn_has_sign;

rewrite Hm in HQm_has_sign;
unfold sign_of in HQm_has_sign;
simpl in HQm_has_sign;
apply SignSetProps.Dec.F.singleton_1 in HQm_has_sign;
apply SignSet.E.eq_leibniz in HQm_has_sign;
```
```9 subgoals
s : SignSet.elt
P, Q : Ensemble Z
x, n, m : Z
HPn : P n
HQm : Q m
Hplus : n + m = x
Hsign_x : SignSet.In s (sign_of (n + m))
t : SignSet.elt
HPn_has_sign : Zero = t
u : SignSet.elt
HQm_has_sign : Zero = u
Hn : n = 0
Hm : m = 0
______________________________________(1/9)
SignSet.In s (sign_plus t u)
(...)
```

Given fixed values for `t` and `u`, we can compute the `sign_plus` in the goals:

```rewrite <- HPn_has_sign;
rewrite <- HQm_has_sign;
unfold sign_plus;
```
```9 subgoals
s : SignSet.elt
P, Q : Ensemble Z
x, n, m : Z
HPn : P n
HQm : Q m
Hplus : n + m = x
Hsign_x : SignSet.In s (sign_of (n + m))
t : SignSet.elt
HPn_has_sign : Zero = t
u : SignSet.elt
HQm_has_sign : Zero = u
Hn : n = 0
Hm : m = 0
______________________________________(1/9)
SignSet.In s (SignSet.singleton Zero)
(...)
______________________________________(6/9)
SignSet.In s AllSigns
(...)
```

For some of the goals (such as goal 6 shown above), we are all but done. The others need us to compute the value of `s`, which we can do from `Hsign_x`:

```rewrite Hn in Hsign_x;
rewrite Hm in Hsign_x;
unfold sign_of in Hsign_x;
simpl in Hsign_x;
```
```9 subgoals
s : SignSet.elt
P, Q : Ensemble Z
x, n, m : Z
HPn : P n
HQm : Q m
Hplus : n + m = x
Hsign_x : SignSet.In s (SignSet.singleton Zero)
t : SignSet.elt
HPn_has_sign : Zero = t
u : SignSet.elt
HQm_has_sign : Zero = u
Hn : n = 0
Hm : m = 0
______________________________________(1/9)
SignSet.In s (SignSet.singleton Zero)
(...)
______________________________________(6/9)
SignSet.In s AllSigns
(...)
```

Now, either `Hsign_x` is the goal we're trying to prove, or we can't compute `s`, in which case `in_allsigns` applies:

```try exact Hsign_x;
try apply in_allsigns.
Qed.
```

For those of you curious, in goals where `s` cannot be computed, `simpl in Hsign_x` gets stuck on the `match`:

```Hsign_x : SignSet.In s
match Z.pos_sub p0 p ?= 0 with
| Eq => SignSet.singleton Zero
| Lt => SignSet.singleton Neg
| Gt => SignSet.singleton Pos
end
```

And that's it! One abstract interpretation and it only took about 300 lines of Coq to prove it.

### Conclusions

For a starter project in Coq, this wasn't a half bad choice. Most of the proofs are pretty straightforward, which gave me a lot of practice with the mechanics of theorem proving. There are also some nontrivial proofs which really get at the heart of constructive logic/proofs as computation. Overall, it's been fun AND educational!

From here, I could build on this machinery to make abstract interpretations of other integer operations (e.g., multiplication and exponentiation). That could be built into a proper abstract interpretation machine for algebraic expressions.

One thing that concerns me is that the way Coq defines integers as either positive, zero, or negative might mean that a lot of these proofs were easier than they “ought” to be. This is especially my concern in the proofs of `alpha_gamma` and `signset_plus_sound`. Perhaps developing an abstract interpretation on intervals would teach more about case splitting and the limitations of symbolic computation on integers.

Another frustration is that `signset_plus` works over ensembles rather than concrete set representations, so it isn't a candidate for code extraction. While I have written a version that uses finite sets, I don't know how to either connect it to ensembles of integers or how to prove that it is equivalent to `signset_plus`. I'll have to think on that some more. I suppose I should finish reading Constructive Galois Connections as it probably has some insight on this problem!