Module NRARewriteContext

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

  Require Import Arith NPeano Omega List.
  
  Require Import Utils BasicRuntime.
  Require Import NRA NRAEq.
  Require Import NRAContext NRARewrite.

  Local Open Scope nra_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.
  
  Lemma lt_nat_compat (x y:nat) : ~ x < y -> ~ y < x -> x = y.

  Lemma insertion_sort_equivlist_nat l l':
    equivlist l l' -> insertion_sort lt_dec l = insertion_sort lt_dec l'.

  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 <- nra_ctxt_equiv_strict_equiv;
    red; simpl; intros; simpl_plugins; simpl.

  Lemma ctxt_and_comm_ctxt :
    $2 ∧ $1 ≡ₐ $1 ∧ $2.

  Lemma ctxt_unnest_singleton_ctxt s1 s2 s3 :
    s1 <> s2 /\ s2 <> s3 /\ s3 <> s1 ->
    χ⟨¬π[s1 ]( ID)
     ⟩( ⋈ᵈ⟨χ⟨‵[| (s2, ID)|] ⟩( (ID) · s1)
          ⟩( ‵{|‵[| (s3, $1)|] ⊕ ‵[| (s1, ‵{| $2|})|]|}))
     ≡ₐ ‵{|‵[| (s3, $1)|] ⊕ ‵[| (s2, $2)|]|}.

  Lemma ctxt_select_union_distr :
    σ⟨ $0 ⟩($1 ⋃ $2) ≡ₐ σ⟨ $0 ⟩($1) ⋃ σ⟨ $0 ⟩($2).

End ROptimContext.