# UniAna.cfg.CFGloop

Require Export CFGdef CFGTac.

Section cfg.
Context `{C : redCFG}.

Notation "p '-a>b' q" := (a_edge p q) (at level 55).
Notation "p '-a>' q" := (p -a>b q = true) (at level 55).
Notation "p '-->b' q" := (edge p q) (at level 55).
Notation "p '-->' q" := (p -->b q = true) (at level 55, right associativity).

# Basic loop facts

Lemma loop_contains_loop_head (qh q : Lab)
: loop_contains qh q -> loop_head qh.
Proof.
intro Q. unfold loop_head, loop_contains in *. destruct Q as [p [_ [Q _]]].
eexists; eauto.
Qed.

Lemma loop_contains_self h : loop_head h -> loop_contains h h.
Proof.
intros Hl. unfold loop_contains.
- unfold loop_head in Hl. destruct Hl.
eapply loop_head_dom in H as Hdom.
eapply back_edge_incl in H as Hreach. specialize (a_reachability x) as Hreach'.
destructH.
eapply subgraph_path' in Hreach' as Hreach'';eauto using a_edge_incl.
eapply Hdom in Hreach''. eapply path_from_elem in Hreach''; eauto.
destructH; eauto.
eapply path_NoDup' in Hreach''0;eauto.
destructH. exists x, π0. firstorder;eauto.
+ eapply subgraph_path';eauto using a_edge_incl.
+ eapply NoDup_rev in Hreach''3.
remember (rev π0) as l.
destruct l;cbn in *;eauto.
assert (π0 = rev l ++ [e]).
{ rewrite rev_rev_eq. rewrite rev_rcons. rewrite rev_involutive. eauto. }
rewrite H1 in Hreach''2. eapply path_back in Hreach''2. subst.
inversion Hreach''3. subst. assumption.
Qed.

## Facts about dominance and loops

Lemma dom_loop h
: forall q: Lab, loop_contains h q -> Dom edge__P root h q.
Proof.
intros q Hq. unfold loop_contains,CPath in *. intros π Hπ.
destructH.
eapply nin_tl_iff in Hq3;eauto.
destruct Hq3.
- eapply path_app' in Hq2. 2: eapply Hπ.
eapply loop_head_dom in Hq2. 2:eauto. eapply in_app_or in Hq2.
- eapply path_contains_front in Hπ. enough (h = q);[subst;eauto|].
destr_r' π0;cbn in *;subst.
+ inversion Hq2.
+ rewrite rev_rcons in H. cbn in H. inversion H. subst. path_simpl' Hq2. reflexivity.
Qed.

Lemma dom_dom_acyclic r p q
: Dom edge__P r p q -> Dom a_edge__P r p q.
Proof.
intros. unfold Dom in *. intros. apply H. eapply subgraph_path'; eauto using a_edge_incl.
Qed.

Instance loop_contains_Antisymmetric : Antisymmetric Lab eq loop_contains.
Proof.
unfold Antisymmetric.
intros.
specialize (a_reachability x) as Hx.
specialize (a_reachability y) as Hy.
destructH. destructH.
eapply dom_loop in H. eapply dom_loop in H0.
eapply dom_dom_acyclic in H. eapply dom_dom_acyclic in H0.
eapply H in Hy as Hy'. eapply H0 in Hx as Hx'.
eapply path_from_elem in Hy;eauto.
eapply path_from_elem in Hx;eauto.
do 2 destructH.
eapply path_path_acyclic';eauto using a_edge_acyclic.
Qed.

Lemma loop_contains_ledge_path
(p qh : Lab)
(Hledge : p qh)
(q : Lab)
(π : list Lab)
(Hpath : Path edge__P q p π)
(Hnin : qh tl (rev π))
(x : Lab)
(Hin : x π)
: loop_contains qh x.
Proof.
unfold loop_contains.
exists p. specialize (@path_from_elem _ edge__P _ q p x) as Hx. exploit Hx. destructH.
exists ϕ. repeat (split;eauto). contradict Hnin. clear - Hx1 Hnin.
induction Hx1; cbn in *;[auto|]. rewrite rev_rcons. cbn. eapply IHHx1 in Hnin.
eapply tl_incl;auto.
Qed.

## Transitivity of loop_contains

Lemma loop_contains_trans h h' p
(Hloop : loop_contains h h')
(Hloop' : loop_contains h' p)
: loop_contains h p.
Proof.
copy Hloop Hloop_save.
unfold loop_contains in Hloop,Hloop'.
decide (h = h');[subst;eauto|].
destructH' Hloop'. destructH' Hloop.
exists p1. specialize (path_app Hloop'2 (back_edge_incl Hloop'0) Hloop2) as .
exists (π0 ++ π);split;eauto;split;eauto. intro N.
cbn in *. rewrite rev_app_distr in N.
destr_r' π;subst;cbn in *. 1: inversion Hloop'2.
rewrite rev_rcons in N. cbn in N.
eapply in_app_or in N. destruct N.
- eapply loop_contains_ledge_path in Hloop'3. 2,3: eauto.
+ eapply loop_contains_Antisymmetric in Hloop_save. eapply Hloop_save in Hloop'3. contradiction.
+ eapply In_rcons. right. eapply in_rev. auto.
rewrite rev_rcons in H. destruct H;subst.
+ rewrite rev_rcons in Hloop3. cbn in Hloop3. contradiction.
Qed.

Lemma loop_reachs_member (h q : Lab)
: loop_contains h q -> h -a>* q.
Proof.
intros Hloop. cbn.
specialize (a_reachability q) as Hπ. destructH.
eapply dom_loop in Hloop. eapply dom_dom_acyclic in Hloop.
eapply Hloop in Hπ as Hin.
eapply path_from_elem in Hπ;eauto. destructH.
eexists;eauto.
Qed.

(Hedge : edge__P p h)
(Hloop : loop_contains h p)
: p h.
Proof.
decide (p h);[assumption|exfalso].
simpl_dec' n.
simpl_dec' H.
eapply loop_reachs_member in Hloop. destruct Hloop.
eapply a_edge_acyclic;eauto.
Qed.
(*
(Hedge : edge p h = true)
(Hloop : loop_contains h' p)
: loop_contains h' h.
Proof.
*)

Lemma path_prefix_path' p q r π ϕ
: Path edge__P p q π -> Prefix (r :: ϕ) π -> Path edge__P p r (r :: ϕ).
Proof.
eapply path_prefix_path.
intros. unfold dec. decide (x --> y); firstorder.
Qed.

Lemma root_loop_root h
: loop_contains h root -> h = root.
Proof.
intros H.
eapply dom_loop in H.
assert (Path edge__P root root [root]) as Hpath;[econstructor|].
eapply H in Hpath. destruct Hpath;[subst;auto|contradiction].
Qed.

Lemma loop_contains_either h1 h2 p
(Hloo : loop_contains h1 p)
(Hlop : loop_contains h2 p)
: loop_contains h1 h2 \/ loop_contains h2 h1.
Proof.
specialize (a_reachability p) as Hr. destructH.
eapply dom_loop in Hloo as Hdom1. eapply dom_dom_acyclic in Hdom1. eapply Hdom1 in Hr as Hr1.
eapply dom_loop in Hlop as Hdom2. eapply dom_dom_acyclic in Hdom2. eapply Hdom2 in Hr as Hr2.
eapply path_from_elem in Hr1;eauto.
eapply path_from_elem in Hr2;eauto.
do 2 destructH.
decide (h1 = p);[subst;right;auto|].
decide (h2 = p);[subst;left ;auto|].
decide (h1 = h2);[subst;left;eauto using loop_contains_self,loop_contains_loop_head|].
eapply postfix_order_destruct in Hr4;eauto.
destruct Hr4.
- left. unfold loop_contains in *. do 2 destructH.
exists p1. eapply path_app' in Hloo2 as Happ;eauto. exists (π1 ++ tl ϕ).
repeat (split;eauto). 2:eauto using subgraph_path',a_edge_incl.
enough (h1 tl ϕ).
+ contradict Hloo3. eapply tl_incl in Hloo3. eapply in_rev in Hloo3.
eapply in_app_or in Hloo3. destruct Hloo3;[|contradiction].
destr_r' π1;subst;[contradiction|]. rewrite rev_rcons. cbn. rewrite <-in_rev.
eapply In_rcons in H1. destruct H1;[|auto]. subst x.
clear - Hloo2 n.
exfalso. contradict n. revert dependent p1.
induction l;cbn in *;intros;inversion Hloo2;subst;auto.
* inversion H3.
* congruence'.
* eapply IHl;eauto.
+ destr_r' ϕ0;subst. 1: inversion Hr2.
destr_r' ϕ;subst. 1: inversion Hr0.
eapply path_back in Hr2 as Hr2'.
eapply path_back in Hr0 as Hr0'. subst x x0.
eapply acyclic_path_NoDup in Hr2. eapply NoDup_rev in Hr2.
inversion H;subst.
* eapply rev_rev_eq in H2;repeat rewrite rev_rcons in H2. inversion H2;subst. contradiction.
* eapply rev_rev_eq in H0;repeat rewrite rev_rcons in H0. inversion H0;subst.
eapply rev_rev_eq in H4. subst l'.
intro N. eapply tl_incl in N. eapply postfix_incl in N;[|eauto].
rewrite rev_rcons in Hr2. inversion Hr2;subst. eapply in_rev in N; contradiction.
- right. unfold loop_contains in *. do 2 destructH.
exists p0. eapply path_app' in Hlop2 as Happ;eauto. 2: clear Hr0;eauto using subgraph_path',a_edge_incl.
exists (π0 ++ tl ϕ0).
repeat (split;eauto).
enough (h2 tl ϕ0).
+ contradict Hlop3. eapply tl_incl in Hlop3. eapply in_rev in Hlop3.
eapply in_app_or in Hlop3. destruct Hlop3;[|contradiction].
destr_r' π0;subst. 1: inversion Hlop2. rewrite rev_rcons. cbn. rewrite <-in_rev.
eapply In_rcons in H1. destruct H1;[|auto]. subst x.
clear - Hlop2 n0.
exfalso. contradict n0. revert dependent p0.
induction l;cbn in *;intros;inversion Hlop2;subst;auto.
* inversion H3.
* congruence'.
* eapply IHl;eauto.
+ destr_r' ϕ0;subst. 1:inversion Hr2.
destr_r' ϕ;subst. 1: inversion Hr0.
eapply path_back in Hr2 as Hr2'.
eapply path_back in Hr0 as Hr0'. subst x x0.
eapply acyclic_path_NoDup in Hr0. eapply NoDup_rev in Hr0.
inversion H;subst.
* eapply rev_rev_eq in H2;repeat rewrite rev_rcons in H2. inversion H2;subst. contradiction.
* eapply rev_rev_eq in H0;repeat rewrite rev_rcons in H0. inversion H0;subst.
eapply rev_rev_eq in H4. subst l'.
intro N. eapply tl_incl in N. eapply postfix_incl in N;[|eauto].
rewrite rev_rcons in Hr0. inversion Hr0;subst. eapply in_rev in N; contradiction.
Qed.

Lemma dom_path p q
: Dom edge__P root p q -> p -->* q.
Proof.
intros Hdom.
specialize reachability asHπ]. specialize (Hdom π Hπ).
eapply path_from_elem in Hπ; eauto using Lab_dec. firstorder.
Qed.

Lemma back_edge_no_a_edge p q
: p q -> ~ a_edge__P p q.
Proof.
intros Hbedge Haedge.
specialize (a_reachability p) as Hreach.
destructH.
eapply dom_dom_acyclic in Hbedge.
specialize (Hbedge _ Hreach).
eapply PathCons in Haedge;eauto.
eapply acyclic_path_NoDup in Haedge.
inversion Haedge. subst.
Qed.

Lemma loop_contains_not_dom h q
: loop_contains h q -> h <> q -> exists p, p h /\ ~ Dom edge__P q h p.
Proof.
intros Hloop Hneq. unfold loop_contains in Hloop. destructH.
unfold Dom; eexists; firstorder; eauto.
- apply back_edge_incl;eauto.
- eapply back_edge_no_a_edge. auto.
- eapply nin_tl_iff in Hloop3;eauto. destruct Hloop3.
+ eauto.
+ contradict Hneq. destr_r' π;subst. 1:inversion Hloop2.
rewrite rev_rcons in H. cbn in *. inversion H. subst. path_simpl' Hloop2. reflexivity.
Qed.

Lemma not_and_iff (A B : Prop) : decidable A -> (~ (A /\ B) <-> ~ A \/ ~ B).
Proof.
firstorder.
Qed.

Lemma in_tl_in {A : Type} (a : A) (l : list A) : a tl l -> a l.
Proof.
destruct l; cbn in *; eauto.
Qed.

(* FIXME: move *)
Lemma hd_rev_tl_rev_cons (A : Type) (l : list A) (a : A)
: hd a (rev (tl (rev (a :: l)))) = a.
Proof.
clear.
rewrite rev_cons. destr_r' l;subst;cbn;auto.
rewrite rev_rcons. cbn. rewrite rev_rcons. cbn. auto.
Qed.

# Path and Dominance facts

Lemma app_tl_switch (A : Type) (a b : A) (π ϕ : list A)
(Heq : hd a (rev π) = hd b ϕ)
(Hπ : π <> nil)
( : ϕ <> nil)
: π ++ tl ϕ = (rev (tl (rev π))) ++ ϕ.
Proof.
destr_r' π;[congruence|].
destruct ϕ;[congruence|].
clear Hπ . subst π. rewrite rev_rcons in Heq. cbn in Heq. subst.
rewrite rev_rcons. cbn. rewrite rev_involutive.
rewrite <-app_assoc. reflexivity.
Qed.

Lemma dom_loop_contains h p q
: loop_contains h q -> ~ loop_contains h p -> Dom edge__P p h q.
Proof.
intros Hloop Hnloop π Hπ.
copy Hloop Hloop'. copy Hnloop Hnloop'.
unfold loop_contains in Hnloop. do 3 simpl_dec' Hnloop.
assert (forall x ϕ, x h -> Path edge__P p x ϕ -> h tl (rev ϕ)) as Q.
{ clear - Hnloop.
intros. specialize (Hnloop x ϕ). firstorder.
}
clear Hnloop.
unfold loop_contains in Hloop. destructH.
eapply path_app' in Hloop2 as Happ;eauto.
erewrite app_tl_switch in Happ.
2: { eapply path_back' in Hloop2. eapply path_front' in Hπ. rewrite <-Hπ. rewrite <-Hloop2. auto. }
2: intro;subst;inversion Hloop2.
2: intro;subst;inversion Hπ.
specialize (Q _ _ Hloop0 Happ).
destr_r' π;subst;[inversion Hπ|subst].
rewrite app_assoc in Q. rewrite rev_rcons in Q. cbn in Q.
eapply in_rev in Q. eapply in_app_or in Q. destruct Q as [Q|Q];[eapply in_rev in Q;contradiction|].
eapply In_rcons;auto.
Unshelve. all:auto.
Qed.

Lemma loop_contains_path h q π
: CPath h q π -> loop_contains h q -> NoDup π -> forall p, p π -> loop_contains h p.
Proof.
intros Hπ Hin Hnd p Hp.
decide (p = h) as [Hph|Hph].
- rewrite Hph. eapply loop_contains_self. eapply loop_contains_loop_head; eauto.
- destruct (loop_contains_dec h p) as [N|N]; [eauto|exfalso].
eapply path_from_elem in Hp; eauto. destructH.
eapply dom_loop_contains in N; eauto; cycle 1.
eapply postfix_incl in Hp1 as Hp1'; eauto.
dependent induction Hp1.
+ eapply Hph. eapply path_back_eq;eauto.
+ clear IHHp1. unfold Dom in N.
eapply postfix_incl in Hp1. eapply Hp1 in N; eauto.
unfold CPath in Hπ. path_simpl' Hπ.
Qed.

Lemma loop_contains_splinter h1 h2 p π
(Hloop1 : loop_contains h1 h2)
(Hloop2 : loop_contains h2 p)
(Hpath : Path edge__P root p π)
: h2 ≻* h1 | π.
Proof.
eapply dom_loop in Hloop2. eapply Hloop2 in Hpath as Hin.
eapply path_to_elem in Hin;eauto. destructH.
eapply splinter_prefix;eauto.
inversion Hin0;subst h2 a.
- eapply dom_loop in Hloop1. eapply Hloop1 in Hin0. rewrite <-H1 in Hin0. inversion Hin0;subst;[|contradiction].
econstructor. econstructor. econstructor. econstructor.
- cbn in *. econstructor. eapply dom_loop in Hloop1. eapply Hloop1 in Hin0. rewrite <-H3 in Hin0.
eapply splinter_single. cbn in *; eauto.
Qed.

# Predecessors

Definition preds `{redCFG Lab edge} p : list Lab
:= filter (decPred_bool (fun q => edge q p)) (elem Lab).

