Module NNRCRewrite

Section NNRCRewrite.
  Require Import String.
  Require Import List ListSet.
  Require Import Arith.
  Require Import EquivDec.

  Require Import Utils BasicRuntime.
  Require Import cNNRC cNNRCShadow.
  Require Import NNRC NNRCShadow NNRCEq.
  Require Import NNRCRewriteUtil.

  Local Open Scope nnrc_scope.

  Context {fruntime:foreign_runtime}.

  Lemma unshadow_ext_preserves sep renamer avoid (e:nnrc) :
    nnrc_ext_eq (unshadow sep renamer avoid e) e.

Proof.

    unfold nnrc_ext_eq.
    intros.
    simpl.
    apply unshadow_ext_eval.
  Qed.

Lemma dot_of_rec a (e:nnrc) :
nnrc_ext_eq (NNRCUnop (ADot a) (NNRCUnop (ARec a) e)) e.

Proof.

    unfold nnrc_ext_eq; intros ? ? _.
    unfold nnrc_ext_eval.
    simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc e)); [|reflexivity]; simpl.
    unfold edot; simpl.
    destruct (string_eqdec a a); congruence.
  Qed.

  Lemma nnrc_merge_concat_to_concat s1 s2 p1 p2:
    s1 <> s2 ->
    ‵[| (s1, p1)|] ⊗ ‵[| (s2, p2)|] ≡ᶜ ‵{|‵[| (s1, p1)|] ⊕ ‵[| (s2, p2)|]|}.

Proof.

    red; intros; simpl.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc p1)); simpl; trivial.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc p2)); simpl; trivial.
    unfold merge_bindings.
    simpl.
    unfold compatible_with; simpl.
    destruct (EquivDec.equiv_dec s1 s2); try congruence.
    simpl.
    reflexivity.
  Qed.

  Lemma for_nil x e2 :
    nnrc_ext_eq (NNRCFor x ‵{||} e2) ‵{||}.

Proof.

red; simpl; trivial.
Qed.

  Lemma for_singleton_to_let x e1 e2:
    nnrc_ext_eq (NNRCFor x (NNRCUnop AColl e1) e2)
                (NNRCUnop AColl (NNRCLet x e1 e2)).

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc e1)); simpl; trivial.
    match_destr.
  Qed.

Lemma flatten_nil_nnrc :
nnrc_ext_eq (♯flatten(‵{||})) ‵{||}.

Proof.

red; simpl; trivial.
Qed.

  Lemma map_sigma_fusion (e1 e2 e3:nnrc) (v1 v2:var) :
    ~ In v1 (nnrc_free_vars e3) ->
    nnrc_ext_eq
      (NNRCFor v2
              (NNRCUnop AFlatten
                       (NNRCFor v1 e1
                               (NNRCIf e2 (NNRCUnop AColl (NNRCVar v1)) (NNRCConst (dcoll nil)))))
              e3)
      (NNRCUnop AFlatten
               (NNRCFor v1 e1
                       (NNRCIf e2
                              (NNRCUnop AColl (NNRCLet v2 (NNRCVar v1) e3))
                              (NNRCConst (dcoll nil))))).

