The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Jonas,

You may want to have a look at Emmanuel Polonowski's generic environments.

Source : http://lacl.u-pec.fr/polonowski/Develop/Generic_Env/gen-env.html
Extended abstract + slides :
http://www.cs.ru.nl/~spitters/coqw_files/program.html

Cheers,

--
guillaume

On 2 December 2011 20:47, Jonas Oberhauser 
<s9joober AT googlemail.com>
 wrote:
> 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