Library hilbert

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).
Proof. mp. mp. S. instantiate (1 := s ---> s). K. K. Qed.
Ltac I := eapply ax_id.

Lemma ax_c s t u : prv ((s ---> t ---> u) ---> t ---> s ---> u).
Proof. mp. mp. S. mp. mp. S. mp. K. mp. mp. S. mp. K. S. K. S. mp. K. K.
Qed.
Ltac C := eapply ax_c.

Lemma ax_b s t u : prv ((s ---> t) ---> ((u ---> s) ---> u ---> t)).
Proof. mp. mp. S. mp. K. S. K. Qed.
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).
Proof. move/r_nec => H. by rule ax_norm. Qed.

Lemma r_preg s t : prv (s ---> t) -> prv (PBox s ---> PBox t).
Proof. move/r_pnec => H. by rule ax_pnorm. Qed.

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.
Proof. move => H1 H2. by cutB. Qed.

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.
Proof. move => x y H H'. by mp. Qed.

Add Parametric Morphism : Imp with
  signature ImpPrv --> ImpPrv ++> ImpPrv as Imp_mor.
Proof.
  move => x' x X y y' Y. rewrite /ImpPrv in X Y *.
  mp. mp. B. mp. B. apply Y. mp. mp. C. B. apply X.
Qed.

Add Parametric Morphism : Box with
  signature ImpPrv ++> ImpPrv as Box_mor.
Proof. exact: r_reg. Qed.

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).
Proof. rewrite /And /Neg. mp. mp. B. C. mp. C. I. Qed.

Lemma ax_aE1 s t : prv (s :/\: t ---> s).
Proof.
  rewrite /And /Neg. cutB. apply ax_dn.
  mp. mp. C. B. mp. B. K.
Qed.

Lemma ax_aE2 s t : prv (s :/\: t ---> t).
Proof. rewrite /And /Neg. cutB. apply ax_dn. mp. mp. C. B. K. Qed.

Lemma ax_aC s t : prv (s :/\: t ---> t :/\: s).
Proof. rule ax_s; last apply ax_aE1. rule ax_s; last apply ax_aE2. mp. K. exact: ax_aI. Qed.

Lemma ax_aI2 s : prv (s ---> s :/\: s).
Proof. rule ax_s; last I. exact: ax_aI. Qed.

Add Parametric Morphism : And with
  signature ImpPrv ==> ImpPrv ==> ImpPrv as And_mor.
Proof.
  move => x x' X y y' Y. rewrite /ImpPrv in X Y *.
  mp; last apply (ax_aE2 x y). rule ax_s. cutB; last apply (ax_aE1 x y).
  rewrite -> X, -> Y. exact: ax_aI.
Qed.

Lemma r_aI s t u : prv (s ---> t) -> prv (s ---> u) -> prv (s ---> t :/\: u).
Proof. move => H1 H2. rewrite <- H1, <- H2. exact: ax_aI2. Qed.

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).
Proof.
  elim: xs; first by rewrite in_nil. move => t xs IH. rewrite inE big_cons.
  case/orP; first by move/eqP->; exact: ax_aE1.
  move/IH => E. rewrite <- E. exact: ax_aE2.
Qed.

Lemma r_intro s t xs : prv ((\and_(<- s :: xs) ---> t)) -> prv (\and_(<- xs) ---> s ---> t).
Proof. rewrite big_cons => H. rewrite <- H, <- (ax_aC _ _). exact: ax_aI. Qed.

Lemma r_hyp s : prv (\and_(<- [::]) ---> s) -> prv s.
Proof. move => H. mp. apply H. rewrite big_nil. I. Qed.

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).
Proof.
  elim: r => [ _ |x r IH H]; first by rewrite big_nil; mp; [K|I].
  rewrite big_cons. apply: r_aI; first by apply: H; rewrite mem_head.
  apply: IH => i Hi. apply: H. by rewrite inE Hi.
Qed.

Lemma sub_behead (T : eqType) x (xs ys : seq T) :
  {subset x :: xs <= ys} -> {subset xs <= ys}.
Proof. move => sub a H. apply: sub. by rewrite inE H. Qed.

Lemma and_sub (T : eqType) (xs ys : seq T) F :
  {subset xs <= ys} -> prv ((\and_(i <- ys) F i) ---> \and_(j <- xs) F j).
Proof.
  elim: xs ys. move => ys _. rewrite big_nil. by mp;[K|I].
  move => s xs IH ys sub. rewrite big_cons.
  apply: r_aI. apply: big_andE. by rewrite sub // mem_head.
  apply: IH. exact: sub_behead sub.
Qed.

Lemma ax_rot s xs : prv (\and_(<- s :: xs) ---> \and_(<- rcons xs s)).
Proof. apply: and_sub => x. by rewrite mem_rcons. Qed.

