(****************************************************************
  Copyright © 2016, 2024  Chelsea Battell, Alberto Momigliano, and Amy Felty

  This file is part of "Two-Level Hybrid in Coq"

  This program is free software: you can redistribute it and/or modify
  it under the terms of the GNU General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
  (at your option) any later version.

  This program is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  GNU General Public License for more details.

  You should have received a copy of the GNU General Public License
  along with this program.  If not, see <https://www.gnu.org/licenses/>.
  ***************************************************************)
(****************************************************************
   File: Hsl.v                                                 

   Date: Apr 2016
   Apr 2024: Current Coq Version: V8.18.0
                                                                 
   An intuitionistic sequent calculus used as a specification
   logic in the style of Abella 2.0
  ***************************************************************)


From HybridSys Require Export Hybrid.
Require Export Ensembles.

(*****
Ensembles documentation:
 https://coq.inria.fr/library/Coq.Sets.Ensembles.html
****)

Set Implicit Arguments.

Section Hsl.

(****************************************************************
   The intuitionistic object logic.
  ****************************************************************)

Variable atm : Set.
Variable con : Set.
Variable X : Set.

Inductive oo : Type :=
  | atom : atm -> oo
  | T : oo
  | Conj : oo -> oo -> oo
  | Imp : oo -> oo -> oo
  | All : (expr con -> oo) -> oo 
  | Allx : (X -> oo) -> oo
  | Some : (expr con -> oo) -> oo.

Variable prog : atm -> oo -> Prop.

Notation "a & b" := (Conj a b) (at level 60, right associativity). 
Notation "a ---> b" := (Imp a b) (at level 61, right associativity).
Notation "<< a >>" := (atom a) (at level 30). 

Notation "A :- b" := (prog A b) (at level 61).


(** Contexts **)

Definition context := Ensemble oo.

Definition empty_con : context := Empty_set oo.

Definition context_cons (c : context) (o : oo) : context :=
 Add oo c o.

Definition elem (o : oo) (c : context) := In oo c o.

Notation " '{}' " := empty_con (at level 50).
Notation " c ',,' o " := (context_cons c o)
  (at level 45, left associativity).

(** Context Lemmas **)

Lemma elem_sub : forall (c : context) (o1 o2 : oo),
 elem o1 c -> elem o1 (c ,, o2).
Proof.
intros; apply Union_introl; auto.
Qed.

Lemma elem_inv : forall (c : context) (o1 o2 : oo),
 elem o1 (c,, o2) -> (elem o1 c \/ o1 = o2).
Proof.
 intros c0 o F Helem;
 inversion Helem; subst.
 apply or_introl; assumption.
 apply or_intror; inversion H; reflexivity.
Qed.

Lemma elem_self : forall (c : context) (o : oo),
 elem o (c ,, o).
Proof.
 intros; apply Union_intror;
 apply In_singleton.
Qed.

Lemma elem_rep : forall (c : context) (o1 o2 : oo),
 elem o1 (c,, o2,, o2) -> elem o1 (c ,, o2).
Proof.
 intros c t1 t2 H;
 apply elem_inv in H.
 inversion H as [Hl | Hr]; clear H; auto.
 subst; apply elem_self.
Qed.

Lemma context_swap : forall (c : context) (o1 o2 : oo),
(c,, o1,, o2) = (c,, o2,, o1).
Proof.
 intros.
 apply Extensionality_Ensembles.
 unfold Same_set.
 split; intros o3 H; apply elem_inv in H;
 inversion H as [H1 | H2]; subst; clear H.
 apply elem_inv in H1; inversion H1;
 subst; clear H1.
 repeat (apply elem_sub); auto.
 apply elem_self.
 apply elem_sub; apply elem_self.
 apply elem_inv in H1; inversion H1;
 subst; clear H1.
 repeat (apply elem_sub); auto.
 apply elem_self.
 apply elem_sub; apply elem_self.
Qed.

