(****************************************************************
   File: hyll_temporal.v                                                 
   Authors: Amy Felty
   Version: Coq V8.4pl2
   Date: January 2014
                                                                 
   Instantiation of HyLL to time constraints plus model of the
   P53/Mdm2 DNA-damage repair mechanism.

  ***************************************************************)

Require Export BoolEq.
Require Export EqNat.
Require Export sl_hyll.

Notation "A ->> B" := (Imp A B) (at level 91, right associativity).
Notation "A &a B" := (ConjA A B) (at level 81, left associativity).
Notation "A +o B" := (DisjA A B) (at level 81, left associativity).
Notation "A *o B" := (ConjM A B) (at level 81, left associativity).
Notation "!! A" := (Bang A) (at level 71).
Notation "A 'at' w" := (At A w) (at level 72).
Notation "A @ w" := (atJ A w) (at level 92).

Section system.

(************************************************************************)
(* Instantiation of world, tm, atm, and definitions that depend on them *)
(************************************************************************)

Definition world:Set := nat.

Inductive tm:Set := p53 | mdm2 | dNAdam.

Inductive atm:Set :=
  | pres_atm: tm -> atm
  | abs_atm: tm -> atm.

Definition eqw := eq_nat.

Lemma eqw_symm: forall (w1 w2:world), eqw w1 w2 -> eqw w2 w1.
Proof.
unfold eqw; induction w1; induction w2; simpl; auto.
Qed.

Lemma eqw_trans:
  forall (w1 w2 w3:world), eqw w1 w2 -> eqw w2 w3 -> eqw w1 w3.
Proof.
unfold eqw; induction w1; induction w2; induction w3;
 simpl; auto.
tauto.
intros h1 h2; apply IHw1 with w2; auto.
Qed.

Add Parametric Relation : world eqw
  reflexivity proved by eq_nat_refl
  symmetry proved by eqw_symm
  transitivity proved by eqw_trans as w_eq.

Hint Resolve eq_nat_refl eqw_symm eqw_trans.

Definition beqtm : tm -> tm -> bool :=
  fun t1 t2 =>
    match t1, t2 with
      | p53, p53 => true
      | mdm2, mdm2 => true
      | dNAdam, dNAdam => true
      | _,_ => false
    end.

(* Note: We adopt the convention in this file that we append an
   underscore to the name of certain instantiated definitions (in
   particular, those definitions where we want to make the
   correspondence between the abstract and concrete names clear). *)

Definition minustm_ := minustm beqtm.
Definition eqtm_ := eqtm beqtm.

Lemma eqtm_refl: forall t:tm, eqtm_ t t.
Proof.
induction t; unfold eqtm_, eqtm; simpl; auto.
Qed.

Lemma eqtm_symm: forall (t1 t2:tm), eqtm_ t1 t2 -> eqtm_ t2 t1.
Proof.
induction t1; induction t2; unfold eqtm_, eqtm; simpl; auto.
Qed.

Lemma eqtm_trans:
  forall (t1 t2 t3:tm), eqtm_ t1 t2 -> eqtm_ t2 t3 -> eqtm_ t1 t3.
Proof.
induction t1; induction t2; induction t3; unfold eqtm_, eqtm; simpl; auto.
Qed.

Hint Resolve eqtm_refl eqtm_symm eqtm_trans.

Add Parametric Relation : tm eqtm_
  reflexivity proved by eqtm_refl
  symmetry proved by eqtm_symm
  transitivity proved by eqtm_trans as tm_eq.

Inductive eqatm : atm -> atm -> Prop :=
| eq_pres: forall (t1 t2:tm), eqtm_ t1 t2 -> eqatm (pres_atm t1) (pres_atm t2)
| eq_abs: forall (t1 t2:tm), eqtm_ t1 t2 -> eqatm (abs_atm t1) (abs_atm t2).

Hint Resolve eq_pres eq_abs.

Lemma eqatm_refl: forall a:atm, eqatm a a.
Proof.
induction a; auto.
Qed.

Lemma eqatm_symm: forall (a1 a2:atm), eqatm a1 a2 -> eqatm a2 a1.
Proof.
intros a1 a2; induction 1; auto.
Qed.

Lemma eqatm_trans:
  forall (a1 a2 a3:atm), eqatm a1 a2 -> eqatm a2 a3 -> eqatm a1 a3.
Proof.
intros a1 a2; induction 1; auto.
intro h; inversion_clear 0; eauto.
intro h; inversion_clear 0; eauto.
Qed.

