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 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).
+ concretely: α {5 + (-5)} = α {0} = {Zero}+ abstractly: (α {5}) ⊕ (α {-5}) = {Pos} ⊕ {Neg} = {Neg, Zero, Pos}{Zero} ⊆ {Neg, Zero, Pos}, we say that this interpretation is sound.
To sum up: we need to define
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.
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.
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 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:
P ⊆ (γ (α P)) —
“throwing away” information about P by “traveling through signset” produces at most a “more general” version of P.
(α (γ 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 ySignSetProps.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).
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.
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!