text:
Require Import List.
Require Import SepTheoryX PropX.
Require Import PropXTac.
Require Import RelationClasses EqdepClass.
Require Import Expr SepExpr.
Require Import DepList.
Require Import Setoid.
Require Import Tactics.
Require Import Bool Folds.
Require Import Reflection.

Set Implicit Arguments.
Set Strict Implicit.

Require NatMap Multimap.

Module FM := NatMap.IntMap.

Remove Hints FM.Raw.Proofs.L.PX.eqk_refl FM.Raw.Proofs.L.PX.eqk_sym
  FM.Raw.Proofs.L.PX.eqk_trans
  FM.Raw.Proofs.PX.eqk_refl FM.Raw.Proofs.PX.eqk_sym FM.Raw.Proofs.PX.eqk_trans
  FM.Raw.Proofs.L.PX.eqke_refl FM.Raw.Proofs.L.PX.eqke_sym FM.Raw.Proofs.L.PX.eqke_trans
  FM.Raw.Proofs.PX.eqke_refl FM.Raw.Proofs.PX.eqke_sym FM.Raw.Proofs.PX.eqke_trans
  FM.Raw.Proofs.L.PX.MO.lt_eq FM.Raw.Proofs.L.PX.MO.eq_lt FM.Raw.Proofs.L.MX.lt_eq
  FM.Raw.Proofs.L.MX.eq_lt FM.Raw.Proofs.PX.MO.lt_eq FM.Raw.Proofs.PX.MO.eq_lt
  FM.Raw.Proofs.MX.lt_eq FM.Raw.Proofs.MX.eq_lt
  FM.Raw.Proofs.L.PX.eqk_ltk FM.Raw.Proofs.L.PX.ltk_eqk FM.Raw.Proofs.L.PX.ltk_trans
  FM.Raw.Proofs.PX.eqk_ltk FM.Raw.Proofs.PX.ltk_eqk FM.Raw.Proofs.PX.ltk_trans
  FM.Raw.Proofs.L.PX.MO.lt_antirefl
  FM.Raw.Proofs.L.MX.lt_antirefl FM.Raw.Proofs.PX.MO.lt_antirefl FM.Raw.Proofs.MX.lt_antirefl
  FM.Raw.Proofs.L.PX.eqk_not_ltk FM.Raw.Proofs.L.PX.ltk_not_eqke
  FM.Raw.Proofs.L.PX.ltk_not_eqk FM.Raw.Proofs.L.PX.MO.lt_not_gt
  FM.Raw.Proofs.L.PX.MO.eq_not_gt FM.Raw.Proofs.L.PX.MO.eq_neq
  FM.Raw.Proofs.L.PX.MO.neq_eq FM.Raw.Proofs.L.PX.MO.eq_le
  FM.Raw.Proofs.L.PX.MO.le_eq FM.Raw.Proofs.L.PX.MO.eq_not_lt
  FM.Raw.Proofs.L.PX.MO.gt_not_eq FM.Raw.Proofs.L.MX.lt_not_gt
  FM.Raw.Proofs.L.MX.eq_not_gt FM.Raw.Proofs.L.MX.eq_neq
  FM.Raw.Proofs.L.MX.neq_eq FM.Raw.Proofs.L.MX.eq_le
  FM.Raw.Proofs.L.MX.le_eq FM.Raw.Proofs.L.MX.eq_not_lt
  FM.Raw.Proofs.L.MX.gt_not_eq FM.Raw.Proofs.PX.eqk_not_ltk
  FM.Raw.Proofs.PX.ltk_not_eqke FM.Raw.Proofs.PX.ltk_not_eqk
  FM.Raw.Proofs.PX.MO.lt_not_gt FM.Raw.Proofs.PX.MO.eq_not_gt
  FM.Raw.Proofs.PX.MO.eq_neq FM.Raw.Proofs.PX.MO.neq_eq
  FM.Raw.Proofs.PX.MO.eq_le FM.Raw.Proofs.PX.MO.le_eq
  FM.Raw.Proofs.PX.MO.eq_not_lt FM.Raw.Proofs.PX.MO.gt_not_eq
  FM.Raw.Proofs.MX.lt_not_gt FM.Raw.Proofs.MX.eq_not_gt
  FM.Raw.Proofs.MX.eq_neq FM.Raw.Proofs.MX.neq_eq
  FM.Raw.Proofs.MX.eq_le FM.Raw.Proofs.MX.le_eq
  FM.Raw.Proofs.MX.eq_not_lt FM.Raw.Proofs.MX.gt_not_eq
  FM.Raw.Proofs.L.PX.Sort_Inf_NotIn FM.Raw.Proofs.PX.Sort_Inf_NotIn
  FM.Raw.Proofs.L.PX.Inf_eq FM.Raw.Proofs.L.PX.MO.Inf_lt
  FM.Raw.Proofs.L.MX.Inf_lt FM.Raw.Proofs.PX.Inf_eq
  FM.Raw.Proofs.PX.MO.Inf_lt FM.Raw.Proofs.MX.Inf_lt
  FM.Raw.Proofs.L.PX.Inf_lt FM.Raw.Proofs.L.PX.MO.Inf_lt
  FM.Raw.Proofs.L.MX.Inf_lt FM.Raw.Proofs.PX.Inf_lt
  FM.Raw.Proofs.PX.MO.Inf_lt FM.Raw.Proofs.MX.Inf_lt
  FM.Raw.InRight FM.Raw.InLeft FM.Raw.InRoot
  FM.Raw.Proofs.L.PX.InA_eqke_eqk FM.Raw.Proofs.L.PX.MO.In_eq
  FM.Raw.Proofs.L.PX.MO.ListIn_In FM.Raw.Proofs.L.MX.In_eq
  FM.Raw.Proofs.L.MX.ListIn_In FM.Raw.Proofs.PX.InA_eqke_eqk
  FM.Raw.Proofs.PX.MO.In_eq FM.Raw.Proofs.PX.MO.ListIn_In
  FM.Raw.Proofs.MX.In_eq FM.Raw.Proofs.MX.ListIn_In
  FM.Raw.Proofs.L.PX.In_inv_3 FM.Raw.Proofs.PX.In_inv_3
  FM.Raw.Proofs.L.PX.In_inv_2 FM.Raw.Proofs.PX.In_inv_2
  FM.Raw.MapsRight FM.Raw.MapsLeft
  FM.Raw.MapsRoot FM.Raw.Proofs.L.PX.MO.Sort_NoDup
  FM.Raw.Proofs.L.MX.Sort_NoDup FM.Raw.Proofs.PX.MO.Sort_NoDup
  FM.Raw.Proofs.MX.Sort_NoDup
  FM.Raw.BSLeaf FM.Raw.BSNode FM.Raw.Leaf FM.Raw.Node
  FM.E.lt_trans FM.E.lt_not_eq FM.E.eq_refl
  FM.E.eq_sym FM.E.eq_trans.

Module MM := Multimap.Make FM.
Module MF := NatMap.MoreFMapFacts FM.

