The Hilbert System for K+

Inductive prv : form -> Prop :=
| r_mp s t : prv (s ---> t) -> prv s -> prv t
| ax_k s t : prv (s ---> t ---> s)
| ax_s s t u : prv ((s ---> (t ---> u)) ---> (s ---> t) ---> (s ---> u))
| ax_dn s : prv (Neg (Neg s) ---> s)

| r_nec s : prv s -> prv (Box s)
| ax_norm s t : prv (Box (s ---> t) ---> Box s ---> Box t)

| r_pnec s : prv s -> prv (PBox s)
| ax_pnorm s t : prv (PBox (s ---> t) ---> PBox s ---> PBox t)
| ax_bpE1 s : prv (PBox s ---> Box (PBox s))
| ax_bpE2 s : prv (PBox s ---> Box s)
| ax_pbI s : prv (Box s ---> Box (PBox s) ---> PBox s)
| ax_seg s : prv (Box s ---> PBox (s ---> Box s) ---> PBox s)
.

Reasoning Infrastructure

Phase 1 - Combinators

The first means to prove modal logic theorems is by giving Ltac scripts that correspond to (linarized) combinator terms. These are obtained from lambda terms via a simple Haskell script

Ltac mp := eapply r_mp.
Ltac S := eapply ax_s.
Ltac K := eapply ax_k.

Lemma ax_id s : prv (s ---> s).
Ltac I := eapply ax_id.

Lemma ax_c s t u : prv ((s ---> t ---> u) ---> t ---> s ---> u).
Ltac C := eapply ax_c.

Lemma ax_b s t u : prv ((s ---> t) ---> ((u ---> s) ---> u ---> t)).
Ltac B := eapply ax_b.

Ltac rule H :=
first [ mp; first eapply H | mp; first mp; first eapply H ].
Ltac cutB := mp; first mp; first B.

Lemma r_reg s t : prv (s ---> t) -> prv (Box s ---> Box t).

Lemma r_preg s t : prv (s ---> t) -> prv (PBox s ---> PBox t).

Phase 2 - Rewriting with the entailment relation

We use Setoid rewriting to rewrite with the entailment relation,i.e., provable implications.

Definition ImpPrv s t := prv (s ---> t).

Definition ImpPrv_refl s : ImpPrv s s := ax_id s.
Definition ImpPrv_trans s t u : ImpPrv s t -> ImpPrv t u -> ImpPrv s u.

Add Parametric Relation : form ImpPrv
reflexivity proved by ImpPrv_refl
transitivity proved by ImpPrv_trans
as ImpPrv_rel.

Add Parametric Morphism : prv with
signature ImpPrv ++> Basics.impl as prv_mor.

Add Parametric Morphism : Imp with
signature ImpPrv --> ImpPrv ++> ImpPrv as Imp_mor.

Add Parametric Morphism : Box with
signature ImpPrv ++> ImpPrv as Box_mor.

Conjunction

Definition And s t := Neg (s ---> Neg t).
Infix ":/\:" := And (at level 30,right associativity).

Lemma ax_aI s t : prv (s ---> t ---> s :/\: t).

Lemma ax_aE1 s t : prv (s :/\: t ---> s).

Lemma ax_aE2 s t : prv (s :/\: t ---> t).

Lemma ax_aC s t : prv (s :/\: t ---> t :/\: s).

Lemma ax_aI2 s : prv (s ---> s :/\: s).

Add Parametric Morphism : And with
signature ImpPrv ==> ImpPrv ==> ImpPrv as And_mor.

Lemma r_aI s t u : prv (s ---> t) -> prv (s ---> u) -> prv (s ---> t :/\: u).

Phase 3 - Assumption Management

Notation "\and_ ( i <- r ) F" := (\big [And/Top]_(i <- r) F)
(at level 41, F at level 41, i at level 0,
format "'[' \and_ ( i <- r ) '/ ' F ']'").

