The Coq mailing list

[Vincent Siles <vincent.siles AT ens-lyon.org>]

Hi list !

I'm trying to remove some boiler plate I wrote some time ago, and replace it with FMapList.

I'm a bit stuck on a proof (mostly because I'm not used to the module yet), but it looks like something is missing, and you might be able to help me prove it.

I have a module built using FMapList.Map_ord, and I'm trying to prove that we can switch independent usage of add.

forall (state: State.t) (x y: Key.t) (a b: V.t), 

    ~ K.eq x y -> State.eq (add y b (add x a state)) (add x a (add y b state))

I plan to do that using eq_equal (https://coq.inria.fr/library/Coq.FSets.FMapList.html bottom of the page), and I'm down to proving something like:

Raw.PX.MapsTo k v1 (add y b (add x a state)) -> K,eq k x -> v1 = b

I can't find anything to prove that other than doing it from scratch.

Anyone familiar with this that could lend a hand ?

Best,

V.