(****************************************************************
   File: sl_hyll.v                                                 
   Authors: Amy Felty
   Version: Coq V8.4pl2
   Date: January 2014
                                                                 
   Hybrid linear logic as a specification logic
  ***************************************************************)

Require Export List.
Require Export Bool.
Require Export multiset.

Hint Resolve ms_eq_refl ms_eq_symm ms_eq_trans.

Section sl.

Set Implicit Arguments.

(****************************************************************
   HyLL connectives and inference rules
  ****************************************************************)

Variable world:Set.
Variable atm:Set.
Variable tm:Set.

(* need to enforce a monoid structure on world, but for now, just add this *)
Variable op: world -> world -> world.

Inductive oo : Set :=
  | atom : atm -> oo
  | T : oo
  | One : oo
  | Zero : oo
  | ConjA : oo -> oo -> oo
  | ConjM : oo -> oo -> oo
  | DisjA : oo -> oo -> oo
  | Imp : oo -> oo -> oo
  | Bang : oo -> oo
  | All : (tm -> oo) -> oo
  | Some : (tm -> oo) -> oo
  | At : oo -> world -> oo
  | Down: (world -> oo) -> oo
  | Wall : (world -> oo) -> oo
  | Wsome : (world -> oo) -> oo.

Definition box : oo -> oo :=
  fun A => (Down (fun u => (Wall (fun w => (At A (op u w)))))).
Definition diamond : oo -> oo :=
  fun A => (Down (fun u => (Wsome (fun w => (At A (op u w)))))).
Definition delt : world -> oo -> oo :=
  fun v A => (Down (fun u => (At A (op u v)))).
Definition dagger :  oo -> oo :=
  fun A => (Wall (fun u => (At A u))).

Inductive judg:Set :=
  atJ : oo -> world -> judg.

(****************************************************************
   Instantiation
  ****************************************************************)

Definition jnil := mnil judg.

(****************************************************************
   Equality
  ****************************************************************)

Variable beqtm:tm -> tm -> bool.

Fixpoint intm (t:tm) (ts:list tm) : bool :=
  match ts with
    | nil => false
    | t' :: ts' => (beqtm t t' || intm t ts')
  end.

Fixpoint minustm (ts1: list tm) (ts2 :list tm) : list tm :=
  match ts1 with
    | nil => nil
    | t::ts => if (intm t ts2) then (minustm ts ts2) else (t::(minustm ts ts2))
  end.

Definition eqtm:tm -> tm -> Prop := fun t1 t2 => (beqtm t1 t2) = true.
Hypothesis eqtm_refl: forall t:tm, eqtm t t.
Hypothesis eqtm_symm: forall (t1 t2:tm), eqtm t1 t2 -> eqtm t2 t1.
Hypothesis eqtm_trans:
  forall (t1 t2 t3:tm), eqtm t1 t2 -> eqtm t2 t3 -> eqtm t1 t3.

Variable eqworld:world -> world -> Prop.
Hypothesis eqworld_refl: forall w:world, eqworld w w.
Hypothesis eqworld_symm: forall (w1 w2:world), eqworld w1 w2 -> eqworld w2 w1.
Hypothesis eqworld_trans:
  forall (w1 w2 w3:world), eqworld w1 w2 -> eqworld w2 w3 -> eqworld w1 w3.

Variable eqatm:atm -> atm -> Prop.
Hypothesis eqatm_refl: forall p:atm, eqatm p p.
Hypothesis eqatm_symm: forall (p1 p2:atm), eqatm p1 p2 -> eqatm p2 p1.
Hypothesis eqatm_trans:
  forall (p1 p2 p3:atm), eqatm p1 p2 -> eqatm p2 p3 -> eqatm p1 p3.

Hint Resolve eqtm_refl eqtm_symm eqtm_trans
             eqworld_refl eqworld_symm eqworld_trans
             eqatm_refl eqatm_symm eqatm_trans : hyll.

