The Coq mailing list

[Quentin Carbonneaux <quentin.carbonneaux AT yale.edu>]

Hello everyone,

I am using Coq to make a formalization of a program analysis

I already implemented.  This analysis works like a Hoare Logic

by building a derivation inductively on the syntax.

What plays the role of pre/postconditions in my system are

what I call "annotations".  In essence, they are maps from

"indices" to Z. My definition for them is obvious

    Definition annot := index -> Z.

Indices are built from program variables.  In my current

implementations there are only two kind of indices but, in

the future, I will have to add more.

    Inductive index := iConst | iInter (a b: var).

The type var is here to represent program variables, I left

it abstract.

My problem comes when defining the semantics of annotations.

These annotations are meant to represent functions from

heaps to Z.  Annotations are simply coordinates in the linear

algebra sense (except that Z is not a field...). If Q is an

annotation, I want

    semantics Q h = \sum_i (Q i) * base i h

    

    Definition base (i: index) (h: heap) :=

      match i with

        | iConst => 1

        | iInter a b => Z.max (h b - h a) 0

      end.

Now my problem is how to define the above sum over all possible

indices.  First, it only makes sense when, either Q is non-zero

for only a finite number of indices (this is what I have on

paper), or the number of variables (hence indices) is finite.

My current solution is to have as a parameter the list of indices

we focus on, and then define my semantics function as follows:

    Parameter indices: list index.

    Definition semantics (Q: annot) (h: heap) :=

      List.fold_right (fun i n => n + Q i * base i h) 0 indices.

But this definition is far from ideal:

+ indices is a list when what I mean is a finite set (i.e. I

  don't want duplicates)

+ presented as a fold, the sum is essentially non-commutative

  which makes many proofs really painful

+ the order imposed by the indices list is often a contraint

  when reasoning

Here is an example lemma that I barely mention in my paper

proof but takes a lot of Coq to go through.

    Definition pay (Q: annot) (n: Z) (i: index) :=

      match i with

        | iConst => Q iConst - n

        | i => Q i

      end.

    Lemma semantics_pay:

      forall (Q: annot) (h: heap) (n: Z),

        semantics Q h = semantics (pay Q n) h + n.

    Proof. (* long! *) Qed.

If you have experience dealing with sums like this, could you

please help me clean this development and tell me how reasoning

can be made with less pain.

Thank you!

PS: Please CC me if you respond, I am not subscribed yet.

-- Quentin