Lemma preds_in_same_loop h p q
(Hl : loop_contains h p)
(Hneq : h <> p)
(Hedge : q --> p)
: loop_contains h q.
Proof.
unfold loop_contains in Hl.
destructH.
specialize (path_rcons (r:=q) Hl2) as Hl2'. exploit Hl2'.
exists p0, (π ++ [q]). repeat (split;eauto).
rewrite rev_rcons. cbn. eapply nin_tl_iff in Hl3;auto.
destruct Hl3 as [Hl3|Hl3];[contradict Hl3;eapply in_rev;auto|].
destr_r' π;subst;[inversion Hl2|]. rewrite rev_rcons in *. cbn in Hl3. path_simpl' Hl2.
Qed.

# Facts about acyclic paths and exits

Lemma exit_a_edge h p q
(Hexit : exit_edge h p q)
: a_edge p q = true.
Proof.
destruct (a_edge p q) eqn:E;[auto|exfalso].
unfold exit_edge in Hexit. destructH.
exists p. unfold back_edge. unfold_edge_op. split; auto.
unfold a_edge__P,is_true2,is_true.
intro N. congruence.
Qed.

Lemma loop_reachs_exit h p q
(Hexit : exit_edge h p q)
: h -a>* q.
Proof.
copy Hexit Hexit'.
destruct Hexit.
eapply loop_reachs_member in H.
destruct H.
exists (q :: x).
econstructor;eauto.
eapply exit_a_edge;eauto.
Qed.

