The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

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