Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype finset bigop.

Require Import edone fset.

Set Implicit Arguments.
Import Prenex Implicits.

Require Import Setoid Morphisms.
Require Import Relation_Definitions.

A Modular Library for Reasoing in Hilbert Systems

We build a modular library for reasoning in Hilbert systems for classical modal logics. The Hilbert systems for these logics often just extend the Hilbert system for a weaker logic with additonal rules and axioms.

We define abstractly what it means for a Hilbert system to implement minimal logic, propositional logic, K, and CTL. The main part is the development for propositional logic, where we define the remaining logical connecitves and use big conjunctions to simulate ND-style reasoing in our assumption free Hilbert systems.

Minimal Logic

We start with a number of Lemmas for minimal logic. This is mostly the very basic combinator infrasutructure a a few tactic definitions.

Record mSystem := MSystem {
                      T :> choiceType;
                      mprv : T -> Prop;
                      Imp : T -> T -> T;
                      rMP' s t : mprv (Imp s t) -> mprv s -> mprv t;
                      axK' s t : mprv (Imp s (Imp t s));
                      axS' s t u : mprv (Imp (Imp u (Imp s t)) (Imp (Imp u s) (Imp u t)))
                    }.

This is reqired to keep preserve the notation for instances under simplification

Definition Imp_op := nosimpl Imp.
Notation "s ---> t" := (@Imp_op _ s t) (at level 35, right associativity).

Lemma rMP (mS : mSystem) (s t : mS) : mprv (s ---> t) -> mprv s -> mprv t.

Lemma axS (mS : mSystem) (s t u : mS) : mprv ((u ---> s ---> t ) ---> (u ---> s ) ---> u ---> t).

Lemma axK (mS : mSystem) (s t : mS) : mprv (s ---> t ---> s).

Ltac mp := eapply rMP.
Ltac S := eapply axS.
Ltac K := eapply axK.

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

Section MTheory0.
  Variable (mS : mSystem).
  Implicit Types s t : mS.

  Lemma axI s : mprv (s ---> s).

  Lemma axC s t u : mprv ((s ---> t ---> u ) ---> t ---> s ---> u).

  Lemma axB u s t : mprv ((u ---> t ) ---> (s ---> u ) ---> (s ---> t )).

  Lemma axDup s t : mprv ((s ---> s ---> t ) ---> s ---> t).

  Definition mImpPrv s t := mprv (s ---> t).

  Definition mImpPrv_refl s : mImpPrv s s := axI s.
  Lemma mImpPrv_trans s t u : mImpPrv s t -> mImpPrv t u -> mImpPrv s u.

  Lemma mp2 s t u :
  mprv (s ---> t ---> u) -> mprv s -> mprv t -> mprv u.
End MTheory0.

Hint Resolve axI.

Ltac C := eapply axC.
Ltac B := eapply axB.
Ltac Cut u := apply (mp2 (axB u _ _)); last first.
Ltac drop := rule axK.
Ltac swap := rule axC.

Ltac Have u := apply (mp2 (axS u _ _)); last first.
Ltac Suff u := apply (mp2 (axS u _ _)).

We enable Setoid rewriting for the mImpPrv relation

Instance mImpPrv_rel (mS : mSystem) : PreOrder (@mImpPrv mS).

Instance mprv_mor (mS : mSystem) :
Proper ((@mImpPrv mS ) ++> Basics.impl) (@mprv mS).

Instance Imp_mor (mS : mSystem) :
Proper ((@mImpPrv mS ) --> (@mImpPrv mS ) ++> (@mImpPrv mS )) (@Imp mS).

Propositional Logic

In the presence of Bot and double negation, we can define the remaining propositional connectives and prove the corresponding lemmas. We also define morphisms for these connectives to enable Setoid rewriting.

Record pSystem := PSystem {
                      msort :> mSystem;
                      Bot : msort;
                      axDN' s : mprv (Imp (Imp (Imp s Bot) Bot) s)
                    }.

Notations for derived logical opertions

Definition Top {pS : pSystem} := @Bot pS ---> Bot.

Definition Neg (pS : pSystem) (s : pS) := (s ---> Bot).
Notation "~~: s" := (Neg s) (at level 25).