Notation "\and_ ( <- r )" := (\and_(i <- r) i)
(at level 41, F at level 41, i at level 0,
format "'[' \and_ ( <- r ) ']'").

Lemma big_andE (T:eqType) (F : T -> form) xs s : s \in xs -> prv ((\and_(x <- xs) F x) ---> F s).

Lemma r_intro s t xs : prv ((\and_(<- s :: xs) ---> t)) -> prv (\and_(<- xs) ---> s ---> t).

Lemma r_hyp s : prv (\and_(<- [::]) ---> s) -> prv s.

Lemma big_andI (T : eqType) s (r : seq T) F :
(forall i, i \in r -> prv (s ---> F i)) -> prv (s ---> \and_(i <- r) F i).

Lemma sub_behead (T : eqType) x (xs ys : seq T) :
{subset x :: xs <= ys} -> {subset xs <= ys}.

Lemma and_sub (T : eqType) (xs ys : seq T) F :
{subset xs <= ys} -> prv ((\and_(i <- ys) F i) ---> \and_(j <- xs) F j).

Lemma ax_rot s xs : prv (\and_(<- s :: xs) ---> \and_(<- rcons xs s)).

Lemma r_apply s xs t : prv (\and_(<- s ---> t :: xs) ---> s) -> prv (\and_(<- s ---> t :: xs) ---> t).

Ltac HYP := apply r_hyp.
Ltac Intro := apply r_intro.
Ltac Hyp := apply: big_andE; by rewrite !inE eqxx.
Ltac Rot := rewrite -> (ax_rot _ _); simpl.
Ltac ApplyH := first [eapply r_apply | rule ax_s ; first eapply r_apply].
Ltac Apply H := first [ mp;[K|]; eapply H | rule ax_s ; first Apply H]; try Hyp.

Lemma ax_aEl u s t : prv ((u ---> s ---> t) ---> (u :/\: s ---> t)).

Lemma r_det s t xs : prv (\and_(<- xs) ---> s ---> t) -> prv ((\and_(<- s :: xs) ---> t)).
Ltac Det := eapply r_det.

Modal Logic Lemmas

We had to prove a number of lemmas about conjunction to set up the assumption management. Once this is in place, we prove the remaining modal logoc lemmas we need using a mix of ND-syle reasoing and rewriting.

Negation

Lemma ax_ex s : prv (Bot ---> s).

Lemma ax_snst s t : prv (s ---> (Neg s) ---> t).

Lemma ax_snns s : prv (s ---> Neg (Neg s)).

Lemma ax_nss s : prv ((Neg s ---> s) ---> s).

Lemma ax_case s t : prv ((s ---> t) ---> (Neg s ---> t) ---> t).

Lemma ax_contra s t : prv ((Neg s ---> Neg t) ---> t ---> s).

Lemma ax_contra' s t : prv ((s ---> t) ---> (Neg t ---> Neg s)).

Disjunction

Definition Or s t := Neg s ---> t.
Notation "s :\/: t" := (Or s t) (at level 33, right associativity).

Lemma ax_orI1 s t : prv (s ---> s :\/: t).

Lemma ax_orI2 s t : prv (t ---> s :\/: t).

Lemma ax_xm s : prv (s :\/: Neg s).

Lemma ax_orE s t u : prv ((s ---> u) ---> (t ---> u) ---> (s :\/: t ---> u)).

Add Parametric Morphism : Or with
signature ImpPrv ==> ImpPrv ==> ImpPrv as Or_mor.

Notation "\or_ ( i <- r ) F" := (\big [Or/Bot]_(i <- r) F)
(at level 42, F at level 42, i at level 0,
format "'[' \or_ ( i <- r ) '/ ' F ']'").

Notation "\or_ ( <- r )" := (\or_(i <- r) i)
(at level 42, F at level 42, i at level 0,
format "'[' \or_ ( <- r ) ']'").

