Library hilbert
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)
.
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).
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)).