The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

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