Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proofs about FMapList / add / MapsTo

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proofs about FMapList / add / MapsTo


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page