Module Qcert.NNRS.Lang.NNRSCrossShadow

Require Import String.
Require Import List.
Require Import Permutation.
Require Import ListSet.
Require Import BinInt.
Require Import Arith.
Require Import EquivDec.
Require Import Morphisms.
Require Import Arith.
Require Import Max.
Require Import Bool.
Require Import Peano_dec.
Require Import EquivDec.
Require Import Decidable.
Require Import Utils.
Require Import DataRuntime.
Require Import NNRS.
Require Import NNRSEval.
Require Import NNRSVars.
Require Import NNRSRename.

Section NNRSCrossShadow.
  
  Context {fruntime:foreign_runtime}.

  Local Open Scope nnrs.

  Section def.
    
    Fixpoint nnrs_stmt_cross_shadow_free_under
             (s:nnrs_stmt)
             (σ ψc ψd:list var)
    : Prop
      := match s with
         | NNRSSeq s₁ s₂ =>
           nnrs_stmt_cross_shadow_free_under s₁ σ ψc ψd
           /\ nnrs_stmt_cross_shadow_free_under s₂ σ ψc ψd
         | NNRSLet v e s₀ =>
           disjoint (nnrs_expr_free_vars e) ψc
           /\ disjoint (nnrs_expr_free_vars e) ψd
           /\ ~ In v ψc
           /\ ~ In v ψd
           /\ nnrs_stmt_cross_shadow_free_under s₀ (v::σ) ψc ψd
         | NNRSLetMut v s₁ s₂ =>
           ~ In v σ
           /\ ~ In v ψc
           /\ ~ In v ψd
           /\ nnrs_stmt_cross_shadow_free_under s₁ σ ψc (v::ψd)
           /\ nnrs_stmt_cross_shadow_free_under s₂ (v::σ) ψc ψd
         | NNRSLetMutColl v s₁ s₂ =>
           ~ In v σ
           /\ ~ In v ψc
           /\ ~ In v ψd
           /\ nnrs_stmt_cross_shadow_free_under s₁ σ (v::ψc) ψd
           /\ nnrs_stmt_cross_shadow_free_under s₂ (v::σ) ψc ψd
         | NNRSAssign v e =>
           disjoint (nnrs_expr_free_vars e) ψc
           /\ disjoint (nnrs_expr_free_vars e) ψd
           /\ ~ In v σ
           /\ ~ In v ψc
         | NNRSPush v e =>
           disjoint (nnrs_expr_free_vars e) ψc
           /\ disjoint (nnrs_expr_free_vars e) ψd
           /\ ~ In v σ
           /\ ~ In v ψd
         | NNRSFor v e s₀ =>
           disjoint (nnrs_expr_free_vars e) ψc
           /\ disjoint (nnrs_expr_free_vars e) ψd
           /\ ~ In v ψc
           /\ ~ In v ψd
           /\ nnrs_stmt_cross_shadow_free_under s₀ (v::σ) ψc ψd
         | NNRSIf e s₁ s₂ =>
           disjoint (nnrs_expr_free_vars e) ψc
           /\ disjoint (nnrs_expr_free_vars e) ψd
           /\ nnrs_stmt_cross_shadow_free_under s₁ σ ψc ψd
           /\ nnrs_stmt_cross_shadow_free_under s₂ σ ψc ψd
         | NNRSEither e x₁ s₁ x₂ s₂ =>
           disjoint (nnrs_expr_free_vars e) ψc
           /\ disjoint (nnrs_expr_free_vars e) ψd
           /\ ~ In x₁ ψc
           /\ ~ In x₁ ψd
           /\ ~ In x₂ ψc
           /\ ~ In x₂ ψd
           /\ nnrs_stmt_cross_shadow_free_under s₁ (x₁::σ) ψc ψd
           /\ nnrs_stmt_cross_shadow_free_under s₂ (x₂::σ) ψc ψd
         end.

    Definition nnrs_cross_shadow_free (s:nnrs)
      := nnrs_stmt_cross_shadow_free_under (fst s) nil nil (snd s::nil).

  End def.

  Section cross_shadow_free_disjointness.

    Lemma nnrs_stmt_cross_shadow_free_under_free_mcenv_env
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_free_mcenv_vars s) σ.

    Lemma nnrs_stmt_cross_shadow_free_under_free_mdenv_env
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_free_mdenv_vars s) σ.

    Lemma nnrs_stmt_cross_shadow_free_under_free_env_mcenv
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_free_env_vars s) ψc.

    Lemma nnrs_stmt_cross_shadow_free_under_free_mdenv_mcenv
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_free_mdenv_vars s) ψc.

    Lemma nnrs_stmt_cross_shadow_free_under_free_env_mdenv
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_free_env_vars s) ψd.

    Lemma nnrs_stmt_cross_shadow_free_under_free_mcenv_mdenv
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_free_mcenv_vars s) ψd.
    
    Lemma nnrs_stmt_cross_shadow_free_under_free_env_cons
          {s:nnrs_stmt} {σ ψc ψd:list var} {v} :
      nnrs_stmt_cross_shadow_free_under s (v::σ) ψc ψd ->
      ~ In v (nnrs_stmt_free_mcenv_vars s) /\ ~ In v (nnrs_stmt_free_mdenv_vars s).

    Lemma nnrs_stmt_cross_shadow_free_under_free_mcenv_cons
          {s:nnrs_stmt} {σ ψc ψd:list var} {v} :
      nnrs_stmt_cross_shadow_free_under s σ (v::ψc) ψd ->
      ~ In v (nnrs_stmt_free_env_vars s) /\ ~ In v (nnrs_stmt_free_mdenv_vars s).

    Lemma nnrs_stmt_cross_shadow_free_under_free_mdenv_cons
          {s:nnrs_stmt} {σ ψc ψd:list var} {v} :
      nnrs_stmt_cross_shadow_free_under s σ ψc (v::ψd) ->
      ~ In v (nnrs_stmt_free_env_vars s) /\ ~ In v (nnrs_stmt_free_mcenv_vars s).

    Lemma nnrs_stmt_cross_shadow_free_under_free_cons
          (s:nnrs_stmt) (σ ψc ψd:list var) v :
      (nnrs_stmt_cross_shadow_free_under s (v::σ) ψc ψd ->
       ~ In v (nnrs_stmt_free_mcenv_vars s) /\ ~ In v (nnrs_stmt_free_mdenv_vars s))
      /\ (nnrs_stmt_cross_shadow_free_under s σ (v::ψc) ψd ->
          ~ In v (nnrs_stmt_free_env_vars s) /\ ~ In v (nnrs_stmt_free_mdenv_vars s))
      /\ (nnrs_stmt_cross_shadow_free_under s σ ψc (v::ψd) ->
          ~ In v (nnrs_stmt_free_env_vars s) /\ ~ In v (nnrs_stmt_free_mcenv_vars s))

    .

    Lemma nnrs_stmt_cross_shadow_free_under_bound_mcenv_env
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_bound_mcenv_vars s) σ.

    Lemma nnrs_stmt_cross_shadow_free_under_bound_mdenv_env
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_bound_mdenv_vars s) σ.

    Lemma nnrs_stmt_cross_shadow_free_under_bound_env_mcenv
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_bound_env_vars s) ψc.

    Lemma nnrs_stmt_cross_shadow_free_under_bound_mdenv_mcenv
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_bound_mdenv_vars s) ψc.

    Lemma nnrs_stmt_cross_shadow_free_under_bound_env_mdenv
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_bound_env_vars s) ψd.

    Lemma nnrs_stmt_cross_shadow_free_under_bound_mcenv_mdenv
          (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      disjoint (nnrs_stmt_bound_mcenv_vars s) ψd.
    
    Lemma nnrs_stmt_cross_shadow_free_under_bound_env_cons
          {s:nnrs_stmt} {σ ψc ψd:list var} {v} :
      nnrs_stmt_cross_shadow_free_under s (v::σ) ψc ψd ->
      ~ In v (nnrs_stmt_bound_mcenv_vars s) /\ ~ In v (nnrs_stmt_bound_mdenv_vars s).

    Lemma nnrs_stmt_cross_shadow_free_under_bound_mcenv_cons
          {s:nnrs_stmt} {σ ψc ψd:list var} {v} :
      nnrs_stmt_cross_shadow_free_under s σ (v::ψc) ψd ->
      ~ In v (nnrs_stmt_bound_env_vars s) /\ ~ In v (nnrs_stmt_bound_mdenv_vars s).

    Lemma nnrs_stmt_cross_shadow_free_under_bound_mdenv_cons
          {s:nnrs_stmt} {σ ψc ψd:list var} {v} :
      nnrs_stmt_cross_shadow_free_under s σ ψc (v::ψd) ->
      ~ In v (nnrs_stmt_bound_env_vars s) /\ ~ In v (nnrs_stmt_bound_mcenv_vars s).

    Lemma nnrs_stmt_cross_shadow_free_under_bound_cons
          (s:nnrs_stmt) (σ ψc ψd:list var) v :
      (nnrs_stmt_cross_shadow_free_under s (v::σ) ψc ψd ->
       ~ In v (nnrs_stmt_bound_mcenv_vars s) /\ ~ In v (nnrs_stmt_bound_mdenv_vars s))
      /\ (nnrs_stmt_cross_shadow_free_under s σ (v::ψc) ψd ->
          ~ In v (nnrs_stmt_bound_env_vars s) /\ ~ In v (nnrs_stmt_bound_mdenv_vars s))
      /\ (nnrs_stmt_cross_shadow_free_under s σ ψc (v::ψd) ->
          ~ In v (nnrs_stmt_bound_env_vars s) /\ ~ In v (nnrs_stmt_bound_mcenv_vars s))

    .

    Lemma nnrs_stmt_cross_shadow_free_under_vars_cons
          (s:nnrs_stmt) (σ ψc ψd:list var) v :
      (nnrs_stmt_cross_shadow_free_under s (v::σ) ψc ψd ->
       ~ In v (nnrs_stmt_free_mcenv_vars s) /\ ~ In v (nnrs_stmt_free_mdenv_vars s)
       /\ ~ In v (nnrs_stmt_bound_mcenv_vars s) /\ ~ In v (nnrs_stmt_bound_mdenv_vars s))
      /\ (nnrs_stmt_cross_shadow_free_under s σ (v::ψc) ψd ->
          ~ In v (nnrs_stmt_free_env_vars s) /\ ~ In v (nnrs_stmt_free_mdenv_vars s)
          /\ ~ In v (nnrs_stmt_bound_env_vars s) /\ ~ In v (nnrs_stmt_bound_mdenv_vars s))
      /\ (nnrs_stmt_cross_shadow_free_under s σ ψc (v::ψd) ->
          ~ In v (nnrs_stmt_free_env_vars s) /\ ~ In v (nnrs_stmt_free_mcenv_vars s)
          /\ ~ In v (nnrs_stmt_bound_env_vars s) /\ ~ In v (nnrs_stmt_bound_mcenv_vars s))
           
    .
    
  End cross_shadow_free_disjointness.

  Section cross_shadow_free_equivs.
    
    Global Instance nnrs_stmt_cross_shadow_free_under_equivs :
      Proper (eq ==> equivlist ==> equivlist ==> equivlist ==> iff) nnrs_stmt_cross_shadow_free_under.

    Global Instance nnrs_stmt_cross_shadow_free_under_incls :
      Proper (eq ==> (@incl string) --> (@incl string) --> (@incl string) --> Basics.impl) nnrs_stmt_cross_shadow_free_under.

  End cross_shadow_free_equivs.


  Section cross_shadow_free_alt.

    Fixpoint nnrs_stmt_cross_shadow_free_alt
             (s:nnrs_stmt)
    : Prop
      := match s with
         | NNRSSeq s₁ s₂ =>
           nnrs_stmt_cross_shadow_free_alt s₁
           /\ nnrs_stmt_cross_shadow_free_alt s₂
         | NNRSLet v e s₀ =>
           ~ In v (nnrs_stmt_free_mcenv_vars s₀)
           /\ ~ In v (nnrs_stmt_bound_mcenv_vars s₀)
           /\ ~ In v (nnrs_stmt_free_mdenv_vars s₀)
           /\ ~ In v (nnrs_stmt_bound_mdenv_vars s₀)
           /\ nnrs_stmt_cross_shadow_free_alt s₀
         | NNRSLetMut v s₁ s₂ =>
           ~ In v (nnrs_stmt_free_env_vars s₁)
           /\ ~ In v (nnrs_stmt_bound_env_vars s₁)
           /\ ~ In v (nnrs_stmt_free_mcenv_vars s₁)
           /\ ~ In v (nnrs_stmt_bound_mcenv_vars s₁)
           /\ ~ In v (nnrs_stmt_free_mcenv_vars s₂)
           /\ ~ In v (nnrs_stmt_bound_mcenv_vars s₂)
           /\ ~ In v (nnrs_stmt_bound_mdenv_vars s₂)
           /\ ~ In v (nnrs_stmt_free_mdenv_vars s₂)
           /\ nnrs_stmt_cross_shadow_free_alt s₁
           /\ nnrs_stmt_cross_shadow_free_alt s₂
         | NNRSLetMutColl v s₁ s₂ =>
           ~ In v (nnrs_stmt_free_env_vars s₁)
           /\ ~ In v (nnrs_stmt_bound_env_vars s₁)
           /\ ~ In v (nnrs_stmt_free_mdenv_vars s₁)
           /\ ~ In v (nnrs_stmt_bound_mdenv_vars s₁)
           /\ ~ In v (nnrs_stmt_free_mcenv_vars s₂)
           /\ ~ In v (nnrs_stmt_bound_mcenv_vars s₂)
           /\ ~ In v (nnrs_stmt_bound_mdenv_vars s₂)
           /\ ~ In v (nnrs_stmt_free_mdenv_vars s₂)
           /\ nnrs_stmt_cross_shadow_free_alt s₁
           /\ nnrs_stmt_cross_shadow_free_alt s₂
         | NNRSAssign v e => True
         | NNRSPush v e => True
         | NNRSFor v e s₀ =>
           ~ In v (nnrs_stmt_free_mcenv_vars s₀)
           /\ ~ In v (nnrs_stmt_bound_mcenv_vars s₀)
           /\ ~ In v (nnrs_stmt_free_mdenv_vars s₀)
           /\ ~ In v (nnrs_stmt_bound_mdenv_vars s₀)
           /\ nnrs_stmt_cross_shadow_free_alt s₀
         | NNRSIf e s₁ s₂ =>
           nnrs_stmt_cross_shadow_free_alt s₁
           /\ nnrs_stmt_cross_shadow_free_alt s₂
         | NNRSEither e x₁ s₁ x₂ s₂ =>
           ~ In x₁ (nnrs_stmt_free_mcenv_vars s₁)
           /\ ~ In x₁ (nnrs_stmt_bound_mcenv_vars s₁)
           /\ ~ In x₁ (nnrs_stmt_free_mdenv_vars s₁)
           /\ ~ In x₁ (nnrs_stmt_bound_mdenv_vars s₁)
           /\ ~ In x₂ (nnrs_stmt_free_mcenv_vars s₂)
           /\ ~ In x₂ (nnrs_stmt_bound_mcenv_vars s₂)
           /\ ~ In x₂ (nnrs_stmt_free_mdenv_vars s₂)
           /\ ~ In x₂ (nnrs_stmt_bound_mdenv_vars s₂)
           /\ nnrs_stmt_cross_shadow_free_alt s₁
           /\ nnrs_stmt_cross_shadow_free_alt s₂
         end.

    Ltac disj_tac :=
      repeat
        (match goal with
         | [ H : disjoint (_ ++ _) _ |- _ ] => apply disjoint_app_l in H; destruct H
         | [ H : disjoint (_ :: _) _ |- _ ] => apply disjoint_cons_inv1 in H; destruct H
         | [ H : disjoint _ (_ :: _) |- _ ] => apply disjoint_cons_inv2 in H; destruct H
         | [H1:disjoint (remove _ ?v ?l1) ?l2,
               H2:In ?v ?l1 -> False |- _ ] => rewrite nin_remove in H1 by apply H2
         | [H1:disjoint (remove _ ?v ?l1) ?l2,
               H2:~ In ?v ?l1 |- _ ] => rewrite nin_remove in H1 by apply H2
         | [H1:disjoint (remove _ ?v ?l1) ?l2,
               H2:In ?v ?l2 -> False |- _ ] => rewrite disjoint_remove_swap in H1; rewrite nin_remove in H1 by apply H2
         | [H1:disjoint (remove _ ?v ?l1) ?l2,
               H2:~ In ?v ?l2 |- _ ] => rewrite disjoint_remove_swap in H1; rewrite nin_remove in H1 by apply H2
         | [H : In _ (replace_all _ _ _ ) |- _ ] => apply in_replace_all in H; try solve [destruct H as [?|[??]]; subst; eauto]
         | [H: ~ In _ (remove _ _ _) |- _ ] => try rewrite <- remove_in_neq in H by congruence
         | [H: In _ (remove _ _ _) -> False |- _ ] => try rewrite <- remove_in_neq in H by congruence
         | [ |- disjoint (_ :: _) _ ] => apply disjoint_cons1
         | [ |- disjoint _ (_ :: _) ] => apply disjoint_cons2
         | [ |- disjoint _ (replace_all _ _ _ )] => try solve [apply disjoint_replace_all; intuition]
                                                        
         end; repeat rewrite in_app_iff in *
        ).

    Theorem nnrs_stmt_cross_shadow_free_alt_under
             (s:nnrs_stmt) :
      nnrs_stmt_cross_shadow_free_alt s ->
      forall (σ ψc ψd:list var),
        disjoint (nnrs_stmt_free_mcenv_vars s) σ ->
        disjoint (nnrs_stmt_bound_mcenv_vars s) σ ->
        disjoint (nnrs_stmt_free_mdenv_vars s) σ ->
        disjoint (nnrs_stmt_bound_mdenv_vars s) σ ->
        disjoint (nnrs_stmt_free_env_vars s) ψc ->
        disjoint (nnrs_stmt_bound_env_vars s) ψc ->
        disjoint (nnrs_stmt_free_mdenv_vars s) ψc ->
        disjoint (nnrs_stmt_bound_mdenv_vars s) ψc ->
        disjoint (nnrs_stmt_free_env_vars s) ψd ->
        disjoint (nnrs_stmt_bound_env_vars s) ψd ->
        disjoint (nnrs_stmt_free_mcenv_vars s) ψd ->
        disjoint (nnrs_stmt_bound_mcenv_vars s) ψd ->
        nnrs_stmt_cross_shadow_free_under s σ ψc ψd.

    Theorem nnrs_stmt_cross_shadow_free_under_alt (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      nnrs_stmt_cross_shadow_free_alt s.


    Ltac fresh_simpl_rewriter
      := repeat autorewrite with nnrs_rename in *
         ; repeat rewrite in_app_iff in *
         ; repeat match goal with
                  | [H: In _ (nnrs_stmt_free_env_vars (nnrs_stmt_rename_env _ _ _)) |- _] => apply nnrs_stmt_free_env_vars_rename_env_in in H
                  | [H: In _ (nnrs_stmt_free_mcenv_vars (nnrs_stmt_rename_mc _ _ _)) |- _] => apply nnrs_stmt_free_mcenv_vars_rename_mcenv_in in H
                  | [H: In _ (nnrs_stmt_free_mdenv_vars (nnrs_stmt_rename_md _ _ _)) |- _] => apply nnrs_stmt_free_mdenv_vars_rename_mdenv_in in H
                  | [H: In _ (remove _ _ _) -> False |- _ ] =>
                    try rewrite <- remove_in_neq in H by congruence
                  end
         ; intuition.

    
    Lemma nnrs_stmt_cross_shadow_free_alt_rename_env s v v' :
      ~ In v' (nnrs_stmt_free_mcenv_vars s) ->
      ~ In v' (nnrs_stmt_bound_mcenv_vars s )->
      ~ In v' (nnrs_stmt_free_mdenv_vars s) ->
      ~ In v' (nnrs_stmt_bound_mdenv_vars s) ->
      nnrs_stmt_cross_shadow_free_alt s ->
      nnrs_stmt_cross_shadow_free_alt
        (nnrs_stmt_rename_env s v v').

    Lemma nnrs_stmt_cross_shadow_free_alt_rename_mcenv s v v' :
      ~ In v' (nnrs_stmt_free_env_vars s) ->
      ~ In v' (nnrs_stmt_bound_env_vars s )->
      ~ In v' (nnrs_stmt_free_mdenv_vars s) ->
      ~ In v' (nnrs_stmt_bound_mdenv_vars s) ->
      nnrs_stmt_cross_shadow_free_alt s ->
      nnrs_stmt_cross_shadow_free_alt
        (nnrs_stmt_rename_mc s v v').

    Lemma nnrs_stmt_cross_shadow_free_alt_rename_mdenv s v v' :
      ~ In v' (nnrs_stmt_free_env_vars s) ->
      ~ In v' (nnrs_stmt_bound_env_vars s )->
      ~ In v' (nnrs_stmt_free_mcenv_vars s) ->
      ~ In v' (nnrs_stmt_bound_mcenv_vars s) ->
      nnrs_stmt_cross_shadow_free_alt s ->
      nnrs_stmt_cross_shadow_free_alt
        (nnrs_stmt_rename_md s v v').

  End cross_shadow_free_alt.


  Section uncross.

    Context (sep:string).
    Fixpoint nnrs_stmt_uncross_shadow_under
             (s:nnrs_stmt)
             (σ ψc ψd:list var)
      : nnrs_stmt
      := match s with
         | NNRSSeq s₁ s₂ =>
           NNRSSeq
             (nnrs_stmt_uncross_shadow_under s₁ σ ψc ψd)
             (nnrs_stmt_uncross_shadow_under s₂ σ ψc ψd)
         | NNRSLet v e s₀ =>
           let s₀' := nnrs_stmt_uncross_shadow_under s₀ (v::σ) ψc ψd in
           let problems :=
               remove equiv_dec v (nnrs_stmt_free_env_vars s₀')
                      ++ remove equiv_dec v (nnrs_stmt_bound_env_vars s₀')
                      ++ (nnrs_stmt_free_mcenv_vars s₀')
                      ++ (nnrs_stmt_bound_mcenv_vars s₀')
                      ++ (nnrs_stmt_free_mdenv_vars s₀')
                      ++ (nnrs_stmt_bound_mdenv_vars s₀')
           in
           let v' := fresh_var_from sep v problems in
           NNRSLet v' e (mk_lazy_lift nnrs_stmt_rename_env s₀' v v')
         | NNRSLetMut v s₁ s₂ =>
           let s₁' := nnrs_stmt_uncross_shadow_under s₁ σ ψc (v::ψd) in
           let s₂' := nnrs_stmt_uncross_shadow_under s₂ (v::σ) ψc ψd in
           let problems := remove equiv_dec v (nnrs_stmt_free_mdenv_vars s₁')
                                  ++ remove equiv_dec v (nnrs_stmt_bound_mdenv_vars s₁')
                                  ++ remove equiv_dec v (nnrs_stmt_free_env_vars s₂')
                                  ++ remove equiv_dec v (nnrs_stmt_bound_env_vars s₂')
                                  ++ σ
                                  ++ ψd
                                  ++ nnrs_stmt_free_env_vars s₁'
                                  ++ nnrs_stmt_bound_env_vars s₁'
                                  ++ nnrs_stmt_free_mcenv_vars s₁'
                                  ++ nnrs_stmt_bound_mcenv_vars s₁'
                                  ++ nnrs_stmt_free_mcenv_vars s₂'
                                  ++ nnrs_stmt_bound_mcenv_vars s₂'
                                  ++ nnrs_stmt_free_mdenv_vars s₂'
                                  ++ nnrs_stmt_bound_mdenv_vars s₂' in
           let v' := fresh_var_from sep v problems in
           NNRSLetMut v'
                      (mk_lazy_lift nnrs_stmt_rename_md s₁' v v')
                      (mk_lazy_lift nnrs_stmt_rename_env s₂' v v')
         | NNRSLetMutColl v s₁ s₂ =>
           let s₁' := nnrs_stmt_uncross_shadow_under s₁ σ (v::ψc) ψd in
           let s₂' := nnrs_stmt_uncross_shadow_under s₂ (v::σ) ψc ψd in
           let problems := remove equiv_dec v (nnrs_stmt_free_mcenv_vars s₁')
                                   ++ remove equiv_dec v (nnrs_stmt_bound_mcenv_vars s₁')
                                   ++ remove equiv_dec v (nnrs_stmt_free_env_vars s₂')
                                   ++ remove equiv_dec v (nnrs_stmt_bound_env_vars s₂')
                                   ++ σ
                                   ++ ψd
                                   ++ ψc
                                   ++ nnrs_stmt_free_env_vars s₁'
                                   ++ nnrs_stmt_bound_env_vars s₁'
                                   ++ nnrs_stmt_free_mdenv_vars s₁'
                                   ++ nnrs_stmt_bound_mdenv_vars s₁'
                                   ++ nnrs_stmt_free_mcenv_vars s₂'
                                   ++ nnrs_stmt_bound_mcenv_vars s₂'
                                   ++ nnrs_stmt_free_mdenv_vars s₂'
                                   ++ nnrs_stmt_bound_mdenv_vars s₂' in
           let v' := fresh_var_from sep v problems in
           NNRSLetMutColl v'
                          (mk_lazy_lift nnrs_stmt_rename_mc s₁' v v')
                          (mk_lazy_lift nnrs_stmt_rename_env s₂' v v')
         | NNRSAssign v e =>
           NNRSAssign v e
         | NNRSPush v e =>
           NNRSPush v e
         | NNRSFor v e s₀ =>
           let s₀' := nnrs_stmt_uncross_shadow_under s₀ (v::σ) ψc ψd in
           let problems := remove equiv_dec v (nnrs_stmt_free_env_vars s₀')
                                  ++ remove equiv_dec v (nnrs_stmt_bound_env_vars s₀')
                                  ++ (nnrs_stmt_free_mcenv_vars s₀')
                                  ++ (nnrs_stmt_bound_mcenv_vars s₀')
                                  ++ (nnrs_stmt_free_mdenv_vars s₀')
                                  ++ (nnrs_stmt_bound_mdenv_vars s₀') in
           let v' := fresh_var_from sep v problems in
           NNRSFor v' e (mk_lazy_lift nnrs_stmt_rename_env s₀' v v')
         | NNRSIf e s₁ s₂ =>
           NNRSIf
             e
             (nnrs_stmt_uncross_shadow_under s₁ σ ψc ψd)
             (nnrs_stmt_uncross_shadow_under s₂ σ ψc ψd)
         | NNRSEither e x₁ s₁ x₂ s₂ =>
           let s₁' := nnrs_stmt_uncross_shadow_under s₁ (x₁::σ) ψc ψd in
           let problems₁ := remove equiv_dec x₁ (nnrs_stmt_free_env_vars s₁')
                                    ++ remove equiv_dec x₁ (nnrs_stmt_bound_env_vars s₁')
                                    ++ (nnrs_stmt_free_mcenv_vars s₁')
                                    ++ (nnrs_stmt_bound_mcenv_vars s₁')
                                    ++ (nnrs_stmt_free_mdenv_vars s₁')
                                    ++ (nnrs_stmt_bound_mdenv_vars s₁') in
           let x₁' := fresh_var_from sep x₁ problems₁ in
           let s₂' := nnrs_stmt_uncross_shadow_under s₂ (x₂::σ) ψc ψd in
           let problems₂ := remove equiv_dec x₂ (nnrs_stmt_free_env_vars s₂')
                                   ++ remove equiv_dec x₂ (nnrs_stmt_bound_env_vars s₂')
                                   ++ (nnrs_stmt_free_mcenv_vars s₂')
                                   ++ (nnrs_stmt_bound_mcenv_vars s₂')
                                   ++ (nnrs_stmt_free_mdenv_vars s₂')
                                   ++ (nnrs_stmt_bound_mdenv_vars s₂') in
           let x₂' := fresh_var_from sep x₂ problems₂ in
           NNRSEither e
                      x₁'
                      (mk_lazy_lift nnrs_stmt_rename_env s₁' x₁ x₁')
                      x₂'
                      (mk_lazy_lift nnrs_stmt_rename_env s₂' x₂ x₂')
         end.

    Definition nnrs_uncross_shadow
               (s:nnrs)
      : nnrs
      :=
        let s' := nnrs_stmt_uncross_shadow_under (fst s) nil nil (snd s::nil) in
        let problems := nnrs_stmt_free_env_vars s'
                                                ++ nnrs_stmt_bound_env_vars s'
                                                ++ nnrs_stmt_free_mcenv_vars s'
                                                ++ nnrs_stmt_bound_mcenv_vars s'
                                                ++ remove equiv_dec (snd s) (nnrs_stmt_free_mdenv_vars s')
                                                ++ remove equiv_dec (snd s) (nnrs_stmt_bound_mdenv_vars s') in
        let v' := fresh_var_from sep (snd s) problems in
        (mk_lazy_lift nnrs_stmt_rename_md s' (snd s) v', v').

  End uncross.

  Section uncross_free.

    Ltac unlazy_tac :=
      try (apply mk_lazy_lift_prop;
         let H := fresh "eqq" in
         intros H; subst; try rewrite <- H; eauto).


    Ltac addremove_inclin_tac
      := let HH:= fresh "inn" in
         let HH2 := fresh "inn" in
         intros HH
         ; match type of HH with
             In ?fv ?l =>
             match fv with
             | (fresh_var_from _ ?v _) => assert (HH2:In fv (remove equiv_dec v l))
                 by (apply remove_in_neq; auto)
             end
           end; revert HH2
         ; apply fresh_var_from_incl_nin
         ; intros ? ?; repeat rewrite in_app_iff; tauto.

    Ltac freeuncross_t IH renH
      := unlazy_tac
         ; [rewrite IH; trivial
           | rewrite renH
             ; [rewrite IH
                ; apply remove_replace_all_nin
                ; addremove_inclin_tac
               | addremove_inclin_tac
           ]].

      Ltac fresh_prover
    :=
      repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_env_vars_rename_env)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_mcenv_vars_rename_env)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mcenv_vars_rename_env)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_mdenv_vars_rename_env)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mdenv_vars_rename_env)
               
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_env_vars_rename_mcenv)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_env_vars_rename_mcenv)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mcenv_vars_rename_mcenv)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_mdenv_vars_rename_mcenv)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mdenv_vars_rename_mcenv)

      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_env_vars_rename_mdenv)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_env_vars_rename_mdenv)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_mcenv_vars_rename_mdenv)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mcenv_vars_rename_mdenv)
      ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mdenv_vars_rename_mdenv)

      ; try solve [apply fresh_var_from_incl_nin
                   ; unfold incl; intros; repeat rewrite in_app_iff; intuition].

    Lemma nnrs_stmt_free_env_vars_uncross_under sep s σ ψc ψd :
      nnrs_stmt_free_env_vars (nnrs_stmt_uncross_shadow_under sep s σ ψc ψd)
      = nnrs_stmt_free_env_vars s.

    Lemma nnrs_stmt_free_mdenv_vars_uncross_under sep s σ ψc ψd :
      nnrs_stmt_free_mdenv_vars (nnrs_stmt_uncross_shadow_under sep s σ ψc ψd)
      = nnrs_stmt_free_mdenv_vars s.

    Lemma nnrs_stmt_free_mcenv_vars_uncross_under sep s σ ψc ψd :
      nnrs_stmt_free_mcenv_vars (nnrs_stmt_uncross_shadow_under sep s σ ψc ψd)
      = nnrs_stmt_free_mcenv_vars s.

  End uncross_free.

  Section correctness.

    Ltac fresh_prover
      :=
        repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_env_vars_rename_env)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_mcenv_vars_rename_env)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mcenv_vars_rename_env)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_mdenv_vars_rename_env)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mdenv_vars_rename_env)
                 
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_env_vars_rename_mcenv)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_env_vars_rename_mcenv)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mcenv_vars_rename_mcenv)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_mdenv_vars_rename_mcenv)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mdenv_vars_rename_mcenv)

        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_env_vars_rename_mdenv)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_env_vars_rename_mdenv)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_free_mcenv_vars_rename_mdenv)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mcenv_vars_rename_mdenv)
        ; repeat rewrite (mk_lazy_lift_under nnrs_stmt_bound_mdenv_vars_rename_mdenv)

        ; try solve [apply fresh_var_from_incl_nin
                     ; unfold incl; intros; repeat rewrite in_app_iff; intuition].
    
    Lemma nnrs_stmt_uncross_shadow_free_alt sep (s:nnrs_stmt)
          (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_alt
        (nnrs_stmt_uncross_shadow_under sep s σ ψc ψd).

    Theorem nnrs_uncross_shadow_free sep (s:nnrs) :
      nnrs_cross_shadow_free (nnrs_uncross_shadow sep s).

    Lemma nnrs_stmt_uncross_shadow_under_eval h c sep (s:nnrs_stmt) σ ψc ψd domσ domψc domψd :
      nnrs_stmt_eval h c σ ψc ψd (nnrs_stmt_uncross_shadow_under sep s domσ domψc domψd) = nnrs_stmt_eval h c σ ψc ψd s.

    Theorem nnrs_uncross_shadow_eval h c sep (s:nnrs) :
      nnrs_eval h c (nnrs_uncross_shadow sep s) = nnrs_eval h c s.

  End correctness.

  Section idempotence.

    Ltac disj_tac :=
      repeat progress
             (repeat rewrite in_app_iff in *
              ; try match goal with
                    | [ H : disjoint (_ ++ _) _ |- _ ] => apply disjoint_app_l in H; destruct H
                    | [ H : disjoint (_ :: _) _ |- _ ] => apply disjoint_cons_inv1 in H; destruct H
                    | [ H : disjoint _ (_ :: _) |- _ ] => apply disjoint_cons_inv2 in H; destruct H
                    | [H1:disjoint (remove _ ?v ?l1) ?l2,
                          H2:In ?v ?l1 -> False |- _ ] => rewrite nin_remove in H1 by apply H2
                    | [H1:disjoint (remove _ ?v ?l1) ?l2,
                          H2:~ In ?v ?l1 |- _ ] => rewrite nin_remove in H1 by apply H2
                    | [H1:disjoint (remove _ ?v ?l1) ?l2,
                          H2:In ?v ?l2 -> False |- _ ] => rewrite disjoint_remove_swap in H1; rewrite nin_remove in H1 by apply H2
                    | [H1:disjoint (remove _ ?v ?l1) ?l2,
                          H2:~ In ?v ?l2 |- _ ] => rewrite disjoint_remove_swap in H1; rewrite nin_remove in H1 by apply H2
                    | [H : In _ (replace_all _ _ _ ) |- _ ] => apply in_replace_all in H; try solve [destruct H as [?|[??]]; subst; eauto]
                    | [H: ~ In _ (remove _ _ _) |- _ ] => try rewrite <- remove_in_neq in H by congruence
                    | [H: In _ (remove _ _ _) -> False |- _ ] => try rewrite <- remove_in_neq in H by congruence
                    | [ |- disjoint (_ :: _) _ ] => apply disjoint_cons1
                    | [ |- disjoint _ (_ :: _) ] => apply disjoint_cons2
                    | [ |- disjoint _ (replace_all _ _ _ )] => try solve [apply disjoint_replace_all; intuition]
                    | [ H: In _ (remove _ _ _) |- _ ] => apply remove_inv in H; destruct H; try congruence
                    end
             ).
    
    Lemma nnrs_stmt_uncross_shadow_under_alt_id sep (s:nnrs_stmt) :
      nnrs_stmt_cross_shadow_free_alt s ->
      forall (σ ψc ψd:list var),
        disjoint (nnrs_stmt_free_mcenv_vars s) σ ->
        disjoint (nnrs_stmt_bound_mcenv_vars s) σ ->
        disjoint (nnrs_stmt_free_mdenv_vars s) σ ->
        disjoint (nnrs_stmt_bound_mdenv_vars s) σ ->
        disjoint (nnrs_stmt_free_env_vars s) ψc ->
        disjoint (nnrs_stmt_bound_env_vars s) ψc ->
        disjoint (nnrs_stmt_free_mdenv_vars s) ψc ->
        disjoint (nnrs_stmt_bound_mdenv_vars s) ψc ->
        disjoint (nnrs_stmt_free_env_vars s) ψd ->
        disjoint (nnrs_stmt_bound_env_vars s) ψd ->
        disjoint (nnrs_stmt_free_mcenv_vars s) ψd ->
        disjoint (nnrs_stmt_bound_mcenv_vars s) ψd ->
        nnrs_stmt_uncross_shadow_under sep s σ ψc ψd = s.

    Lemma nnrs_stmt_uncross_shadow_under_id sep (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmt_cross_shadow_free_under s σ ψc ψd ->
      nnrs_stmt_uncross_shadow_under sep s σ ψc ψd = s.

    Theorem nnrs_uncross_shadow_id sep (s:nnrs) :
      nnrs_cross_shadow_free s ->
      nnrs_uncross_shadow sep s = s.

    Lemma nnrs_uncross_shadow_idempotent' sep sep2 (s:nnrs) :
      nnrs_uncross_shadow sep2 (nnrs_uncross_shadow sep s) = (nnrs_uncross_shadow sep s).

    Theorem nnrs_uncross_shadow_idempotent sep (s:nnrs) :
      nnrs_uncross_shadow sep (nnrs_uncross_shadow sep s) = (nnrs_uncross_shadow sep s).
    
  End idempotence.
  
  Section core.
    
    Lemma nnrs_stmt_uncross_shadow_under_preserves_core_f sep (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmtIsCore s ->
      nnrs_stmtIsCore (nnrs_stmt_uncross_shadow_under sep s σ ψc ψd).

    Lemma nnrs_stmt_uncross_shadow_under_preserves_core_b sep (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmtIsCore (nnrs_stmt_uncross_shadow_under sep s σ ψc ψd) ->
      nnrs_stmtIsCore s.

    Lemma nnrs_stmt_uncross_shadow_under_preserves_core
          sep (s:nnrs_stmt) (σ ψc ψd:list var) :
      nnrs_stmtIsCore (nnrs_stmt_uncross_shadow_under sep s σ ψc ψd) <->
      nnrs_stmtIsCore s.
    
    Theorem nnrs_uncross_shadow_preserves_core sep (s:nnrs) :
      nnrsIsCore (nnrs_uncross_shadow sep s) <->
      nnrsIsCore s.

  End core.
  Section examples.

    Local Open Scope nnrs.
    Local Open Scope string.

    Example expr1 : nnrs_stmt
      := NNRSLet "x"
                 (NNRSConst (dnat 3))
                 (NNRSLetMutColl
                    "x"
                    (NNRSLetMutColl
                       "y"
                       (NNRSLetMutColl
                          "x"
                          (NNRSLetMut
                             "x"
                             (NNRSAssign "x" (NNRSConst (dnat 5)))
                             (NNRSPush "x" (NNRSConst (dnat 4))))
                          (NNRSPush "x" (NNRSConst (dnat 6))))
                       (NNRSPush "x" (NNRSConst (dnat 7))))
                    (NNRSAssign "ret" (NNRSConst (dnat 8)))).
    
    Example expr2 : nnrs_stmt
      := NNRSLet "x"
                 (NNRSConst (dnat 3))
                 (NNRSLetMutColl
                    "x"
                    (NNRSPush "x" (NNRSConst (dnat 8)))
                    (NNRSAssign "ret" (NNRSConst (dnat 8)))).


    Example expr3 : nnrs_stmt
      := (NNRSLetMut
            "x"
            (NNRSPush "x" (NNRSConst (dnat 8)))
            (NNRSAssign "ret" (NNRSConst (dnat 8)))).

    
  End examples.

End NNRSCrossShadow.