Module Qcert.NRA.Context.NRAContext

Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import List.
Require Import Permutation.
Require Import String.
Require Import NPeano.
Require Import Arith.
Require Import Bool.
Require Import Utils.
Require Import BindingsNat.
Require Import DataRuntime.
Require Import NRA.
Require Import NRAEq.

Declare Scope nra_ctxt_scope.

Section NRAContext.
  Local Open Scope nra_scope.

  Context {fruntime:foreign_runtime}.

  Inductive nra_ctxt : Set :=
  | CNRAHole : nat -> nra_ctxt
  | CNRAPlug : nra -> nra_ctxt
  | CNRABinop : binary_op -> nra_ctxt -> nra_ctxt -> nra_ctxt
  | CNRAUnop : unary_op -> nra_ctxt -> nra_ctxt
  | CNRAMap : nra_ctxt -> nra_ctxt -> nra_ctxt
  | CNRAMapProduct : nra_ctxt -> nra_ctxt -> nra_ctxt
  | CNRAProduct : nra_ctxt -> nra_ctxt -> nra_ctxt
  | CNRASelect : nra_ctxt -> nra_ctxt -> nra_ctxt
  | CNRADefault : nra_ctxt -> nra_ctxt -> nra_ctxt
  | CNRAEither : nra_ctxt -> nra_ctxt -> nra_ctxt
  | CNRAEitherConcat : nra_ctxt -> nra_ctxt -> nra_ctxt
  | CNRAApp : nra_ctxt -> nra_ctxt -> nra_ctxt
  .

  Definition CNRAID : nra_ctxt
    := CNRAPlug NRAID.

  Definition CNRAConst : data -> nra_ctxt
    := fun d => CNRAPlug (NRAConst d).

  Fixpoint ac_holes (c:nra_ctxt) : list nat :=
    match c with
      | CNRAHole x => x::nil
      | CNRAPlug a => nil
      | CNRABinop b c1 c2 => ac_holes c1 ++ ac_holes c2
      | CNRAUnop u c' => ac_holes c'
      | CNRAMap c1 c2 => ac_holes c1 ++ ac_holes c2
      | CNRAMapProduct c1 c2 => ac_holes c1 ++ ac_holes c2
      | CNRAProduct c1 c2 => ac_holes c1 ++ ac_holes c2
      | CNRASelect c1 c2 => ac_holes c1 ++ ac_holes c2
      | CNRADefault c1 c2 => ac_holes c1 ++ ac_holes c2
      | CNRAEither c1 c2 => ac_holes c1 ++ ac_holes c2
      | CNRAEitherConcat c1 c2 => ac_holes c1 ++ ac_holes c2
      | CNRAApp c1 c2 => ac_holes c1 ++ ac_holes c2
    end.

  Fixpoint ac_simplify (c:nra_ctxt) : nra_ctxt :=
    match c with
      | CNRAHole x => CNRAHole x
      | CNRAPlug a => CNRAPlug a
      | CNRABinop b c1 c2 =>
        match ac_simplify c1, ac_simplify c2 with
          | (CNRAPlug a1), (CNRAPlug a2) => CNRAPlug (NRABinop b a1 a2)
          | c1', c2' => CNRABinop b c1' c2'
        end
      | CNRAUnop u c =>
        match ac_simplify c with
          | CNRAPlug a => CNRAPlug (NRAUnop u a)
          | c' => CNRAUnop u c'
        end
      | CNRAMap c1 c2 =>
        match ac_simplify c1, ac_simplify c2 with
          | (CNRAPlug a1), (CNRAPlug a2) => CNRAPlug (NRAMap a1 a2)
          | c1', c2' => CNRAMap c1' c2'
        end
      | CNRAMapProduct c1 c2 =>
        match ac_simplify c1, ac_simplify c2 with
          | (CNRAPlug a1), (CNRAPlug a2) => CNRAPlug (NRAMapProduct a1 a2)
          | c1', c2' => CNRAMapProduct c1' c2'
        end
      | CNRAProduct c1 c2 =>
        match ac_simplify c1, ac_simplify c2 with
          | (CNRAPlug a1), (CNRAPlug a2) => CNRAPlug (NRAProduct a1 a2)
          | c1', c2' => CNRAProduct c1' c2'
        end
      | CNRASelect c1 c2 =>
        match ac_simplify c1, ac_simplify c2 with
          | (CNRAPlug a1), (CNRAPlug a2) => CNRAPlug (NRASelect a1 a2)
          | c1', c2' => CNRASelect c1' c2'
        end
      | CNRADefault c1 c2 =>
        match ac_simplify c1, ac_simplify c2 with
          | (CNRAPlug a1), (CNRAPlug a2) => CNRAPlug (NRADefault a1 a2)
          | c1', c2' => CNRADefault c1' c2'
        end
      | CNRAEither c1 c2 =>
        match ac_simplify c1, ac_simplify c2 with
          | (CNRAPlug a1), (CNRAPlug a2) => CNRAPlug (NRAEither a1 a2)
          | c1', c2' => CNRAEither c1' c2'
        end
      | CNRAEitherConcat c1 c2 =>
        match ac_simplify c1, ac_simplify c2 with
          | (CNRAPlug a1), (CNRAPlug a2) => CNRAPlug (NRAEitherConcat a1 a2)
          | c1', c2' => CNRAEitherConcat c1' c2'
        end
      | CNRAApp c1 c2 =>
        match ac_simplify c1, ac_simplify c2 with
          | (CNRAPlug a1), (CNRAPlug a2) => CNRAPlug (NRAApp a1 a2)
          | c1', c2' => CNRAApp c1' c2'
        end
    end.

  Lemma ac_simplify_holes_preserved c :
    ac_holes (ac_simplify c) = ac_holes c.

  Definition ac_nra_of_ctxt c
    := match (ac_simplify c) with
         | CNRAPlug a => Some a
         | _ => None
       end.

  Lemma ac_simplify_nholes c :
    ac_holes c = nil -> {a | ac_simplify c = CNRAPlug a}.

  Lemma ac_nra_of_ctxt_nholes c :
    ac_holes c = nil -> {a | ac_nra_of_ctxt c = Some a}.

  Lemma ac_simplify_idempotent c :
    ac_simplify (ac_simplify c) = ac_simplify c.

  Fixpoint ac_subst (c:nra_ctxt) (x:nat) (p:nra) : nra_ctxt :=
    match c with
      | CNRAHole x'
        => if x == x' then CNRAPlug p else CNRAHole x'
      | CNRAPlug a
        => CNRAPlug a
      | CNRABinop b c1 c2
        => CNRABinop b (ac_subst c1 x p) (ac_subst c2 x p)
      | CNRAUnop u c
        => CNRAUnop u (ac_subst c x p)
      | CNRAMap c1 c2
        => CNRAMap (ac_subst c1 x p) (ac_subst c2 x p)
      | CNRAMapProduct c1 c2
        => CNRAMapProduct (ac_subst c1 x p) (ac_subst c2 x p)
      | CNRAProduct c1 c2
        => CNRAProduct (ac_subst c1 x p) (ac_subst c2 x p)
      | CNRASelect c1 c2
        => CNRASelect (ac_subst c1 x p) (ac_subst c2 x p)
      | CNRADefault c1 c2
        => CNRADefault (ac_subst c1 x p) (ac_subst c2 x p)
      | CNRAEither c1 c2
        => CNRAEither (ac_subst c1 x p) (ac_subst c2 x p)
      | CNRAEitherConcat c1 c2
        => CNRAEitherConcat (ac_subst c1 x p) (ac_subst c2 x p)
      | CNRAApp c1 c2
        => CNRAApp (ac_subst c1 x p) (ac_subst c2 x p)
    end.

  Definition ac_substp (c:nra_ctxt) xp
    := let '(x, p) := xp in ac_subst c x p.
    
  Definition ac_substs c ps :=
    fold_left ac_substp ps c.

    Lemma ac_substs_app c ps1 ps2 :
     ac_substs c (ps1 ++ ps2) =
     ac_substs (ac_substs c ps1) ps2.
   
  Lemma ac_subst_holes_nin c x p :
    ~ In x (ac_holes c) -> ac_subst c x p = c.
  
  Lemma ac_subst_holes_remove c x p :
    ac_holes (ac_subst c x p) = (remove_all x (ac_holes c)).

  Lemma ac_substp_holes_remove c xp :
      ac_holes (ac_substp c xp) = remove_all (fst xp) (ac_holes c).

  Lemma ac_substs_holes_remove c ps :
    ac_holes (ac_substs c ps) =
    fold_left (fun h xy => remove_all (fst xy) h) ps (ac_holes c).

  Lemma ac_substs_Plug a ps :
    ac_substs (CNRAPlug a) ps = CNRAPlug a.
  
  Lemma ac_substs_Binop b c1 c2 ps :
    ac_substs (CNRABinop b c1 c2) ps = CNRABinop b (ac_substs c1 ps) (ac_substs c2 ps).

  Lemma ac_substs_Unop u c ps :
      ac_substs (CNRAUnop u c) ps = CNRAUnop u (ac_substs c ps).

  Lemma ac_substs_Map c1 c2 ps :
    ac_substs ( CNRAMap c1 c2) ps =
    CNRAMap (ac_substs c1 ps) (ac_substs c2 ps).

  Lemma ac_substs_MapProduct c1 c2 ps :
    ac_substs ( CNRAMapProduct c1 c2) ps =
    CNRAMapProduct (ac_substs c1 ps) (ac_substs c2 ps).
  
  Lemma ac_substs_Product c1 c2 ps :
    ac_substs ( CNRAProduct c1 c2) ps =
    CNRAProduct (ac_substs c1 ps) (ac_substs c2 ps).
  
  Lemma ac_substs_Select c1 c2 ps :
    ac_substs ( CNRASelect c1 c2) ps =
    CNRASelect (ac_substs c1 ps) (ac_substs c2 ps).
  
  Lemma ac_substs_Default c1 c2 ps :
    ac_substs ( CNRADefault c1 c2) ps =
    CNRADefault (ac_substs c1 ps) (ac_substs c2 ps).
  
  Lemma ac_substs_Either c1 c2 ps :
    ac_substs ( CNRAEither c1 c2) ps =
    CNRAEither (ac_substs c1 ps) (ac_substs c2 ps).
  
  Lemma ac_substs_EitherConcat c1 c2 ps :
    ac_substs ( CNRAEitherConcat c1 c2) ps =
    CNRAEitherConcat (ac_substs c1 ps) (ac_substs c2 ps).
  
  Lemma ac_substs_App c1 c2 ps :
    ac_substs ( CNRAApp c1 c2) ps =
    CNRAApp (ac_substs c1 ps) (ac_substs c2 ps).

  Local Hint Rewrite
       ac_substs_Plug
       ac_substs_Binop
       ac_substs_Unop
       ac_substs_Map
       ac_substs_MapProduct
       ac_substs_Product
       ac_substs_Select
       ac_substs_Default
       ac_substs_Either
       ac_substs_EitherConcat
       ac_substs_App : ac_substs.
  
  Lemma ac_simplify_holes_binary_op b c1 c2:
    ac_holes (CNRABinop b c1 c2) <> nil ->
    ac_simplify (CNRABinop b c1 c2) = CNRABinop b (ac_simplify c1) (ac_simplify c2).

  Lemma ac_simplify_holes_unary_op u c:
    ac_holes (CNRAUnop u c ) <> nil ->
    ac_simplify (CNRAUnop u c) = CNRAUnop u (ac_simplify c).

  Lemma ac_simplify_holes_map c1 c2:
    ac_holes (CNRAMap c1 c2) <> nil ->
    ac_simplify (CNRAMap c1 c2) = CNRAMap (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_mapconcat c1 c2:
    ac_holes (CNRAMapProduct c1 c2) <> nil ->
    ac_simplify (CNRAMapProduct c1 c2) = CNRAMapProduct (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_product c1 c2:
    ac_holes (CNRAProduct c1 c2) <> nil ->
    ac_simplify (CNRAProduct c1 c2) = CNRAProduct (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_select c1 c2:
    ac_holes (CNRASelect c1 c2) <> nil ->
    ac_simplify (CNRASelect c1 c2) = CNRASelect (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_default c1 c2:
    ac_holes (CNRADefault c1 c2) <> nil ->
    ac_simplify (CNRADefault c1 c2) = CNRADefault (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_either c1 c2:
    ac_holes (CNRAEither c1 c2) <> nil ->
    ac_simplify (CNRAEither c1 c2) = CNRAEither (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_eitherconcat c1 c2:
    ac_holes (CNRAEitherConcat c1 c2) <> nil ->
    ac_simplify (CNRAEitherConcat c1 c2) = CNRAEitherConcat (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_app c1 c2:
    ac_holes (CNRAApp c1 c2) <> nil ->
    ac_simplify (CNRAApp c1 c2) = CNRAApp (ac_simplify c1) (ac_simplify c2).

   Lemma ac_subst_nholes c x p :
     (ac_holes c) = nil -> ac_subst c x p = c.

   Lemma ac_subst_simplify_nholes c x p :
     (ac_holes c) = nil ->
     ac_subst (ac_simplify c) x p = ac_simplify c.

  Lemma ac_simplify_subst_simplify1 c x p :
    ac_simplify (ac_subst (ac_simplify c) x p) =
    ac_simplify (ac_subst c x p).

  Lemma ac_simplify_substs_simplify1 c ps :
    ac_simplify (ac_substs (ac_simplify c) ps) =
    ac_simplify (ac_substs c ps).

  Section equivs.
    Context (base_equiv:nra->nra->Prop).
    
   Definition nra_ctxt_equiv (c1 c2 : nra_ctxt)
     := forall (ps:list (nat * nra)),
          match ac_simplify (ac_substs c1 ps),
                ac_simplify (ac_substs c2 ps)
          with
            | CNRAPlug a1, CNRAPlug a2 => base_equiv a1 a2
            | _, _ => True
          end.

   Definition nra_ctxt_equiv_strict (c1 c2 : nra_ctxt)
     := forall (ps:list (nat * nra)),
          is_list_sorted lt_dec (domain ps) = true ->
          equivlist (domain ps) (ac_holes c1 ++ ac_holes c2) ->
          match ac_simplify (ac_substs c1 ps),
                ac_simplify (ac_substs c2 ps)
          with
            | CNRAPlug a1, CNRAPlug a2 => base_equiv a1 a2
            | _, _ => True
          end.

   Global Instance ac_simplify_proper :
     Proper (nra_ctxt_equiv ==> nra_ctxt_equiv) ac_simplify.
  
  Lemma ac_simplify_proper_inv x y:
    nra_ctxt_equiv (ac_simplify x) (ac_simplify y) -> nra_ctxt_equiv x y.

 Instance ac_subst_proper_part1 :
   Proper (nra_ctxt_equiv ==> eq ==> eq ==> nra_ctxt_equiv) ac_subst.

  Global Instance ac_substs_proper_part1: Proper (nra_ctxt_equiv ==> eq ==> nra_ctxt_equiv) ac_substs.

  Definition nra_ctxt_equiv_strict1 (c1 c2 : nra_ctxt)
     := forall (ps:list (nat * nra)),
          NoDup (domain ps) ->
          equivlist (domain ps) (ac_holes c1 ++ ac_holes c2) ->
          match ac_simplify (ac_substs c1 ps),
                ac_simplify (ac_substs c2 ps)
          with
            | CNRAPlug a1, CNRAPlug a2 => base_equiv a1 a2
            | _, _ => True
          end.

   Lemma ac_subst_swap_neq c x1 x2 y1 y2 :
     x1 <> x2 ->
   ac_subst (ac_subst c x1 y1) x2 y2 =
   ac_subst (ac_subst c x2 y2) x1 y1.
   
   Lemma ac_subst_swap_eq c x1 y1 y2 :
     ac_subst (ac_subst c x1 y1) x1 y2 =
     ac_subst c x1 y1.
           
   Lemma ac_substs_subst_swap_simpl x c y ps :
     ~ In x (domain ps) ->
      ac_substs (ac_subst c x y) ps
      =
      (ac_subst (ac_substs c ps) x y).
   
   Lemma ac_substs_perm c ps1 ps2 :
     NoDup (domain ps1) ->
     Permutation ps1 ps2 ->
     (ac_substs c ps1) =
     (ac_substs c ps2).
       
   Lemma nra_ctxt_equiv_strict_equiv1 (c1 c2 : nra_ctxt) :
     nra_ctxt_equiv_strict1 c1 c2 <-> nra_ctxt_equiv_strict c1 c2.

   Definition nra_ctxt_equiv_strict2 (c1 c2 : nra_ctxt)
     := forall (ps:list (nat * nra)),
          equivlist (domain ps) (ac_holes c1 ++ ac_holes c2) ->
          match ac_simplify (ac_substs c1 ps),
                ac_simplify (ac_substs c2 ps)
          with
            | CNRAPlug a1, CNRAPlug a2 => base_equiv a1 a2
            | _, _ => True
          end.

   Lemma ac_substs_in_nholes c x ps :
         In x (domain ps) ->
      ~ In x (ac_holes (ac_substs c ps)).
    
   Lemma substs_bdistinct_domain_rev c ps :
    (ac_substs c (bdistinct_domain (rev ps)))
    =
    (ac_substs c ps).
  
   Lemma nra_ctxt_equiv_strict1_equiv2 (c1 c2 : nra_ctxt) :
     nra_ctxt_equiv_strict2 c1 c2 <-> nra_ctxt_equiv_strict1 c1 c2.

   Definition nra_ctxt_equiv_strict3 (c1 c2 : nra_ctxt)
     := forall (ps:list (nat * nra)),
          incl (ac_holes c1 ++ ac_holes c2) (domain ps) ->
          match ac_simplify (ac_substs c1 ps),
                ac_simplify (ac_substs c2 ps)
          with
            | CNRAPlug a1, CNRAPlug a2 => base_equiv a1 a2
            | _, _ => True
          end.
   
   Lemma cut_down_to_substs c ps cut :
     incl (ac_holes c) cut ->
     (ac_substs c ps) = (ac_substs c (cut_down_to ps cut)).
         
   Lemma nra_ctxt_equiv_strict2_equiv3 (c1 c2 : nra_ctxt) :
     nra_ctxt_equiv_strict3 c1 c2 <-> nra_ctxt_equiv_strict2 c1 c2.

   Lemma nra_ctxt_equiv_strict3_equiv (c1 c2 : nra_ctxt) :
     nra_ctxt_equiv c1 c2 <-> nra_ctxt_equiv_strict3 c1 c2.

   Theorem nra_ctxt_equiv_strict_equiv (c1 c2 : nra_ctxt) :
     nra_ctxt_equiv c1 c2 <-> nra_ctxt_equiv_strict c1 c2.

   Lemma ac_holes_saturated_subst {B} f c ps :
      incl (ac_holes c) (domain ps) ->
      ac_holes
        (ac_substs c
                   (map (fun xy : nat * B => (fst xy, (f (snd xy)))) ps)) = nil.

  Global Instance nra_ctxt_equiv_refl {refl:Reflexive base_equiv}: Reflexive nra_ctxt_equiv.

  Global Instance nra_ctxt_equiv_sym {sym:Symmetric base_equiv}: Symmetric nra_ctxt_equiv.

  Global Instance nra_ctxt_equiv_trans {trans:Transitive base_equiv}: Transitive nra_ctxt_equiv.

  Global Instance nra_ctxt_equiv_equivalence {equiv:Equivalence base_equiv}: Equivalence nra_ctxt_equiv.

  Global Instance nra_ctxt_equiv_preorder {pre:PreOrder base_equiv} : PreOrder nra_ctxt_equiv.

  Global Instance nra_ctxt_equiv_strict_refl {refl:Reflexive base_equiv}: Reflexive nra_ctxt_equiv_strict.

  Global Instance nra_ctxt_equiv_strict_sym {sym:Symmetric base_equiv}: Symmetric nra_ctxt_equiv_strict.

  Global Instance nra_ctxt_equiv_strict_trans {trans:Transitive base_equiv}: Transitive nra_ctxt_equiv_strict.
  
  Global Instance nra_ctxt_equiv_strict_equivalence {equiv:Equivalence base_equiv}: Equivalence nra_ctxt_equiv_strict.

  Global Instance nra_ctxt_equiv_strict_preorder {pre:PreOrder base_equiv} : PreOrder nra_ctxt_equiv_strict.


  Global Instance CNRAPlug_proper :
    Proper (base_equiv ==> nra_ctxt_equiv) CNRAPlug.

  Global Instance CNRAPlug_proper_strict :
    Proper (base_equiv ==> nra_ctxt_equiv_strict) CNRAPlug.
  End equivs.
End NRAContext.


Delimit Scope nra_ctxt_scope with nra_ctxt.

Notation "'ID'" := (CNRAID) (at level 50) : nra_ctxt_scope.

Notation "‵‵ c" := (CNRAConst (dconst c)) (at level 0) : nra_ctxt_scope.
Notation "‵ c" := (CNRAConst c) (at level 0) : nra_ctxt_scope.
Notation "‵{||}" := (CNRAConst (dcoll nil)) (at level 0) : nra_ctxt_scope.
Notation "‵[||]" := (CNRAConst (drec nil)) (at level 50) : nra_ctxt_scope.

Notation "r1 ∧ r2" := (CNRABinop OpAnd r1 r2) (right associativity, at level 65): nra_ctxt_scope.
Notation "r1 ∨ r2" := (CNRABinop OpOr r1 r2) (right associativity, at level 70): nra_ctxt_scope.
Notation "r1 ≐ r2" := (CNRABinop OpEqual r1 r2) (right associativity, at level 70): nra_ctxt_scope.
Notation "r1 ≤ r2" := (CNRABinop OpLt r1 r2) (no associativity, at level 70): nra_ctxt_scope.
Notation "r1 ⋃ r2" := (CNRABinop OpBagUnion r1 r2) (right associativity, at level 70): nra_ctxt_scope.
Notation "r1 − r2" := (CNRABinop OpBagDiff r1 r2) (right associativity, at level 70): nra_ctxt_scope.
Notation "r1 ♯min r2" := (CNRABinop OpBagMin r1 r2) (right associativity, at level 70): nra_ctxt_scope.
Notation "r1 ♯max r2" := (CNRABinop OpBagMax r1 r2) (right associativity, at level 70): nra_ctxt_scope.
Notation "p ⊕ r" := ((CNRABinop OpRecConcat) p r) (at level 70) : nra_ctxt_scope.
Notation "p ⊗ r" := ((CNRABinop OpRecMerge) p r) (at level 70) : nra_ctxt_scope.

Notation "¬( r1 )" := (CNRAUnop OpNeg r1) (right associativity, at level 70): nra_ctxt_scope.
Notation "ε( r1 )" := (CNRAUnop OpDistinct r1) (right associativity, at level 70): nra_ctxt_scope.
Notation "♯count( r1 )" := (CNRAUnop OpCount r1) (right associativity, at level 70): nra_ctxt_scope.
Notation "♯flatten( d )" := (CNRAUnop OpFlatten d) (at level 50) : nra_ctxt_scope.
Notation "‵{| d |}" := ((CNRAUnop OpBag) d) (at level 50) : nra_ctxt_scope.
Notation "‵[| ( s , r ) |]" := ((CNRAUnop (OpRec s)) r) (at level 50) : nra_ctxt_scope.
Notation "¬π[ s1 ]( r )" := ((CNRAUnop (OpRecRemove s1)) r) (at level 50) : nra_ctxt_scope.
Notation "p · r" := ((CNRAUnop (OpDot r)) p) (left associativity, at level 40): nra_ctxt_scope.

Notation "χ⟨ p ⟩( r )" := (CNRAMap p r) (at level 70) : nra_ctxt_scope.
Notation "⋈ᵈ⟨ e2 ⟩( e1 )" := (CNRAMapProduct e2 e1) (at level 70) : nra_ctxt_scope.
Notation "r1 × r2" := (CNRAProduct r1 r2) (right associativity, at level 70): nra_ctxt_scope.
Notation "σ⟨ p ⟩( r )" := (CNRASelect p r) (at level 70) : nra_ctxt_scope.
Notation "r1 ∥ r2" := (CNRADefault r1 r2) (right associativity, at level 70): nra_ctxt_scope.
Notation "r1 ◯ r2" := (CNRAApp r1 r2) (right associativity, at level 60): nra_ctxt_scope.

Notation "$ n" := (CNRAHole n) (at level 50) : nra_ctxt_scope.

Notation "X ≡ₐ Y" := (nra_ctxt_equiv nra_eq X Y) (at level 90) : nra_ctxt_scope.

Global Hint Rewrite
       @ac_substs_Plug
       @ac_substs_Binop
       @ac_substs_Unop
       @ac_substs_Map
       @ac_substs_MapProduct
       @ac_substs_Product
       @ac_substs_Select
       @ac_substs_Default
       @ac_substs_Either
       @ac_substs_EitherConcat
       @ac_substs_App : ac_substs.