The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Mon, Feb 3, 2020 at 5:54 PM Vincent Siles <vincent.siles AT ens-lyon.org> wrote:

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

Here is the sketch of a simple proof.  Assuming "State.eq" is the "Equal" predicate between maps, you need to prove

  forall z, find z (add y b (add x a state))  = find z (add x a (add y b state))

First you rewrite using add_o from the FMapFacts library of derived facts. Then you do a case analysis on  Key.eq_dec x z and on Key.eq_dec y z.

Hope this helps,

- Xavier Leroy