Skip to Content.
Sympa Menu

coq-club - [Coq-Club] How to model environments?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to model environments?


chronological Thread 
  • From: Jonas Oberhauser <s9joober AT googlemail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] How to model environments?
  • Date: Fri, 2 Dec 2011 21:47:50 +0100

Hello everyone, I'm new to the coq proof system (and even more so to
this mailing list).

I'm looking for a good way to model environments, or 'Program States'.
To clarify, an environment basically is a "function" nat -> nat which
gives every variable its value.
I need to be able to both retrieve and update the value of a variable
in an environment (possibly creating a new environment in the
process).

Since during any state, only a finite number of variables can be used,
the obvious approach to model these would be using a hashmap of some
sort, but such datastructure should not be available in coq (not with
O(1) access). (amirite?)

So I stole the idea of one of my professors to simply use functions
nat -> nat, which are updated by putting (lambda x. if x = updated
then new_value else old_environment x) abstractions around the
environments.

  (* environment *)
  Definition env := nat -> nat.
  (* nat equality, nat -> nat -> bool *)
  Fixpoint eq_ib a b := ...

  (* update a value in an environment, computationally slow but who cares? *)
  Definition update (e : env) (i : nat) (val : nat) : env :=
      (fun (j:nat) => if eq_ib i j then val else e j) .

I didn't think that the computational complexity of this would cause
much headache, but I only get two out of four highly desirable
properties:

 (* these are simple to get since the environment is "evaluated" *)
  update_other n m : forall {e x}, n <> m -> (update e n x m) = e m
  update_same n : forall {e x}, update e n x n = x
 (* can't get these without extensionality *)
  update_redundant n : forall {e x y}, update (update e n x) n y = update e n 
y
  update_swap m n : forall {e x y}, n <> m -> update (update e n x) m
y = update (update e m y) n x

Now I'm looking for a way to model environments which allows me to get
all of these properties without further axioms (bonus if it's
computationally faster, but I don't really notice any speed problems
yet and have already proven some fancy things).

I'm thinking about using a (list nat) to carry all the known
variables, basically env = X1::...::[Xj] where env i = {Xi | 1 <= i <=
j} + { 0 | i > j }
The list would be extended as new variables are assigned (filling gaps
with 0). An extractor function would be needed (which is kinda sad,
since the (update e n x m) syntax was quite neat as opposed to
(retrieve (update e n x) m)).

By merely looking at the problem I would say that I can get all of the
four update properties, since list equality is by constructor &
-arguments.

Are there other viable options? Or can I somehow prove
update_redundant / update_swap thanks to the nested if in the final
abstraction? The list thing seems quite complicated to implement, and
slighly more ugly to use as well.

Thanks in advance,

Jonas



Archive powered by MhonArc 2.6.16.

Top of Page