Definition con_subset (L1 L2 : context) :=
 forall (o : oo), elem o L1 -> elem o L2.

Lemma con_sub_sup : forall (L1 L2 : context) (o : oo),
 con_subset L1 L2 -> con_subset (L1,, o) (L2,, o).
Proof.
Hint Resolve elem_sub elem_self : hsl.
intros L1 L2 o H o0 Helem.
apply elem_inv in Helem; inversion Helem;
clear Helem; subst; auto with hsl.
Qed.



(** Sequents **)

(*
generalized rule
Q_i ->
\forall <x_j : R_j>, seq (L_{1_j}) (o_{1_j}) ->
\forall <y_k : S_k>, bch (L_{2_k}) (o_{2_k}) (a_k) ->
seq c o (resp. bch c o a)
*)

Inductive grseq : context -> oo -> Prop :=
  | g_prog :    (* i=1, j=1, k=0 *)
      forall (L : context) (G : oo) (A : atm),
      (A :- G) -> grseq L G
      -> grseq L (<< A >>)
  | g_dyn :    (* i=1, j=0, k=1 *)
      forall (L : context) (D : oo) (A : atm),
      elem D L -> bcseq L D A
      -> grseq L (<< A >>)
  | g_tt :    (* i=0, j=0, k=0 *)
      forall (L : context), grseq L T
  | g_and :    (* i=0, j=2, k=0 *)
      forall (L : context) (G1 G2 : oo),
      grseq L G1 -> grseq L G2
      -> grseq L (G1 & G2)
  | g_imp :    (* i=0, j=1, k=0 *)
      forall (L : context) (D G : oo),
      grseq (L,, D) G
      -> grseq L (D ---> G)
  | g_all :    (* i=0, j=1, k=0 *)
      forall (L : context) (G : expr con -> oo),
      (forall E : expr con, proper E -> grseq L (G E))
      -> grseq L (All G)
  | g_allx :    (* i=0, j=1, k=0 *)
      forall (L : context) (G : X -> oo),
      (forall E : X, grseq L (G E))
      -> grseq L (Allx G)
  | g_some :    (* i=1, j=1, k=0*)
      forall (L : context) (G : expr con -> oo) (E : expr con),
      proper E -> grseq L (G E)
      -> grseq L (Some G)

with bcseq : context -> oo ->  atm -> Prop :=
 | b_match :    (* i=0, j=0, k=0 *)
     forall (L : context) (A : atm),
     bcseq L (<< A >>) A
 | b_and1 :    (* i=0, j=0, k=1 *)
     forall (L : context) (D1 D2 : oo) (A : atm),
     bcseq L D1 A
     -> bcseq L (D1 & D2) A
 | b_and2 :    (* i=0, j=0, k=1 *)
     forall (L : context) (D1 D2 : oo) (A : atm),
     bcseq L D2 A
     -> bcseq L (D1 & D2) A
 | b_imp :    (* i=0, j=1, k=1 *)
      forall (L : context) (D G : oo) (A : atm),
      grseq L G -> bcseq L D A
     -> bcseq L (G ---> D) A
 | b_all :    (* i=1, j=0, k=1 *)
     forall (L : context) (D : expr con -> oo) (E : expr con) (A : atm),
     proper E -> bcseq L (D E) A
     -> bcseq L (All D) A
 | b_allx :    (* i=0, j=0, k=1 *)
     forall (L : context) (D : X -> oo) (E : X) (A : atm),
     bcseq L (D E) A
     -> bcseq L (Allx D) A
 | b_some :    (* i=0, j=0, k=1 *)
     forall (L : context) (D : expr con -> oo) (A : atm),
     (forall E : expr con, proper E -> bcseq L (D E) A)
     -> bcseq L (Some D) A.

Tactic Notation "inv_and_sub" tactic(h) :=
  inversion h; subst; clear h; try trivial.


(* Minimality - used to define induction principle for mutually inductive type *)

Scheme gr_bc_seq := Minimality for grseq Sort Prop
  with bc_gr_seq := Minimality for bcseq Sort Prop.