Add Parametric Relation : atm eqatm
  reflexivity proved by eqatm_refl
  symmetry proved by eqatm_symm
  transitivity proved by eqatm_trans as atm_eq.

Hint Resolve eqatm_refl eqatm_symm eqatm_trans.

Definition down := (@Down world atm tm).

Definition oo_ := oo world atm tm.
Definition T_ := T world atm tm.
Definition One_ := One world atm tm.
Definition Zero_ := Zero world atm tm.
Definition delt_ : world -> oo_ -> oo_ := (delt plus).
Definition step : oo_ -> oo_ := (delt_ 1).
Definition atom0 := atom world.
Definition atom_ := atom0 atm tm.
Definition judg_ := judg world atm tm.
Definition mnil_ := mnil judg_.
Definition seq_: list judg_ -> multiset judg_ -> judg_ -> Prop :=
  seq eqw eqatm.

Definition pres (x:tm): oo_ := (atom_ (pres_atm x)).
Definition abs (x:tm): oo_ := (atom_ (abs_atm x)).

Definition eqoo_ : oo_ -> oo_ -> Prop := eqoo eqw eqatm.
Definition eqj_ : judg_ -> judg_ -> Prop := eqj eqw eqatm.
Definition eqctx_: multiset judg_ -> multiset judg_ -> Prop :=
  eqctx eqw eqatm.

Lemma eqoo__refl : forall (A:oo_), eqoo_ A A.
Proof.
intro A; unfold eqoo_,eqw; apply eqoo_refl; intro; eauto.
Qed.

Lemma eqoo__symm: forall (A B:oo_), eqoo_ A B -> eqoo_ B A.
Proof.
unfold eqoo_,eqw; intros A B h; apply eqoo_symm; eauto.
exact eqw_symm.
Qed.

Lemma eqoo__trans:
  forall (A B C:oo_), eqoo_ A B -> eqoo_ B C -> eqoo_ A C.
Proof.
unfold eqoo_,eqw; intros A B C h1 h2; apply eqoo_trans with B; eauto.
exact eqw_trans.
Qed.

Add Parametric Relation : oo_ eqoo_
  reflexivity proved by eqoo__refl
  symmetry proved by eqoo__symm
  transitivity proved by eqoo__trans as oo__eq.

Hint Resolve eqoo__refl eqoo__symm eqoo__trans.

Lemma eqj__refl: forall (J:judg_), eqj_ J J.
Proof.
intro J; unfold eqj_; apply eqj_refl; intro; eauto.
apply eq_nat_refl.
Qed.

Lemma eqj__symm: forall (J K:judg_), eqj_ J K -> eqj_ K J.
Proof.
unfold judg_,eqj_; intros J K h; apply eqj_symm; eauto.
Qed.

Lemma eqj__trans: forall (J K L:judg_), eqj_ J K -> eqj_ K L -> eqj_ J L.
Proof.
unfold judg_,eqj_; intros J K L h1 h2; apply eqj_trans with K; eauto.
Qed.

Add Parametric Relation : judg_ eqj_
  reflexivity proved by eqj__refl
  symmetry proved by eqj__symm
  transitivity proved by eqj__trans as j_eq_.

Hint Resolve eqj__refl eqj__symm eqj__trans.

Lemma eqctx__refl: forall (L:multiset judg_), eqctx_ L L.
Proof.
intro J; unfold eqctx_; apply eqctx_refl; intro; eauto.
Qed.

Lemma eqctx__symm: forall (L M:multiset judg_), eqctx_ L M -> eqctx_ M L.
Proof.
unfold eqctx_; intros J K h; apply eqctx_symm; eauto.
Qed.

Lemma eqctx__trans:
  forall (L M N:multiset judg_), eqctx_ L M -> eqctx_ M N -> eqctx_ L N.
Proof.
unfold eqctx_; intros J K L h1 h2; apply eqctx_trans with K; eauto.
Qed.

Add Parametric Relation : (multiset judg_) eqctx_
  reflexivity proved by eqctx__refl
  symmetry proved by eqctx__symm
  transitivity proved by eqctx__trans as ctx_eq_.

Hint Resolve eqctx__refl eqctx__symm eqctx__trans.

(************************************************************************
 * General Definitions for Modeling the Domain
 ************************************************************************)

Definition dont_care (t:tm): oo_ := (pres t +o abs t).

