Library MetaCoq.Template.EnvMap

From Coq Require Import ssreflect RelationClasses OrderedTypeAlt FMapAVL FMapFacts.
From MetaCoq.Template Require Import config utils uGraph Reflect BasicAst Kernames String2pos CanonicalTries.
From Equations Require Import Equations.
Import String2pos.


Implicit Types (cf:checker_flags).

Module EnvMap.
  Section Poly.
  Context {A : Type}.

  Definition t := KernameMap.t A.

  Definition empty : t := KernameMap.empty _.

  Definition lookup (k : kername) (env : t) : option A :=
    KernameMap.find k env.

  Definition add (k : kername) (g : A) (env : t) : t :=
    KernameMap.add k g env.

  Definition remove (k : kername) (env : t) : t :=
    KernameMap.remove k env.

  Lemma gso (e : t) kn kn' g : kn ≠ kn' →
    lookup kn (add kn' g e) = lookup kn e.
  Proof using Type.
    intros ne.
    unfold lookup, add.
    rewrite KernameMapFact.F.add_neq_o //.
    intros eq. apply Kername.compare_eq in eq. congruence.
  Qed.

  Lemma gss (e : t) kn kn' g : kn = kn' →
    lookup kn (add kn' g e) = Some g.
  Proof using Type.
    intros eq.
    unfold lookup, add.
    rewrite KernameMapFact.F.add_eq_o //.
    now apply Kername.compare_eq.
  Qed.

  Definition equal (g g' : t) := KernameMap.Equal g g'.

  Lemma unfold_equal g g' : (∀ i, lookup i g = lookup i g') → equal g g'.
  Proof using Type.
    intros heq.
    intros i. apply heq.
  Qed.



  Definition fresh_global (s : kername) (g : list (kername × A)) :=
    Forall (fun g0 : kername × A ⇒ g0.1 ≠ s) g.

  Inductive fresh_globals : list (kername × A) → Prop :=
    | fresh_globals_empty : fresh_globals []
    | fresh_globals_cons kn d g :
      fresh_globals g → fresh_global kn g →
      fresh_globals ((kn, d) :: g).
  Derive Signature for fresh_globals.

  Lemma fold_left_cons d g acc :
    fold_left (fun (genv : t) (decl : kername × A) ⇒ add decl.1 decl.2 genv) (d :: g) acc =
    fold_left (fun (genv : t) (decl : kername × A) ⇒ add decl.1 decl.2 genv) g (add d.1 d.2 acc).
  Proof using Type. reflexivity. Qed.

  Definition of_global_env (g : list (kername × A)) : t :=
    KernameMapFact.of_list g.

  Definition repr (g : list (kername × A)) (e : t) :=
    equal e (of_global_env g).

  Lemma repr_global_env (g : list (kername × A)) : repr g (of_global_env g).
  Proof using Type. red. reflexivity. Qed.

  Lemma of_global_env_cons d g : fresh_globals (d :: g) →
    of_global_env (d :: g) = add d.1 d.2 (of_global_env g).
  Proof using Type.
    unfold of_global_env. simpl. unfold KernameMapFact.uncurry.
    reflexivity.
  Qed.

  Lemma repr_add {cf} {Σ : list (kername × A)} e k g :
    fresh_globals Σ →
    fresh_global k Σ →
    repr Σ e →
    repr ((k, g) :: Σ) (add k g e).
  Proof using Type.
    intros wfΣ fresh repr.
    red. rewrite /add. do 2 red in repr.
    rewrite repr. rewrite of_global_env_cons //.
    constructor ⇒ //.
  Qed.

  Lemma lookup_add k v g : lookup k (add k v g) = Some v.
  Proof using Type. rewrite gss //. Qed.

  Lemma lookup_add_other k k' v g : k ≠ k' → lookup k (add k' v g) = lookup k g.
  Proof using Type. move⇒ eqk. rewrite gso //. Qed.

  Lemma remove_add_eq Σ k v e :
    fresh_globals Σ →
    fresh_global k Σ →
    repr Σ e →
    equal (remove k (add k v e)) e.
  Proof using Type.
    unfold repr, equal, remove, add.
    intros frΣ frk eq.
    intros k'.
    rewrite KernameMapFact.F.remove_o.
    destruct KernameMap.E.eq_dec. eapply Kername.compare_eq in e0. subst k'.
    - rewrite {}eq. induction frk. now cbn.
      rewrite of_global_env_cons //. depelim frΣ. simpl in H0 |- ×.
      rewrite KernameMapFact.F.add_neq_o //. intros c. eapply Kername.compare_eq in c. contradiction.
      now apply IHfrk.
    - rewrite KernameMapFact.F.add_neq_o //.
  Qed.

  Lemma remove_add_o k k' v e :
    k ≠ k' →
    equal (remove k' (add k v e)) (add k v (remove k' e)).
  Proof using Type.
    unfold repr, equal, remove, add.
    intros neq k''.
    rewrite KernameMapFact.F.remove_o.
    destruct KernameMap.E.eq_dec. eapply Kername.compare_eq in e0. subst k'.
    - rewrite KernameMapFact.F.add_neq_o //. intros c. eapply Kername.compare_eq in c. contradiction.
      rewrite KernameMapFact.F.remove_o.
      destruct KernameMap.E.eq_dec ⇒ //.
      elimtype False; apply n. now apply Kername.compare_eq.
    - rewrite !KernameMapFact.F.add_o //.
      destruct (KernameMap.E.eq_dec k k'') ⇒ //.
      rewrite KernameMapFact.F.remove_neq_o //.
  Qed.

  Fixpoint lookup_global (Σ : list (kername × A)) (kn : kername) {struct Σ} : option A :=
    match Σ with
    | [] ⇒ None
    | d :: tl ⇒ if eq_kername kn d.1 then Some d.2 else lookup_global tl kn
    end.

  Lemma lookup_spec (g : list (kername × A)) (e : t) :
    fresh_globals g →
    repr g e →
    ∀ k, lookup k e = lookup_global g k.
  Proof using Type.
    intros wf eq k. red in eq.
    move: eq.
    induction g in e, k, wf |- *; auto.
    - simpl. intros eq.
      unfold lookup.
      rewrite -KernameMapFact.F.not_find_in_iff.
      intros hin.
      red in eq. rewrite eq in hin.
      now eapply KernameMapFact.F.empty_in_iff in hin.
    - cbn -[of_global_env eqb].
      destruct (eqb_spec k a.1).
      × subst.
        rewrite of_global_env_cons //.
        intros he. unfold lookup. rewrite he.
        now rewrite [KernameMap.find _ _]lookup_add.
      × rewrite of_global_env_cons //.
        intros he. unfold lookup. rewrite he.
        rewrite [KernameMap.find _ _]lookup_add_other //.
        apply IHg. now depelim wf.
        reflexivity.
  Qed.
  End Poly.
  Arguments t : clear implicits.
End EnvMap.