Lemma big_orE (T : eqType) F (xs :seq T) s:
(forall j, j \in xs -> prv (F j ---> s)) -> prv ((\or_(i <- xs) F i) ---> s).

Lemma big_orI (T : eqType) (xs :seq T) j F : j \in xs -> prv (F j ---> \or_(i <- xs) F i).

Lemma or_sub (T : eqType) (xs ys :seq T) F :
{subset xs <= ys} -> prv ((\or_(i<-xs) F i) ---> (\or_(j<-ys) F j)).

Lemma ax_Abox s t : prv (Box s :/\: Box t ---> Box (s :/\: t)).

Lemma ax_boxA s t : prv (Box (s :/\: t) ---> Box s :/\: Box t).

Lemma ax_pboxA s t : prv (PBox s ---> PBox t ---> PBox (s :/\: t)).

Lemma ax_bt : prv (Box Top).

Lemma ax_and_box xs : prv ((\and_(s <- xs) Box s) ---> Box (\and_(<- xs))).

Notation "\or_ ( i \in A ) F" := (\big [Or/Bot]_(i <- enum A) F)
(at level 42, F at level 42, i at level 0,
format "'[' \or_ ( i \in A ) '/ ' F ']'").

Lemma ax_andT s : prv (s ---> s :/\: Top).

Lemma big_orU (T : finType) (A B : {set T}) G :
prv ((\or_(x \in A) G x) :\/: (\or_(x \in B) G x) ---> \or_(x \in (A :|: B)) G x).

Lemma big_orW (T : eqType) (r : seq T) F G :
(forall i , i \in r -> prv (F i ---> G i)) -> prv ((\or_(i <- r) F i) ---> \or_(j <- r) G j).

Lemma ax_imp_or s t : prv ((s ---> t) ---> Neg s :\/: t).

Lemma ax_nil s t : prv (Neg (s ---> t) ---> s).

Lemma ax_nir s t : prv (Neg (s ---> t) ---> Neg t).

Lemma ax_nimp_a s t : prv (Neg (s ---> t) ---> s :/\: Neg t).

Lemma ax_aDl s t u : prv ((s :\/: t) :/\: u ---> s :/\: u :\/: t :/\: u).

Lemma ax_aA1 s t u : prv ((s :/\: t) :/\: u ---> s :/\: t :/\: u).

Definition SBox s := s :/\: PBox s.
Notation "□*" := SBox (at level 0).

Lemma ax_bo s t : prv (Box s :\/: Box t ---> Box (s :\/: t)).

Lemma ax_pbsb s : prv (PBox s ---> Box (SBox s)).

Lemma ax_sbE1 s : prv (SBox s ---> Box (SBox s)).

Lemma ax_sbpb s : prv (Box (SBox s) ---> PBox s).

Lemma big_bo (T : eqType) (r : seq T) F :
prv ( (\or_(i <- r) Box (F i)) ---> Box (\or_(i <- r) F i)).

Lemma ax_aIL u s t : prv ((u :/\: s ---> t) ---> (u ---> s ---> t)).

Lemma big_and_box (T : eqType) (xs : seq T) F :
prv ((\and_(s <- xs) Box (F s)) ---> Box (\and_(s <- xs) F s)).

Notation "\and_ ( i \in A ) F" := (\big [And/Top]_(i <- enum A) F)
(at level 41, F at level 41, i at level 0,
format "'[' \and_ ( i \in A ) '/ ' F ']'").

Lemma and_Ua (T : finType) (A B : {set T}) F :
prv ((\and_(s \in A :|: B) F s) ---> (\and_(s \in A) F s) :/\: (\and_(s \in B) F s)).

Lemma and_aU (T : finType) (A B : {set T}) F :
prv ((\and_(s \in A) F s) :/\: (\and_(s \in B) F s) ---> (\and_(s \in A :|: B) F s)).