Inductive eqoo: oo -> oo -> Prop  :=
  | eq_atm : forall (P1 P2:atm), eqatm P1 P2 -> eqoo (atom P1) (atom P2)
  | eq_T : eqoo T T
  | eq_One : eqoo One One
  | eq_Zero : eqoo Zero Zero
  | eq_ConjA : forall (A1 A2 B1 B2:oo), eqoo A1 B1 -> eqoo A2 B2 ->
      eqoo (ConjA A1 A2) (ConjA B1 B2)
  | eq_ConjM : forall (A1 A2 B1 B2:oo), eqoo A1 B1 -> eqoo A2 B2 ->
      eqoo (ConjM A1 A2) (ConjM B1 B2)
  | eq_DisjA : forall (A1 A2 B1 B2:oo), eqoo A1 B1 -> eqoo A2 B2 ->
      eqoo (DisjA A1 A2) (DisjA B1 B2)
  | eq_Imp : forall (A1 A2 B1 B2:oo), eqoo A1 B1 -> eqoo A2 B2 ->
      eqoo (Imp A1 A2) (Imp B1 B2)
  | eq_Bang : forall (A B:oo), eqoo A B -> eqoo (Bang A) (Bang B)
  | eq_All : forall (A B:tm -> oo),
      (forall x:tm, eqoo (A x) (B x)) -> eqoo (All A) (All B)
  | eq_Some : forall (A B:tm -> oo),
      (forall x:tm, eqoo (A x) (B x)) -> eqoo (Some A) (Some B)
  | eq_At : forall (A B:oo) (W U:world), eqoo A B -> eqworld W U ->
      eqoo (At A W) (At B U)
  | eq_Down : forall (A B:world -> oo),
      (forall w:world, eqoo (A w) (B w)) -> eqoo (Down A) (Down B)
  | eq_Wall : forall (A B:world -> oo),
      (forall w:world, eqoo (A w) (B w)) -> eqoo (Wall A) (Wall B)
  | eq_Wsome : forall (A B:world -> oo),
      (forall w:world, eqoo (A w) (B w)) -> eqoo (Wsome A) (Wsome B).

Hint Resolve eq_atm eq_T eq_One eq_Zero eq_ConjA eq_ConjM eq_DisjA
             eq_Imp eq_Bang eq_All eq_Some eq_At eq_Down eq_Wall
             eq_Wsome :hyll.

Lemma eqoo_refl: forall A:oo, eqoo A A.
Proof.
induction A; eauto with hyll.
Qed.

Lemma eqoo_symm: forall (A B:oo), eqoo A B -> eqoo B A.
Proof.
intros A B; induction 1; eauto with hyll.
Qed.

Lemma eqoo_trans:
  forall (A B C:oo), eqoo A B -> eqoo B C -> eqoo A C.
Proof.
intros A B C h; generalize h C; clear h C.
induction 1; intros C h'; eauto with hyll; inversion_clear h'; eauto with hyll.
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.

Definition eqj (j1 j2:judg) : Prop :=
  match j1 with
    | (atJ A W) =>
      match j2 with
        | (atJ B U) => (eqoo A B) /\ (eqworld W U)
      end
  end.

Lemma eqj_refl: forall (J:judg), eqj J J.
Proof.
unfold eqj; intros [A W]; auto.
Qed.

Lemma eqj_symm: forall (J K:judg), eqj J K -> eqj K J.
Proof.
intros [A W] [B U]; simpl.
intros [h1 h2]; split; auto.
Qed.

Lemma eqj_trans: forall (J K L:judg), eqj J K -> eqj K L -> eqj J L.
Proof.
intros [A W] [B U] [C V] [h1 h2] [h3 h4]; simpl; 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.

Definition eqctx := (ms_eq eqj).

Lemma eqctx_refl: forall (L:multiset judg), eqctx L L.
Proof.
unfold eqctx; auto.
Qed.

Lemma eqctx_symm: forall (L M:multiset judg), eqctx L M -> eqctx M L.
Proof.
unfold eqctx; eauto.
Qed.

Lemma eqctx_trans:
  forall (L M N:multiset judg), eqctx L M -> eqctx M N -> eqctx L N.
Proof.
unfold eqctx; 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.

