Section NRAContext.
Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Program.
Require Import List Permutation.
Require Import String.
Require Import NPeano.
Require Import Arith.
Require Import Bool.
Require Import Utils BasicRuntime.
Require Import NRA NRAEq.
Require Import RBindingsNat.
Local Open Scope nra_scope.
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.
Proof.
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}.
Proof.
induction c;
simpl; [
discriminate |
eauto 2 | ..];
try solve [
intros s0;
apply app_eq_nil in s0;
destruct s0 as [
s10 s20];
destruct (
IHc1 s10)
as [
a1 e1];
destruct (
IHc2 s20)
as [
a2 e2];
rewrite e1,
e2;
eauto 2].
unary operator case *)
intros s0;
destruct (
IHc s0)
as [
a e];
rewrite e;
eauto 2.
Defined.
Lemma ac_nra_of_ctxt_nholes c :
ac_holes c =
nil -> {
a |
ac_nra_of_ctxt c =
Some a}.
Proof.
Lemma ac_simplify_idempotent c :
ac_simplify (
ac_simplify c) =
ac_simplify c.
Proof.
induction c;
simpl;
trivial;
try solve [
destruct (
ac_simplify c);
simpl in *;
trivial;
match_destr;
try congruence
|
destruct (
ac_simplify c1);
simpl;
try rewrite IHc2;
trivial;
destruct (
ac_simplify c2);
simpl in *;
trivial;
match_destr;
try congruence].
Qed.
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.
Proof.
Lemma ac_subst_holes_nin c x p :
~
In x (
ac_holes c) ->
ac_subst c x p =
c.
Proof.
induction c;
simpl;
intros;
[
match_destr;
intuition |
trivial | .. ];
repeat rewrite in_app_iff in *;
f_equal;
auto.
Qed.
Lemma ac_subst_holes_remove c x p :
ac_holes (
ac_subst c x p) = (
remove_all x (
ac_holes c)).
Proof.
induction c;
simpl;
intros;
trivial;
try solve[
rewrite remove_all_app;
congruence].
CHole *)
match_destr;
match_destr;
simpl;
try rewrite app_nil_r;
congruence.
Qed.
Lemma ac_substp_holes_remove c xp :
ac_holes (
ac_substp c xp) =
remove_all (
fst xp) (
ac_holes c).
Proof.
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).
Proof.
Lemma ac_substs_Plug a ps :
ac_substs (
CPlug a)
ps =
CPlug a.
Proof.
induction ps; simpl; trivial; intros.
destruct a0; simpl; auto.
Qed.
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).
Proof.
revert c1 c2.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Lemma ac_substs_Unop u c ps :
ac_substs (
CAUnop u c)
ps =
CAUnop u (
ac_substs c ps).
Proof.
revert c.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Lemma ac_substs_Map c1 c2 ps :
ac_substs (
CAMap c1 c2)
ps =
CAMap (
ac_substs c1 ps) (
ac_substs c2 ps).
Proof.
revert c1 c2.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Lemma ac_substs_MapConcat c1 c2 ps :
ac_substs (
CAMapConcat c1 c2)
ps =
CAMapConcat (
ac_substs c1 ps) (
ac_substs c2 ps).
Proof.
revert c1 c2.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Lemma ac_substs_Product c1 c2 ps :
ac_substs (
CAProduct c1 c2)
ps =
CAProduct (
ac_substs c1 ps) (
ac_substs c2 ps).
Proof.
revert c1 c2.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Lemma ac_substs_Select c1 c2 ps :
ac_substs (
CASelect c1 c2)
ps =
CASelect (
ac_substs c1 ps) (
ac_substs c2 ps).
Proof.
revert c1 c2.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Lemma ac_substs_Default c1 c2 ps :
ac_substs (
CADefault c1 c2)
ps =
CADefault (
ac_substs c1 ps) (
ac_substs c2 ps).
Proof.
revert c1 c2.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Lemma ac_substs_Either c1 c2 ps :
ac_substs (
CAEither c1 c2)
ps =
CAEither (
ac_substs c1 ps) (
ac_substs c2 ps).
Proof.
revert c1 c2.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Lemma ac_substs_EitherConcat c1 c2 ps :
ac_substs (
CAEitherConcat c1 c2)
ps =
CAEitherConcat (
ac_substs c1 ps) (
ac_substs c2 ps).
Proof.
revert c1 c2.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Lemma ac_substs_App c1 c2 ps :
ac_substs (
CAApp c1 c2)
ps =
CAApp (
ac_substs c1 ps) (
ac_substs c2 ps).
Proof.
revert c1 c2.
induction ps; simpl; trivial; intros.
destruct a; simpl; auto.
Qed.
Hint Rewrite
ac_substs_Plug
ac_substs_Binop
ac_substs_Unop
ac_substs_Map
ac_substs_MapConcat
ac_substs_Product
ac_substs_Select
ac_substs_Default
ac_substs_Either
ac_substs_EitherConcat
ac_substs_App :
ac_substs.
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).
Proof.
Lemma ac_simplify_holes_unop u c:
ac_holes (
CAUnop u c ) <>
nil ->
ac_simplify (
CAUnop u c) =
CAUnop u (
ac_simplify c).
Proof.
intros.
simpl in H.
generalize (
ac_simplify_holes_preserved c);
intros pres1;
simpl;
intros.
match_destr.
simpl in *;
rewrite <-
pres1 in H.
simpl in H;
intuition.
Qed.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
Lemma ac_subst_nholes c x p :
(
ac_holes c) =
nil ->
ac_subst c x p =
c.
Proof.
Lemma ac_subst_simplify_nholes c x p :
(
ac_holes c) =
nil ->
ac_subst (
ac_simplify c)
x p =
ac_simplify c.
Proof.
Lemma ac_simplify_subst_simplify1 c x p :
ac_simplify (
ac_subst (
ac_simplify c)
x p) =
ac_simplify (
ac_subst c x p).
Proof.
Lemma ac_simplify_substs_simplify1 c ps :
ac_simplify (
ac_substs (
ac_simplify c)
ps) =
ac_simplify (
ac_substs c ps).
Proof.
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
|
CPlug a1,
CPlug 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
|
CPlug a1,
CPlug a2 =>
base_equiv a1 a2
|
_,
_ =>
True
end.
Global Instance ac_simplify_proper :
Proper (
nra_ctxt_equiv ==>
nra_ctxt_equiv)
ac_simplify.
Proof.
Lemma ac_simplify_proper_inv x y:
nra_ctxt_equiv (
ac_simplify x) (
ac_simplify y) ->
nra_ctxt_equiv x y.
Proof.
Instance ac_subst_proper_part1 :
Proper (
nra_ctxt_equiv ==>
eq ==>
eq ==>
nra_ctxt_equiv)
ac_subst.
Proof.
Global Instance ac_substs_proper_part1:
Proper (
nra_ctxt_equiv ==>
eq ==>
nra_ctxt_equiv)
ac_substs.
Proof.
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
|
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.
Proof.
induction c; simpl;
[ repeat (match_destr; simpl; try congruence) | trivial | .. ];
intuition; congruence.
Qed.
Lemma ac_subst_swap_eq c x1 y1 y2 :
ac_subst (
ac_subst c x1 y1)
x1 y2 =
ac_subst c x1 y1.
Proof.
induction c; simpl;
[ repeat (match_destr; simpl; try congruence) | trivial | .. ];
intuition; congruence.
Qed.
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).
Proof.
revert c.
induction ps;
simpl;
trivial;
intros.
rewrite <-
IHps;
trivial.
+
unfold ac_substp.
destruct a.
rewrite ac_subst_swap_neq;
trivial.
intuition.
+
intuition.
Qed.
Lemma ac_substs_perm c ps1 ps2 :
NoDup (
domain ps1) ->
Permutation ps1 ps2 ->
(
ac_substs c ps1) =
(
ac_substs c ps2).
Proof.
intros nd perm.
revert c.
revert ps1 ps2 perm nd.
apply (
Permutation_ind_bis
(
fun ps1 ps2 =>
NoDup (
domain ps1) ->
forall c :
nra_ctxt,
ac_substs c ps1 =
ac_substs c ps2 ));
intros;
simpl.
-
trivial.
-
inversion H1;
subst.
rewrite H0;
trivial.
-
inversion H1;
subst.
inversion H5;
subst.
rewrite H0;
trivial.
destruct x;
destruct y;
simpl.
rewrite ac_subst_swap_neq;
trivial.
simpl in *.
intuition.
-
rewrite H0,
H2;
trivial.
rewrite <-
H.
trivial.
Qed.
Lemma nra_ctxt_equiv_strict_equiv1 (
c1 c2 :
nra_ctxt) :
nra_ctxt_equiv_strict1 c1 c2 <->
nra_ctxt_equiv_strict c1 c2.
Proof.
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
|
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)).
Proof.
Lemma substs_bdistinct_domain_rev c ps :
(
ac_substs c (
bdistinct_domain (
rev ps)))
=
(
ac_substs c ps).
Proof.
Lemma nra_ctxt_equiv_strict1_equiv2 (
c1 c2 :
nra_ctxt) :
nra_ctxt_equiv_strict2 c1 c2 <->
nra_ctxt_equiv_strict1 c1 c2.
Proof.
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
|
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)).
Proof.
Lemma nra_ctxt_equiv_strict2_equiv3 (
c1 c2 :
nra_ctxt) :
nra_ctxt_equiv_strict3 c1 c2 <->
nra_ctxt_equiv_strict2 c1 c2.
Proof.
Lemma nra_ctxt_equiv_strict3_equiv (
c1 c2 :
nra_ctxt) :
nra_ctxt_equiv c1 c2 <->
nra_ctxt_equiv_strict3 c1 c2.
Proof.
Theorem nra_ctxt_equiv_strict_equiv (
c1 c2 :
nra_ctxt) :
nra_ctxt_equiv c1 c2 <->
nra_ctxt_equiv_strict c1 c2.
Proof.
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.
Proof.
Global Instance nra_ctxt_equiv_refl {
refl:
Reflexive base_equiv}:
Reflexive nra_ctxt_equiv.
Proof.
Global Instance nra_ctxt_equiv_sym {
sym:
Symmetric base_equiv}:
Symmetric nra_ctxt_equiv.
Proof.
unfold nra_ctxt_equiv.
red;
intros.
-
specialize (
H ps).
match_destr;
match_destr.
symmetry.
trivial.
Qed.
Global Instance nra_ctxt_equiv_trans {
trans:
Transitive base_equiv}:
Transitive nra_ctxt_equiv.
Proof.
Global Instance nra_ctxt_equiv_equivalence {
equiv:
Equivalence base_equiv}:
Equivalence nra_ctxt_equiv.
Proof.
constructor; red; intros.
- reflexivity.
- symmetry; trivial.
- etransitivity; eauto.
Qed.
Global Instance nra_ctxt_equiv_preorder {
pre:
PreOrder base_equiv} :
PreOrder nra_ctxt_equiv.
Proof.
constructor; red; intros.
- reflexivity.
- etransitivity; eauto.
Qed.
Global Instance nra_ctxt_equiv_strict_refl {
refl:
Reflexive base_equiv}:
Reflexive nra_ctxt_equiv_strict.
Proof.
Global Instance nra_ctxt_equiv_strict_sym {
sym:
Symmetric base_equiv}:
Symmetric nra_ctxt_equiv_strict.
Proof.
Global Instance nra_ctxt_equiv_strict_trans {
trans:
Transitive base_equiv}:
Transitive nra_ctxt_equiv_strict.
Proof.
Global Instance nra_ctxt_equiv_strict_equivalence {
equiv:
Equivalence base_equiv}:
Equivalence nra_ctxt_equiv_strict.
Proof.
constructor; red; intros.
- reflexivity.
- symmetry; trivial.
- etransitivity; eauto.
Qed.
Global Instance nra_ctxt_equiv_strict_preorder {
pre:
PreOrder base_equiv} :
PreOrder nra_ctxt_equiv_strict.
Proof.
constructor; red; intros.
- reflexivity.
- etransitivity; eauto.
Qed.
Global Instance CPlug_proper :
Proper (
base_equiv ==>
nra_ctxt_equiv)
CPlug.
Proof.
Global Instance CPlug_proper_strict :
Proper (
base_equiv ==>
nra_ctxt_equiv_strict)
CPlug.
Proof.
End equivs.
End NRAContext.
Delimit Scope nra_ctxt_scope with nra_ctxt.
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.
Hint Rewrite
@
ac_substs_Plug
@
ac_substs_Binop
@
ac_substs_Unop
@
ac_substs_Map
@
ac_substs_MapConcat
@
ac_substs_Product
@
ac_substs_Select
@
ac_substs_Default
@
ac_substs_Either
@
ac_substs_EitherConcat
@
ac_substs_App :
ac_substs.