Module NRAEnvRewriteContext

Section ROptimEnvContext.
  Require Import Equivalence.
  Require Import Morphisms.
  Require Import Setoid.
  Require Import EquivDec.
  Require Import Program.

  Require Import Arith List.
  
  Require Import Utils BasicRuntime.
  Require Import NRA cNRAEnv cNRAEnvEq.
  
  Require Import NRAContext NRAEnvRewrite NRARewriteContext.
  Require Import cNRAEnvContext cNRAEnvContextLift.
  Local Open Scope nraenv_core_ctxt.

  Context {fruntime:foreign_runtime}.

  Ltac simpl_domain_eq_const
    := repeat
         match goal with
         | [H: domain ?x = nil |- _ ] =>
           apply domain_nil in H; subst x
         | [H: domain ?x = _::_ |- _ ] =>
           let n := fresh "n" in
           let a := fresh "a" in
           destruct x as [|[n a]]; simpl in H; inversion H; clear H;
           try subst n
         end.

  Ltac simpl_plugins
    := match goal with
         [H1:is_list_sorted lt_dec ?x = true,
             H2:equivlist ?x ?y |- _ ] =>
         apply insertion_sort_equivlist_nat in H2;
           rewrite (insertion_sort_sorted_is_id _ _ H1) in H2;
           simpl in H2; simpl_domain_eq_const; clear H1
       end.

  Ltac simpl_ctxt_equiv :=
    try apply <- nraenv_core_ctxt_equiv_strict_equiv;
    red; simpl; intros; simpl_plugins; simpl.

  Local Open Scope nraenv_core_ctxt_scope.
  Lemma envctxt_and_comm_ctxt :
    $2 ∧ $1 ≡ₑ $1 ∧ $2.
  
  Lemma ctxt_envunion_assoc :
    ($1 ⋃ $2) ⋃ $3 ≡ₑ $1 ⋃ ($2 ⋃ $3).

  Lemma ctxt_app_over_merge :
    (ENV ⊗ $1) ◯ $2 ≡ₑ ENV ⊗ ($1 ◯ $2).

  Lemma envctxt_select_union_distr :
    σ⟨ $0 ⟩($1 ⋃ $2) ≡ₑ σ⟨ $0 ⟩($1) ⋃ σ⟨ $0 ⟩($2).


End ROptimEnvContext.