(**************************************************************** File: Hsl.v Authors: Chelsea Battell and Alberto Momigliano and Amy Felty Version: Coq V8.5 Date: Apr 2016 An intuitionistic sequent calculus used as a specification logic in the style of Abella 2.0 ***************************************************************) 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. intros L1 L2 o H o0 Helem. apply elem_inv in Helem; inversion Helem; clear Helem; subst; auto. Qed. (** Sequents **) (* generalized rule Q_i -> \forall , seq (L_{1_j}) (o_{1_j}) -> \forall , 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. eapply seq_mutind; intros; try (econstructor; eauto; 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) (<>). 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. induction o1; eapply seq_mutind; intros; subst; try (econstructor; eauto; eassumption). (* Case : o1 = , 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 (<>). 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.