The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

The problem is that `Map.Equiv` is defined via `MapsTo` which uses strict equality.

NM.Equiv =
fun (elt : Type) (eq_elt : elt -> elt -> Prop) (m m' : NM.t elt) =>
(forall k : NM.key, NM.In (elt:=elt) k m <-> NM.In (elt:=elt) k m') /\
(forall (k : NM.key) (e e' : elt), NM.MapsTo k e m -> NM.MapsTo k e' m' -> eq_elt e e')
     : forall elt : Type, (elt -> elt -> Prop) -> NM.t elt -> NM.t elt -> Prop

Vadim

--

Vadim Zaliva  

CMU ECE Ph.D. candidate

Mobile/Signal/WhatsApp: +1(510)220-1060

On Fri, May 24, 2019 at 3:15 PM Jasper Hugunin <jasperh AT cs.washington.edu> wrote:

I see. MapsTo is only up to strict equality of the values, while you need it to be up to Ae.

I'm don't think the standard library defines many lemmas about maps up to an equivalence relation on the values; in my experience they often aren't needed, as you can usually track the value equality conditions off to the side (but it is perhaps more proof burden). For example, instead of Map.MapsTo, you want the behavior of

MapsTo' k v m := exists v', Ae v v' * MapsTo k v' m

saying that m maps k to some v' which is the same up to Ae as v.

Map.Equiv Ae is then the right notion of equivalence, and you can then prove MapsTo'_A_proper making use of the Ae x y hypothesis.

- Jasper Hugunin

On Fri, May 24, 2019 at 2:24 PM Vadim Zaliva <vzaliva AT cmu.edu> wrote:

Jasper,

This is where I started, but using `Ae` as a equality for values it is impossible to prove the following:

Instance MapsTo_A_proper: Proper ((eq) ==> (Map.Equiv Ae) ==> (Ae) ==> iff) (NM.MapsTo).

It boils down to:

Ae x y →

Map.Equiv Ae m0 m1 →

Map.MapsTo k x m0 ↔ Map.MapsTo k y m1

(unless I am missing something)

Vadim

--

Vadim Zaliva  

CMU ECE Ph.D. candidate

Mobile/Signal/WhatsApp: +1(510)220-1060

On Fri, May 24, 2019 at 2:06 PM Jasper Hugunin <jasperh AT cs.washington.edu> wrote:

You can use

From Coq Require OrderedTypeEx FMapAVL FMapFacts.

Module Map := FMapAVL.Make OrderedTypeEx.Nat_as_OT.

Check Map.t : Type -> Type. (* The values can be anything you like *)

Check Map.Equiv : forall X, (X -> X -> Prop) -> (Map.t X -> Map.t X -> Prop).

(* You get a relation Map.Equiv for any relation between elements. Proving it is a congruence relation shouldn't be hard, but I'm not sure is in the standard library. *)

(* If the equality on values is Init.Logic.eq, i.e. a1 = a2, then you can instead use Map.Equal, which does have Proper instances proven in MapProperties. *)

Module MapProperties := FMapFacts.Properties Map.

(* Also MapProperties.F has useful stuff. *)

(* This can be used as *)

Axiom A : Type.

Check Map.t A. (* This is the type of maps with keys in nat and values in A. *)

- Jasper Hugunin

On Fri, May 24, 2019 at 11:51 AM Vadim Zaliva <vzaliva AT cmu.edu> wrote:

I am trying to figure out how to use FMap with abstract data type and
equality. I need a map where the keys are natural numbers, but values belong to an abstract type A. I can assume that this type has an equality Ae which is decidable, and a strict ordering.

I will need to have an Equiv relation between two maps (backed up by
Ae for elements). Finally, I would like to be able to prove Proper
instances for basic operations, like:

Instance MapsTo_A_proper:
  Proper ((eq) ==> (equiv) ==> (equiv) ==> iff) (NM.MapsTo).

Instance find_A_proper:
  Proper ((eq) ==> (equiv) ==> (equiv)) (NM.find (elt:=A)).

It looks like the map needs to be abstracted over A using a module.
This post http://www.newartisans.com/2016/10/using-fmap-in-coq/ gives
some good intro but stop shorts from abstracting values. It also looks
like I will need to use Sord functor from FMapInterface. I feel
like all pieces are there but having difficulty putting it all
together. I have not been able to find any relevant examples. Could
somebody please point me in the right direction? Thanks!

—
Vadim Zaliva
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: +1(510)220-1060