Proof.

    intro notinfree.
    unfold nnrc_ext_eq; intros ? ? _.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc e1)); try reflexivity; simpl.
    dest_eqdec; try congruence.
    clear e1 e.
    destruct d; try reflexivity; simpl.
    induction l; try reflexivity; simpl.
    destruct ((nnrc_core_eval h ((v1, a) :: env) (nnrc_ext_to_nnrc e2))); try reflexivity; simpl.
    destruct d; try reflexivity; simpl.
    case_eq b; intros.
    - autorewrite with alg.
      rewrite lift_cons_dcoll.
      autorewrite with alg in IHl.
      unfold olift in *.
      case_eq (rmap
              (fun d1 : data =>
               match nnrc_core_eval h ((v1, d1) :: env) (nnrc_ext_to_nnrc e2) with
               | Some (dbool true) =>
                   match nnrc_core_eval h ((v2, d1) :: (v1, d1) :: env) (nnrc_ext_to_nnrc e3) with
                   | Some x'0 => Some (dcoll (x'0 :: nil))
                   | None => None
                   end
               | Some (dbool false) => Some (dcoll nil)
               | _ => None
               end) l); intros; rewrite H0 in IHl; case_eq (rmap
                (fun d1 : data =>
                 match nnrc_core_eval h ((v1, d1) :: env) (nnrc_ext_to_nnrc e2) with
                 | Some (dbool true) => Some (dcoll (d1 :: nil))
                 | Some (dbool false) => Some (dcoll nil)
                 | _ => None
                 end) l); intros; rewrite H1 in IHl; simpl in *.
      + clear H0 H1.
        unfold lift in *.
        case_eq (rflatten l1); case_eq (rflatten l0); intros; rewrite H0 in *; rewrite H1 in *.
        * simpl.
          assert (exists l4, rmap (fun d1 : data => nnrc_core_eval h ((v2, d1) :: env) (nnrc_ext_to_nnrc e3)) l3 = Some l4).
          destruct (rmap (fun d1 : data => nnrc_core_eval h ((v2, d1) :: env) (nnrc_ext_to_nnrc e3)) l3); try congruence.
          exists l4; reflexivity.
          elim H2; clear H2; intros.
          rewrite H2 in *; clear H2.
          simpl.
          inversion IHl. subst; clear IHl.
          assert (nnrc_core_eval h ((v2, a) :: env) (nnrc_ext_to_nnrc e3) = nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)).
          rewrite nnrc_ext_to_nnrc_free_vars_same in notinfree.
          generalize (@nnrc_core_eval_remove_free_env _ h ((v2,a)::nil) v1 a env (nnrc_ext_to_nnrc e3) notinfree); intros.
          simpl in H.
          rewrite H; clear H; reflexivity.
          rewrite H; clear H.
          destruct (nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
          rewrite (rflatten_cons (d::nil) l0 l2).
          reflexivity.
          assumption.
        * simpl.
          destruct (rmap (fun d1 : data => nnrc_core_eval h ((v2, d1) :: env) (nnrc_ext_to_nnrc e3)) l2); try congruence.
          simpl.
          destruct (nnrc_core_eval h ((v2, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
          destruct (nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
          rewrite rflatten_cons_none; [reflexivity|assumption].
          destruct (nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
          rewrite rflatten_cons_none; [reflexivity|assumption].
        * congruence.
        * destruct (nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
          rewrite rflatten_cons_none; [reflexivity|assumption].
      + unfold lift in *.
        case_eq (rflatten l0); intros; rewrite H2 in *; try congruence.
        destruct (nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
        rewrite rflatten_cons_none; [reflexivity|assumption].
      + unfold lift in *.
        case_eq (rflatten l0); intros; rewrite H2 in *; try congruence.
        simpl in *.
        destruct (nnrc_core_eval h ((v2, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
        destruct (rmap (fun d1 : data => nnrc_core_eval h ((v2, d1) :: env) (nnrc_ext_to_nnrc e3)) l1); try reflexivity; try congruence.
        simpl.
        destruct (nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
        destruct (nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
        destruct (nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
      + destruct (nnrc_core_eval h ((v2, a) :: (v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
    - autorewrite with alg.
      rewrite lift_empty_dcoll.
      rewrite lift_empty_dcoll.
      autorewrite with alg in IHl.
      rewrite IHl.
      reflexivity.
  Qed.

  Lemma map_sigma_fusion_samevar (e1 e2 e3:nnrc) (v1:var) :
    nnrc_ext_eq
      (NNRCFor v1
              (NNRCUnop AFlatten
                       (NNRCFor v1 e1
                               (NNRCIf e2 (NNRCUnop AColl (NNRCVar v1)) (NNRCConst (dcoll nil)))))
              e3)
      (NNRCUnop AFlatten
               (NNRCFor v1 e1
                       (NNRCIf e2
                              (NNRCUnop AColl e3)
                              (NNRCConst (dcoll nil))))).

Proof.

    unfold nnrc_ext_eq; intros ? ? _.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc e1)); try reflexivity; simpl.
    dest_eqdec; try congruence.
    clear e1 e.
    destruct d; try reflexivity; simpl.
    induction l; try reflexivity; simpl.
    destruct ((nnrc_core_eval h ((v1, a) :: env) (nnrc_ext_to_nnrc e2))); try reflexivity; simpl.
    destruct d; try reflexivity; simpl.
    case_eq b; intros.
    - autorewrite with alg.
      rewrite lift_cons_dcoll.
      autorewrite with alg in IHl.
      unfold olift in *.
      case_eq (rmap
              (fun d1 : data =>
               match nnrc_core_eval h ((v1, d1) :: env) (nnrc_ext_to_nnrc e2) with
               | Some (dbool true) =>
                   match nnrc_core_eval h ((v1, d1) :: env) (nnrc_ext_to_nnrc e3) with
                   | Some x'0 => Some (dcoll (x'0 :: nil))
                   | None => None
                   end
               | Some (dbool false) => Some (dcoll nil)
               | _ => None
               end) l); intros; rewrite H0 in IHl; case_eq (rmap
                (fun d1 : data =>
                 match nnrc_core_eval h ((v1, d1) :: env) (nnrc_ext_to_nnrc e2) with
                 | Some (dbool true) => Some (dcoll (d1 :: nil))
                 | Some (dbool false) => Some (dcoll nil)
                 | _ => None
                 end) l); intros; rewrite H1 in IHl; simpl in *.
      + clear H0 H1.
        unfold lift in *.
        case_eq (rflatten l1); case_eq (rflatten l0); intros; rewrite H0 in *; rewrite H1 in *.
        * simpl.
          assert (exists l4, rmap (fun d1 : data => nnrc_core_eval h ((v1, d1) :: env) (nnrc_ext_to_nnrc e3)) l3 = Some l4).
          destruct (rmap (fun d1 : data => nnrc_core_eval h ((v1, d1) :: env) (nnrc_ext_to_nnrc e3)) l3); try congruence.
          exists l4; reflexivity.
          elim H2; clear H2; intros.
          rewrite H2 in *; clear H2.
          simpl.
          inversion IHl. subst; clear IHl.
          destruct (nnrc_core_eval h ((v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
          rewrite (rflatten_cons (d::nil) l0 l2).
          reflexivity.
          assumption.
        * simpl.
          destruct (rmap (fun d1 : data => nnrc_core_eval h ((v1, d1) :: env) (nnrc_ext_to_nnrc e3)) l2); try congruence.
          simpl.
          destruct (nnrc_core_eval h ((v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
          rewrite rflatten_cons_none; [reflexivity|assumption].
        * congruence.
        * destruct (nnrc_core_eval h ((v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
          rewrite rflatten_cons_none; [reflexivity|assumption].
      + unfold lift in *.
        case_eq (rflatten l0); intros; rewrite H2 in *; try congruence.
        destruct (nnrc_core_eval h ((v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
        rewrite rflatten_cons_none; [reflexivity|assumption].
      + unfold lift in *.
        case_eq (rflatten l0); intros; rewrite H2 in *; try congruence.
        simpl in *.
        destruct (nnrc_core_eval h ((v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
        destruct (rmap (fun d1 : data => nnrc_core_eval h ((v1, d1) :: env) (nnrc_ext_to_nnrc e3)) l1); try reflexivity; try congruence.
        simpl.
        destruct (nnrc_core_eval h ((v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
      + destruct (nnrc_core_eval h ((v1, a) :: env) (nnrc_ext_to_nnrc e3)); try reflexivity.
    - autorewrite with alg.
      rewrite lift_empty_dcoll.
      rewrite lift_empty_dcoll.
      autorewrite with alg in IHl.
      rewrite IHl.
      reflexivity.
  Qed.

  Lemma for_over_if x e1 e2 e3 ebody :
    nnrc_ext_eq (NNRCFor x (NNRCIf e1 e2 e3) ebody)
            (NNRCIf e1 (NNRCFor x e2 ebody)
                   (NNRCFor x e3 ebody)).

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc e1)); simpl; trivial.
    destruct d; simpl; trivial.
    destruct b; simpl; trivial.
  Qed.

  Lemma for_over_either_disjoint x e1 xl el xr er ebody:
    disjoint (xl::xr::nil) (nnrc_free_vars ebody) ->
    nnrc_ext_eq (NNRCFor x (NNRCEither e1 xl el xr er) ebody)
            (NNRCEither e1
                       xl (NNRCFor x el ebody)
                       xr (NNRCFor x er ebody)).

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    apply disjoint_cons_inv1 in H.
    destruct H as [disj nin1].
    apply disjoint_cons_inv1 in disj.
    destruct disj as [_ nin2].
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc e1)); simpl; trivial.
    rewrite nnrc_ext_to_nnrc_free_vars_same in nin2, nin1.
    destruct d; simpl; trivial;
      (destruct (equiv_dec (A:=string) xl xl); [|congruence]);
      match_case; simpl; intros; match_destr;
        f_equal;
      apply rmap_ext; intros.
    - generalize (@nnrc_core_eval_remove_free_env _ h ((x,x0)::nil) xl d env (nnrc_ext_to_nnrc ebody)); simpl; intros re1; rewrite re1; trivial.
    - generalize (@nnrc_core_eval_remove_free_env _ h ((x,x0)::nil) xr d env (nnrc_ext_to_nnrc ebody)); simpl; intros re1; rewrite re1; trivial.
  Qed.

  Lemma nnrceither_rename_l e1 xl el xr er xl' :
    ~ In xl' (nnrc_free_vars el) ->
    ~ In xl' (nnrc_bound_vars el) ->
    nnrc_ext_eq (NNRCEither e1 xl el xr er)
            (NNRCEither e1 xl' (nnrc_subst el xl (NNRCVar xl')) xr er).

Proof.

    red; simpl; intros nfree nbound; intros.
    generalize (@nnrc_ext_eval_cons_subst _ h el env xl);
      unfold nnrc_ext_eval; simpl; intros.
    do 2 match_destr.
    rewrite <- nnrc_ext_to_nnrc_subst_comm; simpl.
    specialize (H0 d xl' nfree nbound).
    rewrite <- nnrc_ext_to_nnrc_subst_comm in H0. simpl in H0.
    rewrite H0.
    trivial.
  Qed.

  Lemma nnrceither_rename_r e1 xl el xr er xr' :
    ~ In xr' (nnrc_free_vars er) ->
    ~ In xr' (nnrc_bound_vars er) ->
    nnrc_ext_eq (NNRCEither e1 xl el xr er)
                (NNRCEither e1 xl el xr' (nnrc_subst er xr (NNRCVar xr'))).

Proof.

    red; simpl; intros nfree nbound; intros.
    generalize (@nnrc_ext_eval_cons_subst _ h er env xr);
      unfold nnrc_ext_eval; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    do 2 match_destr.
    rewrite <- nnrc_ext_to_nnrc_subst_comm; simpl.
    specialize (H0 d xr' nfree nbound).
    rewrite <- nnrc_ext_to_nnrc_subst_comm in H0. simpl in H0.
    rewrite H0.
    trivial.
  Qed.

  Lemma for_over_either sep x e1 xl el xr er ebody:
    nnrc_ext_eq (NNRCFor x (NNRCEither e1 xl el xr er) ebody)
            ( let xl' := really_fresh_in_ext sep xl (nnrc_free_vars el ++ nnrc_bound_vars el) ebody in
                 let xr' := really_fresh_in_ext sep xr (nnrc_free_vars er ++ nnrc_bound_vars er) ebody in
              (NNRCEither e1
                       xl' (NNRCFor x (nnrc_subst el xl (NNRCVar xl')) ebody)
                       xr' (NNRCFor x (nnrc_subst er xr (NNRCVar xr')) ebody))).

Proof.

    simpl.
    transitivity (NNRCFor x (NNRCEither e1
                                       (really_fresh_in_ext sep xl (nnrc_free_vars el ++ nnrc_bound_vars el) ebody)
                                       (nnrc_subst el xl (NNRCVar (really_fresh_in_ext sep xl (nnrc_free_vars el ++ nnrc_bound_vars el) ebody)))
                                       (really_fresh_in_ext sep xr (nnrc_free_vars er ++ nnrc_bound_vars er) ebody)
                                       (nnrc_subst er xr (NNRCVar (really_fresh_in_ext sep xr (nnrc_free_vars er ++ nnrc_bound_vars er) ebody)))) ebody).
    - rewrite <- nnrceither_rename_l; simpl.
      rewrite <- nnrceither_rename_r; simpl.
      reflexivity.
      + intro inn.
        assert (inn2:In (really_fresh_in_ext sep xr (nnrc_free_vars er ++ nnrc_bound_vars er) ebody)
                    (nnrc_free_vars er ++ nnrc_bound_vars er))
               by (rewrite in_app_iff; intuition).
        apply really_fresh_from_avoid in inn2; trivial.
      + intro inn.
        assert (inn2:In (really_fresh_in_ext sep xr (nnrc_free_vars er ++ nnrc_bound_vars er) ebody)
                    (nnrc_free_vars er ++ nnrc_bound_vars er))
               by (rewrite in_app_iff; intuition).
        apply really_fresh_from_avoid in inn2; trivial.
      + intro inn.
        assert (inn2:In (really_fresh_in_ext sep xl (nnrc_free_vars el ++ nnrc_bound_vars el) ebody)
                    (nnrc_free_vars el ++ nnrc_bound_vars el))
               by (rewrite in_app_iff; intuition).
        apply really_fresh_from_avoid in inn2; trivial.
      + intro inn.
        assert (inn2:In (really_fresh_in_ext sep xl (nnrc_free_vars el ++ nnrc_bound_vars el) ebody)
                    (nnrc_free_vars el ++ nnrc_bound_vars el))
               by (rewrite in_app_iff; intuition).
        apply really_fresh_from_avoid in inn2; trivial.
    - assert ((nnrc_free_vars ebody) =
              (nnrc_free_vars (nnrc_ext_to_nnrc ebody))).
      apply nnrc_ext_to_nnrc_free_vars_same.
      apply for_over_either_disjoint.
      red; simpl; intuition; subst.
      rewrite H in H1.
      revert H1.
      apply really_fresh_from_free_ext; intros.
      rewrite H in H1.
      revert H1.
      apply really_fresh_from_free_ext; intros.
  Qed.

  Lemma nnrcunop_over_either op e1 xl el xr er:
    nnrc_ext_eq (NNRCUnop op (NNRCEither e1 xl el xr er))
                (NNRCEither e1 xl (NNRCUnop op el) xr (NNRCUnop op er)).

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    repeat match_destr.
  Qed.

  Lemma nnrcunop_over_if op e1 e2 e3:
    nnrc_ext_eq (NNRCUnop op (NNRCIf e1 e2 e3))
                (NNRCIf e1 (NNRCUnop op e2) (NNRCUnop op e3)).

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc e1)); simpl; trivial.
    repeat match_destr.
  Qed.

  Lemma sigma_to_if (e1 e2:nnrc) (v:var) :
    nnrc_ext_eq
      (NNRCUnop AFlatten
                (NNRCFor v (NNRCUnop AColl e2)
                         (NNRCIf e1
                                 (NNRCUnop AColl (NNRCVar v))
                                 (NNRCConst (dcoll nil)))))
      (NNRCLet v e2 (NNRCIf e1 (NNRCUnop AColl (NNRCVar v)) (NNRCConst (dcoll nil)))).

Proof.

    unfold nnrc_ext_eq; intros ? ? _.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc e2)); try reflexivity; simpl.
    dest_eqdec; try congruence.
    destruct (nnrc_core_eval h ((v,d) :: env) (nnrc_ext_to_nnrc e1)); try reflexivity; simpl.
    destruct d0; try reflexivity; simpl.
    destruct b; reflexivity.
  Qed.

Lemma unshadow_free_vars sep renamer (x:var) (e:nnrc):
In x (nnrc_free_vars (unshadow sep renamer nil e)) -> In x (nnrc_free_vars e).

Proof.

    rewrite unshadow_nnrc_free_vars.
    intros; assumption.
  Qed.

optimizations for record projection

  Lemma nnrcproject_over_concat sl p1 p2 :
    π[sl](p1 ⊕ p2)
          ≡ᶜ π[sl](p1) ⊕ π[sl](p2).

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc p2));
      destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc p1)); simpl.
    - destruct d; destruct d0; simpl; trivial.
      rewrite rproject_rec_sort_commute, rproject_app.
      trivial.
    - trivial.
    - destruct d; simpl; trivial.
    - trivial.
  Qed.

Lemma nnrcproject_over_const sl l :
π[sl](NNRCConst (drec l)) ≡ᶜ NNRCConst (drec (rproject l sl)).

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    rewrite rproject_rec_sort_commute.
    rewrite rproject_map_fst_same; intuition.
  Qed.

  Lemma nnrcproject_over_rec_in sl s p :
    In s sl ->
    π[sl](‵[| (s, p) |]) ≡ᶜ ‵[| (s, p) |].

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc p)); simpl; trivial.
    destruct (in_dec string_dec s sl); intuition.
  Qed.

Lemma nnrcproject_over_nnrcproject sl1 sl2 p :
π[sl1](π[sl2](p)) ≡ᶜ π[set_inter string_dec sl2 sl1](p).

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc p)); simpl; trivial.
    destruct d; simpl; trivial.
    rewrite rproject_rproject.
    trivial.
  Qed.

Lemma nnrcproject_over_either sl p xl xr p1 p2 :
π[sl](NNRCEither p xl p1 xr p2) ≡ᶜ NNRCEither p xl (π[sl](p1)) xr (π[sl](p2)).

Proof.

    red; simpl; intros.
    unfold nnrc_ext_eval; simpl.
    destruct (nnrc_core_eval h env (nnrc_ext_to_nnrc p)); simpl; trivial.
    destruct d; simpl; trivial.
  Qed.

End NNRCRewrite.

Hint Rewrite @sigma_to_if : nnrc_rew.