Lemma r_apply s xs t : prv (\and_(<- s ---> t :: xs) ---> s) -> prv (\and_(<- s ---> t :: xs) ---> t).
Proof. move => H. rule ax_s; last apply H. apply: big_andE. by rewrite mem_head. Qed.

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)).
Proof. HYP. do 2 Intro. Rot. ApplyH. Apply (ax_aE1 u s). Apply (ax_aE2 u s). Qed.

Lemma r_det s t xs : prv (\and_(<- xs) ---> s ---> t) -> prv ((\and_(<- s :: xs) ---> t)).
Proof. rewrite big_cons => H. rewrite -> (ax_aC _ _). by rule ax_aEl. Qed.
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).
Proof. HYP. Intro. Apply ax_dn. Intro. by Hyp. Qed.

Lemma ax_snst s t : prv (s ---> (Neg s) ---> t).
Proof. HYP. do 2 Intro. rewrite <- (ax_ex t). ApplyH. by Hyp. Qed.

Lemma ax_snns s : prv (s ---> Neg (Neg s)).
Proof. exact: ax_snst. Qed.

Lemma ax_nss s : prv ((Neg s ---> s) ---> s).
Proof. HYP. Intro. Apply ax_dn. Intro. Apply (ax_snst s). Rot. ApplyH. by Hyp. Qed.

Lemma ax_case s t : prv ((s ---> t) ---> (Neg s ---> t) ---> t).
Proof.
  HYP. do 2 Intro. Apply ax_nss. Intro. Rot. ApplyH. Intro.
  do 2 (do 3 Rot; ApplyH). by Hyp.
Qed.

Lemma ax_contra s t : prv ((Neg s ---> Neg t) ---> t ---> s).
Proof.
  HYP. do 2 Intro. Apply ax_dn. Intro. rewrite {3}/Neg.
  do 2 Rot. by ApplyH; Hyp.
Qed.

Lemma ax_contra' s t : prv ((s ---> t) ---> (Neg t ---> Neg s)).
Proof. HYP. do 3 Intro. Rot; ApplyH. Rot; ApplyH. by Hyp. Qed.

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).
Proof. exact: ax_snst. Qed.

Lemma ax_orI2 s t : prv (t ---> s :\/: t).
Proof. exact: ax_k. Qed.

Lemma ax_xm s : prv (s :\/: Neg s).
Proof. exact: ax_id. Qed.

Lemma ax_orE s t u : prv ((s ---> u) ---> (t ---> u) ---> (s :\/: t ---> u)).
Proof.
  rewrite /Or. HYP. do 3 Intro. Apply (ax_case s).
  Intro. do 2 Rot; ApplyH. do 3 Rot; ApplyH. by Hyp.
Qed.

Add Parametric Morphism : Or with
  signature ImpPrv ==> ImpPrv ==> ImpPrv as Or_mor.
Proof.
  move => x y xy u v uv. HYP. Apply ax_orE; Intro.
  Apply ax_orI1; Apply xy. Apply ax_orI2; Apply uv.
Qed.

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).
Proof.
  elim: xs. move => _. rewrite big_nil. exact: ax_ex.
  move => t xs IH H. rewrite big_cons. rule ax_orE. exact: H (mem_head _ _).
  apply: IH => j in_xs. apply: H. by rewrite inE in_xs.
Qed.

Lemma big_orI (T : eqType) (xs :seq T) j F : j \in xs -> prv (F j ---> \or_(i <- xs) F i).
Proof.
  elim: xs => //= t xs IH.
  rewrite inE big_cons => /orP [/eqP -> |]. exact: ax_orI1.
  move => in_xs. rewrite -> IH => //. exact: ax_orI2.
Qed.

Lemma or_sub (T : eqType) (xs ys :seq T) F :
  {subset xs <= ys} -> prv ((\or_(i<-xs) F i) ---> (\or_(j<-ys) F j)).
Proof.
  elim: xs. move => _. rewrite big_nil. exact: ax_ex.
  move => t xs IH sub. rewrite big_cons. rule ax_orE.
  - apply: big_orI. by rewrite sub // mem_head.
  - apply: IH. exact: sub_behead sub.
Qed.

Lemma ax_Abox s t : prv (Box s :/\: Box t ---> Box (s :/\: t)).
Proof. HYP. Apply ax_aEl. do 2 Intro. Apply ax_norm. Apply (r_reg (ax_aI s t)). Qed.

Lemma ax_boxA s t : prv (Box (s :/\: t) ---> Box s :/\: Box t).
Proof. HYP. Intro. Apply ax_aI; [Apply (r_reg (ax_aE1 s t))|Apply (r_reg (ax_aE2 s t))]. Qed.