Lemma acyclic_path_stays_in_loop (h p q : Lab) π
(Hpath : Path a_edge__P p q π)
(Hp : loop_contains h p)
(Hq : loop_contains h q)
: forall x, x π -> loop_contains h x.
Proof.

enough (h tl (rev π)) as Hnin.
- intros.
eapply subgraph_path' in Hpath;eauto.
eapply (path_from_elem) in Hpath as ;eauto. destructH.
unfold loop_contains in Hq.
destructH.
exists p0, (π0 ++ tl ϕ); split_conj; auto.
+ eapply path_app';eauto.
+ destr_r' π;subst. 1: inversion Hpath.
rename l into π.
destr_r' π0;subst. 1: inversion Hq2.
rename l into π0.
destr_r' ϕ;subst. 1: inversion Hϕ0.
rename l into ϕ.
rewrite rev_app_distr.
rewrite rev_rcons in *.
cbn in *. rewrite <-in_rev in Hq3,Hnin.
path_simpl' Hpath. path_simpl' Hq2. path_simpl' Hϕ0.
destruct ϕ;cbn;[rewrite <-in_rev;auto|].
rewrite rev_rcons. cbn.
intro N. eapply in_app_or in N. destruct N as [N|[N|N]].
* eapply postfix_rcons_rcons in Hϕ1. eapply postfix_incl in Hϕ1.
eapply Hnin. eapply Hϕ1. right. rewrite in_rev. auto.
* cbn in Hϕ0. path_simpl' Hϕ0. subst.
eapply postfix_rcons_rcons in Hϕ1.
eapply Hnin. eapply postfix_incl;eauto.
* rewrite <-in_rev in N. contradiction.
- intro N.
specialize (a_reachability p) as [ϕ ].
eapply dom_loop in Hp.
eapply dom_dom_acyclic in Hp.
eapply Hp in as Hin.
eapply path_app' in Hpath as Hpath';eauto.
eapply acyclic_path_NoDup in Hpath' as Hnd.
enough++ tl ϕ = rev (tl (rev π)) ++ ϕ).
+ rewrite H in Hnd.
eapply NoDup_app;eauto.
rewrite <-in_rev. auto.
+ clear - Hpath .
destr_r' π;subst. 1: inversion Hpath. rewrite rev_rcons. cbn.
rewrite rev_involutive.
eapply path_back in Hpath. subst x.
destruct ϕ;cbn in *.
* inversion ; subst.
* inversion ; subst;auto. rewrite <-app_assoc. cbn. reflexivity.
rewrite <-app_cons_assoc. auto.
Qed.

