The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

Hi Guillaume,

Thanks a lot, I will : )

Kind Regards,

Jonas

2011/12/3 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