Qcert.NRAEnv.Context.cNRAEnvContext

Section cNRAEnvContext.





  Context {fruntime:foreign_runtime}.

  Inductive cnraenv_ctxt : Set :=
  | CNHole : nat → cnraenv_ctxt
  | CNPlug : cnraenv → cnraenv_ctxt
  | CANBinop : binOp → cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANUnop : unaryOp → cnraenv_ctxt → cnraenv_ctxt
  | CANMap : cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANMapConcat : cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANProduct : cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANSelect : cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANDefault : cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANEither : cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANEitherConcat : cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANApp : cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANAppEnv : cnraenv_ctxt → cnraenv_ctxt → cnraenv_ctxt
  | CANMapEnv : cnraenv_ctxt → cnraenv_ctxt
  .

  Definition CANID : cnraenv_ctxt
    := CNPlug ANID.

    Definition CANEnv : cnraenv_ctxt
    := CNPlug ANEnv.

    Definition CANGetConstant s : cnraenv_ctxt
    := CNPlug (ANGetConstant s).

  Definition CANConst : data → cnraenv_ctxt
    := fun d ⇒ CNPlug (ANConst d).

  Fixpoint aec_holes (c:cnraenv_ctxt) : list nat :=
    match c with
      | CNHole x ⇒ x::nil
      | CNPlug a ⇒ nil
      | CANBinop b c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANUnop u c' ⇒ aec_holes c'
      | CANMap c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANMapConcat c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANProduct c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANSelect c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANDefault c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANEither c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANEitherConcat c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANApp c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANAppEnv c1 c2 ⇒ aec_holes c1 ++ aec_holes c2
      | CANMapEnv c1 ⇒ aec_holes c1
    end.

  Fixpoint aec_simplify (c:cnraenv_ctxt) : cnraenv_ctxt :=
    match c with
      | CNHole x ⇒ CNHole x
      | CNPlug a ⇒ CNPlug a
      | CANBinop b c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANBinop b a1 a2)
          | c1', c2' ⇒ CANBinop b c1' c2'
        end
      | CANUnop u c ⇒
        match aec_simplify c with
          | CNPlug a ⇒ CNPlug (ANUnop u a)
          | c' ⇒ CANUnop u c'
        end
      | CANMap c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANMap a1 a2)
          | c1', c2' ⇒ CANMap c1' c2'
        end
      | CANMapConcat c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANMapConcat a1 a2)
          | c1', c2' ⇒ CANMapConcat c1' c2'
        end
      | CANProduct c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANProduct a1 a2)
          | c1', c2' ⇒ CANProduct c1' c2'
        end
      | CANSelect c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANSelect a1 a2)
          | c1', c2' ⇒ CANSelect c1' c2'
        end
      | CANDefault c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANDefault a1 a2)
          | c1', c2' ⇒ CANDefault c1' c2'
        end
      | CANEither c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANEither a1 a2)
          | c1', c2' ⇒ CANEither c1' c2'
        end
      | CANEitherConcat c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANEitherConcat a1 a2)
          | c1', c2' ⇒ CANEitherConcat c1' c2'
        end
      | CANApp c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANApp a1 a2)
          | c1', c2' ⇒ CANApp c1' c2'
        end
      | CANAppEnv c1 c2 ⇒
        match aec_simplify c1, aec_simplify c2 with
          | (CNPlug a1), (CNPlug a2) ⇒ CNPlug (ANAppEnv a1 a2)
          | c1', c2' ⇒ CANAppEnv c1' c2'
        end
      | CANMapEnv c1 ⇒
        match aec_simplify c1 with
          | (CNPlug a1) ⇒ CNPlug (ANMapEnv a1)
          | c1' ⇒ CANMapEnv c1'
        end
    end.

  Lemma aec_simplify_holes_preserved c :
    aec_holes (aec_simplify c) = aec_holes c.

  Definition aec_cnraenv_of_ctxt c
    := match (aec_simplify c) with
         | CNPlug a ⇒ Some a
         | _ ⇒ None
       end.

  Lemma aec_simplify_nholes c :
    aec_holes c = nil → {a | aec_simplify c = CNPlug a}.

  Lemma aec_cnraenv_of_ctxt_nholes c :
    aec_holes c = nil → {a | aec_cnraenv_of_ctxt c = Some a}.

  Lemma aec_simplify_idempotent c :
    aec_simplify (aec_simplify c) = aec_simplify c.

  Fixpoint aec_subst (c:cnraenv_ctxt) (x:nat) (p:cnraenv) : cnraenv_ctxt :=
    match c with
      | CNHole x'
        ⇒ if x == x' then CNPlug p else CNHole x'
      | CNPlug a
        ⇒ CNPlug a
      | CANBinop b c1 c2
        ⇒ CANBinop b (aec_subst c1 x p) (aec_subst c2 x p)
      | CANUnop u c
        ⇒ CANUnop u (aec_subst c x p)
      | CANMap c1 c2
        ⇒ CANMap (aec_subst c1 x p) (aec_subst c2 x p)
      | CANMapConcat c1 c2
        ⇒ CANMapConcat (aec_subst c1 x p) (aec_subst c2 x p)
      | CANProduct c1 c2
        ⇒ CANProduct (aec_subst c1 x p) (aec_subst c2 x p)
      | CANSelect c1 c2
        ⇒ CANSelect (aec_subst c1 x p) (aec_subst c2 x p)
      | CANDefault c1 c2
        ⇒ CANDefault (aec_subst c1 x p) (aec_subst c2 x p)
      | CANEither c1 c2
        ⇒ CANEither (aec_subst c1 x p) (aec_subst c2 x p)
      | CANEitherConcat c1 c2
        ⇒ CANEitherConcat (aec_subst c1 x p) (aec_subst c2 x p)
      | CANApp c1 c2
        ⇒ CANApp (aec_subst c1 x p) (aec_subst c2 x p)
      | CANAppEnv c1 c2
        ⇒ CANAppEnv (aec_subst c1 x p) (aec_subst c2 x p)
      | CANMapEnv c1
        ⇒ CANMapEnv (aec_subst c1 x p)
    end.

  Definition aec_substp (c:cnraenv_ctxt) xp
    := let '(x, p) := xp in aec_subst c x p.

  Definition aec_substs c ps :=
    fold_left aec_substp ps c.


   Lemma aec_substs_app c ps1 ps2 :
     aec_substs c (ps1 ++ ps2) =
     aec_substs (aec_substs c ps1) ps2.

  Lemma aec_subst_holes_nin c x p :
    ¬ In x (aec_holes c) → aec_subst c x p = c.

  Lemma aec_subst_holes_remove c x p :
    aec_holes (aec_subst c x p) = remove_all x (aec_holes c).

    Lemma aec_substp_holes_remove c xp :
      aec_holes (aec_substp c xp) = remove_all (fst xp) (aec_holes c).

 Lemma aec_substs_holes_remove c ps :
    aec_holes (aec_substs c ps) =
    fold_left (fun h xy ⇒ remove_all (fst xy) h) ps (aec_holes c).

  Lemma aec_substs_Plug a ps :
    aec_substs (CNPlug a) ps = CNPlug a.

  Lemma aec_substs_Binop b c1 c2 ps :
    aec_substs (CANBinop b c1 c2) ps = CANBinop b (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_Unop u c ps :
      aec_substs (CANUnop u c) ps = CANUnop u (aec_substs c ps).

  Lemma aec_substs_Map c1 c2 ps :
    aec_substs ( CANMap c1 c2) ps =
    CANMap (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_MapConcat c1 c2 ps :
    aec_substs ( CANMapConcat c1 c2) ps =
    CANMapConcat (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_Product c1 c2 ps :
    aec_substs ( CANProduct c1 c2) ps =
    CANProduct (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_Select c1 c2 ps :
    aec_substs ( CANSelect c1 c2) ps =
    CANSelect (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_Default c1 c2 ps :
    aec_substs ( CANDefault c1 c2) ps =
    CANDefault (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_Either c1 c2 ps :
    aec_substs ( CANEither c1 c2) ps =
    CANEither (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_EitherConcat c1 c2 ps :
    aec_substs ( CANEitherConcat c1 c2) ps =
    CANEitherConcat (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_App c1 c2 ps :
    aec_substs ( CANApp c1 c2) ps =
    CANApp (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_AppEnv c1 c2 ps :
    aec_substs ( CANAppEnv c1 c2) ps =
    CANAppEnv (aec_substs c1 ps) (aec_substs c2 ps).

  Lemma aec_substs_MapEnv c1 ps :
    aec_substs ( CANMapEnv c1) ps =
    CANMapEnv (aec_substs c1 ps).


  Lemma aec_simplify_holes_binop b c1 c2:
    aec_holes (CANBinop b c1 c2) ≠ nil →
    aec_simplify (CANBinop b c1 c2) = CANBinop b (aec_simplify c1) (aec_simplify c2).

  Lemma aec_simplify_holes_unop u c:
    aec_holes (CANUnop u c ) ≠ nil →
    aec_simplify (CANUnop u c) = CANUnop u (aec_simplify c).

  Lemma aec_simplify_holes_map c1 c2:
    aec_holes (CANMap c1 c2) ≠ nil →
    aec_simplify (CANMap c1 c2) = CANMap (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_mapconcat c1 c2:
    aec_holes (CANMapConcat c1 c2) ≠ nil →
    aec_simplify (CANMapConcat c1 c2) = CANMapConcat (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_product c1 c2:
    aec_holes (CANProduct c1 c2) ≠ nil →
    aec_simplify (CANProduct c1 c2) = CANProduct (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_select c1 c2:
    aec_holes (CANSelect c1 c2) ≠ nil →
    aec_simplify (CANSelect c1 c2) = CANSelect (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_default c1 c2:
    aec_holes (CANDefault c1 c2) ≠ nil →
    aec_simplify (CANDefault c1 c2) = CANDefault (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_either c1 c2:
    aec_holes (CANEither c1 c2) ≠ nil →
    aec_simplify (CANEither c1 c2) = CANEither (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_eitherconcat c1 c2:
    aec_holes (CANEitherConcat c1 c2) ≠ nil →
    aec_simplify (CANEitherConcat c1 c2) = CANEitherConcat (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_app c1 c2:
    aec_holes (CANApp c1 c2) ≠ nil →
    aec_simplify (CANApp c1 c2) = CANApp (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_appenv c1 c2:
    aec_holes (CANAppEnv c1 c2) ≠ nil →
    aec_simplify (CANAppEnv c1 c2) = CANAppEnv (aec_simplify c1) (aec_simplify c2).

    Lemma aec_simplify_holes_mapenv c1 :
    aec_holes (CANMapEnv c1) ≠ nil →
    aec_simplify (CANMapEnv c1) = CANMapEnv (aec_simplify c1).

   Lemma aec_subst_nholes c x p :
     (aec_holes c) = nil → aec_subst c x p = c.

   Lemma aec_subst_simplify_nholes c x p :
     (aec_holes c) = nil →
     aec_subst (aec_simplify c) x p = aec_simplify c.

  Lemma aec_simplify_subst_simplify1 c x p :
    aec_simplify (aec_subst (aec_simplify c) x p) =
    aec_simplify (aec_subst c x p).

  Lemma aec_simplify_substs_simplify1 c ps :
    aec_simplify (aec_substs (aec_simplify c) ps) =
    aec_simplify (aec_substs c ps).

    Section equivs.
    Context (base_equiv:cnraenv→cnraenv→Prop).

    Definition cnraenv_ctxt_equiv (c1 c2 : cnraenv_ctxt)
      := ∀ (ps:list (nat × cnraenv)),
           match aec_simplify (aec_substs c1 ps),
                 aec_simplify (aec_substs c2 ps)
           with
             | CNPlug a1, CNPlug a2 ⇒ base_equiv a1 a2
             | _, _ ⇒ True
           end.

   Definition cnraenv_ctxt_equiv_strict (c1 c2 : cnraenv_ctxt)
     := ∀ (ps:list (nat × cnraenv)),
          is_list_sorted lt_dec (domain ps) = true →
          equivlist (domain ps) (aec_holes c1 ++ aec_holes c2) →
          match aec_simplify (aec_substs c1 ps),
                aec_simplify (aec_substs c2 ps)
          with
            | CNPlug a1, CNPlug a2 ⇒ base_equiv a1 a2
            | _, _ ⇒ True
          end.

   Global Instance aec_simplify_proper :
     Proper (cnraenv_ctxt_equiv ==> cnraenv_ctxt_equiv) aec_simplify.

  Lemma aec_simplify_proper_inv x y:
    cnraenv_ctxt_equiv (aec_simplify x) (aec_simplify y) → cnraenv_ctxt_equiv x y.

 Instance aec_subst_proper_part1 :
   Proper (cnraenv_ctxt_equiv ==> eq ==> eq ==> cnraenv_ctxt_equiv) aec_subst.

  Global Instance aec_substs_proper_part1: Proper (cnraenv_ctxt_equiv ==> eq ==> cnraenv_ctxt_equiv) aec_substs.

  Definition cnraenv_ctxt_equiv_strict1 (c1 c2 : cnraenv_ctxt)
     := ∀ (ps:list (nat × cnraenv)),
          NoDup (domain ps) →
          equivlist (domain ps) (aec_holes c1 ++ aec_holes c2) →
          match aec_simplify (aec_substs c1 ps),
                aec_simplify (aec_substs c2 ps)
          with
            | CNPlug a1, CNPlug a2 ⇒ base_equiv a1 a2
            | _, _ ⇒ True
          end.

   Lemma aec_subst_swap_neq c x1 x2 y1 y2 :
     x1 ≠ x2 →
   aec_subst (aec_subst c x1 y1) x2 y2 =
   aec_subst (aec_subst c x2 y2) x1 y1.

   Lemma aec_subst_swap_eq c x1 y1 y2 :
     aec_subst (aec_subst c x1 y1) x1 y2 =
     aec_subst c x1 y1.

   Lemma aec_substs_subst_swap_simpl x c y ps :
     ¬ In x (domain ps) →
      aec_substs (aec_subst c x y) ps
      =
      (aec_subst (aec_substs c ps) x y).

   Lemma aec_substs_perm c ps1 ps2 :
     NoDup (domain ps1) →
     Permutation ps1 ps2 →
     (aec_substs c ps1) =
     (aec_substs c ps2).

   Lemma cnraenv_ctxt_equiv_strict_equiv1 (c1 c2 : cnraenv_ctxt) :
     cnraenv_ctxt_equiv_strict1 c1 c2 ↔ cnraenv_ctxt_equiv_strict c1 c2.

   Definition cnraenv_ctxt_equiv_strict2 (c1 c2 : cnraenv_ctxt)
     := ∀ (ps:list (nat × cnraenv)),
          equivlist (domain ps) (aec_holes c1 ++ aec_holes c2) →
          match aec_simplify (aec_substs c1 ps),
                aec_simplify (aec_substs c2 ps)
          with
            | CNPlug a1, CNPlug a2 ⇒ base_equiv a1 a2
            | _, _ ⇒ True
          end.

   Lemma aec_substs_in_nholes c x ps :
         In x (domain ps) →
      ¬ In x (aec_holes (aec_substs c ps)).

   Lemma substs_bdistinct_domain_rev c ps :
    (aec_substs c (bdistinct_domain (rev ps)))
    =
    (aec_substs c ps).

   Lemma cnraenv_ctxt_equiv_strict1_equiv2 (c1 c2 : cnraenv_ctxt) :
     cnraenv_ctxt_equiv_strict2 c1 c2 ↔ cnraenv_ctxt_equiv_strict1 c1 c2.

   Definition cnraenv_ctxt_equiv_strict3 (c1 c2 : cnraenv_ctxt)
     := ∀ (ps:list (nat × cnraenv)),
          incl (aec_holes c1 ++ aec_holes c2) (domain ps) →
          match aec_simplify (aec_substs c1 ps),
                aec_simplify (aec_substs c2 ps)
          with
            | CNPlug a1, CNPlug a2 ⇒ base_equiv a1 a2
            | _, _ ⇒ True
          end.

   Lemma cut_down_to_substs c ps cut :
     incl (aec_holes c) cut →
     (aec_substs c ps) = (aec_substs c (cut_down_to ps cut)).

   Lemma cnraenv_ctxt_equiv_strict2_equiv3 (c1 c2 : cnraenv_ctxt) :
     cnraenv_ctxt_equiv_strict3 c1 c2 ↔ cnraenv_ctxt_equiv_strict2 c1 c2.

   Lemma cnraenv_ctxt_equiv_strict3_equiv (c1 c2 : cnraenv_ctxt) :
     cnraenv_ctxt_equiv c1 c2 ↔ cnraenv_ctxt_equiv_strict3 c1 c2.

   Theorem cnraenv_ctxt_equiv_strict_equiv (c1 c2 : cnraenv_ctxt) :
     cnraenv_ctxt_equiv c1 c2 ↔ cnraenv_ctxt_equiv_strict c1 c2.

   Lemma aec_holes_saturated_subst {B} f c ps :
      incl (aec_holes c) (domain ps) →
      aec_holes
        (aec_substs c
                   (map (fun xy : nat × B ⇒ (fst xy, (f (snd xy)))) ps)) = nil.

  Global Instance cnraenv_ctxt_equiv_refl {refl:Reflexive base_equiv}: Reflexive cnraenv_ctxt_equiv.

  Global Instance cnraenv_ctxt_equiv_sym {sym:Symmetric base_equiv}: Symmetric cnraenv_ctxt_equiv.

  Global Instance cnraenv_ctxt_equiv_trans {trans:Transitive base_equiv}: Transitive cnraenv_ctxt_equiv.

  Global Instance cnraenv_ctxt_equiv_equivalence {equiv:Equivalence base_equiv}: Equivalence cnraenv_ctxt_equiv.

  Global Instance cnraenv_ctxt_equiv_preorder {pre:PreOrder base_equiv} : PreOrder cnraenv_ctxt_equiv.

  Global Instance cnraenv_ctxt_equiv_strict_refl {refl:Reflexive base_equiv}: Reflexive cnraenv_ctxt_equiv_strict.

  Global Instance cnraenv_ctxt_equiv_strict_sym {sym:Symmetric base_equiv}: Symmetric cnraenv_ctxt_equiv_strict.

  Global Instance cnraenv_ctxt_equiv_strict_trans {trans:Transitive base_equiv}: Transitive cnraenv_ctxt_equiv_strict.

  Global Instance cnraenv_ctxt_equiv_strict_equivalence {equiv:Equivalence base_equiv}: Equivalence cnraenv_ctxt_equiv_strict.

  Global Instance cnraenv_ctxt_equiv_strict_preorder {pre:PreOrder base_equiv} : PreOrder cnraenv_ctxt_equiv_strict.

  Global Instance CNPlug_proper :
    Proper (base_equiv ==> cnraenv_ctxt_equiv) CNPlug.

  Global Instance CNPlug_proper_strict :
    Proper (base_equiv ==> cnraenv_ctxt_equiv_strict) CNPlug.

  End equivs.

End cNRAEnvContext.



Notation "'ID'" := (CANID) (at level 50) : cnraenv_ctxt_scope.
Notation "'ENV'" := (CANEnv) (at level 50) : cnraenv_ctxt_scope.

Notation "‵‵ c" := (CANConst (dconst c)) (at level 0) : cnraenv_ctxt_scope. Notation "‵ c" := (CANConst c) (at level 0) : cnraenv_ctxt_scope. Notation "‵{||}" := (CANConst (dcoll nil)) (at level 0) : cnraenv_ctxt_scope. Notation "‵[||]" := (CANConst (drec nil)) (at level 50) : cnraenv_ctxt_scope.
Notation "r1 ∧ r2" := (CANBinop AAnd r1 r2) (right associativity, at level 65): cnraenv_ctxt_scope. Notation "r1 ∨ r2" := (CANBinop AOr r1 r2) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "r1 ≐ r2" := (CANBinop AEq r1 r2) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "r1 ≤ r2" := (CANBinop ALt r1 r2) (no associativity, at level 70): cnraenv_ctxt_scope. Notation "r1 ⋃ r2" := (CANBinop AUnion r1 r2) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "r1 − r2" := (CANBinop AMinus r1 r2) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "r1 ♯min r2" := (CANBinop AMin r1 r2) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "r1 ♯max r2" := (CANBinop AMax r1 r2) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "p ⊕ r" := ((CANBinop AConcat) p r) (at level 70) : cnraenv_ctxt_scope. Notation "p ⊗ r" := ((CANBinop AMergeConcat) p r) (at level 70) : cnraenv_ctxt_scope.
Notation "¬( r1 )" := (CANUnop ANeg r1) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "ε( r1 )" := (CANUnop ADistinct r1) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "♯count( r1 )" := (CANUnop ACount r1) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "♯flatten( d )" := (CANUnop AFlatten d) (at level 50) : cnraenv_ctxt_scope. Notation "‵{| d |}" := ((CANUnop AColl) d) (at level 50) : cnraenv_ctxt_scope. Notation "‵[| ( s , r ) |]" := ((CANUnop (ARec s)) r) (at level 50) : cnraenv_ctxt_scope. Notation "¬π[ s1 ]( r )" := ((CANUnop (ARecRemove s1)) r) (at level 50) : cnraenv_ctxt_scope. Notation "p · r" := ((CANUnop (ADot r)) p) (left associativity, at level 40): cnraenv_ctxt_scope.
Notation "χ⟨ p ⟩( r )" := (CANMap p r) (at level 70) : cnraenv_ctxt_scope. Notation "⋈ᵈ⟨ e2 ⟩( e1 )" := (CANMapConcat e2 e1) (at level 70) : cnraenv_ctxt_scope. Notation "r1 × r2" := (CANProduct r1 r2) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "σ⟨ p ⟩( r )" := (CANSelect p r) (at level 70) : cnraenv_ctxt_scope. Notation "r1 ∥ r2" := (CANDefault r1 r2) (right associativity, at level 70): cnraenv_ctxt_scope. Notation "r1 ◯ r2" := (CANApp r1 r2) (right associativity, at level 60): cnraenv_ctxt_scope.
Notation "r1 ◯ₑ r2" := (CANAppEnv r1 r2) (right associativity, at level 60): cnraenv_ctxt_scope.
Notation "χᵉ⟨ p ⟩( r )" := (CANMapEnv p r) (at level 70) : cnraenv_ctxt_scope.
Notation "$ n" := (CNHole n) (at level 50) : cnraenv_ctxt_scope.

Notation "X ≡ₑ Y" := (cnraenv_ctxt_equiv cnraenv_eq X Y) (at level 90) : cnraenv_ctxt_scope.