Combined Scheme seq_mutind from gr_bc_seq, bc_gr_seq.


(* Monotonicity - covers weakening, contraction and exchange *)

(*
uses con_sub_sup :
 con_subset L1 L2 -> con_subset (L1,, o) (L2,, o)
*)
Corollary monotone :
 ((forall (L1 : context) (G : oo),
   grseq L1 G ->
    (forall (L2 : context),
      con_subset L1 L2 -> grseq L2 G))) /\
 ((forall (L1 : context) (G : oo) (A : atm),
   bcseq L1 G A ->
    (forall L2 : context,
      con_subset L1 L2 -> bcseq L2 G A))).
Proof.
Hint Resolve con_sub_sup : hsl.
eapply seq_mutind;
intros;
try (econstructor; eauto with hsl; eassumption).
Qed.

Corollary gr_monotone :
forall (L1 L2 : context) (G : oo),
 con_subset L1 L2 -> grseq L1 G ->  grseq L2 G.
Proof.
intros L1 L2 G H1 H2;
revert L1 G H2 L2 H1;
apply monotone.
Qed.

Corollary bc_monotone :
forall (L1 L2 : context) (G : oo) (A : atm),
 con_subset L1 L2 -> bcseq L1 G A ->  bcseq L2 G A.
Proof.
intros L1 L2 G A H1 H2;
revert L1 G A H2 L2 H1;
apply monotone.
Qed.


Corollary gr_weakening : forall (L : context) (G1 G2 : oo),
 grseq L G2 -> grseq (L,, G1) G2.
Proof.
intros; eapply gr_monotone;
 [ intros o He; apply elem_sub; eassumption
 | eassumption ].
Qed.

Corollary bc_weakening : forall (L : context) (G1 G2 : oo) (A : atm),
 bcseq L G2 A -> bcseq (L,, G1) G2 A.
Proof.
intros; eapply bc_monotone;
 [ intros o He; apply elem_sub; eassumption
 | eassumption ].
Qed.


Corollary gr_contraction : forall (L : context) (G1 G2 : oo),
 grseq (L,, G1,, G1) G2 -> grseq (L,, G1) G2.
Proof.
intros; eapply gr_monotone;
try eassumption.
intros o He; apply elem_rep; auto.
Qed.

Corollary bc_contraction : forall (L : context) (G1 G2 : oo) (A : atm),
 bcseq (L,, G1,, G1) G2 A -> bcseq (L,, G1) G2 A.
Proof.
intros; eapply bc_monotone;
try eassumption.
intros o He; apply elem_rep; auto.
Qed.


Corollary monotone_cor : forall (L : context) (G : oo) (A : atm),
 bcseq L G A -> grseq (L,, G) (<<A>>).
Proof.
intros; eapply g_dyn;
 [ apply elem_self | apply bc_weakening; auto ].
Qed.


Theorem grseq_specialization :
  forall (L : context) (G : expr con -> oo),
  grseq L (All G) -> forall (E : expr con), proper E -> grseq L (G E).
Proof.
intros L G H0 E H1.
inversion H0. subst.
apply H3; auto.
Qed.

Theorem bcseq_specialization :
  forall (L : context) (G : expr con -> oo) (A : atm),
  bcseq L (Some G) A -> forall (E : expr con), proper E -> bcseq L (G E) A.
Proof.
intros L G A H0 E H1.
inv_and_sub H0.
auto.
Qed.


Theorem Xseq_specialization :
  forall (L : context) (G : X -> oo),
  grseq L (Allx G) -> forall (E : X), grseq L (G E).
Proof.
intros L G H0 E.
inversion H0; subst; auto.
Qed.


(* Cut *)

Lemma pre_cut : forall o1 : oo,
(forall (L0 : context) (o2 : oo),
 grseq L0 o2 ->
  forall (L : context),
   grseq L o1 -> L0 = (L,, o1) -> grseq L o2)