Lemma acyclic_parallel_exit_path h p q π
(Hπ : Path a_edge__P h q π)
(Hexit : exit_edge h p q)
: forall x, x tl π -> loop_contains h x.
Proof.
assert (e = q) by (inversion Hπ;cbn in *;subst;auto);subst.
intros.
eapply acyclic_path_stays_in_loop;eauto.
- eapply loop_contains_self;unfold exit_edge in Hexit; destructH ;
- eapply exit_pred_loop;eauto.
eapply a_edge_incl;eauto.
Qed.

Lemma loop_contains_ledge qh ql
: ql qh -> loop_contains qh ql.
Proof.
intros. exists ql, ([ql]). split_conj;[auto|constructor|cbn]. exact (fun x => x).
Qed.

Lemma exit_edge_pred_exiting h p q
(Hexit : exit_edge h p q)
(p' : Lab)
(Hedge : edge p' q = true)
: exit_edge h p' q.
Proof.
copy Hexit Hexit'.
unfold exit_edge; unfold exit_edge in Hexit. destructH.
split_conj;eauto.
eapply exit_pred_loop;eauto.
Qed.

Lemma root_no_acyclic_pred p
: a_edge p root <> true.
Proof.
specialize (a_reachability p) asHπ].
intro. eapply a_edge_acyclic;eauto.
Qed.

Lemma exit_edge_acyclic h qe e
(Hexit : exit_edge h qe e)
: a_edge qe e = true.
Proof.
copy Hexit Hexit'.
unfold exit_edge in Hexit.
destructH.
destruct (a_edge qe e) eqn:E;[auto|exfalso].
eexists; unfold back_edge; unfold_edge_op.
split;eauto.
intro. congruence.
Qed.

(Hexit : exit_edge h qe e)
h'
(Hloop : loop_contains h' h)
(Hnloop : ~ loop_contains h' e)
: h' = h.
Proof.
specialize (a_reachability e) asHπ].
inversion Hπ;subst e a.
- exfalso. subst π.
eapply exit_edge_acyclic in Hexit. exfalso. eapply root_no_acyclic_pred;eauto.
- eapply a_edge_incl in H0. eapply exit_pred_loop in H0 as H2;eauto.
eapply single_exit with (p:=b) (q:=c).
+ split;[|split];eauto.
eapply loop_contains_trans;eauto.
+ split;[|split];eauto.
Qed.

Lemma exit_edge_in_loop (h1 h2 p2 e2 : Lab)
(Hexit' : exit_edge h2 p2 e2)
(Hloop : loop_contains h1 h2)
(Hneq : h1 <> h2)
: loop_contains h1 e2.
Proof.
decide (loop_contains h1 e2);[auto|].
copy Hexit' Hexit''.
unfold exit_edge in Hexit'. destructH.
assert (exit_edge h1 p2 e2).
{
unfold exit_edge. split_conj;cycle 1.
+ eauto.
+ eauto.
+ eauto using loop_contains_trans.
}
Qed.

(Hnin : ~ loop_contains h p)
(Hin : loop_contains h q)
(Hedge : p --> q)
: q = h.
Proof.
eapply dom_loop_contains in Hin as Hin';eauto.
assert (Path edge__P p q (q :: [p])) as Hpath.
1: econstructor;eauto;econstructor.
eapply Hin' in Hpath. destruct Hpath;auto.
exfalso.
apply Hnin. eapply loop_contains_self. eauto using loop_contains_loop_head.
Qed.

Lemma in_path_ex_prefix_not_in p q π x
(Hπ : CPath p q π)
(Hin : x π)
: exists ϕ, Prefix (x :: ϕ) π /\ x ϕ.
Proof.
revert dependent q.
induction π.
- inv Hin.
- intros.
replace a with q in *.
+ decide (x π).
* destruct π; [ inv i |].
destruct (IHπ i e) as [ϕ [Hpre Hnin]].
-- inv Hπ. enough (b = e).
++ subst. eassumption.
++ eauto using path_front.
-- exists ϕ. split; [| eassumption ].
econstructor. eassumption.
* inv Hin.
-- exists π. split; [ econstructor | eassumption ].