Module Type SepHeap.
  Declare Module SE : SepExpr.

  Section env.
    Variable types : list type.
    Variable pcType : tvar.
    Variable stateType : tvar.

    Record SHeap : Type :=
    { impures : MM.mmap (exprs types)
    ; pures   : list (expr types)
    ; other   : list (SE.ST.hprop (tvarD types pcType) (tvarD types stateType) nil)
    }.

    Parameter WellTyped_sheap : forall (tf : tfunctions) (tp : SE.tpredicates) (tU tG : tenv) (h : SHeap), bool.

    Parameter WellTyped_impures : forall (tf : tfunctions) (tp : SE.tpredicates) (tU tG : tenv) (imps : MM.mmap (exprs types)), bool.

    (** TODO: What happens if I denote this directly to hprop?
     ** - fewer lemmas about concrete syntax!
     ** - can't re-hash (probably don't want to do this anyways...)
     ** * I think this is Ok for now
     **)
    Parameter sheapD : SHeap -> SE.sexpr types pcType stateType.

    (** Operations on [SHeap]s **)
    Definition SHeap_empty : SHeap :=
      {| impures := MM.empty _
       ; pures := nil
       ; other := nil
       |}.

    Parameter star_SHeap : SHeap -> SHeap -> SHeap.

    Parameter liftSHeap : nat -> nat -> nat -> nat -> SHeap -> SHeap.

    Parameter applySHeap : forall (F : expr types -> expr types) (sh : SHeap), SHeap.

    Axiom applySHeap_defn : forall F sh,
      applySHeap F sh =
      {| impures := MM.mmap_map (map F) (impures sh)
       ; pures := map F (pures sh)
       ; other := other sh
       |}.

    (** Convert an [sexpr] to an [SHeap] **)
    Parameter hash : SE.sexpr types pcType stateType -> variables * SHeap.

    Parameter impuresD : MM.mmap (exprs types) -> SE.sexpr types pcType stateType.

    Parameter starred : forall (T : Type) (F : T -> SE.sexpr types pcType stateType),
      list T -> SE.sexpr types pcType stateType -> SE.sexpr types pcType stateType.

    Section facts.
      Variable funcs : functions types.
      Variable preds : SE.predicates types pcType stateType.
      Variables U G : env types.
      Variable cs : codeSpec (tvarD types pcType) (tvarD types stateType).

      (** Theorems **)
      Axiom hash_denote : forall (s : SE.sexpr types pcType stateType),
        SE.heq funcs preds U G cs s (SE.existsEach (fst (hash s)) (sheapD (snd (hash s)))).

      Axiom star_SHeap_denote : forall s s',
        SE.heq funcs preds U G cs (SE.Star (sheapD s) (sheapD s')) (sheapD (star_SHeap s s')).

      (** Well-typedness **)
      Axiom WellTyped_sheap_eq : forall (tf : tfunctions) (tp : SE.tpredicates) (tU tG : tenv) (h : SHeap),
        WellTyped_sheap tf tp tU tG h =
        WellTyped_impures tf tp tU tG (impures h) && allb (fun e => is_well_typed tf tU tG e tvProp) (pures h).

      Axiom WellTyped_impures_spec_eq : forall tf tp tU tG impures,
        WellTyped_impures tf tp tU tG impures =
        FM.fold (fun p argss acc =>
        acc && match argss , nth_error tp p with
                 | nil , _ => true
                 | _ , None => false
                 | argss , Some ts =>
                   allb (fun args => all2 (is_well_typed tf tU tG) args ts) argss
               end) impures true.

      Axiom WellTyped_impures_eq : forall tf tp tU tG impures,
        WellTyped_impures tf tp tU tG impures = true <->
        (forall k v, FM.find k impures = Some v ->
          match v with
            | nil => True
            | _ => match nth_error tp k with
                     | None => False
                     | Some ts =>
                       allb (fun argss => all2 (is_well_typed tf tU tG) argss ts) v = true
                   end
          end).

      Axiom WellTyped_sheap_star : forall tf tp tU tG h0 h1,
        WellTyped_sheap tf tp tU tG h0 && WellTyped_sheap tf tp tU tG h1 =
        WellTyped_sheap tf tp tU tG (star_SHeap h0 h1).

      Axiom WellTyped_sheap_WellTyped_sexpr : forall tf tp tU tG h,
        WellTyped_sheap tf tp tU tG h = SE.WellTyped_sexpr tf tp tU tG (sheapD h).

      Axiom WellTyped_hash : forall tf tp tU tG (s : SE.sexpr types pcType stateType),
        SE.WellTyped_sexpr tf tp tU tG s =
        WellTyped_sheap tf tp tU (rev (fst (hash s)) ++ tG) (snd (hash s)).

      (** Hash Equations **)
      Axiom hash_Func : forall p args,
        hash (SE.Func p args) = (nil, {| impures := MM.mmap_add p args (MM.empty _)
                                       ; pures   := nil
                                       ; other   := nil
                                       |}).

      (** Definitions **)
      Axiom starred_def : forall (T : Type) (F : T -> SE.sexpr _ _ _) (ls : list T) (base : SE.sexpr _ _ _),
        SE.heq funcs preds U G cs
            (starred F ls base)
            (fold_right (fun x a => SE.Star (F x) a) base ls).

      Axiom starred_base : forall (T : Type) (F : T -> SE.sexpr _ _ _) (ls : list T) (base : SE.sexpr _ _ _),
        SE.heq funcs preds U G cs
            (starred F ls base)
            (SE.Star base (starred F ls SE.Emp)).

      Axiom starred_app : forall (T : Type) (F : T -> SE.sexpr _ _ _) (ls ls' : list T) (base : SE.sexpr _ _ _),
        SE.heq funcs preds U G cs
            (starred F (ls ++ ls') base)
            (starred F ls (starred F ls' base)).

      Axiom starred_perm : forall T L R,
        Permutation.Permutation L R ->
        forall (F : T -> _) base,
          SE.heq funcs preds U G cs (starred F L base) (starred F R base).

      Axiom impuresD_Add : forall f argss i i',
        MM.PROPS.Add f argss i i' ->
        ~FM.In f i ->
        SE.heq funcs preds U G cs
            (impuresD i')
            (SE.Star (starred (SE.Func f) argss SE.Emp) (impuresD i)).

      Axiom impuresD_Empty : forall i,
        FM.Empty i ->
        SE.heq funcs preds U G cs
            (impuresD i) SE.Emp.

      Axiom impuresD_Equiv : forall a b,
        MM.mmap_Equiv a b ->
        SE.heq funcs preds U G cs (impuresD a) (impuresD b).

      Axiom sheapD_def : forall s,
        SE.heq funcs preds U G cs
            (sheapD s)
            (SE.Star (impuresD (impures s))
                     (SE.Star (starred (@SE.Inj _ _ _) (pures s) SE.Emp)
                              (starred (@SE.Const _ _ _) (other s) SE.Emp))).

      (** applySHeap **)
      Axiom applySHeap_wt_spec : forall cs U G U' G' s F,
        (forall e t,
          is_well_typed (typeof_funcs funcs) (typeof_env U) (typeof_env G) e t = true ->
          exprD funcs U G e t = exprD funcs U' G' (F e) t) ->
        WellTyped_sheap (typeof_funcs funcs) (SE.typeof_preds preds) (typeof_env U) (typeof_env G) s = true ->
        SE.ST.heq cs (SE.sexprD funcs preds U G (sheapD s))
                     (SE.sexprD funcs preds U' G' (sheapD (applySHeap F s))).

      Axiom applySHeap_spec : forall cs U G U' G' s F,
        (forall e t,
          exprD funcs U G e t = exprD funcs U' G' (F e) t) ->
        SE.ST.heq cs (SE.sexprD funcs preds U G (sheapD s))
                     (SE.sexprD funcs preds U' G' (sheapD (applySHeap F s))).

      Axiom applySHeap_typed_eq : forall tf tp U G U' G' s F,
        (forall e t,
          is_well_typed tf U G e t = is_well_typed tf U' G' (F e) t) ->
        WellTyped_sheap tf tp U G s = WellTyped_sheap tf tp U' G' (applySHeap F s).

      Axiom applySHeap_typed_impl : forall tf tp U G U' G' s F,
        (forall e t,
          is_well_typed tf U G e t = true ->
          is_well_typed tf U' G' (F e) t = true) ->
        WellTyped_sheap tf tp U G s = true ->
        WellTyped_sheap tf tp U' G' (applySHeap F s) = true.

    End facts.
  End env.
End SepHeap.

Module Make (SE : SepExpr) <: SepHeap with Module SE := SE.
  Module Import SE := SE.
  Module ST := SE.ST.

  Module Import SE_FACTS := SepExpr.SepExprFacts SE.

  Section env.
    Variable types : list type.
    Variable pcType : tvar.
    Variable stateType : tvar.

    Variable funcs : functions types.
    Variable preds : predicates types pcType stateType.

    (** A more efficient representation for sexprs. **)
    Record SHeap : Type :=
    { impures : MM.mmap (exprs types)
    ; pures   : list (expr types)
    ; other   : list (ST.hprop (tvarD types pcType) (tvarD types stateType) nil)
    }.

    Definition SHeap_empty : SHeap :=
      {| impures := @MM.empty _
       ; pures   := nil
       ; other   := nil
       |}.

    Existing Instance himp_rel_relation.
    Existing Instance heq_rel_relation.
    Hint Rewrite heq_star_emp_l heq_star_emp_r : hprop.

    Theorem ST_himp_himp : forall (U G : env types) cs L R,
      SE.himp funcs preds U G cs L R ->
      ST.himp cs (sexprD funcs preds U G L) (sexprD funcs preds U G R).
    Proof.
      clear. auto.
    Qed.

    Theorem ST_heq_heq : forall (U G : env types) cs L R,
      heq funcs preds U G cs L R ->
      ST.heq cs (sexprD funcs preds U G L) (sexprD funcs preds U G R).
    Proof.
      clear. auto.
    Qed.

    (** sexprD (U ++ U') (G ++ G') s =
     ** sexprD (U ++ U'' ++ U') (G ++ G'' ++ G') (liftSHeap (length U) (length U'') (length G) (length G'') s)
     **)
    Definition liftSHeap (ua ub : nat) (a b : nat) (s : SHeap) : SHeap :=
      {| impures := MM.mmap_map (map (liftExpr ua ub a b)) (impures s)
       ; pures   := map (liftExpr ua ub a b) (pures s)
       ; other   := other s
       |}.

    Fixpoint star_SHeap (l r : SHeap) : SHeap :=
      {| impures := MM.mmap_join (impures l) (impures r)
       ; pures := pures l ++ pures r
       ; other := other l ++ other r
       |}.

    Fixpoint hash (s : sexpr types pcType stateType) : ( variables * SHeap ) :=
      match s with
        | Emp => (nil, SHeap_empty)
        | Inj p => (nil,
          {| impures := MM.empty _
           ; pures := p :: nil
           ; other := nil
           |})
        | Star l r =>
          let (vl, hl) := hash l in
          let (vr, hr) := hash r in
          let nr := length vr in
          (vl ++ vr,
            star_SHeap (liftSHeap 0 0 0 nr hl) (liftSHeap 0 0 nr (length vl) hr))
        | Exists t b =>
          let (v, b) := hash b in
          (t :: v, b)
        | Func f a =>
          (nil,
           {| impures := MM.mmap_add f a (MM.empty _)
            ; pures := nil
            ; other := nil
           |})
        | Const c =>
          (@nil tvar,
           {| impures := MM.empty _
            ; pures := @nil (expr types)
            ; other := c :: nil
            |})
      end.

    Definition starred (T : Type) (F : T -> sexpr types pcType stateType) (ls : list T) (base : sexpr _ _ _)
      : sexpr _ _ _ :=
      fold_right (fun x a => match a with
                               | Emp => F x
                               | _ => Star (F x) a
                             end) base ls.

    Definition sheapD (h : SHeap) : sexpr types pcType stateType :=
      let a := starred (@Const _ _ _) (other h) Emp in
      let a := starred (@Inj _ _ _) (pures h) a in
      let a := FM.fold (fun k => starred (Func k)) (impures h) a in
      a.

    Definition WellTyped_impures (tf : tfunctions) (tp : tpredicates) (tU tG : tenv) (imps : MM.mmap (exprs types)) : bool :=
      FM.fold (fun p argss acc =>
        acc && match argss , nth_error tp p with
                 | nil , _ => true
                 | _ , None => false
                 | argss , Some ts =>
                   allb (fun args => all2 (is_well_typed tf tU tG) args ts) argss
               end) imps true.

    Theorem WellTyped_impures_spec_eq : forall tf tp tU tG impures,
        WellTyped_impures tf tp tU tG impures =
        FM.fold (fun p argss acc =>
        acc && match argss , nth_error tp p with
                 | nil , _ => true
                 | _ , None => false
                 | argss , Some ts =>
                   allb (fun args => all2 (is_well_typed tf tU tG) args ts) argss
               end) impures true.
    Proof. reflexivity. Qed.

    Definition WellTyped_sheap (tf : tfunctions) (tp : tpredicates) (tU tG : tenv) (h : SHeap) : bool :=
      WellTyped_impures tf tp tU tG (impures h) && allb (fun e => is_well_typed tf tU tG e tvProp) (pures h).

    Theorem WellTyped_sheap_eq : forall (tf : tfunctions) (tp : SE.tpredicates) (tU tG : tenv) (h : SHeap),
      WellTyped_sheap tf tp tU tG h =
      WellTyped_impures tf tp tU tG (impures h) &&
      allb (fun e => is_well_typed tf tU tG e tvProp) (pures h).
    Proof.
      clear. reflexivity.
    Qed.

    Lemma starred_const_well_typed : forall tf tp tU tG e x,
      WellTyped_sexpr tf tp tU tG (starred (@Const _ _ _) x e) = WellTyped_sexpr tf tp tU tG e.
    Proof.
      clear. induction x; simpl; intros; auto.
      destruct (starred (Const (stateType:=stateType)) x e); auto.
    Qed.

    Lemma starred_pures_well_typed : forall tf tp tU tG e x,
      WellTyped_sexpr tf tp tU tG (starred (@Inj _ _ _) x e) =
      allb (fun e => is_well_typed tf tU tG e tvProp) x && WellTyped_sexpr tf tp tU tG e.
    Proof.
      clear. induction x; simpl; intros; auto.
      consider (is_well_typed tf tU tG a tvProp); intros;
      destruct (starred (Inj (stateType:=stateType)) x e); simpl in *; think; auto.
      rewrite <- IHx. auto.
    Qed.

    Lemma starred_funcs_well_typed : forall tf tp tU tG p,
      forall e x,
      WellTyped_sexpr tf tp tU tG (starred (@Func _ _ _ p) x e) =
      match x , nth_error tp p with
        | nil , _ => true
        | _ , None => false
        | x , Some ts =>
          allb (fun args => all2 (is_well_typed tf tU tG) args ts) x
      end && WellTyped_sexpr tf tp tU tG e.
    Proof.
      clear. induction x; simpl; intros; auto.
      destruct x; simpl in *.
      { destruct e; simpl;
          repeat match goal with
                   | [ |- context [ nth_error ?a ?b ] ] => destruct (nth_error a b)
                   | [ |- context [ all2 ?a ?b ?c ] ] => destruct (all2 a b c)
                 end; auto. }
      { repeat (simpl in *;
        match goal with
          | [ |- context [ match ?X with _ => _ end ] ] => destruct X
        end); auto. }
    Qed.

    Theorem WellTyped_sheap_WellTyped_sexpr : forall tf tp tU tG h,
      WellTyped_sheap tf tp tU tG h = SE.WellTyped_sexpr tf tp tU tG (sheapD h).
    Proof.
      clear. intros. destruct h. unfold WellTyped_sheap, WellTyped_impures, sheapD; simpl.
      eapply MF.PROPS.fold_rec with (m := impures0); intros; simpl.
      { rewrite NatMap.IntMapProperties.fold_Empty; eauto with typeclass_instances.
        rewrite starred_pures_well_typed. rewrite starred_const_well_typed. simpl.
        symmetry; apply andb_true_r. }
      { rewrite NatMap.IntMapProperties.fold_Add with (eqA := fun x y => WellTyped_sexpr tf tp tU tG x = WellTyped_sexpr tf tp tU tG y). 5: eauto. 5: eauto.
        destruct e. simpl. rewrite andb_true_r. eauto.
        rewrite starred_funcs_well_typed. rewrite <- H2.
        rewrite andb_comm. rewrite andb_assoc. rewrite andb_assoc. rewrite andb_comm.
        repeat rewrite <- andb_assoc. f_equal. apply andb_comm.

        { clear; econstructor; auto. red. intros; think. auto. }
        { clear. repeat red; intros; subst. induction y0; simpl; intros; auto.
          consider (starred (Func y) y0 x1);
          consider (starred (Func y) y0 y1); intros; simpl in *; think;
            repeat match goal with
                     | [ |- context [ nth_error ?X ?Y ] ] => destruct (nth_error X Y)
                     | [ H : true = _ |- _ ] => rewrite <- H
                     | [ H : false = _ |- _ ] => rewrite <- H
                   end; auto using andb_true_r. }
        { clear. repeat (red; intros; subst).
          repeat rewrite starred_funcs_well_typed. destruct e; destruct e'; auto.
          generalize (l :: e); generalize (l0 :: e'). intros.
          destruct (nth_error tp k); destruct (nth_error tp k'); auto.
          rewrite andb_comm. rewrite <- andb_assoc. f_equal. apply andb_comm.
          rewrite andb_false_r. auto.
          rewrite andb_false_r; auto. } }
    Qed.

    Definition sheapD' (h : SHeap) : sexpr types pcType stateType :=
      Star (FM.fold (fun k => starred (Func k)) (impures h) Emp)
           (Star (starred (@Inj _ _ _) (pures h) Emp)
                 (starred (@Const _ _ _) (other h) Emp)).

    Definition impuresD (imp : MM.mmap (exprs types)) : sexpr types pcType stateType :=
      FM.fold (fun k ls acc =>
        Star (starred (Func k) ls Emp) acc) imp Emp.

    Section with_envs.
      Variables U G : env types.
      Variable cs : codeSpec (tvarD types pcType) (tvarD types stateType).

      Local Notation "a '<===>' b" := (heq funcs preds U G cs a b) (at level 60, only parsing).

      Theorem starred_def : forall (T : Type) (F : T -> SE.sexpr _ _ _) (ls : list T) (base : SE.sexpr _ _ _),
        (starred F ls base) <===>
        (fold_right (fun x a => SE.Star (F x) a) base ls).
      Proof.
        induction ls; simpl; intros.
          reflexivity.
          specialize (IHls base). revert IHls.
          case_eq (starred F ls base); intros;
            rewrite <- IHls; heq_canceler.
      Qed.

      Theorem starred_base : forall T F ls base,
        (@starred T F ls base) <===> (SE.Star base (@starred T F ls Emp)).
      Proof.
        intros. repeat rewrite starred_def.
        revert base. induction ls; simpl in *; intros.
          heq_canceler.
          rewrite IHls. heq_canceler.
      Qed.

      Ltac heq_canceler :=
        repeat match goal with
                 | [ H : SE.heq _ _ _ _ _ _ _ |- _ ] => rewrite H
                 | [ |- context [ starred ?F ?L ?B ] ] =>
                   match B with
                     | SE.Emp => fail 1
                     | _ => rewrite (@starred_base _ F L B)
                   end
               end;
        SE_FACTS.heq_canceler.

      Global Add Parametric Morphism : (fun k0 : nat => starred (Func k0)) with
        signature (eq ==> eq ==> heq funcs preds U G cs ==> heq funcs preds U G cs)
        as star_himp_mor'.
      Proof.
        intros. repeat rewrite starred_def.
        revert H. revert x; revert y1.
        induction y0; unfold heq in *; simpl in *; intros; try eauto.
        rewrite IHy0; eauto. heq_canceler.
      Qed.

      Lemma transpose_neqkey_starred : NatMap.IntMapProperties.transpose_neqkey (SE.heq funcs preds U G cs)
        (fun k0 : nat => starred (Func k0)).
      Proof.
        red. intros. rewrite starred_base. symmetry.
        rewrite starred_base. repeat rewrite starred_base with (base := a).
        heq_canceler.
      Qed.
      Lemma transpose_neqkey_Star (X : Type) F : NatMap.IntMapProperties.transpose_neqkey (heq funcs preds U G cs)
        (fun (k0 : nat) (ls : X) (a1 : sexpr types _ _) => Star (F k0 ls) a1).
      Proof.
        red. intros. heq_canceler.
      Qed.

      Hint Resolve transpose_neqkey_starred transpose_neqkey_Star : hprop.
      Hint Extern 1 (Morphisms.Proper _ _) =>
        (unfold Morphisms.Proper, Morphisms.respectful; intros; subst;
          repeat match goal with
                   | [ H : heq _ _ _ _ _ _ _ |- _ ] => rewrite H
                 end; reflexivity) : hprop.
      Hint Extern 1 (MM.PROPS.transpose_neqkey _ _) =>
        (clear; red; intros; subst; repeat rewrite MM.FACTS.add_o;
          repeat match goal with
                   | [ |- context [ FM.E.eq_dec ?X ?Y ] ] =>
                     destruct (FM.E.eq_dec X Y)
                   | [ H : FM.E.eq ?X ?Y |- _ ] => rewrite H in *
                 end; solve [ auto | exfalso; auto | heq_canceler ]) : hprop.

      Theorem impuresD_Add : forall f argss i i',
        MM.PROPS.Add f argss i i' ->
        ~FM.In f i ->
        SE.heq funcs preds U G cs
          (impuresD i')
          (SE.Star (starred (SE.Func f) argss SE.Emp) (impuresD i)).
      Proof.
        unfold impuresD; intros.
        rewrite MM.PROPS.fold_Add; eauto with typeclass_instances hprop.
          heq_canceler.
      Qed.

      Theorem impuresD_Empty : forall i,
        FM.Empty i ->
        SE.heq funcs preds U G cs (impuresD i) SE.Emp.
      Proof.
        unfold impuresD; intros.
        rewrite MM.PROPS.fold_Empty; eauto with typeclass_instances. heq_canceler.
      Qed.

      Theorem sheapD_def : forall s,
        SE.heq funcs preds U G cs
          (sheapD s)
          (SE.Star (impuresD (impures s))
                   (SE.Star (starred (@SE.Inj _ _ _) (pures s) SE.Emp)
                            (starred (@SE.Const _ _ _) (other s) SE.Emp))).
      Proof.
        intros; unfold sheapD.
        eapply MM.PROPS.fold_rec; intros.
          rewrite impuresD_Empty; eauto. heq_canceler.
          rewrite impuresD_Add; eauto. heq_canceler.
      Qed.

      Lemma sheapD_sheapD' : forall h,
        sheapD h <===> sheapD' h.
      Proof.
        destruct h. rewrite sheapD_def; unfold sheapD', impuresD; simpl.
        repeat eapply heq_star_frame; try reflexivity.
        generalize (@Emp types pcType stateType) at 2 3.
        clear. intros. eapply MM.PROPS.fold_rec with (m := impures0); intros.
          rewrite MM.PROPS.fold_Empty; eauto with typeclass_instances hprop. reflexivity.

          rewrite MM.PROPS.fold_Add; eauto with typeclass_instances hprop.
            rewrite H2. heq_canceler.
      Qed.

      Lemma starred_In : forall T (F : T -> sexpr _ _ _) x ls' b ls,
        (starred F (ls ++ x :: ls') b) <===> (Star (starred F (ls ++ ls') b) (F x)).
      Proof.
        intros. repeat rewrite starred_def. revert b.
        induction ls; intros; simpl; heq_canceler.
          rewrite IHls. heq_canceler.
      Qed.

      Lemma sheapD_pures : forall stn sm h,
        ST.satisfies cs (sexprD funcs preds U G (sheapD h)) stn sm ->
        AllProvable funcs U G (pures h).
      Proof.
        intros. eapply ST.satisfies_himp in H.
        Focus 2. rewrite sheapD_def. rewrite starred_def. reflexivity.
        simpl in *.

        repeat match goal with
                 | [ H : exists x, _ |- _ ] => destruct H
                 | [ H : ST.satisfies _ (ST.star _ _) _ _ |- _ ] =>
                   apply ST.satisfies_star in H
                 | [ H : _ /\ _ |- _ ] => destruct H
               end.
        revert H2; clear. revert x1.
        induction (pures h); simpl; auto.
        unfold Provable. destruct (exprD funcs U G a tvProp); intros; unfold BadInj in *;
        repeat match goal with
                 | [ H : exists x, _ |- _ ] => destruct H
                 | [ H : ST.satisfies _ (ST.star _ _) _ _ |- _ ] =>
                   apply ST.satisfies_star in H
                 | [ H : ST.satisfies _ (ST.inj _) _ _ |- _ ] =>
                   apply ST.satisfies_pure in H
                 | [ H : _ /\ _ |- _ ] => destruct H
                 | [ |- _ /\ _ ] => split
                 | [ |- _ ] => propxFo
               end; eauto.
      Qed.

      Lemma sheapD_pull_impure : forall h f argss,
        FM.find f (impures h) = Some argss ->
        (sheapD h) <===>
        (Star (sheapD {| impures := FM.remove f (impures h)
          ; pures   := pures h
          ; other   := other h |})
        (starred (Func f) argss Emp)).
      Proof.
        intros. repeat rewrite sheapD_def. simpl.
        rewrite impuresD_Add with (f := f) (argss := argss) (i := FM.remove f (impures h)).
        heq_canceler.
        unfold MM.PROPS.Add; intros; repeat rewrite MM.FACTS.add_o; repeat rewrite MM.FACTS.remove_o.
        destruct (FM.E.eq_dec f y); subst; auto.
        apply FM.remove_1; auto.
      Qed.

      Lemma fold_starred : forall X (F : nat -> X -> sexpr _ _ _) m b,
        (FM.fold (fun k ls a => Star (F k ls) a) m b) <===>
        (Star (FM.fold (fun k ls a => Star (F k ls) a) m Emp) b).
      Proof.
        do 2 intro.
        intro. apply NatMap.IntMapProperties.fold_rec with (m := m).
          intros. rewrite NatMap.IntMapProperties.fold_Empty; eauto with typeclass_instances.
          autorewrite with hprop. reflexivity.

          intros. erewrite MM.PROPS.fold_Add; eauto with typeclass_instances hprop.
          rewrite H2. heq_canceler.
      Qed.

      Theorem starred_app : forall T (F : T -> _) a b B,
        (starred F (a ++ b) B) <===> (starred F a (starred F b B)).
      Proof.
        intros; repeat rewrite starred_def.
        induction a; simpl; intros; repeat rewrite starred_def; try reflexivity.
        rewrite IHa. reflexivity.
      Qed.

      Theorem starred_perm : forall T L R,
        Permutation.Permutation L R ->
        forall (F : T -> _) base,
          (starred F L base) <===> (starred F R base).
      Proof.
        clear. intros.
        repeat rewrite starred_def.
        induction H; simpl; intros;
          repeat match goal with
                   | [ H : _ |- _ ] => rewrite H
                 end; try reflexivity; heq_canceler.
      Qed.

      Theorem impuresD_Equiv : forall a b,
        MM.mmap_Equiv a b ->
        (impuresD a) <===> (impuresD b).
      Proof.
        intro. eapply MM.PROPS.map_induction with (m := a); intros.
        { repeat rewrite impuresD_Empty; auto. reflexivity.
          apply MF.find_empty_iff. intros.
          destruct H0.
          specialize (H0 k).
          eapply MF.find_empty_iff with (k := k) in H.
          apply MM.FACTS.not_find_mapsto_iff.
          intro. apply H0 in H2. apply MM.FACTS.not_find_mapsto_iff in H. auto. }
        { generalize (@MF.Equiv_Add _ _ _ _ _ _ _ H2 H0 H1); intro.
          do 2 destruct H3. intuition.
          repeat rewrite impuresD_Add by eauto. symmetry.
          repeat rewrite impuresD_Add by eauto. symmetry.
          rewrite H; eauto. rewrite starred_perm; eauto. heq_canceler. }
      Qed.

      Lemma multimap_join_star : forall
        (impures0 impures1 : MM.mmap (exprs types)) B,
        (FM.fold
          (fun (k : nat) (ls : list (exprs types)) acc =>
            Star (starred (Func k) ls Emp) acc)
          (MM.mmap_join impures0 impures1) B)
        <===>
        (FM.fold
          (fun (k : nat) (ls : list (exprs types)) acc =>
            Star (starred (Func k) ls Emp) acc) impures0
          (FM.fold
            (fun (k : nat) (ls : list (exprs types)) acc =>
              Star (starred (Func k) ls Emp) acc) impures1 B)).
      Proof.
        unfold MM.mmap_join.
        intro. apply NatMap.IntMapProperties.map_induction with (m := impures0).
        * intros.
          repeat rewrite NatMap.IntMapProperties.fold_Empty with (m := m); eauto with typeclass_instances.
          reflexivity.

        * intros.
          generalize (@NatMap.IntMapProperties.fold_Add (list (exprs types)) _ (@FM.Equal (list (exprs types)))).
          intro.
          rewrite NatMap.IntMapProperties.fold_Equal; try solve [ clear; eauto with typeclass_instances ].
          4: eapply H2; eauto with typeclass_instances.
          clear H2. simpl in *.
          unfold exprs, MM.mmap_extend; simpl in *.
          match goal with
            | [ |- context [ FM.find ?x ?y ] ] => remember y
          end.
          case_eq (FM.find x t); intros.
          { subst.
            rewrite NatMap.IntMapProperties.fold_Equal; eauto with typeclass_instances.
            4: eapply MF.add_remove_Equal.
            symmetry.
            rewrite NatMap.IntMapProperties.fold_Add.
            6: eassumption.
            5: eauto.
            2: eauto with typeclass_instances.
            rewrite fold_starred.
            rewrite NatMap.IntMapProperties.fold_Add with (m2 := impures1).
            2: eauto with typeclass_instances.
            instantiate (3 := x). instantiate (2 := l).
            instantiate (1 := FM.remove x impures1).
            rewrite NatMap.IntMapProperties.fold_add.
            rewrite starred_app. heq_canceler.

            generalize (@MM.mmap_join_remove_acc _ x m impures1 H0). unfold MM.mmap_join. intro.
            symmetry. rewrite NatMap.IntMapProperties.fold_Equal.
            5: eapply H3. clear H3.
            rewrite H. rewrite fold_starred with (b := FM.fold _ _ _). heq_canceler. eauto with typeclass_instances.

            solve [ clear; eauto with typeclass_instances hprop ].

            solve [ clear; eauto with typeclass_instances hprop ].
            solve [ clear; eauto with typeclass_instances hprop ].
            solve [ clear; eauto with typeclass_instances hprop ].
            solve [ clear; eauto with typeclass_instances hprop ].
            apply FM.remove_1; auto.
            solve [ clear; eauto with typeclass_instances hprop ].
            solve [ clear; eauto with typeclass_instances hprop ].
            apply FM.remove_1; auto.

            {
              generalize MM.mmap_join_o.
              unfold MM.mmap_join. intros. unfold MM.mmap_extend in H3. rewrite H3 in H2; auto.
              apply MM.PROPS.F.not_find_in_iff in H0. unfold exprs in H0. rewrite H0 in H2.

              revert H2; clear; intros.
              unfold NatMap.IntMapProperties.Add; intros.
                repeat (rewrite NatMap.IntMapFacts.add_o || rewrite NatMap.IntMapFacts.remove_o).
                destruct (NatMap.Ordered_nat.eq_dec x y); subst; auto.
            }

            solve [ clear; eauto with typeclass_instances hprop ].
            solve [ clear; eauto with typeclass_instances hprop ].
            solve [ clear; eauto with typeclass_instances hprop ].
            solve [ clear; eauto with typeclass_instances hprop ].
        }
        { subst.
          rewrite NatMap.IntMapProperties.fold_add; eauto with typeclass_instances.
          rewrite H. symmetry. rewrite fold_starred.
          rewrite NatMap.IntMapProperties.fold_Add; eauto with typeclass_instances.
          symmetry. rewrite fold_starred with (b := FM.fold _ _ _). heq_canceler.

          repeat (red; intros; subst). rewrite H3. heq_canceler.
          red; intros; heq_canceler.
          repeat (red; intros; subst). rewrite H3; heq_canceler.
          red; intros; heq_canceler.
          intro.
          apply NatMap.IntMapProperties.F.in_find_iff in H3. auto.
        }
        eauto with typeclass_instances.
        solve [ clear; eauto with typeclass_instances hprop ].
        solve [ clear; eauto with typeclass_instances hprop ].
        clear; repeat (red; intros; subst). unfold MM.mmap_extend. rewrite H.
          destruct (FM.find (elt:=list (exprs types)) y y1); try rewrite H; reflexivity.

        eapply MM.transpose_neqkey_mmap_extend.
      Qed.

      Lemma star_SHeap_denote : forall s1 s2,
        (Star (sheapD s1) (sheapD s2)) <===> (sheapD (star_SHeap s1 s2)).
      Proof.
        intros. symmetry. repeat rewrite sheapD_def.
        destruct s1; destruct s2; intros; simpl; unfold star_SHeap; simpl.
        match goal with
          | [ |- heq _ _ _ _ _ _ (Star (Star ?FL (Star ?PL ?OL)) (Star ?FR (Star ?PR ?OR))) ] =>
            transitivity (Star (Star FL FR) (Star (Star PL PR) (Star OL OR)))
        end.
        repeat rewrite starred_app.
        unfold impuresD.
        rewrite multimap_join_star; auto. heq_canceler.
        rewrite <- fold_starred. heq_canceler.

        heq_canceler.
      Qed.

    End with_envs.

    Ltac heq_canceler :=
        repeat match goal with
                 | [ H : SE.heq _ _ _ _ _ _ _ |- _ ] => rewrite H
                 | [ |- context [ starred ?F ?L ?B ] ] =>
                   match B with
                     | SE.Emp => fail 1
                     | _ => rewrite (@starred_base _ _ _ _ F L B)
                   end
               end;
        SE_FACTS.heq_canceler.

    Hint Resolve transpose_neqkey_starred transpose_neqkey_Star : hprop.
    Hint Extern 1 (Morphisms.Proper _ _) =>
      (unfold Morphisms.Proper, Morphisms.respectful; intros; subst;
        repeat match goal with
                 | [ H : heq _ _ _ _ _ _ _ |- _ ] => rewrite H
               end; reflexivity) : hprop.
    Hint Extern 1 (MM.PROPS.transpose_neqkey _ _) =>
      (clear; red; intros; subst; repeat rewrite MM.FACTS.add_o;
        repeat match goal with
                 | [ |- context [ FM.E.eq_dec ?X ?Y ] ] =>
                   destruct (FM.E.eq_dec X Y)
                 | [ H : FM.E.eq ?X ?Y |- _ ] => rewrite H in *
               end; solve [ auto | exfalso; auto | heq_canceler ]) : hprop.

    Lemma heq_ex : forall U G cs t P Q,
      (forall v : tvarD types t, heq funcs preds U (existT (tvarD types) t v :: G) cs P Q) ->
      heq funcs preds U G cs (Exists t P) (Exists t Q).
    Proof.
      unfold heq; simpl; intros; apply ST.heq_ex; auto.
    Qed.

    Lemma heq_existsEach : forall cs X v Y (P Q : sexpr types pcType stateType),
      (forall Z, map (@projT1 _ _) Z = rev v -> heq funcs preds X (Z ++ Y) cs P Q) ->
      heq funcs preds X Y cs (existsEach v P) (existsEach v Q).
    Proof.
      induction v; simpl; intros.
        specialize (H nil); simpl in *; auto.

        apply heq_ex. intros. eapply IHv. intros.
        simpl. specialize (H (Z ++ @existT _ _ _ v0 :: nil)). rewrite map_app in *.
        rewrite H0 in *. simpl in *.
        rewrite app_ass in *. simpl in *. auto.
    Qed.

    Lemma existsEach_app : forall X cs b a Y (P : sexpr _ _ _),
      heq funcs preds X Y cs (existsEach a (existsEach b P)) (existsEach (a ++ b) P).
    Proof.
      induction a; simpl.
      reflexivity.
      intros. apply heq_ex; intros. apply IHa.
    Qed.

    Lemma star_pull_exists : forall EG cs a G s s2,
      heq funcs preds EG G cs (Star (Exists a s) s2) (Exists a (Star s (liftSExpr 0 0 0 1 s2))).
    Proof.
      intros. unfold heq. simpl. rewrite ST.heq_ex_star. apply ST.heq_ex. intros.
      apply ST.heq_star_cancel.
       apply (liftSExpr_sexprD funcs preds cs s2 nil EG nil nil G (existT _ a v :: nil)).
    Qed.

    Lemma star_pull_existsEach : forall EG cs v G s s2,
      heq funcs preds EG G cs (Star (existsEach v s) s2)
                              (existsEach v (Star s (liftSExpr 0 0 0 (length v) s2))).
    Proof.
      induction v; simpl.
        intros; rewrite liftSExpr_0. reflexivity.

        intros.
        rewrite star_pull_exists. apply heq_ex. intros.
        rewrite IHv.

        rewrite liftSExpr_combine. reflexivity.
    Qed.

    Lemma starred_liftSExpr : forall F ua ub a b (ls : exprs types) base,
      (forall a0, liftSExpr ua ub a b (F a0) = F (liftExpr ua ub a b a0)) ->
      liftSExpr ua ub a b (starred F ls base) = starred F (map (liftExpr ua ub a b) ls) (liftSExpr ua ub a b base).
    Proof.
      induction ls; simpl; intros; try reflexivity.
      case_eq (starred F ls base); intros;
        rewrite <- IHls; repeat rewrite H0; simpl; repeat rewrite H; simpl; eauto.
    Qed.

    Lemma liftSExpr_existsEach : forall EG cs v0 s G n v,
      heq funcs preds EG G cs
        (liftSExpr 0 0 n v (existsEach v0 s))
        (existsEach v0 (liftSExpr 0 0 (n + length v0) v s)).
    Proof.
      induction v0; simpl; intros.
        intros. rewrite Plus.plus_0_r. reflexivity.

        apply heq_ex; intros. rewrite IHv0. cutrewrite (S n + length v0 = n + S (length v0)); try reflexivity; omega.
    Qed.

    Lemma skipn_skipn : forall T a (ls : list T) b,
      skipn b (skipn a ls) = skipn (b + a) ls.
    Proof.
      clear; induction a; simpl; intros.
        rewrite Plus.plus_0_r. auto.
        rewrite Plus.plus_comm. simpl. destruct ls; auto. destruct b; auto.
        rewrite IHa. rewrite Plus.plus_comm. auto.
    Qed.

    Lemma heq_liftSExpr : forall cs EG G G' G'' P Q,
      heq funcs preds EG (G ++ G'') cs P Q ->
      heq funcs preds EG (G ++ G' ++ G'') cs (liftSExpr 0 0 (length G) (length G') P) (liftSExpr 0 0 (length G) (length G') Q).
    Proof.
      unfold heq; intros.
      generalize (liftSExpr_sexprD funcs preds cs P nil EG nil). simpl in *.
      generalize (liftSExpr_sexprD funcs preds cs Q nil EG nil). simpl in *. intros.
      etransitivity. symmetry. eapply H1. rewrite H. eauto.
    Qed.

    Lemma sheapD_sexprD_liftVars : forall EG cs s G G' G'',
      heq funcs preds EG (G ++ G' ++ G'') cs
        (liftSExpr 0 0 (length G) (length G') (sheapD' s))
        (sheapD' (liftSHeap 0 0 (length G) (length G') s)).
    Proof.
      destruct s; unfold liftSHeap, sheapD'; simpl; intros; repeat apply heq_star_frame; intros.
      { clear. change Emp with (liftSExpr 0 0 (length G) (length G') (@Emp types pcType stateType)) at 2.
        generalize (@Emp types pcType stateType).
        unfold MM.mmap_map. intros. rewrite MF.fold_map_fusion; eauto with typeclass_instances.
        { revert s.
          apply NatMap.IntMapProperties.map_induction with (m := impures0); intros.
          repeat (rewrite MM.PROPS.fold_Empty; eauto with typeclass_instances). reflexivity.

          symmetry. rewrite MM.PROPS.fold_Add. 6: eauto. 5: eauto. 2: eauto with typeclass_instances.
          rewrite starred_base. rewrite <- H. clear H.
          assert (forall base, heq funcs preds EG (G ++ G' ++ G'') cs
            (starred (Func x) (map (map (liftExpr 0 0 (length G) (length G'))) e) (liftSExpr 0 0 (length G) (length G') base))
            (liftSExpr 0 0 (length G) (length G') (starred (Func x) e base))).
          { clear.
            induction e; intros; try reflexivity. rewrite starred_def. simpl. rewrite <- starred_def.
            rewrite IHe. solve [ destruct (starred (Func x) e base); simpl; heq_canceler ]. }
          rewrite H with (base := Emp).
          change (Star
            (liftSExpr 0 0 (length G) (length G')
              (FM.fold
                (fun (k : FM.key) => starred (Func k)) m s))
            (liftSExpr 0 0 (length G) (length G') (starred (Func x) e Emp)))
            with (liftSExpr 0 0 (length G) (length G')
              (Star
                (FM.fold
                  (fun (k : FM.key) => starred (Func k)) m s)
                (starred (Func x) e Emp))).
          eapply heq_liftSExpr.

          symmetry.
          rewrite MM.PROPS.fold_Add. 6: eauto. rewrite <- starred_base. reflexivity.
          eauto with typeclass_instances hprop.
          eauto with typeclass_instances hprop.
          clear; red; intros; subst; repeat rewrite MM.FACTS.add_o;
            repeat match goal with
                     | [ |- context [ FM.E.eq_dec ?X ?Y ] ] =>
                       destruct (FM.E.eq_dec X Y)
                     | [ H : FM.E.eq ?X ?Y |- _ ] => rewrite H in *
                   end; auto.
          heq_canceler.
          eauto with typeclass_instances hprop.
          clear; do 4 (red; intros; subst); heq_canceler.

          clear; red; intros; subst; repeat rewrite MM.FACTS.add_o.
          heq_canceler. }
          eapply transpose_neqkey_starred. }

        Opaque starred.
        { symmetry. rewrite starred_def. induction pures0; try reflexivity.
          simpl. rewrite IHpures0.
          match goal with
            | [ |- heq _ _ _ _ _ ?X _ ] =>
              change X with
                (liftSExpr 0 0 (length G) (length G') (Star (Inj a) (starred (@Inj types pcType stateType) pures0 Emp)))
          end.
          apply heq_liftSExpr. symmetry. repeat rewrite starred_def. simpl. heq_canceler. }

        { symmetry. etransitivity. rewrite starred_def. reflexivity. induction other0; try reflexivity.
          simpl. rewrite IHother0.
          match goal with
            | [ |- heq _ _ _ _ _ ?X _ ] =>
              change X with
                (liftSExpr 0 0 (length G) (length G') (Star (Const a) (starred (@Const types pcType stateType) other0 Emp)))
          end.
          apply heq_liftSExpr. symmetry. repeat rewrite starred_def. simpl. reflexivity. }
    Qed.

    Lemma hash_denote' : forall EG cs (s : sexpr _ _ _) G,
      heq funcs preds EG G cs s (existsEach (fst (hash s)) (sheapD' (snd (hash s)))).
    Proof.
      Opaque star_SHeap.
      induction s; simpl; try solve [ unfold sheapD'; simpl; intros; repeat (rewrite heq_star_emp_r || rewrite heq_star_emp_l); reflexivity ].
      { (** Star **)
        intros. rewrite IHs1 at 1. intros.
        destruct (hash s1); destruct (hash s2); simpl in *.
        rewrite IHs2.
        rewrite <- (@existsEach_app EG cs) with (Y := G).
        rewrite star_pull_existsEach. apply heq_existsEach. intros.
        rewrite heq_star_comm.

        rewrite liftSExpr_existsEach.
        rewrite star_pull_existsEach. eapply heq_existsEach; intros.
        generalize star_SHeap_denote.
        symmetry. rewrite <- sheapD_sheapD'.
        rewrite <- star_SHeap_denote. simpl plus.
        cutrewrite (length v0 = length Z0).
        cutrewrite (length v = length Z).
        repeat rewrite sheapD_sheapD'.
        rewrite sheapD_sexprD_liftVars.
        rewrite sheapD_sexprD_liftVars with (G := nil). heq_canceler.
        rewrite <- rev_length; rewrite <- H; apply map_length.
        rewrite <- rev_length; rewrite <- H0; apply map_length. }

      { (** Exists **)
        unfold sheapD'; simpl; intros. case_eq (hash s); intros; simpl.
        eapply heq_ex. intros. specialize (IHs (existT (tvarD types) t v0 :: G)). simpl in *.
        rewrite H in IHs. simpl in *. eauto. }
    Qed.

    Theorem hash_denote : forall EG G cs (s : sexpr _ _ _),
      heq funcs preds EG G cs s (existsEach (fst (hash s)) (sheapD (snd (hash s)))).
    Proof.
      intros. specialize (@hash_denote' EG cs s G). etransitivity.
      eassumption. apply heq_existsEach. intros. rewrite sheapD_sheapD'. reflexivity.
    Qed.

    Lemma WellTyped_impures_eq : forall tf tp tU tG impures,
      WellTyped_impures tf tp tU tG impures = true <->
      (forall k v, FM.find k impures = Some v ->
        match v with
          | nil => True
          | _ => match nth_error tp k with
                   | None => False
                   | Some ts =>
                     allb (fun argss => all2 (is_well_typed tf tU tG) argss ts) v = true
                 end
        end).
    Proof.
      clear. do 5 intro. unfold WellTyped_impures. eapply MF.PROPS.map_induction with (m := impures0); intros.
      { rewrite MF.PROPS.fold_Empty; eauto with typeclass_instances. split; intro; auto.
        intros. exfalso. rewrite MF.find_Empty in H1; auto. congruence. }
      { rewrite MF.PROPS.fold_Add. 5: eauto. 5: eauto. split; intros.
        { destruct (FM.E.eq_dec k x); subst.
          { specialize (H1 x).
            rewrite H3 in H1. rewrite MF.FACTS.add_o in H1. destruct (FM.E.eq_dec x x); try congruence.
            inversion H1; clear H1; subst. clear e0. destruct e; auto.
            apply andb_true_iff in H2. destruct H2. destruct (nth_error tp x); auto; congruence. }
          { apply andb_true_iff in H2. destruct H2. eapply H in H2. eauto.
            specialize (H1 k). rewrite H3 in H1. rewrite MF.FACTS.add_o in H1.
            destruct (FM.E.eq_dec x k); subst; try congruence. } }
        { apply andb_true_iff; split. apply H. intros.
          specialize (H1 k). rewrite MF.FACTS.add_o in H1. destruct (FM.E.eq_dec x k); subst.
          exfalso. apply MF.FACTS.find_mapsto_iff in H3. apply H0.
          exists v. auto. rewrite H3 in H1. eapply H2; eauto.

          specialize (H1 x). rewrite MF.FACTS.add_o in H1. destruct (FM.E.eq_dec x x); try congruence.
          specialize (H2 _ _ H1). destruct e; auto. destruct (nth_error tp x); auto. }
        eauto with typeclass_instances.
        { clear; repeat (red; intros; subst). reflexivity. }
        { clear; repeat (red; intros; subst). repeat rewrite <- andb_assoc. f_equal.
          apply andb_comm. } }
    Qed.

    Lemma eq_iff : forall a b A B,
      (a = true <-> A) ->
      (b = true <-> B) ->
      (A <-> B) ->
      a = b.
    Proof.
      clear. destruct a; destruct b; intros; intuition.
    Qed.

    Lemma andb_iff : forall a b A B,
      (a = true <-> A) ->
      (b = true <-> B) ->
      (a && b = true <-> A /\ B).
    Proof.
      clear. destruct a; destruct b; intros; intuition.
    Qed.

    Theorem WellTyped_sheap_weaken : forall tf tp tU tG tU' tG' h,
      WellTyped_sheap tf tp tU tG h = true ->
      WellTyped_sheap tf tp (tU ++ tU') (tG ++ tG') h = true.
    Proof.
      clear. unfold WellTyped_sheap. simpl; intros.
      think. apply andb_true_iff. split. clear - H.
      { rewrite WellTyped_impures_eq in *. intros.
        eapply H in H0. destruct v; auto.
        destruct (nth_error tp k); auto.
        generalize dependent (e :: v). clear.
        intros. eapply allb_impl; eauto; intros.
        simpl in *. eapply all2_impl; eauto. intros. apply is_well_typed_weaken; auto. }
      { eapply allb_impl; eauto. intros. apply is_well_typed_weaken. auto. }
    Qed.

    Theorem WellTyped_sheap_star : forall tf tp tU tG h0 h1,
      WellTyped_sheap tf tp tU tG h0 && WellTyped_sheap tf tp tU tG h1 =
      WellTyped_sheap tf tp tU tG (star_SHeap h0 h1).
    Proof.
      Transparent star_SHeap.
      clear. destruct h0; destruct h1; unfold WellTyped_sheap, star_SHeap; simpl; intros.
      eapply eq_iff;
        repeat match goal with
                 | [ |- _ && _ = true <-> _ ] => eapply andb_iff
                 | [ |- WellTyped_impures _ _ _ _ _ = true <-> _ ] => eapply WellTyped_impures_eq
                 | [ |- _ ] => reflexivity
               end.
      split; intuition.
      { rewrite MM.mmap_join_o in H1.
        repeat match goal with
                 | [ H : match FM.find ?A ?B with _ => _ end = _ |- _ ] =>
                   consider (FM.find A B) ; intros
                 | [ H : Some _ = Some _ |- _ ] => inversion H; clear H; subst
                 | [ H : forall x y, FM.find _ _ = Some _ -> _ , H' : FM.find _ _ = _ |- _ ] =>
                   specialize (H _ _ H')
                 | [ H : match ?X with nil => _ | _ => _ end |- _ ] => destruct X; simpl in *
                 | [ H : match nth_error ?A ?B with _ => _ end |- _ ] => destruct (nth_error A B)
               end; auto;  think; repeat (rewrite allb_app || (apply andb_true_iff; split)); think; simpl; auto. }
      { rewrite allb_app. apply andb_true_iff. auto. }
      { consider (FM.find k impures1); intros.
        specialize (H0 k (v ++ l)). rewrite MM.mmap_join_o in H0.
        think. specialize (H0 refl_equal).
        destruct v; auto. simpl in *. destruct (nth_error tp k); auto.
        think. rewrite allb_app in H3. apply andb_true_iff in H3. intuition.
        specialize (H0 k v). rewrite MM.mmap_join_o in H0. think.
        apply H0. auto. }
      { rewrite allb_app in H1. apply andb_true_iff in H1. destruct H1; auto. }
      { consider (FM.find k impures0); intros.
        specialize (H0 k (l ++ v)). rewrite MM.mmap_join_o in H0. think. specialize (H0 refl_equal).
        destruct v. auto. destruct (nth_error tp k); destruct l; simpl in *; auto.
        think. rewrite allb_app in H3. simpl in *.  think; auto.
        specialize (H0 k v). rewrite MM.mmap_join_o in H0. think. eapply H0; auto. }
      { rewrite allb_app in H1. apply andb_true_iff in H1. destruct H1; auto. }
      Opaque star_SHeap.
    Qed.

    Lemma WellTyped_star_SHeap : forall tf tp tU tG h1 h2,
      WellTyped_sheap tf tp tU tG h1 = true ->
      WellTyped_sheap tf tp tU tG h2 = true ->
      WellTyped_sheap tf tp tU tG (star_SHeap h1 h2) = true.
    Proof.
      clear; intros. rewrite <- WellTyped_sheap_star. think. reflexivity.
    Qed.

    Opaque star_SHeap.

    Lemma fold_ext : forall U V (F F' : _ -> U -> V -> V),
      (forall k v a, F k v a = F' k v a) ->
      forall m a,
        FM.fold F m a = FM.fold F' m a.
    Proof.
      unfold FM.fold. destruct m. simpl. induction this; simpl; try reflexivity.
      inversion is_bst; subst. intros. think. auto.
    Qed.

    Lemma liftExpr_wt : forall (types : list type) tf
      (U U' U'' G G' G'' : list tvar)
      (e : expr types) (t : tvar),
      is_well_typed tf (U'' ++ U) (G'' ++ G) e t =
      is_well_typed tf (U'' ++ U' ++ U) (G'' ++ G' ++ G)
      (liftExpr (length U'') (length U') (length G'') (length G') e) t.
    Proof.
      clear. induction e; simpl; intros;
      repeat match goal with
               | [ |- context [ NPeano.ltb ?a ?b ] ] => consider (NPeano.ltb a b) ; intros
               | [ |- _ ] => rewrite nth_error_app_L by omega
               | [ |- _ ] => rewrite nth_error_app_R by omega
             end; think; auto.
      cutrewrite (length G' + x - length G'' - length G' = x - length G''); [ | omega ]. auto.
      cutrewrite (length U' + x - length U'' - length U' = x - length U''); [ | omega ]. auto.
      consider (nth_error tf f); auto; intros. consider (tvar_seqb t (TRange t0)); intros; auto. think.
      destruct t0; simpl in *. clear -H. revert TDomain; induction H; simpl; auto.
      destruct TDomain; auto. think.  auto.
    Qed.

    Lemma liftSHeap_wt : forall tf tp tU G G' G'' h,
      WellTyped_sheap tf tp tU (G ++ G'') h =
      WellTyped_sheap tf tp tU (G ++ G' ++ G'') (liftSHeap 0 0 (length G) (length G') h).
    Proof.
      clear. unfold liftSHeap, WellTyped_sheap, WellTyped_impures. intros; simpl.

      f_equal. unfold MM.mmap_map. rewrite MF.fold_map_fusion.

      eapply fold_ext; intros. f_equal. destruct v; simpl; auto. destruct (nth_error tp k); auto.
      generalize (liftExpr_wt (types := types) tf tU nil nil G'' G' G). simpl. repeat rewrite app_nil_r.
      intro.

      rewrite all2_map_1.
      erewrite all2_eq. 2: intros; rewrite H; reflexivity.
      destruct (all2
        (fun (x : expr types) (y : tvar) =>
          is_well_typed tf tU (G ++ G' ++ G'')
          (liftExpr 0 0 (length G) (length G') x) y) l t); auto.

      rewrite allb_map.

      apply allb_ext; auto. intros. rewrite all2_map_1. apply all2_eq; auto.
      auto with typeclass_instances.
      { repeat (red; intros; subst). repeat rewrite <- andb_assoc. f_equal. apply andb_comm. }
      { repeat (red; intros; subst). auto. }
      rewrite allb_map. apply allb_ext.
      generalize (liftExpr_wt (types := types) tf tU nil nil G'' G' G). simpl. auto.
    Qed.

    Theorem WellTyped_hash : forall tf tp tU tG (s : SE.sexpr types pcType stateType),
      SE.WellTyped_sexpr tf tp tU tG s =
      WellTyped_sheap tf tp tU (rev (fst (hash s)) ++ tG) (snd (hash s)).
    Proof.
      clear. intros tf tp tU tG s. revert tG.
      induction s; simpl; intros; unfold WellTyped_sheap; simpl in *; think; auto.
      { destruct (is_well_typed tf tU tG e tvProp); auto. }
      { destruct (hash s1); destruct (hash s2); simpl in *.
        rewrite <- WellTyped_sheap_eq. rewrite <- WellTyped_sheap_star.
        rewrite rev_app_distr. rewrite app_ass.
        f_equal.
        rewrite (liftSHeap_wt tf tp tU nil (rev v0) (rev v ++ tG)). simpl. rewrite rev_length. reflexivity.
        rewrite (liftSHeap_wt tf tp tU (rev v0) (rev v) tG). repeat rewrite rev_length. reflexivity. }
      { destruct (hash s); simpl in *. destruct s0; simpl in *.
        rewrite WellTyped_sheap_eq. simpl. repeat rewrite app_ass; reflexivity. }
      { unfold WellTyped_impures, MM.mmap_add. simpl. rewrite andb_true_r.
        rewrite MF.PROPS.fold_add; eauto with typeclass_instances.
        rewrite MF.PROPS.fold_Empty; eauto using FM.empty_1 with typeclass_instances.
        destruct (nth_error tp f); auto. simpl. destruct (all2 (is_well_typed tf tU tG) l t); auto.
        repeat (red; intros);
          repeat match goal with
                   | |- context [ match ?X with _ => _ end ] => destruct X
                   | |- _ => rewrite Bool.andb_true_l
                   | |- _ => rewrite Bool.andb_true_r
                   | |- context [ allb ?A ?B ] => destruct (allb A B)
                 end; try reflexivity.
        rewrite MF.FACTS.empty_in_iff; auto. }
    Qed.

(*
    Theorem WellTyped_hash : forall tf tp tU tG (s : SE.sexpr types pcType stateType),
      SE.WellTyped_sexpr tf tp tU tG s =
      WellTyped_sheap tf tp tU (rev (fst (hash s)) ++ tG) (snd (hash s)).
    Proof.
      clear. intros tf tp tU tG s. revert tG.
      induction s; simpl; intros; unfold WellTyped_sheap; simpl in *; think; auto.
      { destruct (hash s1). destruct (hash s2). simpl in *.
        eapply WellTyped_star_SHeap.
        apply IHs1 in H. rewrite rev_app_distr.
        rewrite (liftSHeap_wt tf tp tU nil (rev v0) (rev v ++ tG)) in H. rewrite app_ass. simpl in *.
        rewrite rev_length in H. auto.
        apply IHs2 in H0. rewrite rev_app_distr. rewrite app_ass.
        rewrite (liftSHeap_wt tf tp tU (rev v0) (rev v) tG) in H0. repeat rewrite rev_length in *; auto. }
      { destruct (hash s); simpl in *. destruct s0; simpl in *. eapply IHs in H.
        repeat rewrite app_ass in *. simpl in *. auto. }
      { unfold WellTyped_impures, MM.mmap_add. simpl. rewrite andb_true_r.
        unfold FM.fold, FM.Raw.fold. simpl. rewrite H. rewrite H0. auto. }
    Qed.
*)

    Definition applySHeap (F : expr types -> expr types) (sh : SHeap) : SHeap :=
      {| impures := MM.mmap_map (map F) (impures sh)
       ; pures := map F (pures sh)
       ; other := other sh
       |}.

    Theorem applySHeap_defn : forall F sh,
      applySHeap F sh =
      {| impures := MM.mmap_map (map F) (impures sh)
       ; pures := map F (pures sh)
       ; other := other sh
       |}.
    Proof. reflexivity. Qed.

    Lemma starred_nil : forall T U G cs (F : T -> _) B,
      heq funcs preds U G cs (starred F nil B) B.
    Proof.
      clear. reflexivity.
    Qed.

    Lemma starred_cons : forall T U G cs (F : T -> _) a A B,
      heq funcs preds U G cs (starred F (a :: A) B) (Star (F a) (starred F A B)).
    Proof.
      clear. intros; rewrite starred_def. simpl. rewrite <- starred_def. reflexivity.
    Qed.

    Theorem applySHeap_spec : forall cs U G U' G' s F,
      (forall e t,
        exprD funcs U G e t = exprD funcs U' G' (F e) t) ->
      SE.ST.heq cs (sexprD funcs preds U G (sheapD s))
                   (sexprD funcs preds U' G' (sheapD (applySHeap F s))).
    Proof.
      clear. intros.
      do 2 rewrite sheapD_def. simpl. repeat eapply SE.ST.heq_star_frame.
      { eapply MM.PROPS.map_induction with (m := impures s); intros.
        repeat rewrite impuresD_Empty by eauto using MF.map_Empty. reflexivity.
        rewrite impuresD_Add by eauto using MF.map_Add, MF.map_not_In.
        symmetry. unfold MM.mmap_map in *. rewrite impuresD_Add. 2: eapply MF.map_Add; eauto.
        2: eapply MF.map_not_In; eauto.
        simpl. rewrite H0. apply ST.heq_star_frame; try reflexivity.
        clear - H. induction e; simpl. reflexivity. repeat rewrite starred_cons.
        simpl. rewrite IHe. apply ST.heq_star_frame; try reflexivity.
        destruct (nth_error preds x); try reflexivity.
        match goal with
          | |- ST.heq _ match ?X with _ => _ end match ?Y with _ => _ end =>
            cutrewrite (X = Y); try reflexivity
        end.
        destruct p. simpl in *; clear -H. generalize dependent SDomain0.
        clear -H; induction a; destruct SDomain0; simpl; intros; auto; try congruence; try reflexivity.
        rewrite H. destruct (exprD funcs U' G' (F a) t); try reflexivity. rewrite IHa. reflexivity. }
      { induction (pures s); try reflexivity.
        simpl. repeat rewrite starred_cons. simpl. rewrite H. rewrite IHl. reflexivity. }
      { induction (other s). reflexivity. etransitivity. rewrite starred_cons. reflexivity.
        etransitivity. 2: rewrite starred_cons; reflexivity. simpl. rewrite IHl. reflexivity. }
    Qed.

    Theorem applySHeap_wt_spec : forall cs U G U' G' s F,
      (forall e t,
        is_well_typed (typeof_funcs funcs) (typeof_env U) (typeof_env G) e t = true ->
        exprD funcs U G e t = exprD funcs U' G' (F e) t) ->
      WellTyped_sheap (typeof_funcs funcs) (typeof_preds preds) (typeof_env U) (typeof_env G) s = true ->
      SE.ST.heq cs (sexprD funcs preds U G (sheapD s))
                   (sexprD funcs preds U' G' (sheapD (applySHeap F s))).
    Proof.
      clear. intros. rewrite WellTyped_sheap_eq in H0. apply andb_true_iff in H0. destruct H0.
      do 2 rewrite sheapD_def. simpl. repeat eapply SE.ST.heq_star_frame.
      { revert H0. clear H1. rewrite WellTyped_impures_spec_eq. eapply MM.PROPS.map_induction with (m := impures s); intros.
        repeat rewrite impuresD_Empty by eauto using MF.map_Empty. reflexivity.
        rewrite impuresD_Add by eauto using MF.map_Add, MF.map_not_In.
        symmetry. unfold MM.mmap_map in *. rewrite impuresD_Add. 2: eapply MF.map_Add; eauto.
        2: eapply MF.map_not_In; eauto.
        simpl. symmetry. rewrite NatMap.IntMapProperties.fold_Add in H3. 5: eauto. 5: eauto.
        apply andb_true_iff in H3. destruct H3. apply ST.heq_star_frame.
        cut (ST.heq cs (sexprD funcs preds U G SE.Emp) (sexprD funcs preds U' G' SE.Emp)); [ | reflexivity ].
        generalize (@SE.Emp types pcType stateType). revert H. clear - H4.
        induction e; simpl; intros. repeat rewrite starred_nil. auto.
        repeat rewrite starred_cons. simpl in *. apply ST.heq_star_frame; eauto.
        unfold typeof_preds in H4. rewrite map_nth_error_full in H4.
        destruct (nth_error preds x); try reflexivity.
        consider (all2 (is_well_typed (typeof_funcs funcs) (typeof_env U) (typeof_env G)) a (typeof_pred p)). intros.
        rewrite applyD_map. revert H1. clear -H. destruct p; simpl. generalize dependent SDomain0.
        { induction a; destruct SDomain0; intros; simpl; auto; try reflexivity.
          simpl in H1. consider (is_well_typed (typeof_funcs funcs) (typeof_env U) (typeof_env G) a t); intros.
          rewrite H; eauto. destruct (exprD funcs U' G' (F a) t); eauto. reflexivity. }
        { destruct (nth_error (typeof_preds preds) x); try congruence.
          consider (all2 (is_well_typed (typeof_funcs funcs) (typeof_env U) (typeof_env G)) a t); intros.
          destruct e. simpl; repeat rewrite starred_nil. eauto.
          generalize dependent (e :: e0); intros.
          eapply IHe; eauto. }
        { eapply H0; eauto. }
        { unfold Basics.flip; constructor; eauto. }
        { clear. unfold Basics.flip. repeat (red; intros; subst). auto. }
        { clear. repeat (red; intros; subst). repeat rewrite <- andb_assoc. f_equal. apply andb_comm. } }
      { cut (ST.heq cs (sexprD funcs preds U G SE.Emp) (sexprD funcs preds U' G' SE.Emp)); [ | reflexivity ].
        revert H1. clear H0. generalize (@SE.Emp types pcType stateType). induction (pures s); intros;
        repeat (rewrite starred_nil || rewrite starred_cons); auto. simpl map. rewrite starred_cons.
        simpl. simpl in H1.
        consider (is_well_typed (typeof_funcs funcs) (typeof_env U) (typeof_env G) a tvProp); intros.
        rewrite IHl; eauto. rewrite H; auto. reflexivity. }
      { cut (ST.heq cs (sexprD funcs preds U G SE.Emp) (sexprD funcs preds U' G' SE.Emp)); [ | reflexivity ].
        generalize (@SE.Emp types pcType stateType). induction (other s); intros.
        etransitivity. rewrite starred_nil. reflexivity. etransitivity; [ | rewrite starred_nil; reflexivity ].
        auto.

        etransitivity; [ rewrite starred_cons; reflexivity | ].
        etransitivity; [ |  rewrite starred_cons; reflexivity ]. simpl. rewrite IHl; eauto. reflexivity. }
    Qed.

    Lemma applySHeap_typed_eq : forall tf tp U G U' G' s F,
      (forall e t,
        is_well_typed tf U G e t = is_well_typed tf U' G' (F e) t) ->
      WellTyped_sheap tf tp U G s = WellTyped_sheap tf tp U' G' (applySHeap F s).
    Proof.
      clear. intros. repeat rewrite WellTyped_sheap_eq in *. destruct s; unfold applySHeap; simpl in *.
      f_equal. unfold WellTyped_impures.
      unfold MM.mmap_map. rewrite MF.fold_map_fusion. eapply fold_ext. intros.
      destruct a; simpl; auto.
      destruct (nth_error tp k); auto; try solve [ destruct v; simpl; auto ].
      cutrewrite (allb (fun args : list (expr types) => all2 (is_well_typed tf U G) args t) v =
        allb (fun args : list (expr types) => all2 (is_well_typed tf U' G') args t) (map (map F) v)); [ destruct v; auto | ].
      induction v; simpl; intros; think; auto.
      rewrite all2_map_1. erewrite all2_eq. 2: eapply H. auto. auto with typeclass_instances.
      repeat red; intros; repeat match goal with
                                   | |- context [ match ?X with _ => _ end ] => destruct X
                                   | |- _ => rewrite andb_true_l
                                   | |- _ => rewrite andb_true_r
                                   | |- context [ allb ?A ?B ] => destruct (allb A B)
                                 end; auto.
      repeat red; intros; repeat match goal with
                                   | |- _ => subst
                                   | |- context [ match ?X with _ => _ end ] => destruct X
                                   | |- _ => rewrite andb_true_l
                                   | |- _ => rewrite andb_true_r
                                   | |- context [ allb ?A ?B ] => destruct (allb A B)
                                 end; auto.
      rewrite allb_map. apply allb_ext. intros. apply H.
    Qed.

    Lemma applySHeap_typed_impl : forall tf tp U G U' G' s F,
      (forall e t,
        is_well_typed tf U G e t = true ->
        is_well_typed tf U' G' (F e) t = true) ->
      WellTyped_sheap tf tp U G s = true ->
      WellTyped_sheap tf tp U' G' (applySHeap F s) = true.
    Proof.
      clear. intros. rewrite WellTyped_sheap_eq in *. destruct s; unfold applySHeap; simpl in *.
      think. apply andb_true_iff; split.
      rewrite WellTyped_impures_eq in H0. apply WellTyped_impures_eq. intros.
      unfold MM.mmap_map in *. rewrite MM.FACTS.map_o in H2. unfold MM.FACTS.option_map in H2.
      consider (FM.find (elt:=list (list (expr types))) k impures0); intros. think.
      specialize (H0 _ _ H2). Opaque allb. destruct l; simpl in *; auto. Transparent allb.
      change (map F l :: map (map F) l0) with (map (map F) (l :: l0)). generalize dependent (l :: l0); intros.
      think. revert H3. clear - H. induction l1; simpl in *; intros; think; auto.
      rewrite all2_map_1. erewrite all2_impl; eauto. congruence.
      rewrite allb_map. eapply allb_impl; eauto.
    Qed.

(*
    (** replace "real" variables [a,b) and replace them with
     ** uvars [c,..]
     **)
    Definition sheapSubstU (a b c : nat) (s : SHeap) : SHeap :=
      {| impures := MM.mmap_map (map (exprSubstU a b c)) (impures s)
       ; pures := map (exprSubstU a b c) (pures s)
       ; other := other s
       |}.
*)

    Theorem hash_Func : forall p (args : exprs types),
      hash (Func p args) = (nil, {| impures := MM.mmap_add p args (MM.empty _)
                                  ; pures   := nil
                                  ; other   := nil
                                  |}).
    Proof. reflexivity. Qed.

  End env.

  Implicit Arguments Emp [ types pcType stateType ].
  Implicit Arguments Star [ types pcType stateType ].
  Implicit Arguments Exists [ types pcType stateType ].
  Implicit Arguments Func [ types pcType stateType ].
  Implicit Arguments Const [ types pcType stateType ].
  Implicit Arguments Inj [ types pcType stateType ].

  Lemma change_ST_himp_himp : forall (types : list type)
    (funcs : functions types) (pc st : tvar)
    (sfuncs : list (predicate types pc st))
    EG G
    (cs : codeSpec (tvarD types pc) (tvarD types st))
    (L R : sexpr types pc st),
    himp funcs sfuncs EG G cs L R ->
    ST.himp cs
      (@sexprD types pc st funcs sfuncs EG G L)
      (@sexprD types pc st funcs sfuncs EG G R).
  Proof.
    unfold himp. intros. auto.
  Qed.

End Make.

Module SepHeapFacts (SH : SepHeap).
  Import SH.SE.
  Module SEP_FACTS := SepExprFacts SH.SE.
  Import SEP_FACTS.

  Section with_env.
    Variable types : list type.
    Variables pcT stT : tvar.
    Variable funcs : functions types.
    Variable preds : predicates types pcT stT.
    Variable cs : PropX.codeSpec (tvarD types pcT) (tvarD types stT).

    Lemma starred_nil : forall T U G cs (F : T -> _) B,
      heq funcs preds U G cs (SH.starred F nil B) B.
    Proof.
      clear. intros; rewrite SH.starred_def. reflexivity.
    Qed.

    Lemma starred_cons : forall T U G cs (F : T -> _) a A B,
      heq funcs preds U G cs (SH.starred F (a :: A) B) (Star (F a) (SH.starred F A B)).
    Proof.
      clear. intros; rewrite SH.starred_def. simpl. rewrite <- SH.starred_def. reflexivity.
    Qed.

    Lemma starred_app : forall T U G cs (F : T -> _) ls ls'  B,
      heq funcs preds U G cs (SH.starred F (ls ++ ls') B) (Star (SH.starred F ls Emp) (SH.starred F ls' B)).
    Proof.
      clear; intros; rewrite SH.starred_def. rewrite fold_right_app. rewrite <- SH.starred_def.
      rewrite SH.starred_base. rewrite <- SH.starred_def. heq_canceler.
    Qed.

    Ltac heq_canceler :=
      repeat (rewrite starred_nil || rewrite starred_cons || rewrite starred_app ||
        match goal with
          | [ |- context [ SH.starred ?A ?B ?X ] ] =>
            match X with
              | Emp => fail 1
              | _ => rewrite SH.starred_base with (F := A) (ls := B) (base := X)
            end
        end);
      SEP_FACTS.heq_canceler.

    Lemma starred_perm : forall T L R,
      Permutation.Permutation L R ->
      forall (F : T -> _) U G cs base,
      heq funcs preds U G cs (SH.starred F L base) (SH.starred F R base).
    Proof.
      clear. intros.
      repeat rewrite SH.starred_def.
      induction H; simpl; intros;
      repeat match goal with
               | [ H : _ |- _ ] => rewrite H
             end; try reflexivity; heq_canceler.
    Qed.

    Lemma himp_pull_pures : forall cs U G s Q,
      (AllProvable funcs U G (SH.pures s) ->
       ST.himp cs (sexprD funcs preds U G (SH.sheapD s)) Q) ->
      ST.himp cs (sexprD funcs preds U G (SH.sheapD s)) Q.
    Proof. clear.
      destruct s; simpl in *. generalize dependent pures.
      induction pures; simpl; intros.
      { apply H; auto. }
      { repeat rewrite SH.sheapD_def in *.
        simpl in *. rewrite starred_cons in *.
        rewrite ST.heq_star_comm with (P := sexprD funcs preds U G (SH.impuresD pcT stT impures)).
        simpl in *.
        repeat rewrite ST.heq_star_assoc with (P := match exprD funcs U G a tvProp with
                                                   | Some p => ST.inj [|p|]
                                                   | None => ST.inj [|BadInj a|]
                                                 end).
        unfold himp, Provable in *.
        destruct (exprD funcs U G a tvProp).
        { eapply ST.himp_star_pure_c. intros.
          etransitivity. 2: eapply IHpures. Focus 2. intros. etransitivity. 2: eapply H; eauto.
          rewrite SH.sheapD_def. simpl.
          repeat (eapply ST.himp_star_frame; [ reflexivity | ]).
          rewrite ST.heq_star_assoc with (P := ST.inj [| t |]).
          eapply ST.himp_star_pure_cc; auto. reflexivity.
          rewrite SH.sheapD_def. simpl.
          repeat (eapply ST.himp_star_frame; [ reflexivity | ]).
          rewrite ST.himp_star_comm. reflexivity. }
        { eapply ST.himp_star_pure_c. intros.
          inversion H0. } }
    Qed.

(*
   Lemma himp_pull_pures : forall cs U G s Q,
      (AllProvable funcs U G (SH.pures s) ->
       himp funcs preds U G cs (SH.sheapD s) Q) ->
      himp funcs preds U G cs (SH.sheapD s) Q.
    Proof. clear.
      destruct s; simpl in *. generalize dependent pures.
      induction pures; simpl; intros.
      { apply H; auto. }
      { repeat rewrite SH.sheapD_def in *.
        simpl in *. rewrite starred_cons in *.
        rewrite heq_star_comm with (P := SH.impuresD pcT stT impures).
        repeat rewrite heq_star_assoc with (P := Inj a).
        unfold himp, Provable in *. simpl in *.
        destruct (exprD funcs U G a tvProp).
        { eapply ST.himp_star_pure_c. intros.
          etransitivity. 2: eapply IHpures. Focus 2. intros. etransitivity. 2: eapply H; eauto.
          rewrite SH.sheapD_def. simpl.
          repeat (eapply ST.himp_star_frame; [ reflexivity | ]).
          rewrite ST.heq_star_assoc with (P := ST.inj [| t |]).
          eapply ST.himp_star_pure_cc; auto. reflexivity.
          rewrite SH.sheapD_def. simpl.
          repeat (eapply ST.himp_star_frame; [ reflexivity | ]).
          rewrite ST.himp_star_comm. reflexivity. }
        { eapply ST.himp_star_pure_c. intros.
          inversion H0. } }
    Qed.
*)

    Definition sheapSubstU (a b c : nat) : SH.SHeap types pcT stT -> SH.SHeap types pcT stT :=
      SH.applySHeap (Expr.exprSubstU a b c).

    Lemma sheapSubstU_WellTyped_eq : forall tf tp tu tg tg' tg'' s,
      SH.WellTyped_sheap (types := types) (pcType := pcT) (stateType := stT) tf tp tu (tg ++ tg' ++ tg'') s =
      SH.WellTyped_sheap tf tp (tu ++ tg') (tg ++ tg'') (sheapSubstU (length tg) (length tg' + length tg) (length tu) s).
    Proof.
      clear. intros.
      eapply SH.applySHeap_typed_eq; eauto. clear.
      intros. rewrite <- exprSubstU_wt. auto.
    Qed.

    (** TODO: deprecated **)
    Lemma sheapSubstU_WellTyped : forall tf tp tu tg tg' tg'' s,
      SH.WellTyped_sheap (types := types) (pcType := pcT) (stateType := stT) tf tp tu (tg ++ tg' ++ tg'') s = true ->
      SH.WellTyped_sheap tf tp (tu ++ tg') (tg ++ tg'') (sheapSubstU (length tg) (length tg' + length tg) (length tu) s) = true.
    Proof.
      clear. intros.
      eapply SH.applySHeap_typed_impl; eauto. clear.
      intros. rewrite <- exprSubstU_wt. auto.
    Qed.

    Lemma sheapSubstU_sheapD : forall U G G' G'' s,
      ST.heq cs (sexprD funcs preds U (G ++ G' ++ G'') (SH.sheapD s))
                (sexprD funcs preds (U ++ G') (G ++ G'') (SH.sheapD (sheapSubstU (length G) (length G' + length G) (length U) s))).
    Proof.
      intros. eapply SH.applySHeap_spec. intros.
      apply exprSubstU_exprD.
    Qed.

  End with_env.

  Ltac heq_canceler :=
    repeat (rewrite starred_nil || rewrite starred_cons || rewrite starred_app ||
      match goal with
        | [ |- context [ SH.starred ?A ?B ?X ] ] =>
          match X with
            | Emp => fail 1
            | _ => rewrite SH.starred_base with (F := A) (ls := B) (base := X)
          end
      end);
    SEP_FACTS.heq_canceler.

  Lemma applySHeap_singleton : forall types pcT stT funcs (preds : SH.SE.predicates types pcT stT)  meta_env vars_env cs F f l,
    heq funcs preds meta_env vars_env cs
    (SH.sheapD (SH.applySHeap F
      {| SH.impures := MM.mmap_add f l (MM.empty (list (expr types)))
        ; SH.pures := nil
        ; SH.other := nil |}))
    (SH.sheapD
      {| SH.impures := MM.mmap_add f (map F l) (MM.empty (list (expr types)))
        ; SH.pures := nil
        ; SH.other := nil |}).
  Proof.
    clear. intros. rewrite SH.applySHeap_defn; simpl. repeat rewrite SH.sheapD_def; simpl.
    heq_canceler. unfold MM.mmap_add. repeat rewrite MM.FACTS.empty_o.
    rewrite SH.impuresD_Add with (f := f) (argss := map F l :: nil) (i := MM.empty _). symmetry.
    rewrite SH.impuresD_Add with (f := f) (argss := map F l :: nil) (i := MM.empty _). reflexivity.
    red; reflexivity. intro; eapply MM.FACTS.empty_in_iff; eassumption.
    red; reflexivity. intro; eapply MM.FACTS.empty_in_iff; eassumption.
  Qed.

  Export SEP_FACTS.

End SepHeapFacts.

author: csgordon

repo: bedrock

save_path: github-repos/coq/csgordon-bedrock


text:
Require Import
        Coq.Vectors.Vector
        Coq.omega.Omega
        Coq.Strings.Ascii
        Coq.Strings.String
        Coq.Bool.Bool
        Coq.Vectors.VectorDef
        Coq.Lists.List.

Require Import
        Fiat.Common.BoundedLookup
        Fiat.Common.SumType
        Fiat.Common.EnumType
        Fiat.QueryStructure.Specification.Representation.Notations
        Fiat.QueryStructure.Specification.Representation.Heading
        Fiat.QueryStructure.Specification.Representation.Tuple.

Require Import
        Bedrock.Word
        Bedrock.Memory.

Import Lists.List.ListNotations.
Import Vectors.VectorDef.VectorNotations.

Local Open Scope string_scope.
Local Open Scope Tuple_scope.
Local Open Scope vector_scope.

Require Export Fiat.Examples.DnsServer.RRecordTypes.

Section QTypes.

  (* DNS packet Query Types are a superset of RR Types. *)
  Definition QTypes :=
    ["TKEY"; (* Transaction Key 	[RFC2930] *)
     "TSIG"; (* Transaction Signature 	[RFC2845] *)
     "IXFR"; (* incremental transfer 	[RFC1995] *)
     "AXFR"; (* transfer of an entire zone 	[RFC1035][RFC5936] *)
     "MAILB"; (* mailbox-related RRs (MB, MG or MR) 	[RFC1035] *)
     "MAILA"; (* mail agent RRs (OBSOLETE - see MX) 	[RFC1035] *)
     "STAR" (*A request for all records the server/cache has available 	[RFC1035][RFC6895] *)
    ].

  Definition QType_Ws : t (word 16) 17 :=
    Eval simpl in RRecordType_Ws ++ Vector.map (natToWord 16)
                             [249; (*"TKEY" *)
                                250; (*"TSIG" *)
                                251; (*"IXFR" *)
                                252; (*"AXFR" *)
                                253;(*"MAILB" *)
                                254;(*"MAILA" *)
                                255 (* "STAR" *)].

  Definition QType := EnumType ((OurRRecordTypes(* ++ ExtraRRecordTypes) *) ++ QTypes)).

  Definition QType_inj (rr : RRecordType) : QType :=
    Fin.L _ rr.

  Definition beq_QType (a b : QType) : bool :=
    fin_beq a b.

  Definition QType_dec (a b : QType) :=
    fin_eq_dec a b.

  Lemma beq_QType_sym :
    forall rrT rrT', beq_QType rrT rrT' = beq_QType rrT' rrT.
  Proof.
    intros; eapply fin_beq_sym.
  Qed.

  Coercion QType_inj : RRecordType >-> QType.

  Definition QType_match (rtype : RRecordType) (qtype : QType) :=
    qtype = ```"STAR" \/ qtype = rtype.

End QTypes.

Section RRecordClass.

  Definition RRecordClasses :=
    [ "Internet"; (* (IN) 	[RFC1035] *)
        "Chaos"; (* (CH) 	[D. Moon, "Chaosnet", A.I. Memo 628, Massachusetts Institute of Technology Artificial Intelligence Laboratory, June 1981.] *)
        "Hesiod" (* (HS) 	[Dyer, S., and F. Hsu, "Hesiod", Project Athena Technical Plan - Name Service, April 1987.] *)
    ].

  Definition RRecordClass_Ws : t (word 16) 3 :=
    Eval simpl in Vector.map (natToWord 16)
                             [1; (* "IN" *)
                                3; (* "CH" *)
                                4 (* "Hesiod" *)].

  Definition RRecordClass := EnumType RRecordClasses.

  Definition beq_RRecordClass (a b : RRecordClass) : bool
    := fin_beq a b.

  Definition RRecordClass_dec (a b : RRecordClass) :=
    fin_eq_dec a b.

  (* DNS Packet Question Classes *)
  Definition QClass := EnumType (RRecordClasses ++ ["Any"]).

  Definition QClass_Ws : t (word 16) 4 :=
    Eval simpl in Vector.append
                    RRecordClass_Ws
                    [natToWord 16 255 (* "Any"*)].

  Definition QClass_inj (qclass : RRecordClass) : QClass :=
    Fin.L _ qclass.

  Definition beq_QClass (a b : QClass) : bool
    := fin_beq a b.

  Definition QClass_dec (a b : QClass) :=
    fin_eq_dec a b.

End RRecordClass.

Section ResponseCode.

    Definition ResponseCodes :=
    ["NoError";  (* No Error [RFC1035] *)
       "FormErr";  (* Format Error [RFC1035] *)
       "ServFail"; (* Server Failure [RFC1035] *)
       "NXDomain"; (* Non-Existent  Domain 	[RFC1035] *)
       "NotImp";   (* Not Implemented [RFC1035] *)
       "Refused";  (* Query Refused [RFC1035] *)
       "YXDomain"; (* Name Exists when it should not [RFC2136][RFC6672] *)
       "YXRRSet";  (* RR Set Exists when it should not 	[RFC2136] *)
       "NXRRSet";  (* RR Set that should exist does not 	[RFC2136] *)
       "NotAuth";  (* Server Not Authoritative for zone 	[RFC2136] *)
                   (* and Not Authorized [RFC2845] *)
       "NotZone" 	 (* Name not  contained in zone 	[RFC2136] *)
    ].

  Definition RCODE_Ws : t (word 4) 11 :=
    Eval simpl in Vector.map (natToWord 4)
    [0;  (* No Error [RFC1035] *)
     1;  (* Format Error [RFC1035] *)
     2; (* Server Failure [RFC1035] *)
     3; (* Non-Existent  Domain 	[RFC1035] *)
     4;   (* Not Implemented [RFC1035] *)
     5;  (* Query Refused [RFC1035] *)
     6; (* Name Exists when it should not [RFC2136][RFC6672] *)
     7;  (* RR Set Exists when it should not 	[RFC2136] *)
     8;  (* RR Set that should exist does not 	[RFC2136] *)
     9;  (* Server Not Authoritative for zone 	[RFC2136] *)
         (* and Not Authorized [RFC2845] *)
     10 	 (* Name not  contained in zone 	[RFC2136] *)
    ].

  Definition ResponseCode := EnumType ResponseCodes.

  Definition beq_ResponseCode (a b : ResponseCode) : bool
    := fin_beq a b.

  Definition ResponseCode_dec (a b : ResponseCode) :=
    fin_eq_dec a b.
End ResponseCode.

Section OpCode.

  Definition OpCodes :=
    ["Query";    (* RFC1035] *)
     "IQuery"; (* Inverse Query  OBSOLETE) [RFC3425] *)
     "Status"; (* [RFC1035] *)
     "Notify"  (* [RFC1996] [RFC2136] *)
    ].

  Definition OpCode := EnumType OpCodes.

  Definition Opcode_Ws : t (word 4) 4 :=
    Eval simpl in Vector.map (natToWord 4)
                             [0;    (* RFC1035] *)
                              1; (* Inverse Query  OBSOLETE) [RFC3425] *)
                              2; (* [RFC1035] *)
                              4  (* [RFC1996] [RFC2136] *)].

  Definition beq_OpCode (a b : OpCode) : bool
    := fin_beq a b.

  Definition OpCode_dec (a b : OpCode) :=
    fin_eq_dec a b.

End OpCode.

Section Packet.

  (* The question section of a DNS packet. *)
  Definition question :=
    @Tuple <
    "qname" :: DomainName,
    "qtype" :: QType,
    "qclass" :: QClass >%Heading.
  (* ["google", "com"] *)

  (* DNS Resource Records. *)
  Definition sRRecords := "ResourceRecords".
  Definition sNAME := "Name".
  Definition sTTL := "TTL".
  Definition sCLASS := "Class".
  Definition sTYPE := "Type".
  Definition sRDATA := "rdata".
  Definition sRLENGTH := "rlength".

  Definition resourceRecordHeading :=
    < sNAME :: DomainName,
      sTTL :: timeT,
      sCLASS :: RRecordClass,
      sRDATA :: RDataType>%Heading.

  Definition resourceRecord := @Tuple resourceRecordHeading.

  (* Variant headings for each RDataType *)
  Definition VariantResourceRecordHeading RDATAT :=
    < sNAME :: DomainName,
      sTTL :: timeT,
      sCLASS :: RRecordClass,
      sRDATA :: RDATAT >%Heading.

  Definition VariantResourceRecord RDATAT := @Tuple (VariantResourceRecordHeading RDATAT).

  (* Aliases for the Common Record Types *)
  Definition CNAME_Record :=
    VariantResourceRecord ResourceRecordTypeTypes[@ OurCNAME].
  Definition A_Record :=
    VariantResourceRecord ResourceRecordTypeTypes[@ OurA ].
  Definition NS_Record :=
    VariantResourceRecord ResourceRecordTypeTypes[@ OurNS].
  Definition MX_Record :=
    VariantResourceRecord ResourceRecordTypeTypes[@ OurMX].
  Definition SOA_Record :=
    VariantResourceRecord ResourceRecordTypeTypes[@ OurSOA].

  Definition RRecord2VariantResourceRecord
             (rr : resourceRecord)
    : VariantResourceRecord ResourceRecordTypeTypes[@(SumType_index ResourceRecordTypeTypes (rr!sRDATA))] :=
    < sNAME :: rr!sNAME,
      sTTL :: rr!sTTL,
      sCLASS :: rr!sCLASS,
      sRDATA :: SumType_proj _ (rr!sRDATA)>.

  Definition VariantResourceRecord2RRecord
             {idx}
             (vrr : VariantResourceRecord ResourceRecordTypeTypes[@idx])
    : resourceRecord :=
    < sNAME :: vrr!sNAME,
      sTTL :: vrr!sTTL,
      sCLASS :: vrr!sCLASS,
      sRDATA :: inj_SumType _ idx (vrr!sRDATA)>.

  Definition CNAME_Record2RRecord
             (vrr : CNAME_Record)
    : resourceRecord := VariantResourceRecord2RRecord vrr.
  Definition A_Record2RRecord
             (vrr : A_Record)
    : resourceRecord := VariantResourceRecord2RRecord vrr.
  Definition NS_Record2RRecord
             (vrr : NS_Record)
    : resourceRecord := VariantResourceRecord2RRecord vrr.
  Definition MX_Record2RRecord
             (vrr : MX_Record)
    : resourceRecord := VariantResourceRecord2RRecord vrr.
  Definition SOA_Record2RRecord
             (vrr : SOA_Record)
    : resourceRecord := VariantResourceRecord2RRecord vrr.

  (* Binary Format of DNS Header:
                              1  1  1  1  1  1
0  1  2  3  4  5  6  7  8  9  0  1  2  3  4  5
+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+
|                      ID                       |
+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+
|QR|   Opcode  |AA|TC|RD|RA|   Z    |   RCODE   |
+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+
|                    QDCOUNT                    |
+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+
|                    ANCOUNT                    |
+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+
|                    NSCOUNT                    |
+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+
|                    ARCOUNT                    |
+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+--+
   *)

  (* DNS Packet Layout:
+---------------------+
|        Header       |
+---------------------+
|       Question      |
+---------------------+
|        Answer       |
+---------------------+
|      Authority      |
+---------------------+
|      Additional     |
+---------------------+
   *)

(* Unique Request IDs *)
Definition ID : Type := word 16.

  Definition packetHeading :=
    < "id" :: ID, (* 16 bit Word. *)
      "QR" :: bool, (* is packet a query (0), or a response (1) *)
      "Opcode" :: OpCode, (* kind of query in packet *)
      "AA" :: bool, (* is responding server authorative *)
      "TC" :: bool, (* is packet truncated *)
      "RD" :: bool, (* are recursive queries desired *)
      "RA" :: bool, (* are recursive queries supported by responding server *)
      "RCODE" :: ResponseCode, (* response code *)
      "question" :: question, (* `list question` in case we can have multiple questions? *)
      "answers" :: list resourceRecord,
      "authority" :: list resourceRecord,
      "additional" :: list resourceRecord >%Heading.

  Definition packet := @Tuple packetHeading.

  Definition buildempty (is_authority : bool)
             (rcode : BoundedIndex ResponseCodes)
             (p : packet) :=
    p ○ [ "AA" ::= is_authority; (* Update Authority field *)
          "QR" ::= true; (* Set response flag to true *)
          "RCODE" ::= ibound (indexb rcode);
          "answers" ::= nil;
          "authority"  ::= nil;
          "additional" ::= nil ].

  (* add a resource record to a packet's answers *)
  Definition add_answer (p : packet) (t : resourceRecord) :=
    p ○ [o !! "answers" / t :: o].

  (* add a resource record authority to a packet's authorities
   (ns = name server). *)
  Definition add_ns (p : packet) (t : resourceRecord) :=
    p ○ [o !! "authority" / t :: o].

  (* combine with above? *)
  Definition add_additional (p : packet) (t : resourceRecord) :=
    p ○ [o !! "additional" / t :: o].

  Definition updateRecords (p : packet) answers' authority' additional' :=
    p ○ ["answers" ::= answers';
           "authority" ::= authority';
           "additional" ::= additional'].

  Definition get_name (r : resourceRecord) := r!sNAME.
  Definition name_length (r : resourceRecord) := String.length (get_name r).

  Definition isQuestion (p : packet) :=
    match p!"answers", p!"authority", p!"additional" with
    | nil, nil, nil => true
    | _, _, _ => false
    end.

  Definition is_empty {A} (l : list A) : bool :=
    match l with
    | nil => true
    | _ => false
    end.

  Lemma is_empty_app {A} :
    forall (l l' : list A),
      is_empty (l ++ l') = andb (is_empty l) (is_empty l').
  Proof.
    induction l; simpl; eauto.
  Qed.

  Definition isAnswer (p : packet) := negb (is_empty (p!"answers")).

  Definition isReferral (p : packet) :=
    is_empty (p!"answers")
             && (negb (is_empty (p!"authority")))
             && (negb (is_empty (p!"additional"))).

  Definition add_answers := List.fold_left add_answer.
  Definition add_nses := List.fold_left add_ns.
  Definition add_additionals := List.fold_left add_additional.

End Packet.

Coercion CNAME_Record2RRecord : CNAME_Record >-> resourceRecord.
Coercion A_Record2RRecord : A_Record >-> resourceRecord.
Coercion NS_Record2RRecord : NS_Record >-> resourceRecord.
Coercion MX_Record2RRecord : MX_Record >-> resourceRecord.
Coercion SOA_Record2RRecord : SOA_Record >-> resourceRecord.

author: proofskiddie

repo: CoqStuff

save_path: github-repos/coq/proofskiddie-CoqStuff


text:
(* (c) Copyright 2006-2018 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq.
From fourcolor Require Import cfmap cfreducible configurations.

(******************************************************************************)
(* Reducibility of configurations number 503 to 506, whose indices in         *)
(* the_configs range over segment [502, 506).                                 *)
(******************************************************************************)

Lemma red502to506 : reducible_in_range 502 506 the_configs.
Proof. CheckReducible. Qed.

author: coq-community

repo: fourcolor


text:
(**
CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.

- Frederic Blanqui, 2007-01-22

dependancy pairs graph

a more general development is given in AGraph.
*)

Set Implicit Arguments.

From Coq Require Import Lia.
From CoLoR Require ACompat.
From CoLoR Require Import LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation
     SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle.
From CoLoR Require Export ADP.

Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation terms := (vector term).
Notation rule := (rule Sig). Notation rules := (list rule).
Notation lhs := (@lhs Sig). Notation rhs := (@rhs Sig).

Variable R : rules.

Variable hyp : rules_preserve_vars R.

Notation DP := (dp R). Notation Chain := (chain R).

Lemma hyp' : rules_preserve_vars DP.

Proof.
apply dp_preserve_vars. exact hyp.
Qed.

(***********************************************************************)
(** dependancy pairs graph *)

Definition dp_graph a1 a2 := In a1 DP /\ In a2 DP
  /\ exists p, exists s,
    int_red R # (sub s (rhs a1)) (sub s (shift p (lhs a2))).

Lemma restricted_dp_graph : is_restricted dp_graph DP.

Proof.
unfold is_restricted, dp_graph, inclusion. intros. intuition.
Qed.

(***********************************************************************)
(** chain relation for a given dependency pair *)

Definition chain_dp a t u := In a DP /\
  exists s, int_red R # t (sub s (lhs a)) /\ u = sub s (rhs a).

Lemma chain_dp_chain : forall a, chain_dp a << Chain.

Proof.
unfold inclusion. intros. destruct H. do 2 destruct H0.
exists (sub x0 (lhs a)). intuition.
subst y. destruct a. simpl. apply hd_red_rule. exact H.
Qed.

Lemma chain_chain_dp : forall t u, Chain t u -> exists a, chain_dp a t u.

Proof.
intros. do 2 destruct H. redtac. subst x. subst u. exists (mkRule l r).
unfold chain_dp. simpl. intuition. exists s. intuition.
Qed.

(***********************************************************************)
(** iteration of chain steps given a list of dependency pairs *)

Fixpoint chain_dps (a : rule) (l : rules) : relation term :=
  match l with
    | nil => chain_dp a
    | b :: m => chain_dp a @ chain_dps b m
  end.

Lemma chain_dps_app : forall l a b m,
  chain_dps a (l ++ b :: m) << chain_dps a l @ chain_dps b m.

Proof. induction l; simpl; intros. refl. assoc. comp. apply IHl. Qed.

Arguments chain_dps_app [l a b m] _ _ _.

Lemma chain_dps_app' : forall a l m b p, a :: l = m ++ b :: p ->
  chain_dps a l << chain_dps a (tail m) % @ chain_dps b p.

Proof.
intros. destruct m; simpl in H; injection H; unfold inclusion; intros.
subst p. subst b. exists x. unfold clos_refl. intuition.
subst r. subst l. simpl. ded (chain_dps_app _ _ H2). do 2 destruct H0.
exists x0. unfold clos_refl. intuition.
Qed.

Arguments chain_dps_app' [a l m b p] _ [x y] _.

Lemma chain_dps_iter_chain :
  forall l a, chain_dps a l << iter Chain (length l).

Proof.
induction l; simpl; intros. apply chain_dp_chain.
comp. apply chain_dp_chain. apply IHl.
Qed.

Lemma iter_chain_chain_dps : forall n t u, iter Chain n t u ->
  exists a, exists l, length l = n /\ chain_dps a l t u.

Proof.
induction n; simpl; intros. ded (chain_chain_dp H). destruct H0.
exists x. exists nil. intuition.
do 2 destruct H. ded (chain_chain_dp H). destruct H1. exists x0.
ded (IHn _ _ H0). do 3 destruct H2. exists (x1 :: x2). simpl. intuition.
exists x. intuition.
Qed.

Arguments iter_chain_chain_dps [n t u] _.

(***********************************************************************)
(** two consecutive chain steps provide a dp_graph step *)

Lemma chain_dp2_dp_graph : forall a1 a2 t u v,
  chain_dp a1 t u -> chain_dp a2 u v -> dp_graph a1 a2.

Proof.
intros. destruct a1 as [l0 r0]. destruct a2 as [l1 r1].
destruct H. simpl in H1. do 2 destruct H1. subst u. rename x into s0.
destruct H0. simpl in H2. do 2 destruct H2. subst v. rename x into s1.
(* [maxvar l0 + 1] for shift *)
unfold dp_graph. intuition. simpl. set (p := maxvar l0 + 1). exists p.
(* take the union of s0 (restricted to [vars l0])
and [comp s1 (shift_inv_sub p l1)] (restricted to [vars (shift p l1)] *)
set (s0' := restrict s0 (vars l0)).
set (s1' := restrict (sub_comp s1 (shift_inv_sub p l1)) (vars (shift p l1))).
set (s := ASubstitution.union s0' s1'). exists s.
(* compatibility *)
assert (compat s0' s1' (vars l0) (vars (shift p l1))). unfold compat. intros.
ded (vars_max H3). ded (in_vars_shift_min H4). unfold p in H6.
absurd (x <= maxvar l0). lia. hyp.
(* domains of substitutions *)
assert (dom_incl s0' (vars l0)). unfold s0'. apply dom_incl_restrict.
assert (dom_incl s1' (vars (shift p l1))). unfold s1'. apply dom_incl_restrict.
(* inclusion in the dp_graph *)
assert (sub s r0 = sub s0' r0). unfold s. eapply sub_union1. apply H5.
apply H3. apply hyp'. hyp. rewrite H6.
assert (sub s0' r0 = sub s0 r0). unfold s0'. sym.
apply sub_restrict_incl. apply hyp'. hyp. rewrite H7.
assert (sub s (shift p l1) = sub s1' (shift p l1)).
unfold s. eapply sub_union2. apply H4. apply H3. refl.
rewrite H8.
assert (sub s1' (shift p l1) = sub s1 l1). unfold s1'.
rewrite <- sub_restrict, <- sub_shift.
refl. rewrite H9. hyp.
Qed.

Lemma chain_dps_path_dp_graph : forall l a b t u,
  chain_dps a (l ++ b :: nil) t u -> path dp_graph a b l.

Proof.
induction l; simpl; intros; do 2 destruct H.
eapply chain_dp2_dp_graph. apply H. apply H0.
ded (IHl _ _ _ _ H0). intuition.
destruct l; simpl in H0; do 2 destruct H0.
eapply chain_dp2_dp_graph. apply H. apply H0.
eapply chain_dp2_dp_graph. apply H. apply H0.
Qed.

Arguments chain_dps_path_dp_graph [l a b t u] _.

(***********************************************************************)
(** hypotheses of the criterion based on cycles
using the same reduction pair for every cycle *)

Import ACompat.

Variables (succ succ_eq : relation term)
  (Hredord : weak_rewrite_ordering succ succ_eq)
  (Hreword : rewrite_ordering succ_eq)
  (Habsorb : absorbs_left succ succ_eq)
  (HcompR : compat succ_eq R)
  (HcompDP : compat succ_eq (dp R))
  (Hwf : WF succ)
  (Hcycle : forall a l, length l < length DP -> cycle_min dp_graph a l ->
    exists b, In b (a :: l) /\ succ (lhs b) (rhs b)).

Notation eq_dec := (@eq_rule_dec Sig).
Notation occur := (occur eq_dec).

(***********************************************************************)
(** compatibility properties of chains *)

Lemma chain_dp_hd_red_mod : forall a, chain_dp a << hd_red_mod R (a::nil).

Proof.
unfold inclusion. intros. destruct H. do 2 destruct H0. subst y.
destruct a. simpl. simpl in H0. exists (sub x0 lhs). split.
apply incl_elim with (R := int_red R #). apply rtc_incl.
apply int_red_incl_red. exact H0. apply hd_red_rule. simpl. auto.
Qed.

Lemma compat_chain_dp : forall a, chain_dp a << succ_eq#.

Proof.
intros. incl_trans (red_mod R DP).
apply incl_trans with Chain; try incl_refl.
apply chain_dp_chain.
incl_trans (hd_red_mod R DP). apply chain_hd_red_mod.
apply hd_red_mod_incl_red_mod. incl_trans (succ_eq!).
apply compat_red_mod_tc; hyp. apply tc_incl_rtc.
Qed.

Lemma compat_chain_dps : forall l a, chain_dps a l << succ_eq#.

Proof.
induction l; simpl; intros. apply compat_chain_dp.
incl_trans (succ_eq# @ succ_eq#).
comp. apply compat_chain_dp. apply IHl. apply comp_rtc_idem.
Qed.

Lemma compat_chain_dp_strict : forall a,
  succ (lhs a) (rhs a) -> chain_dp a << succ.

Proof.
unfold inclusion. intros. destruct H0. do 2 destruct H1. subst y.
apply (absorbs_left_rtc Habsorb). exists (sub x0 (lhs a)). split.
apply incl_elim with (R := int_red R #). 2: exact H1.
apply rtc_incl.
incl_trans (red R). apply int_red_incl_red. apply compat_red; hyp.
destruct Hredord. apply H2. exact H.
Qed.

(***********************************************************************)
(** proof of the criterion based on cycles *)

Lemma WF_cycles : WF (chain R).

Proof.
(* we prove it by looking at paths of length n+3, where n = length DP *)
set (n := length DP). apply WF_iter with (S n). intro.
(* we proceed by induction on succ @ succ_eq# *)
assert (Hwf' : WF (succ @ succ_eq#)). apply absorb_WF_modulo_r; hyp.
gen (Hwf' x). induction 1. apply SN_intro; intros. apply H0.
(* path in the dp_graph corresponding to the chains *)
ded (iter_chain_chain_dps H1). do 3 destruct H2.
assert (length x1 > 0). lia. ded (last_intro H4). do 3 destruct H5.
clear H4. rewrite H5 in H3. ded (chain_dps_path_dp_graph H3).
(* pigeon-hole principle: there is a dp visited twice *)
set (l' := x0 :: x2 ++ x3 :: nil). assert (exists z, occur z l' >= 2).
unfold l'. eapply long_path_occur. apply restricted_dp_graph. apply H4.
rewrite H6, H2. unfold n. lia.
(* we prove (A): in this cycle, a dp is included in succ *)
assert (exists l, exists a, exists m,
  l' = l ++ a :: m /\ succ (lhs a) (rhs a)).
destruct H7. set (p := occur x4 l' - 2). assert (occur x4 l' = S (S p)).
unfold p. lia. ded (occur_S eq_dec H8). do 3 destruct H9. destruct H10.
clear H8. rewrite H9. ded (occur_S eq_dec H11). do 3 destruct H8.
destruct H12. clear H11. clear H13. clear p. rewrite H8. rewrite H8 in H9.
clear H8. clear H10.
(* cycle min *)
assert (cycle dp_graph x4 x7). unfold cycle. eapply sub_path. unfold l' in H9.
apply H9. exact H4. ded (cycle_min_intro eq_dec H8). decomp H10.
(* length x11 < length DP *)
assert (length l' = n+2). unfold l'. simpl. rewrite <- H5. lia.
rewrite H9 in H10. change (length (x5++(x4::x7)++x4::x8) = n+2) in H10.
rewrite H11 in H10. repeat (rewrite length_app in H10; simpl in H10).
unfold n in H10. assert (h : length x11 < length DP).
unfold cycle_min in H14. destruct H14. assert (length (x10::x11) <= length DP).
apply nodup_incl_length. apply eq_dec. exact H14.
apply incl_appr_incl with (x10::nil). simpl. eapply restricted_path_incl.
apply restricted_dp_graph. exact H13. simpl in H15. lia. clear H10.
(* end of the proof of (A) *)
ded (Hcycle h H14). do 2 destruct H10. ded (in_elim H10).
do 2 destruct H15. exists (x5++x9++x14). exists x13. exists (x15++x12++x4::x8).
intuition. rewrite !app_ass. trans (x5++(x4::x7)++x4::x8). refl.
rewrite H11, app_ass. trans (x5++x9++(x10::x11)++x12++x4::x8).
simpl. rewrite app_ass. refl. rewrite H15, app_ass. refl.
(* consequence of (A) *)
do 4 destruct H8. unfold l' in H8. ded (chain_dps_app' H8 H3).
do 2 destruct H10.
(* succ_eq# x x7 *)
assert (succ_eq# x x7). destruct H10. subst x7. intuition.
eapply incl_elim. eapply compat_chain_dps. apply H10.
(* (succ @ succ_eq#) x7 y *)
assert ((succ @ succ_eq#) x7 y). destruct x6; simpl in H11.
ded (compat_chain_dp_strict H9 H11). exists y. intuition.
do 2 destruct H11. exists x8. split. eapply incl_elim.
apply (compat_chain_dp_strict H9). exact H11.
eapply incl_elim. eapply compat_chain_dps. apply H13.
(* (succ @ succ_eq#) x y *)
do 2 destruct H13. exists x8. intuition.
eapply incl_elim with (R := succ_eq# @ succ). apply absorbs_left_rtc.
intuition. exists x7. intuition.
Qed.

End S.

author: fblanqui

repo: color

save_path: github-repos/coq/fblanqui-color