Module NNRCShadow
Section NNRCShadow.
Require Import String.
Require Import List.
Require Import Arith.
Require Import Peano_dec.
Require Import EquivDec Decidable.
Require Import Utils BasicRuntime.
Require Import cNNRC cNNRCShadow.
Require Import NNRC NNRCSize.
Close Scope nnrc_scope.
Context {
fruntime:
foreign_runtime}.
Lemma nnrc_ext_eval_remove_duplicate_env {
h:
brand_relation_t}
l v x l'
x'
l''
e :
@
nnrc_ext_eval _ h (
l ++ (
v,
x)::
l' ++ (
v,
x')::
l'')
e =
@
nnrc_ext_eval _ h (
l ++ (
v,
x)::
l' ++
l'')
e.
Proof.
Lemma nnrc_ext_eval_remove_duplicate_env_weak {
h:
list (
string*
string)}
v1 v2 x x'
x''
l e :
@
nnrc_ext_eval _ h ((
v1,
x)::(
v2,
x')::(
v1,
x'')::
l)
e =
@
nnrc_ext_eval _ h ((
v1,
x)::(
v2,
x')::
l)
e.
Proof.
Lemma nnrc_ext_eval_remove_duplicate_env_weak_cons {
h:
list (
string*
string)}
v1 v2 x x'
x''
l e :
@
nnrc_ext_eval _ h ((
v1,
x)::(
v2,
x')::(
v2,
x'')::
l)
e =
@
nnrc_ext_eval _ h ((
v1,
x)::(
v2,
x')::
l)
e.
Proof.
Lemma nnrc_ext_eval_remove_free_env {
h:
list (
string*
string)}
l v x l'
e :
~
In v (
nnrc_free_vars e) ->
@
nnrc_ext_eval _ h (
l ++ (
v,
x)::
l')
e = @
nnrc_ext_eval _ h (
l ++
l')
e.
Proof.
Lemma nnrc_ext_eval_remove_free_env_weak {
h:
list (
string*
string)}
v1 x1 v x e :
~
In v (
nnrc_free_vars e) ->
@
nnrc_ext_eval _ h ((
v1,
x1)::(
v,
x)::
nil)
e = @
nnrc_ext_eval _ h ((
v1,
x1)::
nil)
e.
Proof.
Lemma nnrc_ext_eval_swap_neq {
h:
list (
string*
string)}
l1 v1 x1 v2 x2 l2 e :
v1 <>
v2 ->
@
nnrc_ext_eval _ h (
l1++(
v1,
x1)::(
v2,
x2)::
l2)
e =
@
nnrc_ext_eval _ h (
l1++(
v2,
x2)::(
v1,
x1)::
l2)
e.
Proof.
Lemma nnrc_ext_eval_subst_dunit {
h:
list (
string*
string)}
env e v :
@
nnrc_ext_eval _ h ((
v,
dunit)::
env)
e =
@
nnrc_ext_eval _ h env (
nnrc_subst e v (
NNRCConst dunit)).
Proof.
Lemma nnrc_ext_eval_cons_subst {
h:
list (
string*
string)}
e env v x v' :
~ (
In v' (
nnrc_free_vars e)) ->
~ (
In v' (
nnrc_bound_vars e)) ->
@
nnrc_ext_eval _ h ((
v',
x)::
env) (
nnrc_subst e v (
NNRCVar v')) =
@
nnrc_ext_eval _ h ((
v,
x)::
env)
e.
Proof.
Lemma nnrc_ext_eval_equiv_free_in_env:
forall n,
forall env1 env2,
(
forall x,
In x (
nnrc_free_vars n) ->
lookup equiv_dec env1 x =
lookup equiv_dec env2 x) ->
forall h,
@
nnrc_ext_eval _ h env1 n = @
nnrc_ext_eval _ h env2 n.
Proof.
intros n.
nnrc_cases (
induction n)
Case;
intros env1 env2 Henv_eq h;
unfold nnrc_ext_eval in *;
simpl.
-
Case "
NNRCVar"%
string.
simpl.
apply Henv_eq.
simpl;
auto.
-
Case "
NNRCConst"%
string.
simpl.
reflexivity.
-
Case "
NNRCBinop"%
string.
simpl.
rewrite (
IHn1 env1 env2).
rewrite (
IHn2 env1 env2).
reflexivity.
+
intros x Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCBinop b n1 n2)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n2)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n;
assumption.
+
intros x Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCBinop b n1 n2)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n1)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n;
assumption.
-
Case "
NNRCUnop"%
string.
simpl.
rewrite (
IHn env1 env2).
reflexivity.
+
intros x Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCUnop u n)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n)); [ |
contradiction ].
simpl in n0.
assumption.
-
Case "
NNRCLet"%
string.
simpl.
rewrite (
IHn1 env1 env2).
destruct (@
nnrc_core_eval _ h env2 (
nnrc_ext_to_nnrc n1));
try congruence.
rewrite (
IHn2 ((
v,
d) ::
env1) ((
v,
d) ::
env2));
try reflexivity.
intros x.
simpl.
destruct (
equiv_dec x v);
try reflexivity.
+
intros Hx.
destruct (
in_dec equiv_dec x (
nnrc_free_vars (
NNRCLet v n1 n2)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n2)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n.
apply (
not_in_remove_impl_not_in x v);
assumption.
+
intros x Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCLet v n1 n2)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n1)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n;
assumption.
-
Case "
NNRCFor"%
string.
simpl.
rewrite (
IHn1 env1 env2).
destruct (@
nnrc_core_eval _ h env2 (
nnrc_ext_to_nnrc n1));
try reflexivity.
destruct d;
try reflexivity.
unfold lift.
assert (
rmap (
fun d1 :
data => @
nnrc_core_eval _ h ((
v,
d1) ::
env1) (
nnrc_ext_to_nnrc n2))
l
=
rmap (
fun d1 :
data => @
nnrc_core_eval _ h ((
v,
d1) ::
env2) (
nnrc_ext_to_nnrc n2))
l)
as Hfun_eq;
try solve [
rewrite Hfun_eq;
reflexivity].
apply rmap_ext;
intros d ind.
rewrite (
IHn2 ((
v,
d) ::
env1) ((
v,
d) ::
env2));
try reflexivity.
intros x.
simpl.
destruct (
equiv_dec x v);
try reflexivity.
+
intros Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCFor v n1 n2)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n2)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n.
apply (
not_in_remove_impl_not_in x v);
assumption.
+
intros x Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCFor v n1 n2)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n1)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n;
assumption.
-
Case "
NNRCIf"%
string.
simpl.
unfold olift.
rewrite (
IHn1 env1 env2).
destruct (@
nnrc_core_eval _ h env2 (
nnrc_ext_to_nnrc n1));
try reflexivity.
destruct d;
try reflexivity.
destruct b.
+
rewrite (
IHn2 env1 env2).
reflexivity.
*
intros x Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCIf n1 n2 n3)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n2)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n.
apply nin_app_or in H0.
destruct H0;
assumption.
+
rewrite (
IHn3 env1 env2).
reflexivity.
*
intros x Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCIf n1 n2 n3)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n3)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n.
apply nin_app_or in H0.
destruct H0;
assumption.
+
intros x Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCIf n1 n2 n3)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n1)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n;
assumption.
-
Case "
NNRCEither"%
string.
simpl.
rewrite (
IHn1 env1 env2).
destruct (@
nnrc_core_eval _ h env2 (
nnrc_ext_to_nnrc n1));
try reflexivity.
destruct (
d);
try reflexivity.
+
rewrite (
IHn2 ((
v,
d0) ::
env1) ((
v,
d0) ::
env2));
try reflexivity.
simpl.
intros x.
destruct (
equiv_dec x v);
try reflexivity.
*
intros Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCEither n1 v n2 v0 n3)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n2)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n.
apply nin_app_or in H0.
destruct H0.
apply (
not_in_remove_impl_not_in x v);
assumption.
+
rewrite (
IHn3 ((
v0,
d0) ::
env1) ((
v0,
d0) ::
env2));
try reflexivity.
simpl.
intros x.
destruct (
equiv_dec x v0);
try reflexivity.
*
intros Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCEither n1 v n2 v0 n3)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n3)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n.
apply nin_app_or in H0.
destruct H0.
apply (
not_in_remove_impl_not_in x v0);
assumption.
+
intros x Hx.
destruct (
in_dec string_eqdec x (
nnrc_free_vars (
NNRCEither n1 v n2 v0 n3)));
[
apply Henv_eq;
assumption | ].
assert (~
In x (
nnrc_free_vars n1)); [ |
contradiction ].
simpl in n.
apply nin_app_or in n.
destruct n;
assumption.
-
Case "
NNRCGroupBy"%
string.
simpl.
rewrite (
IHn env1 env2).
reflexivity.
+
intros x Hx.
apply Henv_eq.
simpl.
assumption.
Qed.
Lemma nnrc_ext_eval_equiv_env:
forall n,
forall env1 env2,
(
forall x,
lookup equiv_dec env1 x =
lookup equiv_dec env2 x) ->
forall h,
@
nnrc_ext_eval _ h env1 n = @
nnrc_ext_eval _ h env2 n.
Proof.
Lemma nnrc_no_free_vars_eval_equiv_env:
forall n,
forall env1 env2,
nnrc_free_vars n =
nil ->
forall h,
@
nnrc_ext_eval _ h env1 n = @
nnrc_ext_eval _ h env2 n.
Proof.
Lemma nnrc_ext_eval_single_context_var_uncons h env n v d:
lookup equiv_dec env v =
Some d ->
@
nnrc_ext_eval _ h env n = @
nnrc_ext_eval _ h ((
v,
d) ::
env)
n.
Proof.
intros.
apply nnrc_ext_eval_equiv_env.
intros x.
case (
string_eqdec x v).
+
Case "
x =
v"%
string.
intros Hx;
rewrite Hx in *;
clear Hx.
rewrite H.
simpl.
match_destr.
congruence.
+
Case "
x <>
v"%
string.
intros Hx.
simpl.
match_destr.
congruence.
Qed.
Lemma nnrc_ext_eval_single_context_var h env n v d:
(
forall x,
In x (
nnrc_free_vars n) ->
x =
v) ->
lookup equiv_dec env v =
Some d ->
@
nnrc_ext_eval _ h ((
v,
d) ::
nil)
n = @
nnrc_ext_eval _ h env n.
Proof.
Lemma nnrc_ext_eval_single_context_var_cons h env n v d:
(
forall x,
In x (
nnrc_free_vars n) ->
x =
v) ->
@
nnrc_ext_eval _ h ((
v,
d) ::
nil)
n = @
nnrc_ext_eval _ h ((
v,
d)::
env)
n.
Proof.
Lemma nnrc_ext_eval_single_context_var_cons_keepone h env n v d v1 d1:
(
forall x,
In x (
nnrc_free_vars n) ->
x =
v) ->
@
nnrc_ext_eval _ h ((
v,
d) :: (
v1,
d1) ::
nil)
n =
@
nnrc_ext_eval _ h ((
v,
d) :: (
v1,
d1) ::
env)
n.
Proof.
Lemma nnrc_ext_eval_single_context_var_two_cons h env n v1 d1 v2 d2 :
(
forall x,
In x (
nnrc_free_vars n) ->
x =
v1 \/
x =
v2) ->
@
nnrc_ext_eval _ h ((
v1,
d1) :: (
v2,
d2) ::
nil)
n =
@
nnrc_ext_eval _ h ((
v1,
d1) :: (
v2,
d2) ::
env)
n.
Proof.
Lemma nnrc_ext_eval_single_context_var_cons_rmap h env n v l:
(
forall x,
In x (
nnrc_free_vars n) ->
x =
v) ->
rmap (
fun d => @
nnrc_ext_eval _ h ((
v,
d) ::
nil)
n)
l =
rmap (
fun d => @
nnrc_ext_eval _ h ((
v,
d)::
env)
n)
l.
Proof.
Lemma nnrc_ext_eval_single_context_var_cons_keepone_rmap h env n v v1 d1 l:
(
forall x,
In x (
nnrc_free_vars n) ->
x =
v) ->
rmap (
fun d => @
nnrc_ext_eval _ h ((
v,
d) :: (
v1,
d1) ::
nil)
n)
l =
rmap (
fun d => @
nnrc_ext_eval _ h ((
v,
d) :: (
v1,
d1) ::
env)
n)
l.
Proof.
Lemma rmap_skip_free_var h v1 v2 d2 n l:
~
In v2 (
nnrc_free_vars n) ->
(
rmap (
fun d :
data => @
nnrc_ext_eval _ h ((
v1,
d) :: (
v2,
d2) ::
nil)
n)
l) =
(
rmap (
fun d :
data => @
nnrc_ext_eval _ h ((
v1,
d) ::
nil)
n)
l).
Proof.
Lemma nnrc_ext_eval_cons_subst_disjoint {
h:
list (
string*
string)}
e e'
env v d :
disjoint (
nnrc_bound_vars e) (
nnrc_free_vars e') ->
@
nnrc_ext_eval _ h env e' =
Some d ->
@
nnrc_ext_eval _ h ((
v,
d)::
env)
e = @
nnrc_ext_eval _ h env (
nnrc_subst e v e').
Proof.
Lemma nnrc_pick_name_neq_nfree sep renamer avoid v e :
v =/=
nnrc_pick_name sep renamer avoid v e ->
~
In (
nnrc_pick_name sep renamer avoid v e) (
nnrc_free_vars e).
Proof.
Lemma nnrc_ext_eval_cons_rename_pick h sep renamer avoid v e d env:
@
nnrc_ext_eval _ h ((
nnrc_pick_name sep renamer avoid v e,
d) ::
env)
(
nnrc_rename_lazy e v (
nnrc_pick_name sep renamer avoid v e)) =
@
nnrc_ext_eval _ h ((
v,
d) ::
env)
e.
Proof.
Theorem unshadow_ext_eval {
h:
list (
string*
string)}
sep renamer avoid e env :
@
nnrc_ext_eval _ h env (
unshadow sep renamer avoid e) = @
nnrc_ext_eval _ h env e.
Proof.
revert env.
generalize nnrc_ext_eval_cons_rename_pick;
intros Hpick.
induction e;
unfold nnrc_ext_eval in *;
simpl;
trivial;
intros;
try congruence.
-
rewrite IHe1.
match_destr.
rewrite Hpick.
trivial.
-
rewrite IHe1.
match_destr.
match_destr.
f_equal.
apply rmap_ext;
intros.
rewrite <-
IHe2.
apply Hpick.
-
rewrite IHe1,
IHe2,
IHe3;
trivial.
-
rewrite IHe1.
match_destr.
match_destr.
+
rewrite Hpick.
rewrite IHe2.
trivial.
+
rewrite Hpick.
rewrite IHe3.
trivial.
-
rewrite IHe.
reflexivity.
Qed.
Lemma nnrc_pick_name_id_nin_eq sep avoid v e :
~
In v (
nnrc_bound_vars e) ->
~
In v avoid ->
(
nnrc_pick_name sep id avoid v e) =
v.
Proof.
Lemma unshadow_id_idempotent sep renamer1 avoid (
e:
nnrc)
:
unshadow sep id avoid (
unshadow sep renamer1 avoid e) =
unshadow sep renamer1 avoid e.
Proof.
Definition nnrc_unshadow_sep := "$"%
string.
Definition unshadow_simpl :=
unshadow nnrc_unshadow_sep id.
Definition nnrc_substlist_subst (
substlist:
list (
var*
var)) (
e:
nnrc) :=
List.fold_left
(
fun e (
subst:
var *
var) =>
let (
x,
x') :=
subst in
nnrc_subst e x (
NNRCVar x'))
substlist e.
End NNRCShadow.