Definition And (pS : pSystem) (s t : pS) := ~~: (s ---> ~~: t ).
Notation "s :/\: t" := (And s t) (at level 30, right associativity).

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

Lemma axDN (pS : pSystem) (s:pS) : mprv ((~~: ~~: s ) ---> s).

Basic Propositional Logic Facts

We prove some basic propositonal lemmas which we need to set up the ND-style reasoning.

Section PTheoryBase.
  Variable pS : pSystem.
  Implicit Types s t u : pS.

  Lemma axT : mprv (@Top pS).

  Lemma axsT s : mprv (s ---> Top).

  Lemma axBE s : mprv (Bot ---> s).

  Lemma axContra s t : mprv (s ---> (~~: s ) ---> t).

  Lemma axDNI s : mprv (s ---> (~~: ~~: s )).

  Lemma axW s t u : mprv ((s ---> t ) ---> ((t ---> u ) ---> s ---> u )).

  Lemma axAEl s t : mprv (s :/\: t ---> s).

  Lemma axAEr s t : mprv (s :/\: t ---> t).

  Lemma axAI s t : mprv (s ---> t ---> s :/\: t).

  Lemma axAC s t : mprv (s :/\: t ---> t :/\: s).

End PTheoryBase.

Hint Resolve axT axAEl axAEr.

Instance Neg_mor (pS : pSystem) :
  Proper ((@mImpPrv pS ) --> (@mImpPrv pS ))(@Neg pS).

Instance And_mor (pS : pSystem) :
  Proper ((@mImpPrv pS ) ==> (@mImpPrv pS ) ==> (@mImpPrv pS )) (@And pS).

Instance Or_mor (pS : pSystem) :
  Proper ((@mImpPrv pS ) ==> (@mImpPrv pS ) ==> (@mImpPrv pS )) (@Or pS).

Equivalence (Experimental)

We extend rewriting from the preorder of imlications to rewriting with equivalences.

Definition Eqi (pS : pSystem) (s t : pS) := (s ---> t ) :/\: (t ---> s ).
Notation "s <--> t" := (Eqi s t) (at level 40, no associativity).

Definition EqiPrv (pS : pSystem) (s t : pS) := mprv (Eqi s t).

Section EqiTheoryBase.
  Variable (pS : pSystem) (s t : pS).

  Lemma axEEl : mprv ((s <--> t ) ---> (s ---> t )).

  Lemma axEEr : mprv ((s <--> t ) ---> (t ---> s )).

  Lemma axEI : mprv ((s ---> t ) ---> (t ---> s ) ---> (s <--> t ) ).
End EqiTheoryBase.

Require Import Basics induced_sym.

Instance eqi_induced_symmety (pS : pSystem) : InducedSym (@mImpPrv pS) (@EqiPrv pS).

Instance induced_eqi (pS : pSystem) : Equivalence (@EqiPrv pS).

Big Boolean Operators

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 ) ']'").

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 ']'").

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 ) ']'").

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 ']'").

Section BigAnd.
  Variable pS : pSystem.
  Implicit Types s t : pS.

  Lemma rAI s t u : mprv (s ---> t) -> mprv (s ---> u) -> mprv (s ---> t :/\: u).

Introduction and eliminiation for big conjunctions

  Lemma bigAE (T:eqType) (F : T -> pS) (xs : seq T) (s:T) :
    s \in xs -> mprv ((\and_(x <- xs ) F x) ---> F s).

  Lemma bigAI (T : eqType) s (r : seq T) F :
    (forall i, i \in r -> mprv (s ---> F i)) -> mprv (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 : T -> pS) :
    {subset xs <= ys } -> mprv ((\and_(i <- ys ) F i) ---> \and_(j <- xs ) F j).

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

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

  Lemma bigAdup s xs : mprv (\and_(<- s :: xs ) ---> \and_(<-[:: s , s & xs ])).

  Lemma bigAdrop s xs : mprv (\and_(<- s :: xs ) ---> \and_(<- xs )).

  Lemma bigA1E s : mprv (\and_(<- [:: s ]) ---> s).