Lemma ax_pboxA s t : prv (PBox s ---> PBox t ---> PBox (s :/\: t)).
Proof. HYP. do 2 Intro. Apply ax_pnorm. Apply (r_preg (ax_aI s t)). Qed.

Lemma ax_bt : prv (Box Top).
Proof. apply: r_nec. I. Qed.

Lemma ax_and_box xs : prv ((\and_(s <- xs) Box s) ---> Box (\and_(<- xs))).
Proof.
  elim: xs. rewrite !big_nil. mp. K. exact: ax_bt.
  move => t xs IH. rewrite !big_cons.
  rewrite -> IH. rewrite -> (ax_Abox _ _). I.
Qed.

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).
Proof. HYP. Intro. Apply ax_aI. Apply ax_id. Qed.

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).
Proof. rule ax_orE; apply or_sub => x; by rewrite !mem_enum inE => ->. Qed.

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).
Proof. move => H. apply big_orE => i in_r. rewrite -> (H _ in_r). exact: big_orI. Qed.

Lemma ax_imp_or s t : prv ((s ---> t) ---> Neg s :\/: t).
Proof. rewrite /Or. HYP. do 2 Intro. Rot. ApplyH. Apply ax_dn. Qed.

Lemma ax_nil s t : prv (Neg (s ---> t) ---> s).
Proof. HYP. Intro. Apply ax_dn. Intro. Rot. ApplyH. Intro. Apply (ax_snst s). Qed.

Lemma ax_nir s t : prv (Neg (s ---> t) ---> Neg t).
Proof. HYP. do 2 Intro. Rot. ApplyH. Intro. by Hyp. Qed.

Lemma ax_nimp_a s t : prv (Neg (s ---> t) ---> s :/\: Neg t).
Proof. HYP. Intro. Apply ax_aI. Apply (ax_nil s t). Apply (ax_nir s t). Qed.

Lemma ax_aDl s t u : prv ((s :\/: t) :/\: u ---> s :/\: u :\/: t :/\: u).
Proof. HYP. Apply ax_aEl. Apply ax_orE; do 2 Intro;[Apply ax_orI1|Apply ax_orI2]; Apply ax_aI. Qed.

Lemma ax_aA1 s t u : prv ((s :/\: t) :/\: u ---> s :/\: t :/\: u).
Proof. HYP. do 2 Apply ax_aEl. do 3 Intro. do 2 Apply ax_aI. Qed.

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

Lemma ax_bo s t : prv (Box s :\/: Box t ---> Box (s :\/: t)).
Proof. rule ax_orE; apply: r_reg. exact: ax_orI1. exact: ax_orI2. Qed.

Lemma ax_pbsb s : prv (PBox s ---> Box (SBox s)).
Proof.
  rewrite /SBox. rewrite <- (ax_Abox _ _). HYP; Intro.
  Apply ax_aI. Apply ax_bpE2. Apply ax_bpE1.
Qed.

Lemma ax_sbE1 s : prv (SBox s ---> Box (SBox s)).
Proof. HYP. Apply ax_aEl. Intro. Apply ax_pbsb. Qed.

Lemma ax_sbpb s : prv (Box (SBox s) ---> PBox s).
Proof. rewrite /SBox. rewrite -> (ax_boxA _ _). rule ax_aEl. constructor. Qed.

Lemma big_bo (T : eqType) (r : seq T) F :
  prv ( (\or_(i <- r) Box (F i)) ---> Box (\or_(i <- r) F i)).
Proof.
  elim: r => [|x r IH]; first by rewrite !big_nil; exact: ax_ex.
  rewrite !big_cons. rewrite <- (ax_bo _ _), <- IH. by I.
Qed.

Lemma ax_aIL u s t : prv ((u :/\: s ---> t) ---> (u ---> s ---> t)).
Proof. HYP. do 3 Intro. do 2 Rot. ApplyH. Apply ax_aI; by Hyp. Qed.

Lemma big_and_box (T : eqType) (xs : seq T) F :
  prv ((\and_(s <- xs) Box (F s)) ---> Box (\and_(s <- xs) F s)).
Proof.
  elim: xs. rewrite !big_nil. mp. K. exact: ax_bt.
  move => t xs IH. rewrite !big_cons.
  rewrite -> IH. rewrite -> (ax_Abox _ _). I.
Qed.

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)).
Proof.
  HYP. Intro. Apply ax_aI; Det; (mp;[K|]); apply: and_sub => x; by rewrite !mem_enum inE => ->.
Qed.

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)).
Proof.
  apply: big_andI => s.
  rewrite mem_enum => /setUP [H|H]; [rewrite -> (ax_aE1 _ _)| rewrite -> (ax_aE2 _ _)];
    apply: big_andE; by rewrite mem_enum.
Qed.