Require Export NuTree.
Definition NtlEq A n n' :=
forall t, Twr t -> t El [n] A <-> t El [n'] A.
Lemma ntl_eq_refl A n :
NtlEq A n n.
Proof.
intros t H1. reflexivity.
Qed.
Section Renaming.
(*
A Rho-Renaming of a nu-tree n is a permutation where all free names are fixed.
In this development we call it just Renaming.
*)
Definition Renaming n p :=
forall a, a el FN n -> p a = a.
Lemma renaming_sub a l p :
Renaming (Tr a l) p -> forall n, n el l -> Renaming n p.
Proof.
intros H1 n H2 b H3. rewrite H1; trivial. now apply (FN_in_sub a H3).
Qed.
Lemma renaming_sub' a n p :
Renaming (Nu a n) p -> p a = a -> Renaming n p.
Proof.
intros H1 H2 b H3. decide(b=a) as [->|H4]; try assumption.
rewrite H1; try reflexivity. simpl. auto.
Qed.
Lemma renaming_nil n p :
FN n = [] -> Renaming n p.
Proof.
intros H1 a H2. rewrite H1 in H2. auto.
Qed.
Lemma renaming_inverse p p' n :
Inv p p' -> Renaming n p -> Renaming n p'.
Proof.
intros H1 H2 a H3. rewrite <-(H2 a H3) at 1. apply H1.
Qed.
(*
A renaming is still a renaming after renaming the tree
*)
Lemma renaming_invariant n p :
Ntwr n -> Perm p -> Renaming n p -> Renaming (p *' n) p.
Proof.
intros H1 H2 H3.
assert(HP: Perm p) by assumption.
destruct H2 as [HP1 [p' HP2]].
destruct H1 as [a' l H5 | a' n H5]; intros c H4;
rewrite FN_equiv_shift with (p':=p') in H4; auto;
rewrite <-(perm_inv c (inv_comm HP2)) at 2;
rewrite <-(H3 (p' c) H4), (perm_inv c); auto.
Qed.
(*
Any free name is still free after renaming
*)
Lemma free_name_in_renaming a n p :
Ntwr n -> Perm p -> a el FN n -> Renaming n p -> a el FN (p *' n).
Proof.
intros H1 H2 H3 H4. assert(HP: Perm p) by assumption.
destruct H2 as [_ [p' H2]]. apply (renaming_inverse H2) in H4.
destruct H1 as [a' l H5| a' n H5]; rewrite (FN_equiv_shift) with (p':=p');auto; now rewrite H4.
Qed.
(*
Inverse direction of the previous lemma
Any free name was free before renaming
Proof uses previous lemma + inverse permutation
*)
Lemma free_name_in_renaming' a n p :
Ntwr n -> Perm p -> Renaming n p -> a el FN (p *' n) -> a el FN n.
Proof.
intros H1 H2 H3 H4. assert(HP: Perm p) by assumption.
destruct H2 as [HP1 [p' HP2]]. apply (free_name_in_renaming) with (p := p') in H4; auto.
- rewrite <-(nt_perm_apply_inv H1 (inv_comm HP2)) in H4; assumption.
- eauto.
- apply renaming_inverse with (p := p); try assumption. apply renaming_invariant; trivial.
Qed.
Lemma free_in_renaming a n p :
Ntwr n -> Perm p -> Renaming n p -> a el FN n <-> a el FN (p *' n).
Proof.
intros H1 H2 H3. split; eauto using free_name_in_renaming, free_name_in_renaming'.
Qed.
(*
If a transposition transposes two names that are not free, then it's a renaming.
*)
Lemma transp_renaming n a b :
Ntwr n -> ~ a el FN n -> ~b el FN n -> Renaming n (a$b).
Proof.
unfold Renaming, transp. intros. solve_dec.
Qed.
Lemma compose_renaming n p p' :
Ntwr n -> Perm p -> Perm p' -> Renaming n p -> Renaming n p' -> Renaming n (p**p').
Proof.
unfold Renaming, compose. intros H1 H2 H3 H4 H5 a H6. rewrite H4, H5; trivial. now rewrite H5.
Qed.
(*
Any renaming for a nu-tree is a renaming for a structurally similar nu-tree
*)
Lemma nt_str_renaming n n' p :
Ntwr n -> Ntwr n' -> NtStr n n' -> Renaming n p -> Renaming n' p.
Proof.
unfold Renaming. intros HW1 HW2 H1 H2 a H3. apply H2. now rewrite (nt_str_FN HW1 HW2 H1).
Qed.
Hint Resolve transp_renaming.
(*
The next four lemmas treat special cases when and which some names are free
*)
Lemma nu_FN n a b :
a el FN(a$b *' n) -> Ntwr n -> rk a = rk b -> b <> a -> b el FN(Nu a n).
Proof.
intros H1 H2 H3 H4. rewrite FN_equiv_shift in H1; eauto.
cbn. apply in_rem_iff. unfold transp in H1. split; trivial. now solve_dec.
Qed.
Lemma nu_FN' n a b c :
c el FN(a$b *' n) -> Ntwr n -> rk a = rk b -> a <> c -> b <> c -> c el FN(Nu a n).
Proof.
intros H1 H2 H3 H4 H5. rewrite FN_equiv_shift in H1; eauto.
cbn. apply in_rem_iff. split; auto. unfold transp in H1. now solve_dec.
Qed.
Lemma transp_FN n a b :
Ntwr n -> rk a = rk b -> a el FN n -> ~b el FN n -> b el FN (a $ b *' n).
Proof.
simpl. intros. rewrite FN_equiv_shift; auto. solve_dec.
Qed.
Lemma transp_FN' n a b c :
Ntwr n -> c el FN n -> rk a = rk b -> c <> a -> c <> b -> c el FN (a $ b *' n).
Proof.
intros. rewrite FN_equiv_shift with (p':=a$b); auto. solve_dec.
Qed.
(*
A renaming doesn't change the nu-tree language
*)
Fact ntl_renaming' n t A :
Ntwr n -> Twr t -> t El [n] A -> forall p, Perm p -> Renaming n p -> t El [p*'n] A.
Proof.
intros H1 H3 H4.
induction H4 as [A' l l' a H5 H6 H7| A' n t a b H4 H5 H6 H7 H8]; simpl; intros p HP H2.
- assert(H8: p a = a) by apply H2, tree_name_free. rewrite H8. constructor; try now rewrite map_length.
intros k H9. rewrite map_length in H9.
rewrite map_nth_indep; trivial. apply H7; trivial; try solve_wr_sub.
apply (renaming_sub H2), nth_In, H9.
- apply DNNu with (b := b); trivial.
+ change (~ b el FN (p *' (Nu a n))). now rewrite <-(free_in_renaming b H1 HP H2).
+ destruct HP as [HP _]. now rewrite <-(HP a).
+ inversion H1 as [|a' n' H9 [H10 H11]]. subst.
rewrite (@nt_swap_perm n H9 p ((p a$p b) ** p ** (a$b))); eauto.
* rewrite <-nt_assoc, nt_assoc3, nt_assoc; eauto. apply H8; auto.
-- apply perm_compose_perm; auto.
apply transp_perm. destruct HP as [HP _]. now rewrite <-(HP a).
-- intros c HC. solve_dec.
++ exfalso. apply H5. apply (nu_FN HC); eauto; congruence.
++ decide (p a = c); trivial. exfalso. apply H5.
enough (c el FN (Nu a n)) by now rewrite (H2 c).
apply (nu_FN' HC); eauto; congruence.
++ exfalso. apply H5. apply (nu_FN HC); eauto. congruence.
++ apply H2. apply (nu_FN' HC); eauto; congruence.
* intros c. solve_dec.
Qed.
(*
The otther direction of renaming is shown using previous fact + permutation inverse
*)
Fact ntl_renaming'' n t A :
Ntwr n -> Twr t -> forall p, Perm p -> Renaming n p -> t El [p*'n] A -> t El [n] A.
Proof.
intros H1 H2 p H3 H4 H5.
assert(HP1: Perm p) by assumption. destruct H3 as [HP2 [p' HP3]].
apply ntl_renaming' with (p := p') in H5; auto.
- rewrite <-(nt_perm_apply_inv) in H5; auto.
- exact (perm_inv_perm HP1 HP3).
- now apply renaming_inverse with (p := p), renaming_invariant.
Qed.
Theorem ntl_renaming n A :
Ntwr n -> forall p, Perm p -> Renaming n p -> NtlEq A n (p*'n).
Proof.
intros H1 p H2 H3. split; intros H5.
- apply ntl_renaming'; assumption.
- apply ntl_renaming'' with (p:=p); assumption.
Qed.
Corollary ntl_closed n A p :
Ntwr n -> Perm p -> FN n = [] -> NtlEq A n (p*'n).
Proof.
intros H1 H2 H3. apply ntl_renaming; auto using renaming_nil.
Qed.
Definition NtlRho n n' :=
exists p, Perm p /\ Renaming n p /\ p*'n = n'.
(*
Rho-equivalent nu-trees have the same language
*)
Corollary ntl_alpha_eq n n' A :
Ntwr n -> Ntwr n' -> NtlRho n n' -> NtlEq A n n'.
Proof.
intros H1 H2 [p [H3 [H4 H5]]]. rewrite <-H5. apply ntl_renaming; assumption.
Qed.
End Renaming.
(*
A Rho-Renaming of a nu-tree n is a permutation where all free names are fixed.
In this development we call it just Renaming.
*)
Definition Renaming n p :=
forall a, a el FN n -> p a = a.
Lemma renaming_sub a l p :
Renaming (Tr a l) p -> forall n, n el l -> Renaming n p.
Proof.
intros H1 n H2 b H3. rewrite H1; trivial. now apply (FN_in_sub a H3).
Qed.
Lemma renaming_sub' a n p :
Renaming (Nu a n) p -> p a = a -> Renaming n p.
Proof.
intros H1 H2 b H3. decide(b=a) as [->|H4]; try assumption.
rewrite H1; try reflexivity. simpl. auto.
Qed.
Lemma renaming_nil n p :
FN n = [] -> Renaming n p.
Proof.
intros H1 a H2. rewrite H1 in H2. auto.
Qed.
Lemma renaming_inverse p p' n :
Inv p p' -> Renaming n p -> Renaming n p'.
Proof.
intros H1 H2 a H3. rewrite <-(H2 a H3) at 1. apply H1.
Qed.
(*
A renaming is still a renaming after renaming the tree
*)
Lemma renaming_invariant n p :
Ntwr n -> Perm p -> Renaming n p -> Renaming (p *' n) p.
Proof.
intros H1 H2 H3.
assert(HP: Perm p) by assumption.
destruct H2 as [HP1 [p' HP2]].
destruct H1 as [a' l H5 | a' n H5]; intros c H4;
rewrite FN_equiv_shift with (p':=p') in H4; auto;
rewrite <-(perm_inv c (inv_comm HP2)) at 2;
rewrite <-(H3 (p' c) H4), (perm_inv c); auto.
Qed.
(*
Any free name is still free after renaming
*)
Lemma free_name_in_renaming a n p :
Ntwr n -> Perm p -> a el FN n -> Renaming n p -> a el FN (p *' n).
Proof.
intros H1 H2 H3 H4. assert(HP: Perm p) by assumption.
destruct H2 as [_ [p' H2]]. apply (renaming_inverse H2) in H4.
destruct H1 as [a' l H5| a' n H5]; rewrite (FN_equiv_shift) with (p':=p');auto; now rewrite H4.
Qed.
(*
Inverse direction of the previous lemma
Any free name was free before renaming
Proof uses previous lemma + inverse permutation
*)
Lemma free_name_in_renaming' a n p :
Ntwr n -> Perm p -> Renaming n p -> a el FN (p *' n) -> a el FN n.
Proof.
intros H1 H2 H3 H4. assert(HP: Perm p) by assumption.
destruct H2 as [HP1 [p' HP2]]. apply (free_name_in_renaming) with (p := p') in H4; auto.
- rewrite <-(nt_perm_apply_inv H1 (inv_comm HP2)) in H4; assumption.
- eauto.
- apply renaming_inverse with (p := p); try assumption. apply renaming_invariant; trivial.
Qed.
Lemma free_in_renaming a n p :
Ntwr n -> Perm p -> Renaming n p -> a el FN n <-> a el FN (p *' n).
Proof.
intros H1 H2 H3. split; eauto using free_name_in_renaming, free_name_in_renaming'.
Qed.
(*
If a transposition transposes two names that are not free, then it's a renaming.
*)
Lemma transp_renaming n a b :
Ntwr n -> ~ a el FN n -> ~b el FN n -> Renaming n (a$b).
Proof.
unfold Renaming, transp. intros. solve_dec.
Qed.
Lemma compose_renaming n p p' :
Ntwr n -> Perm p -> Perm p' -> Renaming n p -> Renaming n p' -> Renaming n (p**p').
Proof.
unfold Renaming, compose. intros H1 H2 H3 H4 H5 a H6. rewrite H4, H5; trivial. now rewrite H5.
Qed.
(*
Any renaming for a nu-tree is a renaming for a structurally similar nu-tree
*)
Lemma nt_str_renaming n n' p :
Ntwr n -> Ntwr n' -> NtStr n n' -> Renaming n p -> Renaming n' p.
Proof.
unfold Renaming. intros HW1 HW2 H1 H2 a H3. apply H2. now rewrite (nt_str_FN HW1 HW2 H1).
Qed.
Hint Resolve transp_renaming.
(*
The next four lemmas treat special cases when and which some names are free
*)
Lemma nu_FN n a b :
a el FN(a$b *' n) -> Ntwr n -> rk a = rk b -> b <> a -> b el FN(Nu a n).
Proof.
intros H1 H2 H3 H4. rewrite FN_equiv_shift in H1; eauto.
cbn. apply in_rem_iff. unfold transp in H1. split; trivial. now solve_dec.
Qed.
Lemma nu_FN' n a b c :
c el FN(a$b *' n) -> Ntwr n -> rk a = rk b -> a <> c -> b <> c -> c el FN(Nu a n).
Proof.
intros H1 H2 H3 H4 H5. rewrite FN_equiv_shift in H1; eauto.
cbn. apply in_rem_iff. split; auto. unfold transp in H1. now solve_dec.
Qed.
Lemma transp_FN n a b :
Ntwr n -> rk a = rk b -> a el FN n -> ~b el FN n -> b el FN (a $ b *' n).
Proof.
simpl. intros. rewrite FN_equiv_shift; auto. solve_dec.
Qed.
Lemma transp_FN' n a b c :
Ntwr n -> c el FN n -> rk a = rk b -> c <> a -> c <> b -> c el FN (a $ b *' n).
Proof.
intros. rewrite FN_equiv_shift with (p':=a$b); auto. solve_dec.
Qed.
(*
A renaming doesn't change the nu-tree language
*)
Fact ntl_renaming' n t A :
Ntwr n -> Twr t -> t El [n] A -> forall p, Perm p -> Renaming n p -> t El [p*'n] A.
Proof.
intros H1 H3 H4.
induction H4 as [A' l l' a H5 H6 H7| A' n t a b H4 H5 H6 H7 H8]; simpl; intros p HP H2.
- assert(H8: p a = a) by apply H2, tree_name_free. rewrite H8. constructor; try now rewrite map_length.
intros k H9. rewrite map_length in H9.
rewrite map_nth_indep; trivial. apply H7; trivial; try solve_wr_sub.
apply (renaming_sub H2), nth_In, H9.
- apply DNNu with (b := b); trivial.
+ change (~ b el FN (p *' (Nu a n))). now rewrite <-(free_in_renaming b H1 HP H2).
+ destruct HP as [HP _]. now rewrite <-(HP a).
+ inversion H1 as [|a' n' H9 [H10 H11]]. subst.
rewrite (@nt_swap_perm n H9 p ((p a$p b) ** p ** (a$b))); eauto.
* rewrite <-nt_assoc, nt_assoc3, nt_assoc; eauto. apply H8; auto.
-- apply perm_compose_perm; auto.
apply transp_perm. destruct HP as [HP _]. now rewrite <-(HP a).
-- intros c HC. solve_dec.
++ exfalso. apply H5. apply (nu_FN HC); eauto; congruence.
++ decide (p a = c); trivial. exfalso. apply H5.
enough (c el FN (Nu a n)) by now rewrite (H2 c).
apply (nu_FN' HC); eauto; congruence.
++ exfalso. apply H5. apply (nu_FN HC); eauto. congruence.
++ apply H2. apply (nu_FN' HC); eauto; congruence.
* intros c. solve_dec.
Qed.
(*
The otther direction of renaming is shown using previous fact + permutation inverse
*)
Fact ntl_renaming'' n t A :
Ntwr n -> Twr t -> forall p, Perm p -> Renaming n p -> t El [p*'n] A -> t El [n] A.
Proof.
intros H1 H2 p H3 H4 H5.
assert(HP1: Perm p) by assumption. destruct H3 as [HP2 [p' HP3]].
apply ntl_renaming' with (p := p') in H5; auto.
- rewrite <-(nt_perm_apply_inv) in H5; auto.
- exact (perm_inv_perm HP1 HP3).
- now apply renaming_inverse with (p := p), renaming_invariant.
Qed.
Theorem ntl_renaming n A :
Ntwr n -> forall p, Perm p -> Renaming n p -> NtlEq A n (p*'n).
Proof.
intros H1 p H2 H3. split; intros H5.
- apply ntl_renaming'; assumption.
- apply ntl_renaming'' with (p:=p); assumption.
Qed.
Corollary ntl_closed n A p :
Ntwr n -> Perm p -> FN n = [] -> NtlEq A n (p*'n).
Proof.
intros H1 H2 H3. apply ntl_renaming; auto using renaming_nil.
Qed.
Definition NtlRho n n' :=
exists p, Perm p /\ Renaming n p /\ p*'n = n'.
(*
Rho-equivalent nu-trees have the same language
*)
Corollary ntl_alpha_eq n n' A :
Ntwr n -> Ntwr n' -> NtlRho n n' -> NtlEq A n n'.
Proof.
intros H1 H2 [p [H3 [H4 H5]]]. rewrite <-H5. apply ntl_renaming; assumption.
Qed.
End Renaming.
Section NuIndep.
Variable n : NuTree.
Hypothesis HW1 : Ntwr n.
Lemma ntl_weakening A B c t :
Twr t -> t El [n] A -> A === (c::B) -> t El [n] B.
Proof.
intros HW2 H1. revert B c.
induction H1 as [A l l' a H1 H2 H3| A n t a b H1 H2 H3 H4 H5]; simpl.
- intros B c H4. constructor; trivial. intros k H7. apply H3 with (c:=c); try assumption; try solve_wr_sub.
rewrite H4. apply equi_swap.
- intros B c H6. apply DNNu with (b:=b); try assumption.
+ rewrite H6 in H1. auto.
+ inversion HW1. subst. apply H5 with (c:=c); auto. now rewrite equi_swap, <-H6.
Qed.
(*
If a name doesn't bind anything, we can ignore it.
*)
Lemma ntl_nu_ignore a A t :
Twr t -> t El [Nu a n] A -> ~ a el FN n -> t El [n] A.
Proof.
intros HW2. inversion 1; subst; intros.
apply ntl_renaming in H7; auto.
- apply ntl_weakening with (A:=b::A)(c:=b); auto.
- apply transp_renaming; try assumption. decide (b=a) as [|E1]; try now subst.
intros H8. now apply E1, bind_free_name with (n:=n).
Qed.
Lemma ntl_strengthening A B c t :
Twr t -> t El [n] A -> (c::A) === B -> ~ c el names t -> t El [n] B.
Proof.
intros HW2 HD. revert B c.
induction HD as [A l l' a H1 H2 H3| A n t a b H1 H2 H3 H4 H5]; simpl.
- intros B c H4 H5. constructor; trivial.
intros k H7. apply H3 with (c := c); auto; try solve_wr_sub.
+ rewrite <-H4. apply equi_swap.
+ intros H6. apply H5. right. apply concat_map_el. exists (nth k l' DTR).
split; try assumption. apply nth_In. congruence.
- intros B c H6 H7. inversion HW1. subst.
decide(b=c) as [E3|E3].
+ subst c. decide (b el FN n) as [E1|E1].
* apply (bind_free_name E1) in H2. subst b.
rewrite nt_swap_perm with (p':=id), nt_id in H4; auto.
contradict H7. apply ntl_name_in with (A:=a::A)(n:=n); assumption.
* decide (a el FN n) as [E2|E2].
-- contradict H7. apply ntl_name_in with (A:=b::A)(n:=a$b *'n); auto. now apply transp_FN.
-- destruct (fresh_name (b::B) (Nu a n) t (rk a)) as [f [HF1 [HF2 [HF3 HF4]]]].
simpl in *. apply DNNu with (b:=f), ntl_renaming; try apply transp_renaming; auto.
apply ntl_renaming with (p:=a$b); auto using transp_renaming.
apply H5 with (c:=f); auto. now rewrite <-H6.
+ apply DNNu with (b:=b); auto.
* rewrite <-H6. intros [H9|H9]; auto.
* apply H5 with (c:=c); auto. rewrite <-H6. apply equi_swap.
Qed.
(*
We can add a nu that doesn't bind anything.
We show that the newly added nu can be instantiated by
a fresh name and that won't change the nu-tree language
*)
Lemma ntl_nu_add A a t :
Twr t -> t El [n] A -> ~ a el FN n -> t El [Nu a n] A.
Proof.
intros HW2 HD H1.
destruct (fresh_name A (Nu a n) t (rk a)) as [c [HF1 [HF2 [HF3 HF4]]]].
simpl in *. apply DNNu with (b:=c); try apply free_sub_not; try apply freshness; auto.
apply ntl_renaming; auto.
- apply transp_renaming; auto.
- apply ntl_strengthening with (A:=A)(c:=c); auto.
Qed.
Theorem ntl_nu_indep A a :
~ a el FN n -> NtlEq A n (Nu a n).
Proof.
intros H1 H2. split; eauto using ntl_nu_add, ntl_nu_ignore.
Qed.
Hint Resolve ntl_nu_indep ntl_nu_add ntl_nu_ignore.
End NuIndep.
Variable n : NuTree.
Hypothesis HW1 : Ntwr n.
Lemma ntl_weakening A B c t :
Twr t -> t El [n] A -> A === (c::B) -> t El [n] B.
Proof.
intros HW2 H1. revert B c.
induction H1 as [A l l' a H1 H2 H3| A n t a b H1 H2 H3 H4 H5]; simpl.
- intros B c H4. constructor; trivial. intros k H7. apply H3 with (c:=c); try assumption; try solve_wr_sub.
rewrite H4. apply equi_swap.
- intros B c H6. apply DNNu with (b:=b); try assumption.
+ rewrite H6 in H1. auto.
+ inversion HW1. subst. apply H5 with (c:=c); auto. now rewrite equi_swap, <-H6.
Qed.
(*
If a name doesn't bind anything, we can ignore it.
*)
Lemma ntl_nu_ignore a A t :
Twr t -> t El [Nu a n] A -> ~ a el FN n -> t El [n] A.
Proof.
intros HW2. inversion 1; subst; intros.
apply ntl_renaming in H7; auto.
- apply ntl_weakening with (A:=b::A)(c:=b); auto.
- apply transp_renaming; try assumption. decide (b=a) as [|E1]; try now subst.
intros H8. now apply E1, bind_free_name with (n:=n).
Qed.
Lemma ntl_strengthening A B c t :
Twr t -> t El [n] A -> (c::A) === B -> ~ c el names t -> t El [n] B.
Proof.
intros HW2 HD. revert B c.
induction HD as [A l l' a H1 H2 H3| A n t a b H1 H2 H3 H4 H5]; simpl.
- intros B c H4 H5. constructor; trivial.
intros k H7. apply H3 with (c := c); auto; try solve_wr_sub.
+ rewrite <-H4. apply equi_swap.
+ intros H6. apply H5. right. apply concat_map_el. exists (nth k l' DTR).
split; try assumption. apply nth_In. congruence.
- intros B c H6 H7. inversion HW1. subst.
decide(b=c) as [E3|E3].
+ subst c. decide (b el FN n) as [E1|E1].
* apply (bind_free_name E1) in H2. subst b.
rewrite nt_swap_perm with (p':=id), nt_id in H4; auto.
contradict H7. apply ntl_name_in with (A:=a::A)(n:=n); assumption.
* decide (a el FN n) as [E2|E2].
-- contradict H7. apply ntl_name_in with (A:=b::A)(n:=a$b *'n); auto. now apply transp_FN.
-- destruct (fresh_name (b::B) (Nu a n) t (rk a)) as [f [HF1 [HF2 [HF3 HF4]]]].
simpl in *. apply DNNu with (b:=f), ntl_renaming; try apply transp_renaming; auto.
apply ntl_renaming with (p:=a$b); auto using transp_renaming.
apply H5 with (c:=f); auto. now rewrite <-H6.
+ apply DNNu with (b:=b); auto.
* rewrite <-H6. intros [H9|H9]; auto.
* apply H5 with (c:=c); auto. rewrite <-H6. apply equi_swap.
Qed.
(*
We can add a nu that doesn't bind anything.
We show that the newly added nu can be instantiated by
a fresh name and that won't change the nu-tree language
*)
Lemma ntl_nu_add A a t :
Twr t -> t El [n] A -> ~ a el FN n -> t El [Nu a n] A.
Proof.
intros HW2 HD H1.
destruct (fresh_name A (Nu a n) t (rk a)) as [c [HF1 [HF2 [HF3 HF4]]]].
simpl in *. apply DNNu with (b:=c); try apply free_sub_not; try apply freshness; auto.
apply ntl_renaming; auto.
- apply transp_renaming; auto.
- apply ntl_strengthening with (A:=A)(c:=c); auto.
Qed.
Theorem ntl_nu_indep A a :
~ a el FN n -> NtlEq A n (Nu a n).
Proof.
intros H1 H2. split; eauto using ntl_nu_add, ntl_nu_ignore.
Qed.
Hint Resolve ntl_nu_indep ntl_nu_add ntl_nu_ignore.
End NuIndep.
Section NuRename.
Variable n : NuTree.
Variable A : list Name.
Hypothesis HW1 : Ntwr n.
Fact ntl_nu_rename_1 a b t :
Twr t -> t El [Nu a n] A -> rk a = rk b -> ~ b el FN (Nu a n) -> t El [a$b *' Nu a n] A.
Proof.
intros HW2 H1 H2 H3.
apply ntl_renaming; auto. apply transp_renaming; simpl; auto.
Qed.
Fact ntl_nu_rename_2 a b t :
Twr t -> rk a = rk b -> ~ b el FN (Nu a n) -> t El [a$b *' Nu a n] A -> t El [Nu a n] A.
Proof.
intros HW2 H1 H2 H3.
apply ntl_renaming in H3; auto. apply transp_renaming; simpl; auto.
Qed.
Corollary ntl_nu_rename a b :
rk a = rk b -> ~ b el FN (Nu a n) -> NtlEq A (Nu a n) (a$b *' Nu a n).
Proof.
intros H1 H2 H3. split; intros H4.
- now apply ntl_nu_rename_1.
- now apply ntl_nu_rename_2 with (b:=b).
Qed.
End NuRename.
Variable n : NuTree.
Variable A : list Name.
Hypothesis HW1 : Ntwr n.
Fact ntl_nu_rename_1 a b t :
Twr t -> t El [Nu a n] A -> rk a = rk b -> ~ b el FN (Nu a n) -> t El [a$b *' Nu a n] A.
Proof.
intros HW2 H1 H2 H3.
apply ntl_renaming; auto. apply transp_renaming; simpl; auto.
Qed.
Fact ntl_nu_rename_2 a b t :
Twr t -> rk a = rk b -> ~ b el FN (Nu a n) -> t El [a$b *' Nu a n] A -> t El [Nu a n] A.
Proof.
intros HW2 H1 H2 H3.
apply ntl_renaming in H3; auto. apply transp_renaming; simpl; auto.
Qed.
Corollary ntl_nu_rename a b :
rk a = rk b -> ~ b el FN (Nu a n) -> NtlEq A (Nu a n) (a$b *' Nu a n).
Proof.
intros H1 H2 H3. split; intros H4.
- now apply ntl_nu_rename_1.
- now apply ntl_nu_rename_2 with (b:=b).
Qed.
End NuRename.
Section NuSwap.
Variable n : NuTree.
Variable A : list Name.
Hypothesis HW1 : Ntwr n.
(*
Technical lemma showing that the free names below two bindings stay
the same when the bindings are instantiated in different order.
Only needed in the ntl_nu_swap fact.
*)
Lemma nu_swap_FN a b c d :
Ntwr n -> ~ c el FN (Nu a (Nu b n)) -> ~ d el FN (Nu ((a $ c) b) (a $ c *' n)) -> rk a = rk c-> rk b = rk d -> c<>d -> a<>b -> ~ c el FN (Nu ((b $ d) a) (b $ d *' n)).
Proof.
intros H1 H2 H3 H4 H5 H6 H7. simpl. rewrite in_rem_iff, FN_equiv_shift with (p':=b$d); auto; try (apply transp_perm; solve_dec).
intros [H8 H9]. simpl in *.
repeat rewrite in_rem_iff in H2.
repeat rewrite in_rem_iff, FN_equiv_shift in H3; auto.
unfold transp in *. solve_dec; auto.
Qed.
Fact ntl_nu_swap' a b t :
Twr t -> t El [Nu a (Nu b n)] A -> t El [Nu b (Nu a n)] A.
Proof.
intros HW2 H3.
inversion H3 as [| A' n' t' a' c H4 H5 H6 H7 H8 [H9 H10] H11].
simpl in H7. subst.
inversion H7 as [| A' n' t' b' d H8 H9 H10 H11 H12 [H13 H14] H15].
subst. rewrite <-nt_assoc in H11; try assumption.
assert(H12: c <> d).
{ intros H12. subst. now apply H8. }
decide (a=b) as [ES|ES]; try now subst.
apply DNNu with (b:=d); auto.
- simpl. intros [[H13 H14] % in_rem_iff H15] % in_rem_iff. apply H9.
apply in_rem_iff; fold FN. split.
+ apply transp_FN'; auto.
+ apply transp_diff; congruence.
- rewrite <-H10. solve_dec.
- simpl. unfold transp in H10.
apply DNNu with (b:=c); simpl; auto.
+ apply nu_swap_FN; auto. solve_dec.
+ now solve_dec.
+ rewrite nt_swap_perm'' with (p'':= (a$c)b$d ** a$c); auto using transp_chain'.
apply ntl_swap_list with (A:=d::c::A); auto. apply equi_swap.
Qed.
(*
Showing one direction of a "swapping" lemma gives you a proof for both directions.
*)
Theorem ntl_nu_swap a b :
NtlEq A (Nu a (Nu b n)) (Nu b (Nu a n)).
Proof.
split; intros; apply ntl_nu_swap'; assumption.
Qed.
End NuSwap.
Variable n : NuTree.
Variable A : list Name.
Hypothesis HW1 : Ntwr n.
(*
Technical lemma showing that the free names below two bindings stay
the same when the bindings are instantiated in different order.
Only needed in the ntl_nu_swap fact.
*)
Lemma nu_swap_FN a b c d :
Ntwr n -> ~ c el FN (Nu a (Nu b n)) -> ~ d el FN (Nu ((a $ c) b) (a $ c *' n)) -> rk a = rk c-> rk b = rk d -> c<>d -> a<>b -> ~ c el FN (Nu ((b $ d) a) (b $ d *' n)).
Proof.
intros H1 H2 H3 H4 H5 H6 H7. simpl. rewrite in_rem_iff, FN_equiv_shift with (p':=b$d); auto; try (apply transp_perm; solve_dec).
intros [H8 H9]. simpl in *.
repeat rewrite in_rem_iff in H2.
repeat rewrite in_rem_iff, FN_equiv_shift in H3; auto.
unfold transp in *. solve_dec; auto.
Qed.
Fact ntl_nu_swap' a b t :
Twr t -> t El [Nu a (Nu b n)] A -> t El [Nu b (Nu a n)] A.
Proof.
intros HW2 H3.
inversion H3 as [| A' n' t' a' c H4 H5 H6 H7 H8 [H9 H10] H11].
simpl in H7. subst.
inversion H7 as [| A' n' t' b' d H8 H9 H10 H11 H12 [H13 H14] H15].
subst. rewrite <-nt_assoc in H11; try assumption.
assert(H12: c <> d).
{ intros H12. subst. now apply H8. }
decide (a=b) as [ES|ES]; try now subst.
apply DNNu with (b:=d); auto.
- simpl. intros [[H13 H14] % in_rem_iff H15] % in_rem_iff. apply H9.
apply in_rem_iff; fold FN. split.
+ apply transp_FN'; auto.
+ apply transp_diff; congruence.
- rewrite <-H10. solve_dec.
- simpl. unfold transp in H10.
apply DNNu with (b:=c); simpl; auto.
+ apply nu_swap_FN; auto. solve_dec.
+ now solve_dec.
+ rewrite nt_swap_perm'' with (p'':= (a$c)b$d ** a$c); auto using transp_chain'.
apply ntl_swap_list with (A:=d::c::A); auto. apply equi_swap.
Qed.
(*
Showing one direction of a "swapping" lemma gives you a proof for both directions.
*)
Theorem ntl_nu_swap a b :
NtlEq A (Nu a (Nu b n)) (Nu b (Nu a n)).
Proof.
split; intros; apply ntl_nu_swap'; assumption.
Qed.
End NuSwap.
Section NuPush.
(*
The list only matters when instantiating nus.
If there are no nus in the nu-tree, then the list doesn't matter.
*)
Lemma ntl_pure_list n A B t :
NoNus n -> t El [n] A -> t El [n] B.
Proof.
intros H1 H2. revert B; induction H2; intros B; inversion H1; subst.
constructor; trivial. intros k H5. apply H2; auto.
Qed.
(*
If there are no nus of rank k in the tree, then we can add any name of rank k to the list.
*)
Lemma ntl_nusk_list n A B t c k :
NoNusk k n -> Ntwr n -> t El [n] A -> B === (c::A) -> rk c = k -> t El [n] B.
Proof.
intros H1 HW H2. revert B; induction H2 as [A l l' a H2 H3 H4| A n t a b H2 H3 H4 H5 H6]; intros B H7 H8; inversion H1; subst.
- constructor; trivial. intros k H8. apply H4; auto; try solve_wr_sub. rewrite H7. apply equi_swap.
- apply DNNu with (b:=b); auto.
+ rewrite H7. simpl. intros [|]; subst; auto.
+ inversion HW. apply H6; auto.
* apply no_nusk_equiv; auto.
* rewrite H7. apply equi_swap.
Qed.
(*
The next three lemmas treat certain cases of freshness conditions
that need to be considered when pushing nu-bindings
*)
Lemma FN_nu_sub a b c n nl :
~c el FN (Nu a (Tr b nl)) -> n el nl -> ~c el FN (Nu a n).
Proof.
simpl. intros.
rewrite in_rem_iff. intros [H14 H15].
apply H, in_rem_iff. split; trivial.
right. apply concat_map_el. exists n. now split.
Qed.
Lemma FN_sub_other a b c n nl :
~c el FN (Nu a (Tr b nl)) -> n el nl -> ~ a el FN n -> ~ c el FN n.
Proof.
simpl. intros H1 H2 H3 H4. apply H1. apply in_rem_iff. split.
- right. apply concat_map_el. now exists n.
- intros H5. now subst c.
Qed.
Lemma FN_sub_incl a b c n nl k k' A :
k < |nl| -> k' < |nl| -> k <> k' -> (filter (fun x => Dec(~x el b::A)) (FN (Nu a (Tr b (rep_nth k nl n))))) <<= FN (Nu a n) -> ~ a el FN (nth k' nl DNT) -> ~ c el (FN (Nu a n)) -> ~c el b::A -> ~ c el FN (nth k' nl DNT).
Proof.
intros HL1 HL2 HK H1 H2 H3 H4 H5.
apply H3, H1. simpl. apply in_filter_iff. split; auto.
apply in_rem_iff. split; try congruence.
right. apply concat_map_el. exists (nth k' nl DNT).
split; trivial. apply rep_nth_el'; assumption.
Qed.
Fact ntl_nu_push' a b nl t A k :
Ntwr (Tr b nl) -> Twr t ->
a <> b -> k < |nl| ->
(forall k', k' < |nl| -> k <> k' -> ~ a el FN (nth k' nl DNT)) ->
t El [Nu a (Tr b nl)] A ->
t El [Tr b (rep_nth k nl (Nu a (nth k nl DNT)))] A.
Proof.
intros HW1 HW2 H2 H3 H5 H1.
inversion H1 as [| A' n' t' a' c H6 H7 H8 H9 H10 [H11 H12] H13]. subst.
simpl in H9.
inversion H9 as [A' nl' tl' a' H10 H11 H12 [H13 H14] H15 |]. subst.
assert(HA: b = (a$c)b). {
solve_dec. contradict H7. simpl. apply in_rem_iff. split; auto.
}
rewrite <-HA, map_length in *. inversion HW1. subst.
constructor; try now apply rep_nth_len'. rewrite rep_nth_len. intros k' H13.
specialize(H11 k' H13).
- decide (k=k') as [E1|E1].
+ subst k'. rewrite rep_nth_exact; trivial. unfold transp in HA.
apply DNNu with (b:=c); trivial; simpl in *.
* solve_dec. auto.
* apply FN_nu_sub with (b:=b)(nl:=nl); auto.
* rewrite map_nth_indep in H11; trivial.
apply ntl_swap_list with (A:=b::c::A); auto using equi_swap.
+ apply ntl_weakening with (B:=b::A)(c:=c) in H11; try apply equi_swap; try solve_wr_sub; try rewrite map_nth_indep; auto.
rewrite rep_nth_indep; trivial. rewrite map_nth_indep in H11; trivial.
apply ntl_renaming in H11; auto; try solve_wr_sub.
apply transp_renaming; auto; try solve_wr_sub.
apply FN_sub_other with (a:=a)(b:=b)(nl:=nl); auto.
Qed.
(*
This direction needs more assumptions because of the freshness conditions
*)
Fact ntl_nu_push'' a b nl n t A k :
Ntwr (Tr b nl) -> Twr t ->
a <> b ->
k < |nl| -> nth k nl DNT = (Nu a n) ->
(forall k', k' < |nl| -> k <> k' -> ~ a el FN (nth k' nl DNT)) ->
(forall k', k' < |nl| -> k <> k' -> NoNusk (rk a) (nth k' nl DNT)) ->
(filter (fun x => Dec (~ x el b::A)) (FN (Nu a (Tr b (rep_nth k nl n))))) <<= FN (Nu a n) ->
t El [Tr b nl] A ->
t El [Nu a (Tr b (rep_nth k nl n))] A.
Proof.
intros HW1 HW2 H2 H3 H4 H6 HT HF H1.
inversion H1 as [A' nl' tl' a' H7 H8 H9 [H10 H11] H12 |]. subst.
assert(HN : nth k tl' DTR El [nth k nl DNT] b :: A) by now apply H8.
rewrite H4 in HN.
inversion HN as [| A' n' t' a' c H9 H10 H11 H12 H13 [H14 H15] H16]. subst.
assert(HB: b = (a$c)b).
{ solve_dec. contradict H9. now left. }
apply DNNu with (b:=c); auto.
- intros H13.
apply H10, HF, in_filter_iff. split; auto.
- simpl. rewrite <-HB in *. constructor; rewrite map_length, rep_nth_len; trivial.
intros k' H13.
rewrite nth_indep with (d':=a$c*'DNT); try now rewrite map_length, rep_nth_len.
rewrite map_nth. decide (k=k') as [E1|E1].
+ subst k'. rewrite rep_nth_exact; trivial. apply ntl_swap_list with (A:=c::b::A); auto using equi_swap.
+ rewrite rep_nth_indep; trivial.
apply ntl_renaming; auto; try solve_wr_sub.
* apply transp_renaming; auto; try solve_wr_sub.
apply FN_sub_incl with (a:=a)(b:=b)(n:=n)(k:=k)(A:=A); auto.
* apply ntl_nusk_list with (A:=b::A)(c:=c)(k:=rk a); auto using equi_swap; try solve_wr_sub.
Qed.
Theorem ntl_nu_push a b nl n A k :
Ntwr (Tr b nl) ->
a <> b -> k < |nl| ->
nth k nl DNT = (Nu a n) ->
(forall k', k' < |nl| -> k <> k' -> ~ a el FN (nth k' nl DNT)) ->
(forall k', k' < |nl| -> k <> k' -> NoNusk (rk a) (nth k' nl DNT)) ->
(filter (fun x => Dec (~ x el b::A)) (FN (Nu a (Tr b (rep_nth k nl n))))) <<= FN (Nu a n) ->
NtlEq A (Tr b nl) (Nu a (Tr b (rep_nth k nl n))).
Proof.
intros. intros t H6. split.
- now apply ntl_nu_push''; trivial.
- rewrite <-rep_nth_id with (X:=NuTree)(k:=k)(l:=nl)(xd:=DNT) at 2; trivial.
rewrite H2. intros H7.
replace (rep_nth k nl (Nu a n)) with
(rep_nth k (rep_nth k nl n) (Nu a (nth k (rep_nth k nl (n)) DNT))).
+ apply ntl_nu_push'; auto; try now rewrite rep_nth_len.
* inversion H. subst. constructor; try now rewrite rep_nth_len.
intros n' [H12 |H12] % rep_nth_el_or; auto. subst.
specialize(H10 (nth k nl DNT) (nth_In nl DNT H1)).
rewrite H2 in H10. now inversion H10.
* intros k'. rewrite rep_nth_len. intros H8 H9 H10. apply (H3 k'); trivial.
now rewrite rep_nth_indep in H10.
+ rewrite rep_nth_exact, rep_nth_overwrite; trivial.
Qed.
End NuPush.