We use big conjuctions for assumption management to allow for ND-style reasoning

  Lemma rIntro s t xs : mprv ((\and_(<- s :: xs ) ---> t)) -> mprv (\and_(<- xs ) ---> s ---> t).

  Lemma rHyp s : mprv (\and_(<- [::]) ---> s) -> mprv s.

  Lemma rHyp1 s t : mprv (\and_(<- [:: s ]) ---> t) -> mprv (s ---> t).

  Lemma rDup s xs t : mprv (\and_(<-[:: s , s & xs ]) ---> t) -> mprv (\and_(<- s :: xs ) ---> t).

  Lemma axRot s xs : mprv (\and_(<- s :: xs ) ---> \and_(<- rcons xs s )).

  Lemma rRot s xs t : mprv (\and_(<- rcons xs s ) ---> t) -> mprv (\and_(<- s :: xs ) ---> t).

  Lemma rApply s xs t : mprv (\and_(<-xs ) ---> s) -> mprv (\and_(<- s ---> t :: xs ) ---> t).

  Lemma rApply2 s0 s1 xs t :
    mprv (\and_(<-xs ) ---> s0) -> mprv (\and_(<-xs ) ---> s1) ->
    mprv (\and_(<- s0 ---> s1 ---> t :: xs ) ---> t).

  Lemma rApply3 s0 s1 s2 xs t :
    mprv (\and_(<-xs ) ---> s0) -> mprv (\and_(<-xs ) ---> s1) -> mprv (\and_(<-xs ) ---> s2) ->
    mprv (\and_(<- s0 ---> s1 ---> s2 ---> t :: xs ) ---> t).

End BigAnd.

Ltac Asm := by apply: bigAE; rewrite !inE !eqxx.
Ltac Intro := first [apply rIntro | apply rHyp1].
Ltac Apply := first [eapply rApply | eapply rApply2 | eapply rApply3 ]; try Asm.
Tactic Notation "Apply*" integer(n) := (do n apply rRot); Apply.

Lemma axAcase (pS : pSystem) (u s t : pS) : mprv ((u ---> s ---> t ) ---> (u :/\: s ---> t )).

Lemma rRev (pS : pSystem) (s t : pS) xs : mprv (\and_(<- xs ) ---> s ---> t) -> mprv ((\and_(<- s :: xs ) ---> t)).

Lemma rRev1 (pS : pSystem) (s t : pS) : mprv (s ---> t) -> mprv ((\and_(<- [:: s ]) ---> t)).

Ltac Rev := first [eapply rRev1 | eapply rRev].

Ltac ApplyH H := first [ drop; by apply H
                       | rule axS; first (drop; by apply H)
                       | rule axS; first (rule axS; first (drop; by apply H))
                       | rule axS; first (rule axS; first (rule axS ; first (drop; by apply H))) ]; try Asm.

Ltac Rot n := do n (apply rRot).
Tactic Notation "Rev*" integer(n) := (do n apply rRot); Rev.

Remaining Propostional Logic Facts

Section PTheory.
  Variable pS : pSystem.
  Implicit Types s t u : pS.

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

  Lemma ax_contra s t : mprv ((~~:t ---> ~~: s ) ---> (s ---> t )).

  Lemma ax_contraNN s t : mprv ((s ---> t ) ---> ~~:t ---> ~~: s).

  Lemma axATs s : mprv (s ---> Top :/\: s).

  Lemma axAsT s : mprv (s ---> s :/\: Top).

  Lemma axOIl s t : mprv (s ---> s :\/: t).

  Lemma axOIr s t : mprv (t ---> s :\/: t).

  Lemma axOE s t u : mprv ((s ---> u ) ---> (t ---> u ) ---> (s :\/: t ---> u )).

  Lemma axOC s t : mprv (s :\/: t ---> t :\/: s).

  Lemma axOF s : mprv (Bot :\/: s ---> s).

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

  Lemma bigOI (T : eqType) (xs :seq T) j (F : T -> pS) :
     j \in xs -> mprv (F j ---> \or_(i <- xs ) F i).

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

  Lemma axIO s t : mprv ((s ---> t ) ---> (~~: s :\/: t )).

  Lemma dmI s t : mprv (~~: (s ---> t ) ---> s :/\: ~~: t).

End PTheory.

Lemma axADr (pS : pSystem) (s t u : pS) :
  mprv ((s :\/: t ) :/\: u <--> s :/\: u :\/: t :/\: u).

