Require Import Forms. Require Import Hilbert. Open Scope lbk_scope. Set Implicit Arguments. Section semantic_defs. (* Models for CTL *) Variables (W : Set) (R : W -> W -> W -> Prop) (v_at : Atom -> W -> Prop). (* extension of some valuation on atoms to all formulae *) Fixpoint val (F : Form) : W -> Prop := match F with | At a => v_at a | A o B => fun x => exists y : W, (exists z : W, R x y z /\ val A y /\ val B z) | C // B => fun y => forall x z : W, R x y z -> val B z -> val C x | A \\ C => fun z => forall x y : W, R x y z -> val A y -> val C x end. Definition satisfies (w : W) (A : Form) : Prop := val A w. End semantic_defs. Notation "w |= A" := (satisfies w A) (at level 60). Definition sem_implies : Form -> Form -> Prop := fun A B : Form => forall (W : Set) (R : W -> W -> W -> Prop) (v_at : Atom -> W -> Prop), forall w : W, satisfies R v_at w A -> satisfies R v_at w B. Notation "A |== B" := (sem_implies A B) (at level 60). (* semantic versions of derivation rules *) Lemma ONE : forall A , A |== A. Proof. unfold sem_implies, satisfies in |- *; auto. Qed. Lemma COMP : forall A B C, A |== B -> B |== C -> A |== C. Proof. unfold sem_implies, satisfies in |- *; auto. Qed. Lemma GAMMA' : forall A B C, B |== A \\ C -> A o B |== C. Proof. unfold sem_implies, satisfies in |- *; simpl in |- *; auto. intros A B C H W R v_at w H1. case H1; intros y H2. case H2; intros z H3. case H3; intros H4 H5. case H5; eauto. Qed. Lemma GAMMA : forall A B C, sem_implies (Dot A B) C -> sem_implies B (Backslash A C). Proof. unfold sem_implies, satisfies in |- *; simpl in |- *; auto. intros A B C H W R v_at w H1 x y H2 H3. apply H. exists y; exists w; auto. Qed. Lemma BETA' : forall A B C : Form, sem_implies A (Slash C B) -> sem_implies (Dot A B) C. Proof. unfold sem_implies, satisfies in |- *; simpl in |- *; auto. intros A B C H W R v_at w H1. case H1; intros y H2. case H2; intros z H3. case H3; intros H4 H5. case H5; eauto. Qed. Lemma BETA : forall A B C : Form , sem_implies (Dot A B) C -> sem_implies A (Slash C B). Proof. unfold sem_implies, satisfies in |- *; simpl in |- *; auto. intros A B C H W R v_at w H1 x y H2 H3. apply H. exists w; exists y; auto. Qed. Lemma GAMMA'BETA : forall A B C : Form, sem_implies B (Backslash A C) -> sem_implies A (Slash C B). Proof. unfold sem_implies, satisfies in |- *; simpl in |- *; eauto. Qed. Section soundness. Definition NL_sound := forall A B : Form, NL_arrow A B -> sem_implies A B. Theorem NL_sound_thm : NL_sound. Proof. unfold NL_sound. simple induction 1. apply ONE. intros; eapply COMP; eauto. intros; apply GAMMA'BETA; apply GAMMA; auto. intros; apply BETA'; assumption. intros; apply GAMMA; auto. intros; apply GAMMA'; assumption. Qed. End soundness. Section completeness. (* the syntactical model *) (* coercion to Prop *) Inductive weak (A : Set) : Prop := weak_intro : forall a : A, weak A. Definition WK : Set := Form. Definition RK (A B C : Form) := weak (NL_arrow A (B o C)). Definition valK (a : Atom) (A : WK) : Prop := weak (NL_arrow A (At a)). Definition truth_lemma_spec := forall phi A : Form, weak (NL_arrow A phi) <-> satisfies RK valK A phi. Definition NL_complete := forall A B : Form, sem_implies A B -> weak (NL_arrow A B). (* weak combinators for NL_arrow *) Lemma weak_one : forall A, weak (A -NL-> A). Proof. intros; split. apply one. Qed. Hint Resolve weak_one: ctl. Lemma weak_comp : forall A B C, weak (NL_arrow A B) -> weak (NL_arrow B C) -> weak (NL_arrow A C). Proof. intros A B C H H0. case H; case H0. split. apply comp with B; auto. Qed. Hint Resolve weak_comp: ctl. Lemma weak_beta : forall A B C, weak (NL_arrow (A o B) C) -> weak (NL_arrow A (C // B)). Proof. intros A B C H. case H. split. apply beta; auto. Qed. Hint Resolve weak_beta: ctl. Lemma weak_beta' : forall A B C, weak (NL_arrow A (C // B)) -> weak (NL_arrow (A o B) C). Proof. intros A B C H. case H. split. apply beta'; auto. Qed. Lemma weak_gamma : forall A B C, weak (NL_arrow (A o B) C) -> weak (B -NL-> (A \\ C)). Proof. intros A B C H. case H. split. apply gamma; auto. Qed. Hint Resolve weak_gamma: ctl. Lemma weak_gamma' : forall A B C, weak (B -NL-> (A \\ C)) -> weak (A o B -NL-> C). Proof. intros A B C H. case H. split. apply gamma'; auto. Qed. Hint Resolve weak_gamma: ctl. Lemma weak_Dot_mono : forall A B C D, weak (NL_arrow A C) -> weak (NL_arrow B D) -> weak (NL_arrow (A o B) (C o D)). Proof. intros A B C D H H0. case H. case H0. intros. split. apply Dot_mono; auto. Qed. Lemma weak_Dot_mono_right : forall A B B', weak (NL_arrow B' B) -> weak (NL_arrow (A o B') (A o B)). Proof. intros A B B' H. case H. split. apply Dot_mono_right; auto. Qed. Lemma weak_Dot_mono_left : forall A B A', weak (NL_arrow A' A) -> weak (NL_arrow (A' o B) (A o B)). Proof. intros A B A' H. case H; split. apply Dot_mono_left; auto. Qed. Lemma weak_Slash_isotonicity : forall C B C', weak (NL_arrow C' C) -> weak (NL_arrow (C' // B) (C // B)). Proof. intros C B C' H. case H; split. apply Slash_isotonicity; auto. Qed. Lemma weak_Slash_antitonicity : forall C B B', weak (NL_arrow B' B) -> weak (NL_arrow (C // B) (C // B')). Proof. intros C B B' H. case H; split. apply Slash_antitonicity; auto. Qed. Lemma weak_Backslash_antitonicity : forall A C A', weak (NL_arrow A A') -> weak (NL_arrow (A' \\ C) (A \\ C)). Proof. intros A C A' H. case H; split. apply Backslash_antitonicity; auto. Qed. Lemma weak_Backslash_isotonicity : forall A C C', weak (NL_arrow C' C) -> weak (NL_arrow (A \\ C') (A \\ C)). Proof. intros A C C' H. case H; split. apply Backslash_isotonicity; auto. Qed. Lemma truth_lemma: truth_lemma_spec. Proof. unfold truth_lemma_spec, satisfies in |- *; simple induction phi. (* atomic formulae *) unfold WK, RK, valK in |- *; simpl in |- *; tauto. (* phi = C/B *) intros C HC B HB A. split; intro. simpl in |- *; intros x z H0 H1. elim (HB A); intros. cut (weak (NL_arrow z B)). intro. cut (weak (NL_arrow x C)). intro. elim (HC x); tauto. apply weak_comp with (Dot A B). apply weak_comp with (Dot A z). apply H0. apply weak_Dot_mono_right; auto. apply weak_beta'. auto. elim (HB z); tauto. simpl in H. apply weak_beta. elim (HC (Dot A B)); intros H0 H1. apply H1. apply (H (Dot A B) B). unfold RK in |- *; auto with ctl. elim (HB B); intros. auto with ctl. (* phi = (B o C) *) intros A HA C HC B. split; intro. simpl in |- * . intros x y H0 H1. elim (HC (Dot A B)); intros H2 H3. elim (HC x); intros. apply H4. apply weak_comp with (Dot A B). apply weak_comp with (Dot y B). auto. apply weak_Dot_mono_left. elim (HA y); auto. apply weak_gamma'. auto. apply weak_gamma. simpl in H. elim (HC (Dot A B)); intros. apply H1. eapply H. unfold RK in |- *; apply weak_one. elim (HA A); auto with ctl. intros B HB C HC A. split; intro. simpl in |- *. exists B; exists C. split. unfold RK in |- *; auto. split. elim (HB B); auto with ctl. elim (HC C); auto with ctl. simpl in H; elim H. clear H. simple induction 1. intros x0 H0. case H0; intros H1 H2. case H2; intros H3 H4. apply weak_comp with (Dot x x0). apply H1. apply weak_comp with (Dot B x0). apply weak_Dot_mono_left. elim (HB x); auto. apply weak_Dot_mono_right. elim (HC x0); auto. Qed. Lemma NL_compl_aux : forall A B, (forall w : WK, satisfies RK valK w A -> satisfies RK valK w B) -> weak (NL_arrow A B). Proof. intros A B H. elim (truth_lemma B A). intros. apply H1. apply H. elim (truth_lemma A A). auto with ctl. Qed. Lemma NL_completeness_thm : NL_complete. Proof. unfold NL_complete in |- *; intros A B H. apply NL_compl_aux; auto. Qed. End completeness.