Fixpoint dont_cares (V:list tm): oo_ :=
  match V with
  | nil => One_
  | (t::nil) => (dont_care t)
  | (t::ts) => ((dont_care t) *o (dont_cares ts))
  end.

Definition unchanged1: tm -> world -> oo_ :=
  fun x w =>  (!! ((pres x at w ->> pres x at (w+1)) &a
                  (abs x at w ->> abs x at (w+1)))).

Fixpoint unchanged (V:list tm) (w:world) {struct V} : oo_ :=
  match V with
  | nil => One_
  | (t::nil) => (unchanged1 t w)
  | (t::ts) => ((unchanged1 t w) *o (unchanged ts w))
  end.

Fixpoint well_defined (V: list tm) : list oo_ :=
  match V with
  | nil => nil
  | (t::ts) => ((pres t *o abs t ->> Zero_)::
                (pres t +o abs t)::(well_defined ts))
  end.

Definition vars := (p53::mdm2::dNAdam::nil).

Definition oo2daggerJudg : oo_ -> judg_ :=
  fun A => (atJ (dagger A) 0).

(* ********************************************************************
 * General Rules
 ******************************************************************** *)

Definition active : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    ((pres a +o (pres a *o pres b) +o (pres a *o abs b)) ->>
     ((step (pres a *o pres b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u)))).

Definition active_c : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    ((pres a +o (pres a *o pres b) +o (pres a *o abs b)) ->>
     ((step (abs a *o pres b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u)))).

Definition active_s : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    ((abs a +o (abs a *o pres b) +o (abs a *o abs b)) ->>
     ((step (abs a *o abs b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u)))).

Definition inhib (V:list tm) (a b:tm): oo_ :=
    ((pres a +o (pres a *o pres b) +o (pres a *o abs b)) ->>
     ((step (pres a *o abs b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u)))).

Definition inhib_c : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    ((pres a +o (pres a *o pres b) +o (pres a *o abs b)) ->>
     ((step (abs a *o abs b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u)))).

Definition inhib_s : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    ((abs a +o (abs a *o pres b) +o (abs a *o abs b)) ->>
     ((step (abs a *o pres b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u)))).

Definition rule1 := inhib vars dNAdam mdm2.
Definition rule2 := inhib_s vars mdm2 p53.
Definition rule3 := active vars p53 mdm2.
Definition rule4 := inhib vars mdm2 p53.
Definition rule5 := inhib_c vars p53 dNAdam.
Definition rule6 := inhib_s vars dNAdam mdm2.
Definition system_oo :list oo_ :=
  (rule1::rule2::rule3::rule4::rule5::rule6::nil) ++ (well_defined vars).
Definition system := map oo2daggerJudg system_oo.

Inductive fireable: nat -> oo_ -> Prop :=
| f1: fireable 1 ((pres dNAdam +o (pres dNAdam *o pres mdm2) +o
                   (pres dNAdam *o abs mdm2)) *o (dont_care p53))
| f2: fireable 2 ((abs mdm2 +o (abs mdm2 *o pres p53) +o
                   (abs mdm2 *o abs p53)) *o (dont_care dNAdam))
| f3: fireable 3 ((pres p53 +o (pres p53 *o pres mdm2) +o
                   (pres p53 *o abs mdm2)) *o (dont_care dNAdam))
| f4: fireable 4 ((pres mdm2 +o (pres mdm2 *o pres p53) +o
                   (pres mdm2 *o abs p53)) *o (dont_care dNAdam))
| f5: fireable 5 ((pres p53 +o (pres p53 *o pres dNAdam) +o
                   (pres p53 *o abs dNAdam)) *o (dont_care mdm2))
| f6: fireable 6 ((abs dNAdam +o (abs dNAdam *o pres mdm2) +o
                   (abs dNAdam *o abs mdm2)) *o (dont_care p53)).

Inductive not_fireable: nat -> oo_ -> Prop :=
| nf1: not_fireable 1 (abs dNAdam *o (dont_cares (mdm2::p53::nil)))
| nf2: not_fireable 2 (pres mdm2 *o (dont_cares (p53::dNAdam::nil)))
| nf3: not_fireable 3 (abs p53 *o (dont_cares (mdm2::dNAdam::nil)))
| nf4: not_fireable 4 (abs mdm2 *o (dont_cares (p53::dNAdam::nil)))
| nf5: not_fireable 5 (abs p53 *o (dont_cares (dNAdam::mdm2::nil)))
| nf6: not_fireable 6 (pres dNAdam *o (dont_cares (mdm2::p53::nil))).

