Require Import List.
Import List.ListNotations.
Open Scope list_scope.
Require Import Omega Preamble Term.

Inductive St: Set :=
| stop: Plc → Evidence → St
| conf: AnnoTerm → Plc → Evidence → St
| rem: Plc → Plc → St → St
| ls: St → AnnoTerm → St
| bsl: nat → St → AnnoTerm → Plc → Evidence → St
| bsr: nat → Evidence → St → St
| bp: nat → St → St → St.

Fixpoint pl (s:St) :=
  match s with
  | stop p _ ⇒ p
  | conf _ p _ ⇒ p
  | rem _ p _ ⇒ p
  | ls st _ ⇒ pl st
  | bsl _ _ _ p _ ⇒ p
  | bsr _ _ st ⇒ pl st
  | bp _ _ st ⇒ pl st
  end.

Fixpoint seval st :=
  match st with
  | stop _ e ⇒ e
  | conf t p e ⇒ aeval t p e
  | rem _ _ st ⇒ seval st
  | ls st t ⇒ aeval t (pl st) (seval st)
  | bsl _ st t p e ⇒ ss (seval st) (aeval t p e)
  | bsr _ e st ⇒ ss e (seval st)
  | bp _ st0 st1 ⇒ pp (seval st0) (seval st1)
end.

Inductive step: St → option Ev → St → Prop :=

| stasp:
    ∀ r x p e,
      step (conf (aasp r x) p e)
           (Some (asp_event (fst r) x p e))
           (stop p (aeval (aasp r x) p e))

| statt:
    ∀ r x p q e,
      step (conf (aatt r q x) p e)
           (Some (req (fst r) p q e))
           (rem (snd r) p (conf x q e))
| stattstep:
    ∀ st0 ev st1 p j,
      step st0 ev st1 →
      step (rem j p st0) ev (rem j p st1)
| stattstop:
    ∀ j p q e,
      step (rem j p (stop q e))
           (Some (rpy (pred j) p q e))
           (stop p e)

| stlseq:
    ∀ r x y p e,
      step (conf (alseq r x y) p e)
           None
           (ls (conf x p e) y)
| stlseqstep:
    ∀ st0 ev st1 t,
      step st0 ev st1 →
      step (ls st0 t) ev (ls st1 t)
| stlseqstop:
    ∀ t p e,
      step (ls (stop p e) t) None (conf t p e)

| stbseq:
    ∀ r s x y p e,
      step (conf (abseq r s x y) p e)
           (Some (split (fst r) p e (sp (fst s) e)
                        (sp (snd s) e)))
           (bsl (snd r) (conf x p (sp (fst s) e))
                y p (sp (snd s) e))
| stbslstep:
    ∀ st0 ev st1 j t p e,
      step st0 ev st1 →
      step (bsl j st0 t p e) ev (bsl j st1 t p e)
| stbslstop:
    ∀ j e e' t p p',
      step (bsl j (stop p e) t p' e')
           None
           (bsr j e (conf t p' e'))
| stbsrstep:
    ∀ st0 ev st1 j e,
      step st0 ev st1 →
      step (bsr j e st0) ev (bsr j e st1)
