HyPre.util.MapExtra

From ExtLib Require Export
  Core.RelDec
  Data.Map.FMapAList.

From ExtLib Require Import
  Data.String.

From Coq Require Export
  Classes.EquivDec
  Classes.Morphisms
  Classes.RelationClasses
  Program.Basics.

From HyPre Require Import
  ListExtra.

Import ListNotations.

Global Existing Instance Nat.RelDec_eq.

Definition alist_incl {K V : Type} {R : K -> K -> Prop} {RD_K : RelDec R} (a b : alist K V) : Prop
  := forall k v, mapsto_alist RD_K a k v -> mapsto_alist RD_K b k v.

Definition alist_eq (i i' : alist nat nat) : Prop
  := forall k, alist_find _ k i = alist_find _ k i'.

Definition alist_intersect (l : list nat) (i : alist nat nat) : alist nat nat
  := fold_left (fun i' k => match alist_find _ k i with
                         | Some v => alist_add _ k v i'
                         | None => i'
                         end) l [].

Definition alist_intersect_eq (l : list nat) (i i' : alist nat nat) : Prop
  := alist_eq (alist_intersect l i) (alist_intersect l i').

Global Instance alist_eq_refl
  : Reflexive alist_eq.
Proof.
  econstructor.
Qed.

Lemma string_eqdec
  : EqDec String.string eq.
Proof.
  unfold EqDec.
  intros.
  destruct (String.eqb x y) eqn:E.
  - left.
    eapply String.eqb_eq;eauto.
  - right.
    eapply String.eqb_neq;eauto.
Qed.

Definition env := alist nat nat.

Global Instance alist_intersecq_eq_Reflexive
  : forall l, Reflexive (alist_intersect_eq l).
Proof.
  unfold Reflexive.
  intros.
  unfold alist_intersect_eq.
  reflexivity.
Qed.