(****************************************************************
   HyLL inference rules
  ****************************************************************)

Inductive seq : list judg -> multiset judg -> judg -> Prop :=
  | s_init :
      forall (Pt:atm) (W:world) (G:list judg),
      seq G (msingl (atJ (atom Pt) W)) (atJ (atom Pt) W)
  | s_copy :
      forall (A C:oo) (W U:world) (G:list judg) (D D':multiset judg),
      In (atJ A U) G ->
      eqctx D' (madd (atJ A U) D) ->
      seq G D' (atJ C W) ->
      seq G D (atJ C W)
  | s_ConjMR :
      forall (A B:oo) (W:world) (G:list judg) (D D' D'': multiset judg),
      eqctx D'' (munion D D') ->
      seq G D (atJ A W) ->
      seq G D' (atJ B W) ->
      seq G D'' (atJ (ConjM A B) W)
  | s_ConjML :
      forall (A B C:oo) (W U:world) (G:list judg) (D D' D'': multiset judg),
      eqctx D' (madd (atJ A U) (madd (atJ B U) D)) ->
      eqctx D'' (madd (atJ (ConjM A B) U) D) ->
      seq G D' (atJ C W) ->
      seq G D'' (atJ C W)
  | s_OneR :
      forall (W:world) (G:list judg), seq G jnil (atJ One W)
  | s_OneL :
      forall (C:oo) (W U:world) (G:list judg) (D D': multiset judg),
      eqctx D' (madd (atJ One U) D) ->
      seq G D (atJ C W) ->
      seq G D' (atJ C W)
  | s_ImpR :
      forall (A B:oo) (W:world) (G:list judg) (D D': multiset judg),
      D' = (madd (atJ A W) D) ->
      seq G D' (atJ B W) ->
      seq G D (atJ (Imp A B) W)
  | s_ImpL :
      forall (A B C:oo) (W U:world) (G:list judg) (D D' D1 D2: multiset judg),
      eqctx D1 (madd (atJ B U) D') ->
      eqctx D2 (madd (atJ (Imp A B) U) (munion D D')) ->
      seq G D (atJ A U) ->
      seq G D1 (atJ C W) ->
      seq G D2 (atJ C W)
  | s_TR :
      forall (W:world) (G:list judg) (D: multiset judg), seq G D (atJ T W)
  | s_ZeroL :
      forall (C:oo) (W U:world) (G:list judg) (D D': multiset judg),
      eqctx D' (madd (atJ Zero U) D) ->
      seq G D' (atJ C W)
  | s_ConjAR :
      forall (A B:oo) (W:world) (G:list judg) (D: multiset judg),
      seq G D (atJ A W) ->
      seq G D (atJ B W) ->
      seq G D (atJ (ConjA A B) W)
  | s_ConjAL1 :
      forall (A1 A2 C:oo) (W U:world) (G:list judg) (D D1 D2: multiset judg),
      eqctx D1 (madd (atJ A1 U) D) ->
      eqctx D2 (madd (atJ (ConjA A1 A2) U) D) ->
      seq G D1 (atJ C W) ->
      seq G D2 (atJ C W)
  | s_ConjAL2 :
      forall (A1 A2 C:oo) (W U:world) (G:list judg) (D D1 D2: multiset judg),
      eqctx D1 (madd (atJ A2 U) D) ->
      eqctx D2 (madd (atJ (ConjA A1 A2) U) D) ->
      seq G D1 (atJ C W) ->
      seq G D2 (atJ C W)
  | s_DisjAR1 :
      forall (A1 A2:oo) (W:world) (G:list judg) (D: multiset judg),
      seq G D (atJ A1 W) ->
      seq G D (atJ (DisjA A1 A2) W)
  | s_DisjAR2 :
      forall (A1 A2:oo) (W:world) (G:list judg) (D: multiset judg),
      seq G D (atJ A2 W) ->
      seq G D (atJ (DisjA A1 A2) W)
  | s_DisjAL :
      forall (A B C:oo) (W U:world) (G:list judg) (D D1 D2 D3: multiset judg),
      eqctx D1 (madd (atJ A U) D) ->
      eqctx D2 (madd (atJ B U) D) ->
      eqctx D3 (madd (atJ (DisjA A B) U) D) ->
      seq G D1 (atJ C W) ->
      seq G D2 (atJ C W) ->
      seq G D3 (atJ C W)
  | s_AllR :
      forall (A:tm -> oo) (W:world) (G:list judg) (D:multiset judg),
      (forall x:tm, seq G D (atJ (A x) W)) ->
      seq G D (atJ (All A) W)
  | s_AllL :
      forall (A:tm -> oo) (C:oo) (W U:world) (T:tm)
             (G:list judg) (D D1 D2:multiset judg),
      eqctx D1 (madd (atJ (A T) U) D) ->
      eqctx D2 (madd (atJ (All A) U) D) ->
      seq G D1 (atJ C W) ->
      seq G D2 (atJ C W)
  | s_SomeR :
      forall (A:tm -> oo) (W:world) (T:tm) (G:list judg) (D:multiset judg),
      seq G D (atJ (A T) W) ->
      seq G D (atJ (Some A) W)
  | s_SomeL :
      forall (A:tm -> oo) (C:oo) (W U:world)
             (G:list judg) (D1:tm -> multiset judg) (D D2:multiset judg),
      (forall x:tm, (D1 x) = (madd (atJ (A x) U) D) ->
                    seq G (D1 x) (atJ C W)) -> 
      eqctx D2 (madd (atJ (Some A) U) D) ->
      seq G D2 (atJ C W)
  | s_WallR :
      forall (A:world -> oo) (W:world) (G:list judg) (D:multiset judg),
      (forall v:world, seq G D (atJ (A v) W)) ->
      seq G D (atJ (Wall A) W)
  | s_WallL :
      forall (A:world -> oo) (C:oo) (W U:world) (V:world)
             (G:list judg) (D D1 D2:multiset judg),
      eqctx D1 (madd (atJ (A V) U) D) ->
      eqctx D2 (madd (atJ (Wall A) U) D) ->
      seq G D1 (atJ C W) ->
      seq G D2 (atJ C W)
  | s_WsomeR :
      forall (A:world -> oo) (W V:world) (G:list judg) (D:multiset judg),
      seq G D (atJ (A V) W) ->
      seq G D (atJ (Wsome A) W)
  | s_WsomeL :
      forall (A:world -> oo) (C:oo) (W U:world)
             (G:list judg) (D1:world -> multiset judg) (D D2:multiset judg),
      (forall v:world, (D1 v) = (madd (atJ (A v) U) D) ->
                       seq G (D1 v) (atJ C W)) ->
      eqctx D2 (madd (atJ (Wsome A) U) D) ->
      seq G D2 (atJ C W)
  | s_BangR :
      forall (A:oo) (W:world) (G:list judg),
      seq G jnil (atJ A W) ->
      seq G jnil (atJ (Bang A) W)
  | s_BangL :
      forall (A C:oo) (W U:world) (G:list judg) (D D':multiset judg),
      eqctx D' (madd (atJ (Bang A) U) D) ->
      seq (atJ A U::G) D (atJ C W) ->
      seq G D' (atJ C W)
  | s_AtR :
      forall (A:oo) (W U:world) (G:list judg) (D: multiset judg),
      seq G D (atJ A U) ->
      seq G D (atJ (At A U) W)
  | s_AtL :
      forall (A C:oo) (W U V:world) (G:list judg) (D D1 D2:multiset judg),
      eqctx D1 (madd (atJ A U) D) ->
      eqctx D2 (madd (atJ (At A U) V) D) ->
      seq G D1 (atJ C W) ->
      seq G D2 (atJ C W)
  | s_DownR :
      forall (A:world -> oo) (W:world) (G:list judg) (D: multiset judg),
      seq G D (atJ (A W) W) ->
      seq G D (atJ (Down A) W)
  | s_DownL :
      forall (A:world -> oo) (C:oo) (W V:world)
             (G:list judg) (D D1 D2:multiset judg),
      eqctx D1 (madd (atJ (A V) V) D) ->
      eqctx D2 (madd (atJ (Down A) V) D) ->
      seq G D1 (atJ C W) ->
      seq G D2 (atJ C W).

Hint Resolve s_init s_copy s_ConjMR s_ConjML s_OneR s_OneL s_ImpR s_ImpL
             s_TR s_ZeroL s_ConjAR s_ConjAL1 s_ConjAL2 s_DisjAR1 s_DisjAR2
             s_DisjAL s_AllR s_AllL s_SomeR s_SomeL s_WallR s_WallL
             s_WsomeR s_WsomeL s_BangR s_BangL s_AtR s_AtL s_DownR
             s_DownL : hyll.

(* Structural Rules *)
Theorem structural :
  forall (J:judg) (G G':list judg) (D:multiset judg),
  (forall j:judg, In j G -> In j G') ->
  seq G D J -> seq G' D J.
intros J G G' D H H0.
generalize H0 G' H; clear H0 H G'.
simple induction 1; try auto with hyll.  (* auto takes care of 11 cases *)
(* s_copy *)
eauto with hyll.
(* s_ConjMR *)
intros A B W G0 D0 D' D'' H H1 H2 H3 H4 G' H5.
apply s_ConjMR with D0 D'; auto.
(* s_ConjML *)
intros A B C W U G0 D0 D' D'' H H1 H2 H3 G' H4.
apply s_ConjML with A B U D0 D'; auto.
(* s_OneL *)
eauto with hyll.
(* s_ImpR *)
intros A B W G0 D0 D' H H1 H2 G' H3.
apply s_ImpR with D'; auto.
(* s_ImpL *)
intros A B C W U G0 D0 D' D1 D2 H H1 H2 H3 H4 H5 G' H6.
apply s_ImpL with A B U D0 D' D1; auto.
(* s_ZeroL *)
eauto with hyll.
(* s_ConjAL1 *)
intros A1 A2 C W U G0 D0 D1 D2 H H1 H2 H3 G' H4.
apply s_ConjAL1 with A1 A2 U D0 D1; auto.
(* s_ConjAL2 *)
intros A1 A2 C W U G0 D0 D1 D2 H H1 H2 H3 G' H4.
apply s_ConjAL2 with A1 A2 U D0 D1; auto.
(* s_DisjAL *)
intros A B C W U G0 D0 D1 D2 D3 H H1 H2 H3 H4 H5 H6 G' H7.
apply s_DisjAL with A B U D0 D1 D2; auto.
(* s_AllL *)
intros A C W U T0 G0 D0 D1 D2 H H1 H2 H3 G' H4.
apply s_AllL with A U T0 D0 D1; auto.
(* s_SomeR *)
intros A W T0 G0 D0 H H1 G' H2.
apply s_SomeR with T0; auto.
(* s_SomeL *)
intros A C W U G0 D1 D0 D2 H H1 H2 G' H3.
apply s_SomeL with A U D1 D0; auto.
(* s_WallL *)
intros A C W U V G0 D0 D1 D2 H H1 H2 H3 G' H4.
apply s_WallL with A U V D0 D1; auto.
(* s_WsomeR *)
intros A W V G0 D0 H H1 G' H2.
apply s_WsomeR with V; auto.
(* s_WsomeL *)
intros A C W U G0 D1 D0 D2 H H1 H2 G' H3.
apply s_WsomeL with A U D1 D0; auto.
(* s_BangL *)
intros A C W U G0 D0 D' H H1 H2 G' H3.
apply s_BangL with A U D0; auto.
apply H2; auto.
intro j; specialize H3 with (j:=j); intros [h | h].
simpl; auto.
simpl; right; apply H3; auto.
(* s_atL *)
intros A C W U V G0 D0 D1 D2 H H1 H2 H3 G' H4.
apply s_AtL with A U V D0 D1; auto.
(* s_DownL *)
intros A C W V G0 D0 D1 D2 H H1 H2 H3 G' H4.
apply s_DownL with A V D0 D1; auto.
Qed.

Unset Implicit Arguments.

End sl.