The Coq mailing list

[Jasper Hugunin <jasperh AT cs.washington.edu>]

Here is how you can prove MapsTo'_A_proper:

From Coq Require OrderedTypeEx FMapAVL FMapFacts.

Module Map := FMapAVL.Make OrderedTypeEx.Nat_as_OT.

Module MapProperties := FMapFacts.Properties Map.

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

Axiom A : Type.

Axiom Ae : A -> A -> Prop.

Axiom Ae_sym : forall {x y}, Ae x y -> Ae y x.

Axiom Ae_trans : forall {x y z}, Ae x y -> Ae y z -> Ae x z.

Definition MapsTo' k v m : Prop := exists v', (Ae v v' * Map.MapsTo k v' m)%type.

Definition MapsTo'_A_proper_helper k x y m0 m1

  : Ae x y ->

    Map.Equiv Ae m0 m1 ->

    MapsTo' k x m0 -> MapsTo' k y m1

  := fun x_Ae_y m0_equiv_m1 k_mapsto'_x_in_m0 =>

     let '(ex_intro _ x' (x_Ae_x', k_mapsto_x'_in_m0)) := k_mapsto'_x_in_m0 in

     let '(ex_intro _ y' k_mapsto_y'_in_m1)

      := proj1 (proj1 m0_equiv_m1 k) (ex_intro _ x' k_mapsto_x'_in_m0)

      : Map.In k m1 in

     let x'_Ae_y' : Ae x' y'

      := proj2 m0_equiv_m1 k x' y' k_mapsto_x'_in_m0 k_mapsto_y'_in_m1 in

     let y_Ae_y' : Ae y y'

      := Ae_trans (Ae_sym x_Ae_y) (Ae_trans x_Ae_x' x'_Ae_y') in

     ex_intro _ y' (y_Ae_y', k_mapsto_y'_in_m1).

From Coq Require Import Morphisms.

Axiom Map_Equiv_sym : forall {m0 m1}, Map.Equiv Ae m0 m1 -> Map.Equiv Ae m1 m0.

Instance MapsTo'_A_proper

  : Proper ((eq) ==> (Ae) ==> (Map.Equiv Ae) ==> iff) MapsTo'

  := fun k1 k2 ke =>

     match ke with eq_refl => fun x y x_Ae_y m1 m2 me => conj

       (MapsTo'_A_proper_helper k1 x y m1 m2 x_Ae_y me)

       (MapsTo'_A_proper_helper k1 y x m2 m1 (Ae_sym x_Ae_y) (Map_Equiv_sym me))

     end.

(* Map.Equiv with MapsTo' instead *)

Definition Equiv' m1 m2 : Prop

  := (forall k : Map.key,

      Map.In (elt:=A) k m1 <->

      Map.In (elt:=A) k m2) /\

     (forall (k : Map.key) (e e' : A),

      MapsTo' k e m1 -> MapsTo' k e' m2 -> Ae e e').

(* Equiv <-> Equiv' left as exercise to the reader *)

Best,

- Jasper Hugunin

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

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