| stbsrstop:
    ∀ j e p e',
      step (bsr j e (stop p e'))
           (Some (join (pred j) p e e' (ss e e')))
           (stop p (ss e e'))

| stbpar:
    ∀ r s x y p e,
      step (conf (abpar r s x y) p e)
           (Some (split (fst r) p e
                        (sp (fst s) e)
                        (sp (snd s) e)))
           (bp (snd r)
               (conf x p (sp (fst s) e))
               (conf y p (sp (snd s) e)))
| stbpstepleft:
    ∀ st0 st1 st2 ev j,
      step st0 ev st2 →
      step (bp j st0 st1) ev (bp j st2 st1)
| stbpstepright:
    ∀ st0 st1 st2 ev j,
      step st1 ev st2 →
      step (bp j st0 st1) ev (bp j st0 st2)
| stbpstop:
    ∀ j p e p' e',
      step (bp j (stop p e) (stop p' e'))
           (Some (join (pred j) p' e e' (pp e e')))
           (stop p' (pp e e')).
Hint Constructors step.

Lemma step_pl_eq:
  ∀ st0 ev st1,
    step st0 ev st1 → pl st0 = pl st1.

Lemma step_seval:
  ∀ st0 ev st1,
    step st0 ev st1 →
    seval st0 = seval st1.

Inductive lstar: St → list Ev → St → Prop :=
| lstar_refl: ∀ st, lstar st [] st
| lstar_tran: ∀ st0 e st1 tr st2,
    step st0 (Some e) st1 → lstar st1 tr st2 → lstar st0 (e :: tr) st2
| lstar_silent_tran: ∀ st0 st1 tr st2,
    step st0 None st1 → lstar st1 tr st2 → lstar st0 tr st2.
Hint Resolve lstar_refl.

Lemma lstar_transitive:
  ∀ st0 tr0 st1 tr1 st2,
    lstar st0 tr0 st1 →
    lstar st1 tr1 st2 →
    lstar st0 (tr0 ++ tr1) st2.

Inductive star: St → St → Prop :=
| star_refl: ∀ st, star st st
| star_tran: ∀ st0 e st1 st2,
    step st0 e st1 → star st1 st2 → star st0 st2.
Hint Resolve star_refl.

Lemma star_transitive:
  ∀ st0 st1 st2,
    star st0 st1 →
    star st1 st2 →
    star st0 st2.

Lemma lstar_star:
  ∀ st0 tr st1,
    lstar st0 tr st1 → star st0 st1.

Lemma star_lstar:
  ∀ st0 st1,
    star st0 st1 → ∃ tr, lstar st0 tr st1.

Lemma star_seval:
  ∀ st0 st1,
    star st0 st1 → seval st0 = seval st1.

Lemma steps_preserves_eval:
  ∀ t p p' e0 e1,
    star (conf t p e0) (stop p' e1) →
    aeval t p e0 = e1.

Lemma star_strem:
  ∀ st0 st1 j p,
    star st0 st1 → star (rem j p st0) (rem j p st1).

Lemma star_stls:
  ∀ st0 st1 t,
    star st0 st1 → star (ls st0 t) (ls st1 t).

Lemma star_stbsl:
  ∀ st0 st1 j t p e,
    star st0 st1 →
    star (bsl j st0 t p e) (bsl j st1 t p e).

Lemma star_stbsr:
  ∀ st0 st1 j e,
    star st0 st1 →
    star (bsr j e st0) (bsr j e st1).

Lemma star_stbp:
  ∀ st0 st1 st2 st3 j,
    star st0 st1 →
    star st2 st3 →
    star (bp j st0 st2) (bp j st1 st3).

Theorem correct_path_exists:
  ∀ t p e,
    star (conf t p e) (stop p (aeval t p e)).

Definition halt st :=
  match st with
  | stop _ _ ⇒ True
  | _ ⇒ False
  end.

Theorem never_stuck:
  ∀ st0,
    halt st0 ∨ ∃ e st1, step st0 e st1.

Inductive nstar: nat → St → St → Prop :=
| nstar_refl: ∀ st, nstar 0 st st
| nstar_tran: ∀ st0 st1 st2 e n,
    nstar n st0 st1 → step st1 e st2 → nstar (S n) st0 st2.
Hint Resolve nstar_refl.

Lemma nstar_transitive:
  ∀ m n st0 st1 st2,
    nstar m st0 st1 →
    nstar n st1 st2 →
    nstar (m + n) st0 st2.

Lemma nstar_star:
  ∀ n st0 st1,
    nstar n st0 st1 → star st0 st1.

Lemma star_nstar:
  ∀ st0 st1,
    star st0 st1 →
    ∃ n, nstar n st0 st1.

Fixpoint tsize t: nat :=
  match t with
  | aasp _ _ ⇒ 1
  | aatt _ _ x ⇒ 2 + tsize x
  | alseq _ x y ⇒ 2 + tsize x + tsize y
  | abseq _ _ x y ⇒ 3 + tsize x + tsize y
  | abpar _ _ x y ⇒ 2 + tsize x + tsize y
  end.

Fixpoint ssize s: nat :=
  match s with
  | stop _ _ ⇒ 0
  | conf t _ _ ⇒ tsize t
  | rem _ _ x ⇒ 1 + ssize x
  | ls x t ⇒ 1 + ssize x + tsize t
  | bsl _ x t _ _ ⇒ 2 + ssize x + tsize t
  | bsr _ _ x ⇒ 1 + ssize x
  | bp _ x y ⇒ 1 + ssize x + ssize y
  end.

Lemma halt_size:
  ∀ st,
    halt st ↔ ssize st = 0.

Lemma step_size:
  ∀ st0 e st1,
    step st0 e st1 →
    S (ssize st1) = ssize st0.

Lemma step_count:
  ∀ n t p e st,
    nstar n (conf t p e) st →
    tsize t = n + ssize st.

Theorem steps_to_stop:
  ∀ t p e st,
    nstar (tsize t) (conf t p e) st →
    halt st.

Inductive nlstar: nat → St → list Ev → St → Prop :=
| nlstar_refl: ∀ st, nlstar 0 st [] st
| nlstar_tran: ∀ n st0 e st1 tr st2,
    step st0 (Some e) st1 → nlstar n st1 tr st2 → nlstar (S n) st0 (e :: tr) st2
| nlstar_silent_tran: ∀ n st0 st1 tr st2,
    step st0 None st1 → nlstar n st1 tr st2 → nlstar (S n) st0 tr st2.
Hint Resolve nlstar_refl.

Lemma nlstar_transitive:
  ∀ m n st0 tr0 st1 tr1 st2,
    nlstar m st0 tr0 st1 →
    nlstar n st1 tr1 st2 →
    nlstar (m + n) st0 (tr0 ++ tr1) st2.

Lemma nlstar_lstar:
  ∀ n st0 tr st1,
    nlstar n st0 tr st1 → lstar st0 tr st1.

Lemma lstar_nlstar:
  ∀ st0 tr st1,
    lstar st0 tr st1 →
    ∃ n, nlstar n st0 tr st1.

Lemma nlstar_step_size:
  ∀ n st0 tr st1,
    nlstar n st0 tr st1 →
    ssize st1 ≤ ssize st0.

Lemma lstar_nlstar_size:
  ∀ st0 tr st1,
    lstar st0 tr st1 →
    nlstar (ssize st0 - ssize st1) st0 tr st1.

Inductive rlstar: nat → St → list Ev → St → Prop :=
| rlstar_refl: ∀ st, rlstar 0 st [] st
| rlstar_tran: ∀ n st0 e st1 tr st2,
    rlstar n st0 tr st1 → step st1 (Some e) st2 →
    rlstar (S n) st0 (tr ++ [e]) st2
| rlstar_silent_tran: ∀ n st0 st1 tr st2,
    rlstar n st0 tr st1 → step st1 None st2 →
    rlstar (S n) st0 tr st2.
Hint Resolve rlstar_refl.

Lemma rlstar_transitive:
  ∀ m n st0 tr0 st1 tr1 st2,
    rlstar m st0 tr0 st1 →
    rlstar n st1 tr1 st2 →
    rlstar (m + n) st0 (tr0 ++ tr1) st2.

Lemma rlstar_lstar:
  ∀ n st0 tr st1,
    rlstar n st0 tr st1 → lstar st0 tr st1.

Lemma lstar_rlstar:
  ∀ st0 tr st1,
    lstar st0 tr st1 →
    ∃ n, rlstar n st0 tr st1.

Lemma rlstar_nlstar:
  ∀ n st0 tr st1,
    rlstar n st0 tr st1 ↔ nlstar n st0 tr st1.