Require Import Coq.Classes.EquivDec.
Require Import Coq.Program.Equality.
Require Import Coq.Program.Utils.
Require Import Coq.Logic.Classical.
Require Import List.
Require Import Nat.
Require Import Bool.Bool.
Require Import Coq.Logic.Eqdep_dec.

Require Export Tagged LastCommon.

Section eval.

  Context `{C : redCFG}.

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

  Parameter Var : Type.
  Parameter Var_dec : EqDec Var eq.
  Parameter is_def : Var -> Lab -> Lab -> bool.

  Parameter def_edge :
    forall p q x, is_def x p q = true -> p --> q.

  Definition is_def_lab x p := exists q, is_def x q p = true.

(*  Lemma Lab_var_dec :
    forall (x y : (Lab * Var)), { x = y } + { x <> y }.
    destruct x as xa xb, y as ya yb.

    decide ((xa, xb) = (ya, yb)); firstorder.
  Program Instance lab_var_eq_eqdec : EqDec (Lab * Var) eq := Lab_var_dec.*)

  Parameter Val : Type.

  Definition State := Var -> Val.

  Parameter Val_dec : EqDec Val eq.
  Parameter Tag_dec : EqDec Tag eq.
  Parameter State_dec : EqDec State eq.

  Global Existing Instance Val_dec.
  Global Existing Instance Tag_dec.
  Global Existing Instance State_dec.

  Parameter S : list State.

  Definition Conf := ((@Coord Lab)* State)%type.

  Hint Unfold Conf Coord.

  Definition lab_of (k : Conf) :=
    match k with
      ((p, i), s) => p

Effect function

  Parameter eff' : Lab * State -> option (Lab * State).

  Definition eff (k : Conf) : option Conf
    := match k with
       | (p, i, s) => match eff' (p,s) with
                     | None => None
                     | Some (q, r) => match eff_tag p q i with
                                     | Some j => Some (q, j, r)
                                     | None => None

  Ltac eff_unf :=
    lazymatch goal with
    | H : context [eff (?q,?j,?r)] |- _
      => unfold eff, eff_tag in H;
        destruct (eff' (q,r));
        [match type of H with
         | context[let (_,_) := ?x in _ ]
           => let x1 := fresh "x" in
             let x2 := fresh "x" in
             destruct x as [x1 x2];
             decide (edge__P q x1);[|try congruence; try contradiction]
        |try congruence; try contradiction]
    | H : context [eff ?x] |- _
      => destruct x as [[? ?] ?]; eff_unf

  Ltac some_match_subst :=
    lazymatch goal with
    | H: match _ with
         | Some _ => Some (?x, _, _)
         | None => _
         end = Some (?y, _, _) |- _
      => let Q := fresh "Q" in
        assert (x = y) as Q;[
          destruct (match edge_Edge _ with
                    | Enormal _ => _
                    | Eback _ => _
                    | Eentry _ => _
                    | Eexit _ => _
            inversion H;subst;eauto

  Program Instance conf_eq_eqdec : EqDec Conf eq.
  Next Obligation.
    destruct x as [[p i] s], y as [[q j] r].

    destruct ((p, i, s) == (q, j, r)); firstorder.
  Definition Conf_dec := conf_eq_eqdec.

  Definition is_effect_on (p q : Lab) :=
    exists i i' s s', eff ((p, i), s) = Some ((q, i'), s').
  Parameter zero : State.

  Parameter edge_spec :
    forall p q, is_effect_on p q -> p --> q.

  Lemma step_conf_implies_edge :
    forall p q i j s r, eff (p, i, s) = Some (q, j, r) -> (p --> q).
    eapply edge_spec.
    unfold is_effect_on. eauto.

  Lemma eff_eff_tag q j r p i s :
    eff (q,j,r) = Some (p,i,s)
    -> eff_tag q p j = Some i.
    intros Heff.
    eff_unf. some_match_subst. unfold eff_tag.
    decide (edge__P q p);[|contradiction].
    unfold eff_tag.
    rewrite Edge_eq with (Q:=e).
    destruct (edge_Edge e);inversion Heff;subst;eauto.
    1,2: destruct j;inversion Heff;subst;eauto.

Edge on the Trace-Graph

  Definition eval_edge := (fun k k' : Conf
                           => match eff k with
                             | Some k => k = k'
                             | None => False

  Parameter def_spec :
    forall p q x, (exists i j s r, eff (p, i, s) = Some (q, j, r) /\ r x <> s x) ->
             is_def x p q = true.

  Definition option_chain (A B : Type) (f : A -> option B) (a : option A) : option B
    := match a with
       | Some a' => f a'
       | _ => None

  Definition sem_step l k := option_chain eff (hd_error l) = Some k.


  Inductive Tr : list Conf -> Prop :=
  | Init : forall s, s S -> Tr [(root, start_tag, s)]
  | Step : forall l (k : Conf), Tr l -> sem_step l k -> Tr (k :: l).

  Definition EPath := Path eval_edge.

  Hint Unfold Conf Coord.


  Lemma EPath_Tr s0 p i s π :
    s0 S -> EPath (root,start_tag,s0) (p,i,s) π -> Tr π.
    intros Hel H. remember (root, start_tag, s0) as start_c.
    remember (p,i,s) as pis_c. revert p i s Heqpis_c.
    induction H; intros p i s Heqpis_c; [rewrite Heqstart_c|];econstructor.
    2,3: destruct b as [[b1 b2] b3].
    - eauto.
    - eapply IHPath; eauto.
    - subst c. destruct π;[inversion H|].
      unfold sem_step;cbn.
      path_simpl' H.
      unfold eval_edge in H0. clear - H0.
      unfold Coord in *.
      destruct (eff (b1,b2,b3)).
      + subst. reflexivity.
      + contradiction.

  Lemma Tr_EPath p i s π :
    Tr π -> hd_error π = Some (p,i,s) -> exists s0, EPath (root,start_tag,s0) (p,i,s) π.
    intros HTr Hfront.
    revert p i s Hfront. dependent induction HTr; cbn; intros p i s' Hfront.
    - inversion Hfront. subst p i s'. eexists;econstructor.
    - inversion Hfront. subst k.
      remember (hd_error l) as c.
      destruct c.
      + destruct c as [[q j] r].
        specialize (IHHTr q j r). exploit IHHTr.
        destructH. eexists;econstructor;eauto.
        unfold eval_edge.
        unfold sem_step in H.
        destruct l;cbn in H;[congruence|]. unfold EPath in IHHTr. path_simpl' IHHTr.
        destruct (eff (q,j,r)).
        * inversion H;eauto.
        * congruence.
      + unfold sem_step in H. destruct l;cbn in *;congruence.

  Lemma eval_edge_tcfg_edge p q i j s r
        (Heval : eval_edge (q,j,r) (p,i,s))
    : tcfg_edge (q,j) (p,i).
    unfold eval_edge in Heval.
    - destruct (eff (q,j,r)) eqn:E;[|contradiction].
      eapply step_conf_implies_edge. subst c;eauto.
    - destruct (eff (q,j,r)) eqn:E;[subst c|contradiction].
      eff_unf. unfold eff_tag. some_match_subst. decide (edge__P q p);[|contradiction].
      rewrite (Edge_eq) with (Q:=e).
      destruct (edge_Edge e).
      all: inversion E;eauto.
      1,2: destruct j;[congruence|]; inversion E;eauto.

  Lemma EPath_TPath k k' π :
    EPath k k' π -> TPath (fst k) (fst k') (map fst π).
    intros H. dependent induction H; [|destruct c]; econstructor.
    - apply IHPath.
    - cbn. destruct b. cbn. destruct c0, c. eapply eval_edge_tcfg_edge;eauto.

  Definition proj_Tr_TPath (π : list Conf)
    := map fst π.

  Definition proj_Tr_TPath_list (T : list (list Conf))
    := map (map fst) T.

  Lemma EPath_TPath' k k' c c' π ϕ :
    EPath k k' π -> c = fst k -> c' = fst k' -> ϕ = map fst π -> TPath c c' ϕ.
    intros. eapply EPath_TPath in H;subst; eauto.

  Ltac inv_dep H Dec := inversion H; subst;
                        repeat match goal with
                               | [ H0: @existT _ _ _ _ = @existT _ _ _ _ |- _ ]
                                 => apply inj_pair2_eq_dec in H0; try (apply Dec); subst

  Ltac inv_tr H := inversion H; subst;
                   repeat match goal with
                          | [ H0: @existT Conf _ _ _ = @existT _ _ _ _ |- _ ]
                            => apply inj_pair2_eq_dec in H0; try (apply Conf_dec); subst

  Definition trace := {l : list Conf | Tr l}.

  Open Scope prg.

  Definition Traces := trace -> Prop.
  Definition Hyper := Traces -> Prop.

Concrete transformer

Concrete transformer for sets of traces

  Definition sem_trace (ts : Traces) : Traces :=
    fun tr' => exists tr k', ts tr /\ `tr' = (k' :: `tr).

Hypertrace transformer

  (* Essentially, it lifts the trace set transformers to set of trace sets *)
  Definition sem_hyper (T : Hyper) : Hyper :=
    fun ts' => exists ts, T ts /\ ts' = sem_trace ts.


  Lemma Tr_eff_Some c k t
        (Htr : Tr (c :: k :: t))
    : eff k = Some c.
    inversion Htr.
    unfold sem_step in H2. cbn in H2. eauto.

  Lemma in_pred_exists p i s k t :
    (p,i,s) (k :: t) ->
    p <> root ->
    Tr (k :: t) ->
    exists q j r, (q, j, r) t /\ eff (q, j, r) = Some (p, i, s).
    revert k.
    dependent induction t; intros k Hin Hneq Htr; inversion Htr.
    - exfalso.
      destruct Hin;[|contradiction].
      subst k. inversion H. eapply Hneq. rewrite H2. reflexivity.
    - inversion H1.
    - subst.
      destruct Hin.
      + subst k.
        destruct a as [[q j] r].
        exists q, j, r. split;[left;auto|].
        eapply Tr_eff_Some;eauto.
      + specialize (IHt a).
        exploit IHt.
        destructH. do 3 eexists;eauto.

  Lemma ivec_fresh : forall p i s (t : trace),
      sem_step (`t) (p, i, s) -> forall j r, In (p, j, r) (`t) -> j <> i.
    destruct t; cbn in *.
    remember (hd_error x) as c. destruct c.
    - destruct c,c. eapply eff_tag_fresh;cycle 2.
      + eapply in_map with (f:=fst) in H0. eauto.
      + eapply Tr_EPath in t;eauto. destruct t as [s1 t].
        eapply EPath_TPath in t; eauto.
      + destruct x;cbn in Heqc;[congruence|].
        inversion Heqc. subst c.
        unfold sem_step in H.
        unfold hd_error in H. unfold option_chain in H.
        { eapply step_conf_implies_edge;eauto. }
        cbn in H.
        destruct (eff' (e,s0)).
        * destruct p0. unfold eff_tag in *.
          decide (edge__P e e0). 2:congruence.
          decide (edge__P e p);[|congruence].
          rewrite (Edge_eq _ e1).
          destruct (edge_Edge e1);inversion H;eauto.
          1,2: destruct t0; inversion H;eauto.
        * congruence.
    - destruct x.
      + inversion t.
      + cbn in Heqc. congruence.

  Lemma ivec_det : forall q j r r' p i i' s s',
      eff (q, j, r) = Some (p, i, s) ->
      eff (q, j, r') = Some (p, i', s') ->
      i = i'.
    intros. eff_unf. eff_unf. some_match_subst. some_match_subst. auto.
    assert (x1 = p).
    { clear H0. some_match_subst. auto. }
    subst x1.
    rewrite (Edge_eq _ e0) in H0.
    destruct (edge_Edge e0);try congruence.
    1,2: destruct j;congruence.

  Definition Precedes' (l : list Conf) (k k' : Conf) : Prop :=
    exists l', Prefix (k' :: l') l /\ Precedes lab_of (k' :: l') k.

  Lemma start_no_tgt :
    forall i' s' k, eff k = Some (root, i', s') -> False.
    destruct k as [p i] s.
    unfold start_coord in H.
    cut (is_effect_on p root); intros.
    apply edge_spec in H0.
    eapply root_no_pred. eassumption.
    unfold is_effect_on.
    exists i, i', s, s'.

  Lemma precedes_cons (k k' : Conf) l : Precedes' l k' k' -> Precedes' (k :: l) k' k'.
    intro H. destruct H as [l' [H1 H2]].
    unfold Precedes'.
    exists l'. split; econstructor. eauto.

  Lemma precedes_self c t :
    In c t -> Precedes' t c c.
    intros H.
    destruct c as [[p i] s].
    induction t.
    + inv_tr H.
    + destruct a as [[q j] r].
      inv_tr H; eauto using Precedes.
      * rewrite H0. exists t. split; econstructor.
      * eapply precedes_cons; eauto.

  Lemma precedes_step_inv :
    forall k t p s, Precedes' (k :: t) p s ->
               Tr (k :: t) ->
               lab_of p <> lab_of s ->
               In p t.
    destruct H as [l [Hpre Hprec]].
    inv_tr Hprec.
    - firstorder.
    - eapply precedes_in in H5.
      eapply prefix_cons_cons in Hpre.
      eapply in_prefix_in; eauto.

  Lemma in_exists_pred p i s k (t : trace) :
    In (p, i, s) (k :: `t) ->
    sem_step (`t) k ->
    p <> root ->
    exists q j r, In (q, j, r) (`t) /\ eff (q, j, r) = Some (p, i, s).
    intros H Heff Hneq.
    destruct t as [l tr]; cbn in H, Heff. unfold "`".
    destruct H; [subst k| revert dependent k];
      dependent induction l; inversion tr; subst; intros.
    - exists root, start_tag, s0. split; [ constructor | eauto ]; eauto.
    - cbn in Heff, H2. destruct a as [[q j] r]. exists q,j,r. firstorder.
    - exfalso. inversion H; inversion H0. subst p; contradiction.
    - destruct H.
      + subst a. remember (hd_error l) as qjr. destruct qjr as [qjr|qjr].
        2: destruct l; unfold sem_step in H3;cbn in *;congruence.
        destruct qjr as [[q j] r].
        exists q,j,r. split; [econstructor 2 | eauto].
        * destruct l;[inversion H2|]. cbn in Heqqjr. inversion Heqqjr.
          setoid_rewrite H0. left. auto.
        * unfold sem_step in H3.
          destruct l;[inversion H2|].
          cbn in H3. cbn in Heqqjr. inversion Heqqjr. subst c. eauto.
      + eapply IHl in H2; eauto. destruct H2 as [q [j [r [Hin Hstep]]]].
        exists q, j, r. split; eauto.

  Lemma root_prefix (t : trace) : exists s, Prefix ((root, start_tag, s) :: nil) (`t).
    destruct t as [l tr].
    induction l; inversion tr; subst; cbn in *.
    - exists s. econstructor.
    - destruct IHl as [s IHl']; eauto. exists s. econstructor; eauto.

  Lemma root_start_tag s i (t : trace) : In (root, i, s) (`t) -> i = start_tag.
    intros Hin.
    revert dependent i.
    destruct t as [l tr]. induction l; inversion tr; subst; cbn in *; intros i Hin.
    - destruct Hin as [Hin|Hin]; [inversion Hin; eauto|contradiction].
    - destruct Hin.
      + exfalso. destruct l;[inversion H1|]. destruct c as [[q j] r].
        eapply root_no_pred. subst a.
        apply edge_spec. unfold is_effect_on. exists j,i,r,s.
        eapply Tr_eff_Some;eauto.
      + eapply IHl; eauto.

  Lemma trace_destr_in_in k k' (t : trace) :
    In k (`t) -> In k' (`t)
    -> exists (t': trace), hd_error (`t') = Some k' /\ In k (`t') \/ hd_error (`t') = Some k /\ In k' (`t').
    intros Hin Hin'.
    destruct t as [t tr]. cbn in *.
    induction t; inversion tr; cbn in *.
    - subst t. destruct Hin; [|contradiction]; destruct Hin'; [|contradiction].
      subst a k.
      exists (exist _ [k'] tr). cbn. tauto.
    - destruct Hin, Hin'; [| | |eapply IHt; eauto]; subst.
      + exists (exist _ (k' :: t) tr ). cbn. tauto.
      + exists (exist _ (k :: t) tr). cbn. tauto.
      + exists (exist _ (k' :: t) tr). cbn. tauto.

  Ltac trace_proj t :=
    lazymatch goal with
    | [ H : Tr t |- _ ] =>
      replace t with ( ` (exist Tr t H)) in * by (cbn; reflexivity)

  Lemma tag_inj p i s r (t : trace) : In (p,i,s) (`t) -> In (p,i,r) (`t) -> s = r.
    intros His Hir. eapply trace_destr_in_in in His; eauto.
    destruct His as [[t' tr'] [[Hf Hin]|[Hf Hin]]]; cbn in *.
    - induction t'; inversion tr'.
      + cbn in Hin,Hf. subst t'. destruct Hin; [|contradiction]. subst a. inversion Hf. reflexivity.
      + subst. cbn in *. destruct a as [[q j] r']. inversion Hf. subst.
        destruct Hin; [inversion H; reflexivity|].
        trace_proj t'.
        eapply ivec_fresh in H2; eauto. contradiction.
    - induction t'; inversion tr'.
      + cbn in Hin,Hf. subst t'. destruct Hin; [|contradiction]. subst a. inversion Hf. reflexivity.
      + cbn in *. subst. destruct a as [[q j] r']. inversion Hf. subst.
        destruct Hin; [inversion H; reflexivity|].
        trace_proj t'. eapply ivec_fresh in H2; eauto. contradiction.

  Lemma prefix_trace (l l' : list Conf) c :
    Prefix (c :: l) l' -> Tr l' -> Tr (c :: l).
    intros Hpr Htr. induction Htr;cbn in *.
    - inversion Hpr;[econstructor|]. 1:eauto. inversion H2.
    - inversion Hpr.
      + subst. econstructor;eauto.
      + eapply IHHtr;eauto.

  Lemma eval_det c0 c c' : eval_edge c0 c -> eval_edge c0 c' -> c = c'.
    intros Hcc Hcc'. unfold eval_edge in *. destruct (eff c0); subst;auto. contradiction.

(*  Lemma tr_succ_eq (l : list Conf) (k k' : Conf) :
    ne_back (k :: l) = ne_back (k' :: l) -> Tr (k :: l) -> Tr (k' :: l) -> k = k'.
    intros Hback Htr Htr'.
    inversion Htr; inversion Htr'; subst.
    1,2: destruct l;cbn in H0,H1;|congruence.
    3: destruct l;cbn in H3;|congruence.
    all: cbn in Hback;eauto.
    eapply necons_nlcons_inv in H2 as H21 H22;eapply necons_nlcons_inv in H as H01 H02.
    subst k0 k1. destruct l;exfalso;eapply ne_to_list_not_nil;eauto|.
    rewrite nlcons_to_list in H22. rewrite nlcons_to_list in H02.
    apply ne_to_list_inj in H22. apply ne_to_list_inj in H02. rewrite H22 in H4. rewrite H02 in H1.
    simpl_nl' H1. simpl_nl' H4.
    eapply eval_det; unfold eval_edge; rewrite H1|rewrite H4; conv_bool; reflexivity.

  Lemma prefix_eff_cons_cons k k' l l' :
    (*    eff (ne_front l) = Some k
    -> l' = ne_to_list l''
    -> Tr (k' :<: l'')
    -> Prefix l l'
    -> Prefix (k :: l) (k' :: l').

    l <> nil
    -> Tr (k :: l)
    -> Tr (k' :: l')
    -> Prefix l l'
    -> Prefix (k :: l) (k' :: l').
    intros Hemp Htr Htr' Hpre.
    revert dependent k'.
    induction Hpre; intros k' Htr'.
    - enough (k = k').
      + subst k'. econstructor.
      + destruct k as [[q j] r]. destruct k' as [[q' j'] r'].
        eapply Tr_EPath in Htr. 2: cbn;reflexivity.
        eapply Tr_EPath in Htr'. 2: cbn;reflexivity.
        do 2 destructH.
        inversion Htr. 1: symmetry in H4;contradiction.
        inversion Htr'. 1: symmetry in H9;contradiction.
        subst. destruct l. 1: inversion H0.
        path_simpl' H0. path_simpl' H5.
        eapply eval_det;eauto.
    - econstructor. eapply IHHpre; eauto. inversion Htr'; eauto.

  Lemma precedes_succ (t : trace) q j r q' j' r' p i s k' :
    Precedes' (`t) (q', j', r') (q, j, r) ->
    eff (q, j, r) = Some (p, i, s) ->
    p <> q' ->
    Tr (k' :: (`t)) ->
    Precedes' (k' :: (`t)) (q', j', r') (p, i, s).
    intros Hprec Heff Hneq Htr.
    destruct Hprec as [t' [Hpre Hprec]].
    exists ((q,j,r) :: t').
    - clear Hprec Hneq.
      unfold Conf in Hpre. unfold Coord in Hpre.
      set (t2 := (q,j,r) :: t') in *.
      destruct t as [t tr]. unfold "`" in *. cbn. subst t2.
      eapply prefix_eff_cons_cons; eauto;[congruence| eauto].
      cbn. econstructor.
      + eapply prefix_trace.
        * eauto.
        * inversion Htr; eauto. subst t. inversion Hpre.
      + eauto.
    - econstructor; cbn; eauto.

  (* possibly unused
  Lemma precedes_step l q j r p i s :
    forall k, (q, j, r) ∈ l ->
         p <> q ->
         eff (q, j, r) = Some (p, i, s) ->
         Tr (k :: l) ->
         Precedes' (k :: l) (q, j, r) (p, i, s).
    intros k Hin Hneq Heff Htr.
    assert ((p,i,s) ∈ (k :: l)) as Hin'.
      revert dependent k.
      induction l; intros k Htr; cbn in Htr; inversion Htr; inversion Hin; cbn; subst.
      - left. rewrite H2 in Heff. inversion Heff. reflexivity.
      - right. cbn in IHl. eauto.
    exists (prefix_nincl (p,i,s) (k :: l)). split.
    - eapply prefix_nincl_prefix; eauto.
    - revert dependent k. induction l; intros k Htr Hin'; inversion Hin; inversion Hin'; subst.
      + cbn. destruct ((p,i,s) == (p,i,s)); destruct e|exfalso; eapply c; reflexivity.
        econstructor; cbn; eauto|. destruct l; cbn; econstructor.
      + exfalso.
        inversion Htr; subst.
        assert (k = (p,i,s)) as Hk.
        { eapply Tr_eff_Some in Htr. rewrite Htr in Heff. inversion Heff. auto. }
        subst k.
        eapply ivec_fresh.
        * instantiate (4:=exist _ _ H2). unfold "`". eapply H3.
        * cbn. eauto.
        * reflexivity.
      + exfalso.
        inversion Htr; subst.
        destruct a as [q' j'] r'.
        eapply ivec_fresh.
        * instantiate (4:=exist _ _ H2). unfold "`". eauto.
        * cbn. give_up.
        * reflexivity.
      + cbn. destruct ((p,i,s) == k).
        * destruct e. exfalso.
          inversion Htr; subst.
          eapply ivec_fresh.
          -- instantiate (4:=exist _ _ Htr). unfold "`". eauto. give_up.
          -- cbn. eauto.
          -- reflexivity.
        * eapply IHl; eauto. cbn in Htr. inversion Htr; subst; eauto.

  Lemma no_def_untouched :
    forall p q x, is_def x q p = false -> forall i j s r, eff (q, j, r) = Some (p, i, s) -> r x = s x.
    specialize (@def_spec q p x).
    cut (forall (a b : Prop), (a -> b) -> (~ b -> ~ a)); intros Hrev; [| eauto].
    assert (Hds := def_spec).
    eapply Hrev in Hds.
    - cut (forall x y : Val, ~ (x <> y) -> x = y).
      * intros.
        apply H1; clear H1.
        intro. apply Hds.
        exists j; exists i; exists r; exists s; eauto.
      * intros y z. destruct (equiv_dec y z); intros; auto.
        exfalso. apply H1. auto.
    - intro.
      rewrite H in H1.
      inversion H1.

  Definition lift (tr : Traces) : Hyper :=
    fun ts => ts = tr.

  Definition red_prod (h h' : Hyper) : Hyper :=
    fun ts => h ts /\ h' ts.

  (* not used:
  Lemma postfix_rcons_trace_eff l k k' l' :
    Tr l'
    -> Postfix ((l :r: k) :r: k') l'
    -> eff k' = Some k.

  Lemma Tr_CPath l :
    Tr l -> CPath root (fst (fst (hd (root,start_tag,zero) l))) (map fst (map fst l)).
    intro H. destruct l;[inversion H|].
    eapply Tr_EPath in H;[| repeat rewrite <-surjective_pairing; reflexivity].
    destruct H as [s0 H]. cbn.
    eapply EPath_TPath in H. cbn in H. eapply TPath_CPath in H. eauto.

  Definition Tr' (l : list Conf) :=
    exists l', Tr l' /\ Postfix l l'.

  Lemma tr_lc_lt p i s1 s2 l1 l2 q1 q2 j1 j2 r1 r2
        (Htr1 : Tr ((p, i, s1) :: (q1,j1,r1) :: l1))
        (Htr2 : Tr ((p, i, s2) :: (q2,j2,r2) :: l2))
    : exists brk,
      last_common ((q1,j1) :: map fst l1) ((q2,j2) :: map fst l2) (brk).
    inversion Htr1. subst k l.
    inversion Htr2. subst k l.
    eapply Tr_EPath in H1. 2:cbn;eauto.
    eapply Tr_EPath in H3. 2:cbn;eauto.
    do 2 destructH.
    setoid_rewrite cons_rcons' in H1.
    setoid_rewrite cons_rcons' in H3.
    pose (l1' := (rev (tl (rev ((q1, j1, r1) :: l1))))).
    pose (l2' := (rev (tl (rev ((q2, j2, r2) :: l2))))).
    eapply path_back in H1 as Hback1. rewrite <-Hback1 in *.
    eapply path_back in H3 as Hback2. rewrite <-Hback2 in *.
    specialize (ne_last_common (map fst l1') (map fst l2') (root,start_tag)) as Hlc.
    exists s.
    enough ((q2,j2) :: map fst l2 = map fst l2' :r: (root,start_tag)).
    enough ((q1,j1) :: map fst l1 = map fst l1' :r: (root,start_tag)).
    * rewrite H. rewrite H0. eauto.
    * clear - Hback1. subst l1'.
      fold (fst (root,start_tag,s3)).
      rewrite <-map_rcons.
      rewrite Hback1.
      rewrite <-cons_rcons'. cbn. eauto.
    * clear - Hback2. subst l2'.
      fold (fst (root,start_tag,s0)).
      rewrite <-map_rcons.
      rewrite Hback2.
      rewrite <-cons_rcons'. cbn. eauto.

  Lemma tr_tpath_cons2 p i s q j r l
        (Htr : Tr ((p,i,s) :: (q,j,r) :: l))
    : TPath (root,start_tag) (p,i) ((p, i) :: (q, j) :: map fst l).
    eapply Tr_EPath in Htr as Htr; cbn;eauto. destruct Htr as [s01 Htr].
    eapply EPath_TPath in Htr.
    cbn in *. auto.

  Lemma Tr_NoDup l
        (Htr : Tr l)
    : NoDup (map fst l).
    destruct l;[inversion Htr|].
    destruct c as [[q j] r]. cbn.
    eapply Tr_EPath in Htr;[|cbn;reflexivity].
    eapply EPath_TPath in Htr. cbn in Htr.
    eapply tpath_NoDup;eauto.

  Lemma tr_lift_succ l q q' j j'
        (Hpath : Tr l)
        (Hsucc : (q',j') (q,j) | map fst l)
    : exists r r', (q',j',r') (q,j,r) | l.
    unfold succ_in in Hsucc. destructH.
    revert dependent l1. revert dependent l.
    induction l2;intros;cbn in Hsucc.
    - revert dependent l1. revert q q' j j'. induction l;intros.
      + cbn in *. congruence.
      + cbn in *. inversion Hpath;subst.
        1:cbn in Hsucc; congruence.
        exploit' IHl. destruct l1.
        * destruct a. inversion H1;subst;cbn in Hsucc; inversion Hsucc;[subst q j|].
          -- cbn in *.
             exists s0, s, nil, nil. cbn. reflexivity.
          -- exfalso. destruct l0; cbn in H6;[inversion H|congruence].
        * destruct a. cbn in *. destruct c.
          specialize (IHl e q t j l1). inversion Hsucc;subst. exploit IHl. destructH.
          exists r', s, ((e,t,r) :: (tl (tl l))), nil. cbn.
          unfold succ_in in IHl. destructH.
          destruct l2;cycle 1.
            eapply Tr_NoDup in H1.
            enough (fst c = (q,j)).
            - rewrite IHl in H1. cbn in H1. rewrite H in H1.
              rewrite map_app in H1. clear - H1.
              inversion H1. eapply H2.
              eapply in_or_app. right. auto.
            - clear - IHl Hsucc.
              inversion Hsucc. rewrite IHl in H0. cbn in H0.
              inversion H0. reflexivity.
          assert (l1 = map fst l0).
            cbn in IHl. clear - IHl H3.
            rewrite IHl in H3. cbn in H3. inversion H3. reflexivity.
          rewrite H in H3. cbn in IHl.
          inversion H1.
          -- exfalso. cbn in *. congruence.
          -- cbn in Hsucc,H2,H3. destruct k. cbn in Hsucc,H3.
             rewrite <-H5 in IHl.
             inversion H0.
             ++ cbn. destruct c. inversion IHl. subst. congruence.
             ++ cbn. destruct c. inversion IHl. subst. f_equal. f_equal. inversion H13. auto.
    - destruct l; cbn.
      + exfalso. destruct l2;cbn in Hsucc; inversion Hsucc.
      + cbn in Hsucc. inversion Hsucc.
        destruct l. 1: cbn in H1;congruence'.
        inversion Hpath;subst.
        eapply IHl2 in H1;eauto.
        destructH. do 2 eexists. eapply succ_cons. eauto.

  Lemma tr_succ_eff' p q q' br i j k s r r' r0 l
        (Htr : Tr ((p, i, s) :: l))
        (Hsucc : (q, j, r) (br, k, r0) | (p, i, s) :: l)
        (Heff : eff' (br,r0) = Some (q',r'))
    : q = q'.
    unfold succ_in in Hsucc. destructH.
    revert dependent l1. revert dependent l. revert p i s.
    induction l2;intros.
    - cbn in Hsucc.
      destruct l. 1: cbn in *; congruence.
      inversion Hsucc. subst.
      eapply Tr_eff_Some in Htr.
      eff_unf. some_match_subst. destruct (edge_Edge e); congruence.
    - cbn in Hsucc.
      destruct l. 1: cbn in *; destruct l2; cbn in Hsucc;congruence.
      destruct p0. destruct p0.
      eapply IHl2.
      + cbn in Htr. inversion Htr. eapply H1.
      + cbn in Hsucc. inversion Hsucc;subst. eauto.

  Lemma succ_in_rcons2 {A : Type} (a b : A) l
    : a b | l :r: a :r: b.
    exists nil, l. rewrite <-app_assoc. rewrite <-app_comm_cons. cbn. reflexivity.

  Lemma succ_in_cons_eq (A : Type) (a b c : A) l
        (Hsucc : a b | a :: c :: l)
        (Hnd : NoDup (a :: c :: l))
    : b = c.
    inversion Hnd. subst.
(*    destruct (b == c);auto|.*)
    unfold succ_in in Hsucc. destructH.
    destruct l2.
    - cbn in *. inversion Hsucc. auto.
    - exfalso.
      eapply H1. cbn in Hsucc. inversion Hsucc;subst.
      clear - H3. destruct l2;intros;inversion H3;subst;cbn in *;eauto.

  Lemma succ_in_cons_neq (A : Type) (a b c d : A) l
        (Hsucc : a b | d :: c :: l)
        (Hnd : NoDup (c :: l))
        (Hneq : a <> d)
    : a b | c :: l.
    unfold succ_in in Hsucc. destructH.
    destruct l2.
    - cbn in Hsucc. inversion Hsucc. subst. contradiction.
    - cbn in Hsucc. inversion Hsucc. subst. eexists;eexists. eauto.

  Lemma eff_tcfg p q i j s r
        (Heff : eff (p,i,s) = Some (q,j,r))
    : tcfg_edge (p,i) (q,j).
    eapply eff_eff_tag in Heff as Heff'. unfold tcfg_edge.
    eapply step_conf_implies_edge in Heff. conv_bool; firstorder.

  (* possibly unused
  Lemma tr_tpath_cons1 (l : list Conf) c
        (Htr : Tr (c :: l))
    : TPath (root,start_tag) (fst c) ((fst c) :: map fst l).
    revert dependent c.
    induction l; intros c Htr; inversion Htr; cbn; econstructor|. unfold TPath'. cbn.
    econstructor. eapply IHl;eauto.

    simpl_nl' H2. destruct a as [p i] s. destruct c as [q j] r. cbn. simpl_nl.
    eapply eff_tcfg;eauto.

  Lemma prec_lab_prec_fst p i s l
        (Hprec : Precedes lab_of l (p,i,s))
    : Precedes fst (map fst l) (p,i).
    induction l; inversion Hprec;subst;cbn in *.
    - econstructor.
    - econstructor;eauto.
      destruct a as [[a1 a2] a]; cbn in *;eauto.

End eval.

spot_path tactic

Ltac spot_path_e :=
  let H := fresh "H" in
  let Q := fresh "Q" in
  let p := fresh "p" in
  let i := fresh "i" in
  let s := fresh "s" in
  lazymatch goal with
  | [ H : Tr ((?p,?i,?s) :: ?t) |- _ ] => eapply Tr_EPath in H;[|cbn;reflexivity]; destructH' H; cbn in H
  | [ H : Tr ?t |- _ ] => destruct (hd_error t) as [[[p i] s]|N] eqn:Q;
                        [eapply Tr_EPath in H;[clear Q|apply Q]; destructH' H; cbn in H
                        |inversion H]

Ltac spot_path_t :=
  try spot_path_e;
  lazymatch goal with
  | [ H : EPath _ _ _ |- _ ] => eapply EPath_TPath in H; cbn in H

Ltac spot_path_c :=
  try spot_path_t;
  lazymatch goal with
    [ H : TPath _ _ _ |- _ ] => eapply TPath_CPath in H; cbn in H

Ltac spot_path :=
  lazymatch goal with
  | [ |- CPath _ _ _ ] => repeat (spot_path_c;eauto)
  | [ |- TPath _ _ _ ] => repeat (spot_path_t;eauto)
  | [ |- EPath _ _ _ ] => repeat (spot_path_e;eauto)