Qcert.NRA.Context.NRAContext

Section NRAContext.





  Context {fruntime:foreign_runtime}.

  Inductive nra_ctxt : Set :=
  | CHole : nat → nra_ctxt
  | CPlug : nra → nra_ctxt
  | CABinop : binOp → nra_ctxt → nra_ctxt → nra_ctxt
  | CAUnop : unaryOp → nra_ctxt → nra_ctxt
  | CAMap : nra_ctxt → nra_ctxt → nra_ctxt
  | CAMapConcat : nra_ctxt → nra_ctxt → nra_ctxt
  | CAProduct : nra_ctxt → nra_ctxt → nra_ctxt
  | CASelect : nra_ctxt → nra_ctxt → nra_ctxt
  | CADefault : nra_ctxt → nra_ctxt → nra_ctxt
  | CAEither : nra_ctxt → nra_ctxt → nra_ctxt
  | CAEitherConcat : nra_ctxt → nra_ctxt → nra_ctxt
  | CAApp : nra_ctxt → nra_ctxt → nra_ctxt
  .

  Definition CAID : nra_ctxt
    := CPlug AID.

  Definition CAConst : data → nra_ctxt
    := fun d ⇒ CPlug (AConst d).

  Fixpoint ac_holes (c:nra_ctxt) : list nat :=
    match c with
      | CHole x ⇒ x::nil
      | CPlug a ⇒ nil
      | CABinop b c1 c2 ⇒ ac_holes c1 ++ ac_holes c2
      | CAUnop u c' ⇒ ac_holes c'
      | CAMap c1 c2 ⇒ ac_holes c1 ++ ac_holes c2
      | CAMapConcat c1 c2 ⇒ ac_holes c1 ++ ac_holes c2
      | CAProduct c1 c2 ⇒ ac_holes c1 ++ ac_holes c2
      | CASelect c1 c2 ⇒ ac_holes c1 ++ ac_holes c2
      | CADefault c1 c2 ⇒ ac_holes c1 ++ ac_holes c2
      | CAEither c1 c2 ⇒ ac_holes c1 ++ ac_holes c2
      | CAEitherConcat c1 c2 ⇒ ac_holes c1 ++ ac_holes c2
      | CAApp c1 c2 ⇒ ac_holes c1 ++ ac_holes c2
    end.

  Fixpoint ac_simplify (c:nra_ctxt) : nra_ctxt :=
    match c with
      | CHole x ⇒ CHole x
      | CPlug a ⇒ CPlug a
      | CABinop b c1 c2 ⇒
        match ac_simplify c1, ac_simplify c2 with
          | (CPlug a1), (CPlug a2) ⇒ CPlug (ABinop b a1 a2)
          | c1', c2' ⇒ CABinop b c1' c2'
        end
      | CAUnop u c ⇒
        match ac_simplify c with
          | CPlug a ⇒ CPlug (AUnop u a)
          | c' ⇒ CAUnop u c'
        end
      | CAMap c1 c2 ⇒
        match ac_simplify c1, ac_simplify c2 with
          | (CPlug a1), (CPlug a2) ⇒ CPlug (AMap a1 a2)
          | c1', c2' ⇒ CAMap c1' c2'
        end
      | CAMapConcat c1 c2 ⇒
        match ac_simplify c1, ac_simplify c2 with
          | (CPlug a1), (CPlug a2) ⇒ CPlug (AMapConcat a1 a2)
          | c1', c2' ⇒ CAMapConcat c1' c2'
        end
      | CAProduct c1 c2 ⇒
        match ac_simplify c1, ac_simplify c2 with
          | (CPlug a1), (CPlug a2) ⇒ CPlug (AProduct a1 a2)
          | c1', c2' ⇒ CAProduct c1' c2'
        end
      | CASelect c1 c2 ⇒
        match ac_simplify c1, ac_simplify c2 with
          | (CPlug a1), (CPlug a2) ⇒ CPlug (ASelect a1 a2)
          | c1', c2' ⇒ CASelect c1' c2'
        end
      | CADefault c1 c2 ⇒
        match ac_simplify c1, ac_simplify c2 with
          | (CPlug a1), (CPlug a2) ⇒ CPlug (ADefault a1 a2)
          | c1', c2' ⇒ CADefault c1' c2'
        end
      | CAEither c1 c2 ⇒
        match ac_simplify c1, ac_simplify c2 with
          | (CPlug a1), (CPlug a2) ⇒ CPlug (AEither a1 a2)
          | c1', c2' ⇒ CAEither c1' c2'
        end
      | CAEitherConcat c1 c2 ⇒
        match ac_simplify c1, ac_simplify c2 with
          | (CPlug a1), (CPlug a2) ⇒ CPlug (AEitherConcat a1 a2)
          | c1', c2' ⇒ CAEitherConcat c1' c2'
        end
      | CAApp c1 c2 ⇒
        match ac_simplify c1, ac_simplify c2 with
          | (CPlug a1), (CPlug a2) ⇒ CPlug (AApp a1 a2)
          | c1', c2' ⇒ CAApp 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
         | CPlug a ⇒ Some a
         | _ ⇒ None
       end.

  Lemma ac_simplify_nholes c :
    ac_holes c = nil → {a | ac_simplify c = CPlug 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
      | CHole x'
        ⇒ if x == x' then CPlug p else CHole x'
      | CPlug a
        ⇒ CPlug a
      | CABinop b c1 c2
        ⇒ CABinop b (ac_subst c1 x p) (ac_subst c2 x p)
      | CAUnop u c
        ⇒ CAUnop u (ac_subst c x p)
      | CAMap c1 c2
        ⇒ CAMap (ac_subst c1 x p) (ac_subst c2 x p)
      | CAMapConcat c1 c2
        ⇒ CAMapConcat (ac_subst c1 x p) (ac_subst c2 x p)
      | CAProduct c1 c2
        ⇒ CAProduct (ac_subst c1 x p) (ac_subst c2 x p)
      | CASelect c1 c2
        ⇒ CASelect (ac_subst c1 x p) (ac_subst c2 x p)
      | CADefault c1 c2
        ⇒ CADefault (ac_subst c1 x p) (ac_subst c2 x p)
      | CAEither c1 c2
        ⇒ CAEither (ac_subst c1 x p) (ac_subst c2 x p)
      | CAEitherConcat c1 c2
        ⇒ CAEitherConcat (ac_subst c1 x p) (ac_subst c2 x p)
      | CAApp c1 c2
        ⇒ CAApp (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 (CPlug a) ps = CPlug a.

  Lemma ac_substs_Binop b c1 c2 ps :
    ac_substs (CABinop b c1 c2) ps = CABinop b (ac_substs c1 ps) (ac_substs c2 ps).

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

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

  Lemma ac_substs_MapConcat c1 c2 ps :
    ac_substs ( CAMapConcat c1 c2) ps =
    CAMapConcat (ac_substs c1 ps) (ac_substs c2 ps).

  Lemma ac_substs_Product c1 c2 ps :
    ac_substs ( CAProduct c1 c2) ps =
    CAProduct (ac_substs c1 ps) (ac_substs c2 ps).

  Lemma ac_substs_Select c1 c2 ps :
    ac_substs ( CASelect c1 c2) ps =
    CASelect (ac_substs c1 ps) (ac_substs c2 ps).

  Lemma ac_substs_Default c1 c2 ps :
    ac_substs ( CADefault c1 c2) ps =
    CADefault (ac_substs c1 ps) (ac_substs c2 ps).

  Lemma ac_substs_Either c1 c2 ps :
    ac_substs ( CAEither c1 c2) ps =
    CAEither (ac_substs c1 ps) (ac_substs c2 ps).

  Lemma ac_substs_EitherConcat c1 c2 ps :
    ac_substs ( CAEitherConcat c1 c2) ps =
    CAEitherConcat (ac_substs c1 ps) (ac_substs c2 ps).

  Lemma ac_substs_App c1 c2 ps :
    ac_substs ( CAApp c1 c2) ps =
    CAApp (ac_substs c1 ps) (ac_substs c2 ps).


  Lemma ac_simplify_holes_binop b c1 c2:
    ac_holes (CABinop b c1 c2) ≠ nil →
    ac_simplify (CABinop b c1 c2) = CABinop b (ac_simplify c1) (ac_simplify c2).

  Lemma ac_simplify_holes_unop u c:
    ac_holes (CAUnop u c ) ≠ nil →
    ac_simplify (CAUnop u c) = CAUnop u (ac_simplify c).

  Lemma ac_simplify_holes_map c1 c2:
    ac_holes (CAMap c1 c2) ≠ nil →
    ac_simplify (CAMap c1 c2) = CAMap (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_mapconcat c1 c2:
    ac_holes (CAMapConcat c1 c2) ≠ nil →
    ac_simplify (CAMapConcat c1 c2) = CAMapConcat (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_product c1 c2:
    ac_holes (CAProduct c1 c2) ≠ nil →
    ac_simplify (CAProduct c1 c2) = CAProduct (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_select c1 c2:
    ac_holes (CASelect c1 c2) ≠ nil →
    ac_simplify (CASelect c1 c2) = CASelect (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_default c1 c2:
    ac_holes (CADefault c1 c2) ≠ nil →
    ac_simplify (CADefault c1 c2) = CADefault (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_either c1 c2:
    ac_holes (CAEither c1 c2) ≠ nil →
    ac_simplify (CAEither c1 c2) = CAEither (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_eitherconcat c1 c2:
    ac_holes (CAEitherConcat c1 c2) ≠ nil →
    ac_simplify (CAEitherConcat c1 c2) = CAEitherConcat (ac_simplify c1) (ac_simplify c2).

    Lemma ac_simplify_holes_app c1 c2:
    ac_holes (CAApp c1 c2) ≠ nil →
    ac_simplify (CAApp c1 c2) = CAApp (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)
     := ∀ (ps:list (nat × nra)),
          match ac_simplify (ac_substs c1 ps),
                ac_simplify (ac_substs c2 ps)
          with
            | CPlug a1, CPlug a2 ⇒ base_equiv a1 a2
            | _, _ ⇒ True
          end.

   Definition nra_ctxt_equiv_strict (c1 c2 : nra_ctxt)
     := ∀ (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
            | CPlug a1, CPlug 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)
     := ∀ (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
            | CPlug a1, CPlug 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)
     := ∀ (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
            | CPlug a1, CPlug 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)
     := ∀ (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
            | CPlug a1, CPlug 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 CPlug_proper :
    Proper (base_equiv ==> nra_ctxt_equiv) CPlug.

  Global Instance CPlug_proper_strict :
    Proper (base_equiv ==> nra_ctxt_equiv_strict) CPlug.
  End equivs.
End NRAContext.



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

Notation "‵‵ c" := (CAConst (dconst c)) (at level 0) : nra_ctxt_scope. Notation "‵ c" := (CAConst c) (at level 0) : nra_ctxt_scope. Notation "‵{||}" := (CAConst (dcoll nil)) (at level 0) : nra_ctxt_scope. Notation "‵[||]" := (CAConst (drec nil)) (at level 50) : nra_ctxt_scope.
Notation "r1 ∧ r2" := (CABinop AAnd r1 r2) (right associativity, at level 65): nra_ctxt_scope. Notation "r1 ∨ r2" := (CABinop AOr r1 r2) (right associativity, at level 70): nra_ctxt_scope. Notation "r1 ≐ r2" := (CABinop AEq r1 r2) (right associativity, at level 70): nra_ctxt_scope. Notation "r1 ≤ r2" := (CABinop ALt r1 r2) (no associativity, at level 70): nra_ctxt_scope. Notation "r1 ⋃ r2" := (CABinop AUnion r1 r2) (right associativity, at level 70): nra_ctxt_scope. Notation "r1 − r2" := (CABinop AMinus r1 r2) (right associativity, at level 70): nra_ctxt_scope. Notation "r1 ♯min r2" := (CABinop AMin r1 r2) (right associativity, at level 70): nra_ctxt_scope. Notation "r1 ♯max r2" := (CABinop AMax r1 r2) (right associativity, at level 70): nra_ctxt_scope. Notation "p ⊕ r" := ((CABinop AConcat) p r) (at level 70) : nra_ctxt_scope. Notation "p ⊗ r" := ((CABinop AMergeConcat) p r) (at level 70) : nra_ctxt_scope.
Notation "¬( r1 )" := (CAUnop ANeg r1) (right associativity, at level 70): nra_ctxt_scope. Notation "ε( r1 )" := (CAUnop ADistinct r1) (right associativity, at level 70): nra_ctxt_scope. Notation "♯count( r1 )" := (CAUnop ACount r1) (right associativity, at level 70): nra_ctxt_scope. Notation "♯flatten( d )" := (CAUnop AFlatten d) (at level 50) : nra_ctxt_scope. Notation "‵{| d |}" := ((CAUnop AColl) d) (at level 50) : nra_ctxt_scope. Notation "‵[| ( s , r ) |]" := ((CAUnop (ARec s)) r) (at level 50) : nra_ctxt_scope. Notation "¬π[ s1 ]( r )" := ((CAUnop (ARecRemove s1)) r) (at level 50) : nra_ctxt_scope. Notation "p · r" := ((CAUnop (ADot r)) p) (left associativity, at level 40): nra_ctxt_scope.
Notation "χ⟨ p ⟩( r )" := (CAMap p r) (at level 70) : nra_ctxt_scope. Notation "⋈ᵈ⟨ e2 ⟩( e1 )" := (CAMapConcat e2 e1) (at level 70) : nra_ctxt_scope. Notation "r1 × r2" := (CAProduct r1 r2) (right associativity, at level 70): nra_ctxt_scope. Notation "σ⟨ p ⟩( r )" := (CASelect p r) (at level 70) : nra_ctxt_scope. Notation "r1 ∥ r2" := (CADefault r1 r2) (right associativity, at level 70): nra_ctxt_scope. Notation "r1 ◯ r2" := (CAApp r1 r2) (right associativity, at level 60): nra_ctxt_scope.
Notation "$ n" := (CHole n) (at level 50) : nra_ctxt_scope.

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