coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Xavier Leroy <xavier.leroy AT college-de-france.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Proofs about FMapList / add / MapsTo
- Date: Mon, 3 Feb 2020 19:09:02 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=xavier.leroy AT college-de-france.fr; spf=Pass smtp.mailfrom=xavier.leroy AT college-de-france.fr; spf=None smtp.helo=postmaster AT smtpout01-ext1.partage.renater.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
- [Coq-Club] Proofs about FMapList / add / MapsTo, Vincent Siles, 02/03/2020
- Re: [Coq-Club] Proofs about FMapList / add / MapsTo, Xavier Leroy, 02/03/2020
- Re: [Coq-Club] Proofs about FMapList / add / MapsTo, Vincent Siles, 02/04/2020
- Re: [Coq-Club] Proofs about FMapList / add / MapsTo, Xavier Leroy, 02/03/2020
Archive powered by MHonArc 2.6.18.