/\
(forall (L0 : context) (o2 : oo) (a : atm),
 bcseq L0 o2 a ->
  forall (L : context),
   grseq L o1 ->
    L0 = (L,, o1) -> bcseq L o2 a).
Proof.
Hint Resolve gr_weakening context_swap : hsl.
induction o1;
eapply seq_mutind;
intros; subst;
try (econstructor; eauto with hsl; eassumption).

(* Case : o1 = <a>, g_dyn, D = o1 *)

apply elem_inv in H;
inversion H; subst; clear H.
eapply g_dyn; eauto.

inversion H0; subst; auto.

(* Case : o1 = T, g_dyn, D = o1 *)

apply elem_inv in H;
inversion H; subst; clear H.
eapply g_dyn; eauto.

inversion H0; subst; auto.

(* Case : o1 = o1_1 & o1_2, g_dyn, D = o1 *)

apply elem_inv in H;
inversion H; subst; clear H.
eapply g_dyn; eauto.

generalize (H1 L0 H2 eq_refl); intro Hb.
inversion H2; subst.
inversion Hb; subst.

eapply IHo1_1; auto;
apply monotone_cor; auto.

eapply IHo1_2; auto;
apply monotone_cor; auto.

(* Case : o1 = o1_1 ---> o1_2, g_dyn, D = o1 *)

apply elem_inv in H;
inversion H; subst; clear H.
eapply g_dyn; eauto.

generalize (H1 L0 H2 eq_refl); intro Hb.
inversion Hb; subst.
inversion H2; subst.
eapply IHo1_2; auto.
apply monotone_cor; auto.
eapply IHo1_1; auto; eassumption.

(* Case : o1 = All o, g_dyn, D = o1 *)

apply elem_inv in H0;
inversion H0; subst; clear H0.
eapply g_dyn; eauto.

generalize (H2 L0 H3 eq_refl); intro Hb.
inversion Hb; subst.
inversion H3; subst.
eapply H; auto.
apply monotone_cor; eassumption.
auto.

(* Case : o1 = Allx o, g_dyn, D = o1 *)

apply elem_inv in H0;
inversion H0; subst; clear H0.
eapply g_dyn; eauto.

generalize (H2 L0 H3 eq_refl); intro Hb.
inversion Hb; subst.
inversion H3; subst.
eapply H; auto.
apply monotone_cor; eassumption.

(* Case : o1 = Some o, g_dyn, D = o1 *)

apply elem_inv in H0;
inversion H0; subst; clear H0.
eapply g_dyn; eauto.

generalize (H2 L0 H3 eq_refl); intro Hb.
inversion Hb; subst.
inversion H3; subst.
apply H5 in H4.
eapply H; auto.
apply monotone_cor; eassumption.
auto.

Qed.


Lemma gr_cut : forall (L : context) (o1 o2 : oo),
grseq (L,, o1) o2 -> grseq L o1 -> grseq L o2.
Proof.
intros; eapply pre_cut; auto; eassumption.
Qed.


Lemma bc_cut : forall (L : context) (o1 o2 : oo) (a : atm),
bcseq (L,, o1) o2 a -> grseq L o1 -> bcseq L o2 a.
Proof.
intros; eapply pre_cut; auto; eassumption.
Qed.

Lemma cut_admissible :
(forall (L : context) (o1 o2 : oo),
  grseq (L,, o1) o2 -> grseq L o1 -> grseq L o2) /\
(forall (L : context) (o1 o2 : oo) (a : atm),
  bcseq (L,, o1) o2 a -> grseq L o1 -> bcseq L o2 a).
Proof.
split; [apply gr_cut | apply bc_cut].
Qed.

Lemma cut_lem : forall (L : context) (o : oo) (a : atm),
grseq L o -> bcseq L o a -> grseq L (<<a>>).
Proof.
intros.
apply gr_cut with o; auto.
apply g_dyn with o.
apply elem_self.
apply bc_weakening; auto.
Qed.


Unset Implicit Arguments.

End Hsl.