Lemma axAA (pS : pSystem) (s t u : pS) : mprv ((s :/\: t ) :/\: u <--> s :/\: t :/\: u).

Basic Modal Logic

Record kSystem := KSystem { psort :> pSystem;
                            AX : psort -> psort;
                            rNec s : mprv s -> mprv (AX s);
                            axN s t: mprv (AX (s ---> t) ---> AX s ---> AX t) }.

Lemma rNorm (kS : kSystem) (s t : kS) : mprv (s ---> t) -> mprv (AX s ---> AX t).

Instance AX_mor (kS : kSystem) : Proper ((@mImpPrv kS ) ==> (@mImpPrv kS )) (@AX kS).

Definition EX (kS : kSystem) (s : kS) := ~~: AX (~~: s).

Instance EX_mor (kS : kSystem) : Proper ((@mImpPrv kS ) ==> (@mImpPrv kS )) (@EX kS).

Section KTheory.
  Variable kS : kSystem.
  Implicit Types s t u : kS.

  Lemma axBT : mprv (@AX kS Top).
  Hint Resolve axBT.

  Lemma axDF : mprv (@EX kS Bot ---> Bot).

  Lemma axABBA s t : mprv (AX s :/\: AX t ---> AX (s :/\: t)).

  Lemma axBAAB s t : mprv (AX (s :/\: t) ---> AX s :/\: AX t).

  Lemma bigABBA (T : eqType) (xs : seq T) (F : T -> kS) :
    mprv ((\and_(s <- xs ) AX (F s)) ---> AX (\and_(s <- xs ) F s)).

  Lemma axDBD s t : mprv (EX s ---> AX t ---> EX (s :/\: t)).

  Lemma rEXn s t : mprv (s ---> t) -> mprv (EX s ---> EX t).

  Lemma axEXAEl s t : mprv (EX (s :/\: t) ---> EX s).

  Lemma dmAX s : mprv (~~: AX s <--> EX (~~: s)).
End KTheory.

Record ksSystem :=
  KSSystem { ksort' :> kSystem;
             AG : ksort' -> ksort';
             axAGN s t : mprv (AG (s ---> t) ---> AG s ---> AG t);
             axAGEl s : mprv (AG s ---> s) ;
             axAGEr s : mprv (AG s ---> AX (AG s)) ;
             rAG_ind s : mprv (s ---> AX s) -> mprv (s ---> AG s)
           }.

Definition EF {ksS : ksSystem} (s : ksS) := ~~: AG (~~: s).

Section KStarTheory.
  Variables (ksS : ksSystem).
  Implicit Types s t u : ksS.

  Lemma rNecS s : mprv s -> mprv (AG s).

  Lemma rNormS s t : mprv (s ---> t) -> mprv (AG s ---> AG t).

  Instance AG_mor : Proper ((@mImpPrv ksS ) ==> (@mImpPrv ksS )) (@AG ksS).

  Lemma axAGI s : mprv (s ---> AX (AG s) ---> AG s).

  Lemma segerberg s : mprv (s ---> AG (s ---> AX s) ---> AG s).
End KStarTheory.

CTL

Record ctlSystem :=
  CTLSystem { ksort :> kSystem;
              AU : ksort -> ksort -> ksort;
              AR : ksort -> ksort -> ksort;
              rAU_ind s t u : mprv (t ---> u) -> mprv (s ---> AX u ---> u) -> mprv ((AU s t ) ---> u);
              axAUI s t : mprv (t ---> AU s t);
              axAUf s t : mprv (s ---> AX (AU s t) ---> AU s t);
              rAR_ind s t u :
                mprv (u ---> t) -> mprv (u ---> (s ---> Bot ) ---> AX u) -> mprv (u ---> AR s t);
              axARE s t : mprv (AR s t ---> t);
              axARu s t : mprv (AR s t ---> (s ---> Bot ) ---> AX (AR s t))
            }.

Definition ER {cS : ctlSystem} (s t : cS) := ~~: AU (~~: s) (~~: t).
Definition EU {cS : ctlSystem} (s t : cS) := ~~: AR (~~: s) (~~: t).
Notation "'EG' s" := (ER Bot s) (at level 8).

Instance AU_mor (cS : ctlSystem) :
  Proper ((@mImpPrv cS ) ==> (@mImpPrv cS ) ==> (@mImpPrv cS ))(@AU cS).