(* ********************************************************************
 * Strong Rules
 ******************************************************************** *)

Definition s_active : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    (pres a *o abs b) ->>
     ((step (pres a *o pres b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u))).

Definition s_active_c : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    (pres a *o abs b) ->>
     ((step (abs a *o pres b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u))).

Definition s_active_s : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    (abs a *o pres b) ->>
     ((step (abs a *o abs b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u))).

Definition s_inhib : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    (pres a *o pres b) ->>
     ((step (pres a *o abs b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u))).

Definition s_inhib_c : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    (pres a *o pres b) ->>
     ((step (abs a *o abs b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u))).

Definition s_inhib_s : list tm -> tm -> tm -> oo_ :=
  fun V a b =>
    (abs a *o abs b) ->>
     ((step (abs a *o pres b)) *o
      (Down (fun u => unchanged (minustm_ V (a::b::nil)) u))).

Definition s_rule1 := s_inhib vars dNAdam mdm2.
Definition s_rule2 := s_inhib_s vars mdm2 p53.
Definition s_rule3 := s_active vars p53 mdm2.
Definition s_rule4 := s_inhib vars mdm2 p53.
Definition s_rule5 := s_inhib_c vars p53 dNAdam.
Definition s_rule6 := s_inhib_s vars dNAdam mdm2.
Definition s_system_oo :list oo_ :=
  (s_rule1::s_rule2::s_rule3::s_rule4::s_rule5::s_rule6::nil) ++
  (well_defined vars).
Definition s_system := map oo2daggerJudg s_system_oo.

Inductive s_fireable: nat -> oo_ -> Set :=
| sf1: s_fireable 1 (pres dNAdam *o pres mdm2 *o dont_care p53)
| sf2: s_fireable 2 (abs mdm2 *o abs p53 *o dont_care dNAdam)
| sf3: s_fireable 3 (pres p53 *o abs mdm2 *o dont_care dNAdam)
| sf4: s_fireable 4 (pres mdm2 *o pres p53 *o dont_care dNAdam)
| sf5: s_fireable 5 (pres p53 *o pres dNAdam *o dont_care mdm2)
| sf6: s_fireable 6 (abs dNAdam *o abs mdm2 *o dont_care p53).

Inductive s_not_fireable: nat -> oo_ -> Set :=
| snf1: s_not_fireable 1 (((abs dNAdam *o pres mdm2) +o
                           (pres dNAdam *o abs mdm2) +o
                           (abs dNAdam *o abs mdm2)) *o (dont_care p53))
| snf2: s_not_fireable 2 (((pres mdm2 *o abs p53) +o
                           (abs mdm2 *o pres p53) +o
                           (pres mdm2 *o pres p53)) *o (dont_care dNAdam))
| snf3: s_not_fireable 3 (((abs p53 *o abs mdm2) +o
                           (pres p53 *o pres mdm2) +o
                           (abs p53 *o pres mdm2)) *o (dont_care dNAdam))
| snf4: s_not_fireable 4 (((abs mdm2 *o pres p53) +o
                           (pres mdm2 *o abs p53) +o
                           (abs mdm2 *o abs p53)) *o (dont_care dNAdam))
| snf5: s_not_fireable 5 (((abs p53 *o pres dNAdam) +o
                           (pres p53 *o abs dNAdam) +o
                           (abs p53 *o abs dNAdam)) *o (dont_care mdm2))
| snf6: s_not_fireable 6 (((pres dNAdam *o abs mdm2) +o
                           (abs dNAdam *o pres mdm2) +o
                           (pres dNAdam *o pres mdm2)) *o (dont_care p53)).

End system.

Definition state0 : oo_ := (abs p53 *o pres mdm2).
Definition state1 : oo_ := (pres p53 *o abs mdm2).

Hint Resolve eq_nat_refl eqw_symm eqw_trans.
Hint Resolve eqtm_refl eqtm_symm eqtm_trans.
Hint Resolve eqatm_refl eqatm_symm eqatm_trans.
Hint Resolve eqoo__refl eqoo__symm eqoo__trans.
Hint Resolve eqj__refl eqj__symm eqj__trans.
Hint Resolve eqctx__refl eqctx__symm eqctx__trans.
Hint Resolve eqoo_refl eqoo_symm eqoo_trans.
Hint Resolve eqj_refl eqj_symm eqj_trans.
Hint Resolve eqctx_refl eqctx_symm eqctx_trans.