UniAna.disj.TeqPaths
Require Export DiamondIncl CncLoop.
Require Import Lia LastCommon.
Lemma only_inner_heads_tag_prefix `(C : redCFG) p i q j l
(Hdep : | i | = depth p)
(Hpath : TPath (p, i) (q, j) l)
(Hnhead : forall (h' : Lab) (k' : Tag), (h',k') ∈ tl (rev l) -> loop_contains h' q -> False)
(Hdeqq : forall (h' : Lab) (k' : Tag), (h',k') ∈ l -> deq_loop h' q)
: Prefix j i.
Proof.
clear - Hpath Hnhead Hdeqq Hdep.
remember (l) as l' in Hpath.
assert (Postfix l' l) as Hpost by (rewrite Heql';econstructor;eauto).
assert ((p,i) ∈ l') as Hel.
{ (rewrite Heql';eapply path_contains_back;subst;eauto). }
remember p as p'. remember i as i'. rewrite Heqp' in Hpath. rewrite Heqi' in Hpath.
rewrite Heqp' in Hdep. rewrite Heqi' in Hdep.
clear Heql' Heqp' Heqi'.
revert p' i' Hel p i Hpath Hdep.
rinduction l'.
- contradiction.
- eapply In_rcons in Hel. destruct Hel.
+ subst a.
specialize (rcons_destruct l0) as Hl0. destruct Hl0;[|destructH];subst l0.
* cbn in *.
inversion Hpath;subst. 2: { inversion H4. }
destruct l;[inversion Hpost;congruence'|]; eapply postfix_hd_eq in Hpost;
inversion Hpost;subst;cbn.
econstructor;auto.
* destruct a.
unfold TPath in Hpath.
assert ((p',i') ∈ l) as Helpi.
{ eapply postfix_incl;eauto. }
replace i' with (snd (p',i')) by (cbn;auto).
path_simpl' Hpath. cbn. copy Hpath Hpath'.
eapply path_nlrcons_edge in Hpath.
exploit' H.
1: { eapply postfix_step_left;eauto. }
specialize (H e t). exploit' H. specialize (H e t). exploit H.
1: eapply path_rcons_rinv;eauto.
1: eapply tcfg_edge_depth_iff in Hpath;eapply Hpath;eauto.
eapply tcfg_edge_destruct in Hpath as Q.
assert ((e,t) ∈ l) as Helet.
{ eapply postfix_incl;eauto. }
destruct Q as [Q|[Q|[Q|Q]]]. all: subst.
-- eauto. (* normal *)
-- inversion H;subst. (* entry *)
++ exfalso.
specialize (Hdeqq p i). exploit Hdeqq.
eapply deq_loop_depth in Hdeqq.
assert (|i| < |0 :: i|) as Q by (cbn;lia). clear Helet.
eapply tag_depth_unroot in Hpath';eauto. lia.
++ auto.
-- inversion H. (* back_edge *)
++ subst.
destruct i. 1:cbn;econstructor.
exfalso.
eapply Hnhead.
** eapply postfix_rev_prefix in Hpost.
rewrite rev_rcons in Hpost.
eapply prefix_tl in Hpost.
eapply prefix_incl;eauto. rewrite rev_rcons. left. reflexivity.
** specialize (tag_back_edge_iff Hpath) as [Q _]. exploit Q;eauto.
eapply deq_loop_head_loop_contains.
--- eapply deq_loop_depth_eq.
+++ eapply Hdeqq;eauto.
+++ eapply tag_depth_unroot in Hpath';eauto. cbn in Hpath',Hdep.
eapply back_edge_eq_loop in Q. rewrite <-Q. lia.
--- exists p;eauto.
++ subst. destruct i.
** cbn in H0. congruence.
** inversion H0. subst. econstructor. eauto.
-- clear - H;destruct i;cbn in *;[auto|]. inversion H;subst;econstructor;auto.
+ destruct l0;[cbn in *;contradiction|].
unfold TPath in Hpath. path_simpl' Hpath. cbn in Hpath. path_simpl' Hpath.
eapply tag_depth_unroot in Hpath as Hdepq;eauto.
eapply path_rcons_inv in Hpath. destructH. destruct p0.
eapply H;eauto.
* eapply postfix_step_left;eauto.
* eapply tag_depth_unroot2 in Hpath;eauto.
Qed.
Lemma teq_l_len1 `(T : TeqPaths)
: | l1 | = depth u1.
Proof.
destruct T.
eapply tag_depth_unroot2 in Tpath1;eauto.
Qed.
Lemma teq_l_len2 `(T : TeqPaths)
: | l2 | = depth u2.
Proof.
destruct T.
eapply tag_depth_unroot2 in Tpath2;eauto;rewrite <-Tjj_len;rewrite <-Tloop;eassumption.
Qed.
Hint Resolve teq_l_len1 teq_l_len2 : teq.
Lemma teq_root_all_nil1 `(T : TeqPaths)
(Hin : root ∈ (q1 :: map fst r1))
: u1 = root /\ l1 = [] /\ j1 = [] /\ j2 = [] /\ depth q1 = 0 /\ forall x, deq_loop x q1.
Proof.
assert (u1 = root) as Hroot.
{ destruct T. clear - Tpath1 Hin.
revert q1 j1 Tpath1 Hin.
induction r1;cbn in *;intros.
- eapply path_single in Tpath1. destructH. inv Tpath0. destruct Hin;[|contradiction]. subst;auto.
- inv_path Tpath1. destruct a. eapply IHr1. 1: eapply H.
destruct Hin.
+ subst q1. eapply tcfg_edge_edge in H0. eapply root_no_pred in H0. contradiction.
+ destruct H1. cbn in H1. subst e.
* destruct r1;[left;auto|]. inv_path H. destruct p.
eapply tcfg_edge_edge in H2. eapply root_no_pred in H2. contradiction.
* right;auto.
}
subst u1. split;auto.
assert (l1 = []) as Hnil1.
{
eapply teq_l_len1 in T. rewrite depth_root in T. destruct l1;[|cbn in T;congruence]. reflexivity.
}
split;auto.
assert (j1 = []) as Hnilj1.
{ destruct T. destruct Tlj_eq1;subst;auto. destruct H. congruence. }
split;auto.
split.
- destruct T. subst l1 j1. cbn in Tjj_len. destruct j2;[|cbn in Tjj_len;congruence]. auto.
- destruct T. subst j1. cbn in Tj_len. split;eauto.
intros x y Hy.
symmetry in Tj_len. eapply depth_zero_iff in Tj_len;eauto. contradiction.
Qed.
Lemma teq_root_all_nil2 `(T : TeqPaths)
(Hin : root ∈ (q2 :: map fst r2))
: u2 = root /\ l2 = [] /\ j1 = [] /\ j2 = [] /\ depth q1 = 0 /\ forall x, deq_loop x q1.
Proof.
assert (u2 = root) as Hroot.
{ destruct T. clear - Tpath2 Hin.
revert q2 j2 Tpath2 Hin.
induction r2;cbn in *;intros.
- eapply path_single in Tpath2. destructH. inv Tpath0. destruct Hin;[|contradiction]. subst;auto.
- inv_path Tpath2. destruct a. eapply IHr2. 1: eapply H.
destruct Hin.
+ subst q2. eapply tcfg_edge_edge in H0. eapply root_no_pred in H0. contradiction.
+ destruct H1. cbn in H1. subst e.
* destruct r2;[left;auto|]. inv_path H. destruct p.
eapply tcfg_edge_edge in H2. eapply root_no_pred in H2. contradiction.
* right;auto.
}
subst u2. split;auto.
assert (l2 = []) as Hnil2.
{
eapply teq_l_len2 in T. rewrite depth_root in T. destruct l2;[|cbn in T;congruence]. reflexivity.
}
split;auto.
assert (j1 = []) as Hnilj2.
{ destruct T. destruct Tlj_eq2;subst;auto. destruct H.
- destruct H. congruence.
- eapply loop_contains_loop_head in H. eapply loop_contains_self in H. eapply root_no_loop in H.
contradiction.
}
split;auto.
split.
- destruct T. subst l2 j1. cbn in Tjj_len. destruct j2;[|cbn in Tjj_len;congruence]. auto.
- destruct T. subst j1. cbn in Tj_len. split;eauto.
intros x y Hy.
symmetry in Tj_len. eapply depth_zero_iff in Tj_len;eauto. contradiction.
Qed.
Section teq.
Context `(T : TeqPaths).
Lemma teq_r1_incl_head_q : forall x, x ∈ (q1 :: map fst r1) -> deq_loop x q1.
Proof.
destruct T. destructH.
intros.
eapply spath_r1_incl_head_q in TS0;eauto.
eapply postfix_map with (f:=fst) in TS2.
eapply postfix_incl;eauto.
Qed.
Lemma teq_r2_incl_head_q : forall x, x ∈ (q2 :: map fst r2) -> deq_loop x q1.
Proof.
destruct T. destructH.
intros.
eapply spath_r2_incl_head_q in TS0;eauto.
eapply postfix_map with (f:=fst) in TS3.
eapply postfix_incl;eauto.
Qed.
Lemma teq_u1_deq_q
: deq_loop u1 q1.
Proof.
eapply teq_r1_incl_head_q;eauto.
destruct T.
inv_path Tpath1. 1:left;eauto.
eapply path_contains_back in H.
fold (fst (u1,l1)). right.
eapply in_map;eauto.
Qed.
Lemma teq_u2_deq_q
: deq_loop u2 q1.
Proof.
eapply teq_r2_incl_head_q;eauto.
destruct T.
inv_path Tpath2. 1:left;eauto.
eapply path_contains_back in H.
fold (fst (u2,l2)). right.
eapply in_map;eauto.
Qed.
End teq.
Lemma jj_tagle `(T : TeqPaths)
: j1 ⊴ j2.
Proof.
copy T T'.
destruct T.
assert (loop_contains u2 q1 -> j1 ⊴ j2) as Hncont.
{
intro Q.
eapply tagle_or in Tjj_len;destruct Tjj_len;[auto|exfalso].
destructH.
eapply SplitPaths_sym in TS0.
eapply spath_no_back in TS0;eauto.
+ eapply TS0. rewrite <-Tloop. eapply Q.
+ eapply postfix_map with (f:=fst) in TS3.
eapply postfix_incl;eauto. eapply TPath_CPath in Tpath2. cbn in Tpath2.
eapply path_contains_back in Tpath2. eauto.
}
decide (loop_contains u2 q1) as [Hcont|HNcont];[eauto|].
destruct Tlj_eq2 as [Q|[Q|Q]].
- subst l2. eapply tagle_monotone with (n:=depth q1) in Tpath2.
+ rewrite take_r_geq in Tpath2;[|lia].
rewrite take_r_geq in Tpath2;[|lia].
eassumption.
+ eapply tag_depth_unroot2;eauto. rewrite <-Tloop. rewrite <-Tjj_len. assumption.
+ eapply teq_u2_deq_q;eauto.
+ rewrite Tloop. reflexivity.
+ reflexivity.
- destructH. subst l2.
eapply tcfg_enroot in Tpath2 as Hroot.
2: { eapply tag_depth_unroot2;eauto. rewrite <-Tloop. rewrite <-Tjj_len. assumption. }
destructH.
destruct t';cbn in Hroot.
{ exfalso. rewrite <-app_nil_end in Hroot.
destr_r' r2;subst.
- eapply path_single in Tpath2. inv Tpath2. eapply path_single in Hroot. inv Hroot. inv H.
cbn in Tjj_len. lia.
- rewrite app_comm_cons in Hroot. eapply path_back in Hroot. subst x.
rewrite app_comm_cons in Tpath2. eapply path_back in Tpath2. inv Tpath2.
}
destruct c.
assert (TPath (e, t) (q2, j2) ((q2, j2) :: r2 ++ [(e, t)])) as Hpath.
{ rewrite app_comm_cons. eapply path_postfix_path;eauto.
setoid_rewrite app_cons_rcons at 2. eapply postfix_eq. exists t'. reflexivity.
}
copy Hpath Hpath'.
eapply path_rcons_inv' in Hpath. destructH.
replace p with (u2, 0 :: j1) in *.
2: { destr_r' r2;subst.
- eapply path_single in Tpath2. inv Tpath2. inv H. inv Hpath0;eauto. inv H1.
- rewrite app_comm_cons in Hpath0. eapply path_back in Hpath0.
rewrite app_comm_cons in Tpath2. eapply path_back in Tpath2. subst x p. reflexivity.
}
eapply tcfg_edge_destruct' in Hpath1.
destruct Hpath1 as [M|[M|[M|M]]].
all: destruct M as [Htag Hedge].
+ exfalso. eapply basic_edge_no_loop2 in Hedge. contradiction.
+ symmetry in Htag. inv Htag.
eapply tagle_monotone with (n:=depth q1) in Hpath'.
* rewrite take_r_geq in Hpath';[|lia].
rewrite take_r_geq in Hpath';[|lia].
eassumption.
* eapply tag_depth_unroot2;eauto. rewrite <-Tloop. rewrite <-Tjj_len. assumption.
* intros h Hh. eapply teq_u2_deq_q in Hh as Hh'. 2: eauto.
eapply deq_loop_entry_or in Hh'. 2:eauto. destruct Hh';[auto|]. subst h.
contradiction.
* rewrite Tloop. reflexivity.
* reflexivity.
+ destruct t;cbn in Htag;congruence.
+ destruct Hedge. exfalso. eapply no_exit_head;eauto.
- contradiction.
Qed.
Section teq.
Context `(T : TeqPaths).
Lemma teq_no_back : forall x : Lab, x ∈ (q1 :: map fst r1) -> ~ loop_contains x q1.
Proof.
destruct T. destructH. intros.
eapply spath_no_back in TS0;eauto.
- eapply jj_tagle;eauto.
- eapply postfix_map with (f:=fst) in TS2. eapply postfix_incl;eauto.
Qed.
Lemma teq_no_back2
(Htageq : j1 = j2)
: forall x : Lab, x ∈ (q2 :: map fst r2) -> ~ loop_contains x q1.
Proof.
destruct T. destructH.
intros. eapply SplitPaths_sym in TS0.
subst j2.
eapply spath_no_back in TS0;eauto.
- rewrite Tloop. eauto.
- reflexivity.
- eapply postfix_map with (f:=fst) in TS3. eapply postfix_incl;eauto.
Qed.
Lemma teq_tag_eq1
: forall j, j ∈ map snd ((q1,j1) :: r1) -> take_r (depth q1) j = j1.
Proof.
destruct T. destructH. intros.
eapply spath_tag_eq1 in TS0;eauto.
- eapply jj_tagle;eauto.
- eapply postfix_map with (f:=snd) in TS2. eapply postfix_incl;eauto.
Qed.
Lemma q1_neq_q2
(Hjeq : j1 = j2)
: q1 <> q2.
Proof.
destruct T. subst j2.
intro HEq.
eapply Tdisj;left;eauto.
f_equal. symmetry;eauto.
Qed.
Lemma q1_no_head
: ~ loop_head q1.
Proof.
intro N. eapply teq_no_back.
- left. reflexivity.
- eapply loop_contains_self;eauto.
Qed.
End teq.
Lemma u1_exit_eq_q `(T : TeqPaths) h p
(Hexit : exit_edge h p u1)
: eq_loop u1 q1.
Proof.
copy T T'.
destruct T'.
destruct Tlj_eq1.
- eapply tag_depth_unroot2 in Tpath1;eauto. subst l1. split.
+ eapply teq_u1_deq_q;eauto.
+ eapply deq_loop_depth_eq. 1: eapply teq_u1_deq_q;eauto. rewrite <-Tj_len. assumption.
- destructH. subst l1. exfalso. eapply no_exit_head;eauto.
Qed.
Lemma u2_exit_eq_q `(T : TeqPaths) h p
(Hexit : exit_edge h p u2)
: eq_loop u2 q1.
Proof.
copy T T'.
destruct T'.
destruct Tlj_eq2. 2:destruct H.
- eapply tag_depth_unroot2 in Tpath2;eauto. subst l2. split.
+ eapply teq_u2_deq_q;eauto.
+ eapply deq_loop_depth_eq. 1: eapply teq_u2_deq_q;eauto. rewrite <-Tj_len. assumption.
+ rewrite <-Tjj_len. rewrite <-Tloop. assumption.
- destructH. subst l2. exfalso. eapply no_exit_head;eauto.
- split.
+ eapply teq_u2_deq_q;eauto.
+ eapply loop_contains_deq_loop;eauto.
Qed.
Hint Resolve Tpath1 Tpath2 Tdisj Tloop Tjj_len Ttl_eq Tlj_eq1 Tlj_eq2 Tj_len : teq.
Hint Resolve teq_r1_incl_head_q teq_r2_incl_head_q teq_u1_deq_q teq_u2_deq_q Tloop : teq.
Lemma TeqPaths_sym `(C : redCFG) u1 u2 q1 q2 l1 l2 j r1 r2
(T : TeqPaths u1 u2 q1 q2 l1 l2 j j r1 r2)
: TeqPaths u2 u1 q2 q1 l2 l1 j j r2 r1.
Proof.
copy T T'.
destruct T.
econstructor;eauto.
- eapply Disjoint_sym;eauto.
- symmetry. eauto.
- destruct Tlj_eq2;[firstorder|].
destruct H;[right;auto|].
exfalso. eapply teq_no_back2 in T';eauto.
eapply TPath_CPath in Tpath2. cbn in Tpath2. eapply path_contains_back;eauto.
- destruct Tlj_eq1;[left|right];firstorder.
- rewrite <-Tloop. eauto.
- destructH. do 4 eexists. split_conj.
+ eapply SplitPaths_sym;eauto.
+ eauto.
+ eauto.
Qed.
Lemma node_disj_find_head `(T : TeqPaths)
(x : Lab)
(Hx1 : x el map fst ((q1, j1) :: r1))
(h : Lab)
(n : ocnc_loop h x q1)
(Hdep : depth h = S (depth q1))
(Hpath1 : TPath (u1, l1) (q1, j1) ((q1, j1) :: r1))
(b b0 : Tag)
(Hin1' : (x, b) el (q1, j1) :: r1)
(Hin2' : (x, b0) el (q2, j1) :: r2)
(ϕ : list (Lab * Tag))
(Hin0 : Path tcfg_edge (u1, l1) (x, b) ϕ)
(Hin3 : Prefix ϕ ((q1, j1) :: r1))
(ϕ0 : list (Lab * Tag))
(Hin1 : Path tcfg_edge (u2, l2) (x, b0) ϕ0)
(Hin4 : Prefix ϕ0 ((q2, j1) :: r2))
: (h, 0 :: j1) ∈ ϕ.
Proof.
decide (h = u1).
- subst u1. eapply path_contains_back in Hin0.
specialize Tlj_eq1 as [Heq|Hentry];[exfalso|destructH];subst.
+ eapply tag_depth_unroot2 in Hpath1;eauto with teq.
destruct T. rewrite <-Tj_len in Hdep. lia.
+ eassumption.
- eapply ex_entry with (p:=u1).
+ destruct n. destruct c. exact l.
+ eapply tag_depth_unroot2 in Hpath1 as Hdepu;eauto with teq.
specialize Tlj_eq1 as [Heq|Hentry];[|destructH].
* subst l1. intro N. rewrite Tj_len in Hdepu. rewrite Hdepu in Hdep.
eapply loop_contains_deq_loop in N. eapply deq_loop_depth in N. lia.
* contradict n0. destruct n. eapply eq_loop_same.
-- split. 2: eapply loop_contains_deq_loop;eassumption.
eapply deq_loop_depth_eq. 1: eapply loop_contains_deq_loop;eassumption.
rewrite Hentry0 in Hdepu. cbn in Hdepu. erewrite Tj_len in Hdepu. lia.
-- eapply loop_contains_loop_head;eauto.
-- eauto.
+ eapply Hin0.
+ eapply tag_depth_unroot2 in Hpath1;eauto with teq.
+ setoid_rewrite <-teq_tag_eq1 at 3. 2:eapply T.
eapply take_take_r. all: cycle 1.
* eapply in_map with (f:=snd) in Hin1'. cbn in *. eauto.
* eapply tag_depth_unroot2 in Hpath1;eauto with teq.
eapply tag_depth_unroot in Hin0;eauto. rewrite Hin0.
destruct n. destruct c. eapply loop_contains_deq_loop in l. eapply deq_loop_depth in l.
instantiate (1:=depth x - depth q1). lia.
+ rewrite Hdep. cbn. rewrite Tj_len. lia.
Qed.
Lemma teq_node_disj `(T : TeqPaths)
(Hjeq : j1 = j2)
: Disjoint (q1 :: map fst r1) (q2 :: map fst r2).
Proof.
intros x Hx1 Hx2.
replace (q1 :: map fst r1) with (map fst ((q1,j1) :: r1)) in Hx1 by (cbn;eauto).
replace (q2 :: map fst r2) with (map fst ((q2,j2) :: r2)) in Hx2 by (cbn;eauto).
decide (deq_loop q1 x).
- assert (eq_loop q1 x) as Heq.
{ cbn in Hx1. split;eauto. eapply teq_r1_incl_head_q;eauto. }
replace (q1 :: map fst r1) with (map fst ((q1,j1) :: r1)) in Hx1 by (cbn;eauto).
replace (q2 :: map fst r2) with (map fst ((q2,j2) :: r2)) in Hx2 by (cbn;eauto).
eapply in_fst in Hx1. destructH.
eapply in_fst in Hx2. destructH.
enough (b = b0).
{ subst. eapply Tdisj;eauto. }
assert (| b | = depth x) as Hxb1.
{
eapply path_to_elem in Hx1;eauto. 2: eapply Tpath1. destructH.
eapply tag_depth_unroot in Hx0;eauto. destruct T. eapply tag_depth_unroot2 in Tpath1;eauto.
}
assert (| b0 | = depth x) as Hxb2.
{
eapply path_to_elem in Hx2;eauto. 2: eapply Tpath2. destructH.
eapply tag_depth_unroot in Hx0;eauto. destruct T. eapply tag_depth_unroot2 in Tpath2;eauto.
rewrite <-Tjj_len. rewrite <-Tloop. eassumption.
}
assert (b = j1) as Hbj1.
{
erewrite <-take_r_geq with (n:=depth q1) at 1.
2: rewrite Heq,Hxb1;eauto.
eapply teq_tag_eq1;eauto.
eapply in_map with (f:=snd) in Hx1. cbn in *. eauto.
}
assert (b0 = j1) as Hbj2.
{
erewrite <-take_r_geq with (n:=depth q1) at 1.
2: rewrite Heq,Hxb2;eauto.
rewrite Tloop. subst j2.
eapply TeqPaths_sym in T.
eapply teq_tag_eq1;eauto.
eapply in_map with (f:=snd) in Hx2. cbn in *. eassumption.
}
subst. reflexivity.
- eapply ex_ocnc_loop in n. destructH.
eapply ocnc_depth in n as Hdep.
specialize Tpath1 as Hpath1.
specialize Tpath2 as Hpath2.
subst j2. eapply TeqPaths_sym in T as Tsym.
eapply in_fst in Hx1 as Hin1. destructH.
eapply in_fst in Hx2 as Hin2. destructH.
copy Hin1 Hin1'. copy Hin2 Hin2'.
eapply path_to_elem in Hin1;eauto. destructH.
eapply path_to_elem in Hin2;eauto. destructH.
assert ((h, 0 :: j1) ∈ ϕ) as Hinϕ.
{ clear Tsym. eapply node_disj_find_head;eauto. }
assert ((h, 0 :: j1) ∈ ϕ0) as Hinϕ0.
{ clear T. eapply node_disj_find_head;eauto.
- unfold ocnc_loop, cnc_loop.
split;destruct n;eauto. destruct H;split;eauto. contradict H1.
eapply eq_loop1;eauto with teq.
- setoid_rewrite Tloop. eassumption.
}
eapply Tdisj. 1,2: eapply prefix_incl;eauto.
Qed.
Require Import Lia LastCommon.
Lemma only_inner_heads_tag_prefix `(C : redCFG) p i q j l
(Hdep : | i | = depth p)
(Hpath : TPath (p, i) (q, j) l)
(Hnhead : forall (h' : Lab) (k' : Tag), (h',k') ∈ tl (rev l) -> loop_contains h' q -> False)
(Hdeqq : forall (h' : Lab) (k' : Tag), (h',k') ∈ l -> deq_loop h' q)
: Prefix j i.
Proof.
clear - Hpath Hnhead Hdeqq Hdep.
remember (l) as l' in Hpath.
assert (Postfix l' l) as Hpost by (rewrite Heql';econstructor;eauto).
assert ((p,i) ∈ l') as Hel.
{ (rewrite Heql';eapply path_contains_back;subst;eauto). }
remember p as p'. remember i as i'. rewrite Heqp' in Hpath. rewrite Heqi' in Hpath.
rewrite Heqp' in Hdep. rewrite Heqi' in Hdep.
clear Heql' Heqp' Heqi'.
revert p' i' Hel p i Hpath Hdep.
rinduction l'.
- contradiction.
- eapply In_rcons in Hel. destruct Hel.
+ subst a.
specialize (rcons_destruct l0) as Hl0. destruct Hl0;[|destructH];subst l0.
* cbn in *.
inversion Hpath;subst. 2: { inversion H4. }
destruct l;[inversion Hpost;congruence'|]; eapply postfix_hd_eq in Hpost;
inversion Hpost;subst;cbn.
econstructor;auto.
* destruct a.
unfold TPath in Hpath.
assert ((p',i') ∈ l) as Helpi.
{ eapply postfix_incl;eauto. }
replace i' with (snd (p',i')) by (cbn;auto).
path_simpl' Hpath. cbn. copy Hpath Hpath'.
eapply path_nlrcons_edge in Hpath.
exploit' H.
1: { eapply postfix_step_left;eauto. }
specialize (H e t). exploit' H. specialize (H e t). exploit H.
1: eapply path_rcons_rinv;eauto.
1: eapply tcfg_edge_depth_iff in Hpath;eapply Hpath;eauto.
eapply tcfg_edge_destruct in Hpath as Q.
assert ((e,t) ∈ l) as Helet.
{ eapply postfix_incl;eauto. }
destruct Q as [Q|[Q|[Q|Q]]]. all: subst.
-- eauto. (* normal *)
-- inversion H;subst. (* entry *)
++ exfalso.
specialize (Hdeqq p i). exploit Hdeqq.
eapply deq_loop_depth in Hdeqq.
assert (|i| < |0 :: i|) as Q by (cbn;lia). clear Helet.
eapply tag_depth_unroot in Hpath';eauto. lia.
++ auto.
-- inversion H. (* back_edge *)
++ subst.
destruct i. 1:cbn;econstructor.
exfalso.
eapply Hnhead.
** eapply postfix_rev_prefix in Hpost.
rewrite rev_rcons in Hpost.
eapply prefix_tl in Hpost.
eapply prefix_incl;eauto. rewrite rev_rcons. left. reflexivity.
** specialize (tag_back_edge_iff Hpath) as [Q _]. exploit Q;eauto.
eapply deq_loop_head_loop_contains.
--- eapply deq_loop_depth_eq.
+++ eapply Hdeqq;eauto.
+++ eapply tag_depth_unroot in Hpath';eauto. cbn in Hpath',Hdep.
eapply back_edge_eq_loop in Q. rewrite <-Q. lia.
--- exists p;eauto.
++ subst. destruct i.
** cbn in H0. congruence.
** inversion H0. subst. econstructor. eauto.
-- clear - H;destruct i;cbn in *;[auto|]. inversion H;subst;econstructor;auto.
+ destruct l0;[cbn in *;contradiction|].
unfold TPath in Hpath. path_simpl' Hpath. cbn in Hpath. path_simpl' Hpath.
eapply tag_depth_unroot in Hpath as Hdepq;eauto.
eapply path_rcons_inv in Hpath. destructH. destruct p0.
eapply H;eauto.
* eapply postfix_step_left;eauto.
* eapply tag_depth_unroot2 in Hpath;eauto.
Qed.
Lemma teq_l_len1 `(T : TeqPaths)
: | l1 | = depth u1.
Proof.
destruct T.
eapply tag_depth_unroot2 in Tpath1;eauto.
Qed.
Lemma teq_l_len2 `(T : TeqPaths)
: | l2 | = depth u2.
Proof.
destruct T.
eapply tag_depth_unroot2 in Tpath2;eauto;rewrite <-Tjj_len;rewrite <-Tloop;eassumption.
Qed.
Hint Resolve teq_l_len1 teq_l_len2 : teq.
Lemma teq_root_all_nil1 `(T : TeqPaths)
(Hin : root ∈ (q1 :: map fst r1))
: u1 = root /\ l1 = [] /\ j1 = [] /\ j2 = [] /\ depth q1 = 0 /\ forall x, deq_loop x q1.
Proof.
assert (u1 = root) as Hroot.
{ destruct T. clear - Tpath1 Hin.
revert q1 j1 Tpath1 Hin.
induction r1;cbn in *;intros.
- eapply path_single in Tpath1. destructH. inv Tpath0. destruct Hin;[|contradiction]. subst;auto.
- inv_path Tpath1. destruct a. eapply IHr1. 1: eapply H.
destruct Hin.
+ subst q1. eapply tcfg_edge_edge in H0. eapply root_no_pred in H0. contradiction.
+ destruct H1. cbn in H1. subst e.
* destruct r1;[left;auto|]. inv_path H. destruct p.
eapply tcfg_edge_edge in H2. eapply root_no_pred in H2. contradiction.
* right;auto.
}
subst u1. split;auto.
assert (l1 = []) as Hnil1.
{
eapply teq_l_len1 in T. rewrite depth_root in T. destruct l1;[|cbn in T;congruence]. reflexivity.
}
split;auto.
assert (j1 = []) as Hnilj1.
{ destruct T. destruct Tlj_eq1;subst;auto. destruct H. congruence. }
split;auto.
split.
- destruct T. subst l1 j1. cbn in Tjj_len. destruct j2;[|cbn in Tjj_len;congruence]. auto.
- destruct T. subst j1. cbn in Tj_len. split;eauto.
intros x y Hy.
symmetry in Tj_len. eapply depth_zero_iff in Tj_len;eauto. contradiction.
Qed.
Lemma teq_root_all_nil2 `(T : TeqPaths)
(Hin : root ∈ (q2 :: map fst r2))
: u2 = root /\ l2 = [] /\ j1 = [] /\ j2 = [] /\ depth q1 = 0 /\ forall x, deq_loop x q1.
Proof.
assert (u2 = root) as Hroot.
{ destruct T. clear - Tpath2 Hin.
revert q2 j2 Tpath2 Hin.
induction r2;cbn in *;intros.
- eapply path_single in Tpath2. destructH. inv Tpath0. destruct Hin;[|contradiction]. subst;auto.
- inv_path Tpath2. destruct a. eapply IHr2. 1: eapply H.
destruct Hin.
+ subst q2. eapply tcfg_edge_edge in H0. eapply root_no_pred in H0. contradiction.
+ destruct H1. cbn in H1. subst e.
* destruct r2;[left;auto|]. inv_path H. destruct p.
eapply tcfg_edge_edge in H2. eapply root_no_pred in H2. contradiction.
* right;auto.
}
subst u2. split;auto.
assert (l2 = []) as Hnil2.
{
eapply teq_l_len2 in T. rewrite depth_root in T. destruct l2;[|cbn in T;congruence]. reflexivity.
}
split;auto.
assert (j1 = []) as Hnilj2.
{ destruct T. destruct Tlj_eq2;subst;auto. destruct H.
- destruct H. congruence.
- eapply loop_contains_loop_head in H. eapply loop_contains_self in H. eapply root_no_loop in H.
contradiction.
}
split;auto.
split.
- destruct T. subst l2 j1. cbn in Tjj_len. destruct j2;[|cbn in Tjj_len;congruence]. auto.
- destruct T. subst j1. cbn in Tj_len. split;eauto.
intros x y Hy.
symmetry in Tj_len. eapply depth_zero_iff in Tj_len;eauto. contradiction.
Qed.
Section teq.
Context `(T : TeqPaths).
Lemma teq_r1_incl_head_q : forall x, x ∈ (q1 :: map fst r1) -> deq_loop x q1.
Proof.
destruct T. destructH.
intros.
eapply spath_r1_incl_head_q in TS0;eauto.
eapply postfix_map with (f:=fst) in TS2.
eapply postfix_incl;eauto.
Qed.
Lemma teq_r2_incl_head_q : forall x, x ∈ (q2 :: map fst r2) -> deq_loop x q1.
Proof.
destruct T. destructH.
intros.
eapply spath_r2_incl_head_q in TS0;eauto.
eapply postfix_map with (f:=fst) in TS3.
eapply postfix_incl;eauto.
Qed.
Lemma teq_u1_deq_q
: deq_loop u1 q1.
Proof.
eapply teq_r1_incl_head_q;eauto.
destruct T.
inv_path Tpath1. 1:left;eauto.
eapply path_contains_back in H.
fold (fst (u1,l1)). right.
eapply in_map;eauto.
Qed.
Lemma teq_u2_deq_q
: deq_loop u2 q1.
Proof.
eapply teq_r2_incl_head_q;eauto.
destruct T.
inv_path Tpath2. 1:left;eauto.
eapply path_contains_back in H.
fold (fst (u2,l2)). right.
eapply in_map;eauto.
Qed.
End teq.
Lemma jj_tagle `(T : TeqPaths)
: j1 ⊴ j2.
Proof.
copy T T'.
destruct T.
assert (loop_contains u2 q1 -> j1 ⊴ j2) as Hncont.
{
intro Q.
eapply tagle_or in Tjj_len;destruct Tjj_len;[auto|exfalso].
destructH.
eapply SplitPaths_sym in TS0.
eapply spath_no_back in TS0;eauto.
+ eapply TS0. rewrite <-Tloop. eapply Q.
+ eapply postfix_map with (f:=fst) in TS3.
eapply postfix_incl;eauto. eapply TPath_CPath in Tpath2. cbn in Tpath2.
eapply path_contains_back in Tpath2. eauto.
}
decide (loop_contains u2 q1) as [Hcont|HNcont];[eauto|].
destruct Tlj_eq2 as [Q|[Q|Q]].
- subst l2. eapply tagle_monotone with (n:=depth q1) in Tpath2.
+ rewrite take_r_geq in Tpath2;[|lia].
rewrite take_r_geq in Tpath2;[|lia].
eassumption.
+ eapply tag_depth_unroot2;eauto. rewrite <-Tloop. rewrite <-Tjj_len. assumption.
+ eapply teq_u2_deq_q;eauto.
+ rewrite Tloop. reflexivity.
+ reflexivity.
- destructH. subst l2.
eapply tcfg_enroot in Tpath2 as Hroot.
2: { eapply tag_depth_unroot2;eauto. rewrite <-Tloop. rewrite <-Tjj_len. assumption. }
destructH.
destruct t';cbn in Hroot.
{ exfalso. rewrite <-app_nil_end in Hroot.
destr_r' r2;subst.
- eapply path_single in Tpath2. inv Tpath2. eapply path_single in Hroot. inv Hroot. inv H.
cbn in Tjj_len. lia.
- rewrite app_comm_cons in Hroot. eapply path_back in Hroot. subst x.
rewrite app_comm_cons in Tpath2. eapply path_back in Tpath2. inv Tpath2.
}
destruct c.
assert (TPath (e, t) (q2, j2) ((q2, j2) :: r2 ++ [(e, t)])) as Hpath.
{ rewrite app_comm_cons. eapply path_postfix_path;eauto.
setoid_rewrite app_cons_rcons at 2. eapply postfix_eq. exists t'. reflexivity.
}
copy Hpath Hpath'.
eapply path_rcons_inv' in Hpath. destructH.
replace p with (u2, 0 :: j1) in *.
2: { destr_r' r2;subst.
- eapply path_single in Tpath2. inv Tpath2. inv H. inv Hpath0;eauto. inv H1.
- rewrite app_comm_cons in Hpath0. eapply path_back in Hpath0.
rewrite app_comm_cons in Tpath2. eapply path_back in Tpath2. subst x p. reflexivity.
}
eapply tcfg_edge_destruct' in Hpath1.
destruct Hpath1 as [M|[M|[M|M]]].
all: destruct M as [Htag Hedge].
+ exfalso. eapply basic_edge_no_loop2 in Hedge. contradiction.
+ symmetry in Htag. inv Htag.
eapply tagle_monotone with (n:=depth q1) in Hpath'.
* rewrite take_r_geq in Hpath';[|lia].
rewrite take_r_geq in Hpath';[|lia].
eassumption.
* eapply tag_depth_unroot2;eauto. rewrite <-Tloop. rewrite <-Tjj_len. assumption.
* intros h Hh. eapply teq_u2_deq_q in Hh as Hh'. 2: eauto.
eapply deq_loop_entry_or in Hh'. 2:eauto. destruct Hh';[auto|]. subst h.
contradiction.
* rewrite Tloop. reflexivity.
* reflexivity.
+ destruct t;cbn in Htag;congruence.
+ destruct Hedge. exfalso. eapply no_exit_head;eauto.
- contradiction.
Qed.
Section teq.
Context `(T : TeqPaths).
Lemma teq_no_back : forall x : Lab, x ∈ (q1 :: map fst r1) -> ~ loop_contains x q1.
Proof.
destruct T. destructH. intros.
eapply spath_no_back in TS0;eauto.
- eapply jj_tagle;eauto.
- eapply postfix_map with (f:=fst) in TS2. eapply postfix_incl;eauto.
Qed.
Lemma teq_no_back2
(Htageq : j1 = j2)
: forall x : Lab, x ∈ (q2 :: map fst r2) -> ~ loop_contains x q1.
Proof.
destruct T. destructH.
intros. eapply SplitPaths_sym in TS0.
subst j2.
eapply spath_no_back in TS0;eauto.
- rewrite Tloop. eauto.
- reflexivity.
- eapply postfix_map with (f:=fst) in TS3. eapply postfix_incl;eauto.
Qed.
Lemma teq_tag_eq1
: forall j, j ∈ map snd ((q1,j1) :: r1) -> take_r (depth q1) j = j1.
Proof.
destruct T. destructH. intros.
eapply spath_tag_eq1 in TS0;eauto.
- eapply jj_tagle;eauto.
- eapply postfix_map with (f:=snd) in TS2. eapply postfix_incl;eauto.
Qed.
Lemma q1_neq_q2
(Hjeq : j1 = j2)
: q1 <> q2.
Proof.
destruct T. subst j2.
intro HEq.
eapply Tdisj;left;eauto.
f_equal. symmetry;eauto.
Qed.
Lemma q1_no_head
: ~ loop_head q1.
Proof.
intro N. eapply teq_no_back.
- left. reflexivity.
- eapply loop_contains_self;eauto.
Qed.
End teq.
Lemma u1_exit_eq_q `(T : TeqPaths) h p
(Hexit : exit_edge h p u1)
: eq_loop u1 q1.
Proof.
copy T T'.
destruct T'.
destruct Tlj_eq1.
- eapply tag_depth_unroot2 in Tpath1;eauto. subst l1. split.
+ eapply teq_u1_deq_q;eauto.
+ eapply deq_loop_depth_eq. 1: eapply teq_u1_deq_q;eauto. rewrite <-Tj_len. assumption.
- destructH. subst l1. exfalso. eapply no_exit_head;eauto.
Qed.
Lemma u2_exit_eq_q `(T : TeqPaths) h p
(Hexit : exit_edge h p u2)
: eq_loop u2 q1.
Proof.
copy T T'.
destruct T'.
destruct Tlj_eq2. 2:destruct H.
- eapply tag_depth_unroot2 in Tpath2;eauto. subst l2. split.
+ eapply teq_u2_deq_q;eauto.
+ eapply deq_loop_depth_eq. 1: eapply teq_u2_deq_q;eauto. rewrite <-Tj_len. assumption.
+ rewrite <-Tjj_len. rewrite <-Tloop. assumption.
- destructH. subst l2. exfalso. eapply no_exit_head;eauto.
- split.
+ eapply teq_u2_deq_q;eauto.
+ eapply loop_contains_deq_loop;eauto.
Qed.
Hint Resolve Tpath1 Tpath2 Tdisj Tloop Tjj_len Ttl_eq Tlj_eq1 Tlj_eq2 Tj_len : teq.
Hint Resolve teq_r1_incl_head_q teq_r2_incl_head_q teq_u1_deq_q teq_u2_deq_q Tloop : teq.
Lemma TeqPaths_sym `(C : redCFG) u1 u2 q1 q2 l1 l2 j r1 r2
(T : TeqPaths u1 u2 q1 q2 l1 l2 j j r1 r2)
: TeqPaths u2 u1 q2 q1 l2 l1 j j r2 r1.
Proof.
copy T T'.
destruct T.
econstructor;eauto.
- eapply Disjoint_sym;eauto.
- symmetry. eauto.
- destruct Tlj_eq2;[firstorder|].
destruct H;[right;auto|].
exfalso. eapply teq_no_back2 in T';eauto.
eapply TPath_CPath in Tpath2. cbn in Tpath2. eapply path_contains_back;eauto.
- destruct Tlj_eq1;[left|right];firstorder.
- rewrite <-Tloop. eauto.
- destructH. do 4 eexists. split_conj.
+ eapply SplitPaths_sym;eauto.
+ eauto.
+ eauto.
Qed.
Lemma node_disj_find_head `(T : TeqPaths)
(x : Lab)
(Hx1 : x el map fst ((q1, j1) :: r1))
(h : Lab)
(n : ocnc_loop h x q1)
(Hdep : depth h = S (depth q1))
(Hpath1 : TPath (u1, l1) (q1, j1) ((q1, j1) :: r1))
(b b0 : Tag)
(Hin1' : (x, b) el (q1, j1) :: r1)
(Hin2' : (x, b0) el (q2, j1) :: r2)
(ϕ : list (Lab * Tag))
(Hin0 : Path tcfg_edge (u1, l1) (x, b) ϕ)
(Hin3 : Prefix ϕ ((q1, j1) :: r1))
(ϕ0 : list (Lab * Tag))
(Hin1 : Path tcfg_edge (u2, l2) (x, b0) ϕ0)
(Hin4 : Prefix ϕ0 ((q2, j1) :: r2))
: (h, 0 :: j1) ∈ ϕ.
Proof.
decide (h = u1).
- subst u1. eapply path_contains_back in Hin0.
specialize Tlj_eq1 as [Heq|Hentry];[exfalso|destructH];subst.
+ eapply tag_depth_unroot2 in Hpath1;eauto with teq.
destruct T. rewrite <-Tj_len in Hdep. lia.
+ eassumption.
- eapply ex_entry with (p:=u1).
+ destruct n. destruct c. exact l.
+ eapply tag_depth_unroot2 in Hpath1 as Hdepu;eauto with teq.
specialize Tlj_eq1 as [Heq|Hentry];[|destructH].
* subst l1. intro N. rewrite Tj_len in Hdepu. rewrite Hdepu in Hdep.
eapply loop_contains_deq_loop in N. eapply deq_loop_depth in N. lia.
* contradict n0. destruct n. eapply eq_loop_same.
-- split. 2: eapply loop_contains_deq_loop;eassumption.
eapply deq_loop_depth_eq. 1: eapply loop_contains_deq_loop;eassumption.
rewrite Hentry0 in Hdepu. cbn in Hdepu. erewrite Tj_len in Hdepu. lia.
-- eapply loop_contains_loop_head;eauto.
-- eauto.
+ eapply Hin0.
+ eapply tag_depth_unroot2 in Hpath1;eauto with teq.
+ setoid_rewrite <-teq_tag_eq1 at 3. 2:eapply T.
eapply take_take_r. all: cycle 1.
* eapply in_map with (f:=snd) in Hin1'. cbn in *. eauto.
* eapply tag_depth_unroot2 in Hpath1;eauto with teq.
eapply tag_depth_unroot in Hin0;eauto. rewrite Hin0.
destruct n. destruct c. eapply loop_contains_deq_loop in l. eapply deq_loop_depth in l.
instantiate (1:=depth x - depth q1). lia.
+ rewrite Hdep. cbn. rewrite Tj_len. lia.
Qed.
Lemma teq_node_disj `(T : TeqPaths)
(Hjeq : j1 = j2)
: Disjoint (q1 :: map fst r1) (q2 :: map fst r2).
Proof.
intros x Hx1 Hx2.
replace (q1 :: map fst r1) with (map fst ((q1,j1) :: r1)) in Hx1 by (cbn;eauto).
replace (q2 :: map fst r2) with (map fst ((q2,j2) :: r2)) in Hx2 by (cbn;eauto).
decide (deq_loop q1 x).
- assert (eq_loop q1 x) as Heq.
{ cbn in Hx1. split;eauto. eapply teq_r1_incl_head_q;eauto. }
replace (q1 :: map fst r1) with (map fst ((q1,j1) :: r1)) in Hx1 by (cbn;eauto).
replace (q2 :: map fst r2) with (map fst ((q2,j2) :: r2)) in Hx2 by (cbn;eauto).
eapply in_fst in Hx1. destructH.
eapply in_fst in Hx2. destructH.
enough (b = b0).
{ subst. eapply Tdisj;eauto. }
assert (| b | = depth x) as Hxb1.
{
eapply path_to_elem in Hx1;eauto. 2: eapply Tpath1. destructH.
eapply tag_depth_unroot in Hx0;eauto. destruct T. eapply tag_depth_unroot2 in Tpath1;eauto.
}
assert (| b0 | = depth x) as Hxb2.
{
eapply path_to_elem in Hx2;eauto. 2: eapply Tpath2. destructH.
eapply tag_depth_unroot in Hx0;eauto. destruct T. eapply tag_depth_unroot2 in Tpath2;eauto.
rewrite <-Tjj_len. rewrite <-Tloop. eassumption.
}
assert (b = j1) as Hbj1.
{
erewrite <-take_r_geq with (n:=depth q1) at 1.
2: rewrite Heq,Hxb1;eauto.
eapply teq_tag_eq1;eauto.
eapply in_map with (f:=snd) in Hx1. cbn in *. eauto.
}
assert (b0 = j1) as Hbj2.
{
erewrite <-take_r_geq with (n:=depth q1) at 1.
2: rewrite Heq,Hxb2;eauto.
rewrite Tloop. subst j2.
eapply TeqPaths_sym in T.
eapply teq_tag_eq1;eauto.
eapply in_map with (f:=snd) in Hx2. cbn in *. eassumption.
}
subst. reflexivity.
- eapply ex_ocnc_loop in n. destructH.
eapply ocnc_depth in n as Hdep.
specialize Tpath1 as Hpath1.
specialize Tpath2 as Hpath2.
subst j2. eapply TeqPaths_sym in T as Tsym.
eapply in_fst in Hx1 as Hin1. destructH.
eapply in_fst in Hx2 as Hin2. destructH.
copy Hin1 Hin1'. copy Hin2 Hin2'.
eapply path_to_elem in Hin1;eauto. destructH.
eapply path_to_elem in Hin2;eauto. destructH.
assert ((h, 0 :: j1) ∈ ϕ) as Hinϕ.
{ clear Tsym. eapply node_disj_find_head;eauto. }
assert ((h, 0 :: j1) ∈ ϕ0) as Hinϕ0.
{ clear T. eapply node_disj_find_head;eauto.
- unfold ocnc_loop, cnc_loop.
split;destruct n;eauto. destruct H;split;eauto. contradict H1.
eapply eq_loop1;eauto with teq.
- setoid_rewrite Tloop. eassumption.
}
eapply Tdisj. 1,2: eapply prefix_incl;eauto.
Qed.