Instance ER_mor (cS : ctlSystem) :
  Proper ((@mImpPrv cS ) ==> (@mImpPrv cS ) ==> (@mImpPrv cS ))(@ER cS).

Instance AR_mor (cS : ctlSystem) :
  Proper ((@mImpPrv cS ) ==> (@mImpPrv cS ) ==> (@mImpPrv cS ))(@AR cS).

Instance EU_mor (cS : ctlSystem) :
  Proper ((@mImpPrv cS ) ==> (@mImpPrv cS ) ==> (@mImpPrv cS ))(@EU cS).

Section CTLTheory.
  Variable cS : ctlSystem.
  Implicit Types s t u : cS.

  Lemma rER_ind u s t : mprv (u ---> t) -> mprv (u ---> ~~: s ---> EX u) -> mprv (u ---> ER s t).

  Lemma axAUu s t : mprv (AU s t ---> t :\/: (s :/\: AX (AU s t))).

  Lemma rAUw s t s' t' : mprv (s ---> s') -> mprv (t ---> t') -> mprv (AU s t ---> AU s' t').

  Lemma axAUEGF s t : mprv (AU s t ---> EG (~~: t ) ---> Bot).

de Morgan Lemmas

  Lemma dmAU s t : mprv ((~~: AU s t ) ---> ER (~~: s) (~~: t)).

  Lemma dmER s t : mprv ((~~: ER s t ) ---> AU (~~: s) (~~: t)).

  Lemma dmO s t : mprv (~~: (s :\/: t ) ---> (~~: s ) :/\: (~~: t )).

  Lemma dmA s t : mprv (~~: (s :/\: t ) ---> (~~: s ) :\/: (~~: t )).

  Lemma dmAi s t : mprv ((~~: s ) :\/: (~~: t ) ---> ~~: (s :/\: t )).

  Lemma dmAUi s t : mprv (ER (~~: s) (~~: t) ---> (~~: AU s t )).

  Lemma dmERi s t : mprv (AU (~~: s) (~~: t) ---> (~~: ER s t )).

  Lemma axERu s t : mprv (ER s t ---> t :/\: (s :\/: EX (ER s t))).

  Lemma axAUERF s t : mprv (AU s t :/\: ER (~~: s) (~~: t) ---> Bot).

  Lemma axAUAEr s t u : mprv (AU (s :/\: u) (t :/\: u) ---> u).

  Lemma axAUAw s t u : mprv (AU (s :/\: u) (t :/\: u) ---> AU s t).

  Lemma EU_ind s t u :
    mprv (t ---> u) -> mprv (s ---> EX u ---> u) -> mprv (EU s t ---> u).

  Lemma dmAR s t : mprv (~~: (AR s t ) <--> EU (~~: s) (~~: t)).

  Lemma axEUI s t : mprv (t ---> EU s t).

  Lemma axEUI2 s t : mprv (s ---> EX (EU s t) ---> EU s t).

  Lemma axAReq s t : mprv (AR s t <--> t :/\: (s :\/: AX (AR s t))).

  Lemma axEUeq s t : mprv (EU s t <--> t :\/: s :/\: EX (EU s t)).

  Lemma axEUw s t u : mprv (EU (s :/\: u) (t :/\: u) ---> EU s t).

  Lemma axEUEr s t u : mprv (EU (s :/\: u) (t :/\: u) ---> u).

  Lemma rAU_ind_weak u s t :
    mprv (t ---> u) -> mprv (AX u ---> u) -> mprv ((AU s t ) ---> u).

  Lemma rER_ind_weak u s t :
    mprv (u ---> t) -> mprv (u ---> EX u) -> mprv (u ---> ER s t).

End CTLTheory.

fset lemmas

Lemma andU (T : choiceType) (pS : pSystem) (F : T -> pS) (X Y : {fset T }) :
mprv ((\and_(s <- X `|` Y ) F s) <--> (\and_(s <- X ) F s) :/\: (\and_(s <- Y ) F s)).

Lemma bigA1 (T : choiceType) (pS : pSystem) (F : T -> pS) (s : T) :
mprv ((\and_(s <- [fset s ]) F s ) <--> F s).