coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] How to model environments?, Jonas Oberhauser
- Re: [Coq-Club] How to model environments?,
gallais @ ensl.org
- Re: [Coq-Club] How to model environments?, Jonas Oberhauser
- Re: [Coq-Club] How to model environments?,
gallais @ ensl.org
Archive powered by MhonArc 2.6.16.