PDL.v

Require Import Classical.

Set Implicit Arguments.
Unset Strict Implicit.



Inductive var := Var : nat -> var.
Inductive varp := Varp : nat -> varp.

Inductive prog :=
    | atomp : varp -> prog
    | seq : prog -> prog -> prog
    | orp : prog -> prog -> prog
    | star : prog -> prog 
    | test : form -> prog


with  form  :=
    | atomf : var -> form
    | false
    | not : form -> form
    | orf : form -> form -> form
    | box : prog -> form -> form.

Scheme form_mind := Induction for form Sort Prop 
with prog_mind := Induction for prog Sort Prop.



Notation "A ;; B" := (seq A B) (at level 45, right associativity, format "A  ;;  B").
Notation "A ∪ B" := (orp A B) (at level 50, left associativity, format "A  ∪  B").
Notation "A ⋆" := (star A)(at level 30, format "A ⋆").
Notation "[ a ] A" := (box a A)(right associativity, at level 0, format "[ a ] A").
Notation "A ?" := (test A) (at level 1,format "A ?").    

Notation  "¬ A" := (not A)(at level 60).
Infix "∨" := orf (at level 70).


Definition and A B := ¬ (¬ A ∨ ¬ B).
Definition true := ¬ false.
Definition imp A B :=  (¬ A) ∨ B.

Infix "∧" := and (at level 70).
Infix "→" := imp (at level 80, right associativity).



Definition dia a A := ¬ ([a] (¬ A)).
Notation "< a > A" := (dia a A)(right associativity, at level 0, format "< a > A").


Fixpoint exp (a : prog) (n : nat) : prog :=
    match n with 
    | O => true?
    | S n' => a ;; exp a n'
    end.

Definition pls a := a ;; a⋆.
Notation "a ⁺" := (pls a) (at level 70).


Structure PDL := {
    state :> Set;
    relation : varp -> state -> state -> Prop;
    valuation : var -> state -> Prop;
}.



Inductive step {S : PDL} (R : S -> S -> Prop) : S -> S -> Prop :=
    | rel x : step R x x
    | next x y z : R x y -> step R y z -> step R x z.

Fixpoint eval {M : PDL} (A : form) (x : M) : Prop :=
    match A with 
    | atomf a => valuation a x
    | false => False
    | ¬ A => ~ (eval A x)
    | L ∨ R => eval L x \/ eval R x
    | [a]A => forall y : M, trans a x y -> eval A y
    end

with trans {M : PDL} (p : prog) (x y : M) : Prop :=
    match p with 
    | atomp a => relation a x y
    | a ;; b => exists z, trans a x z /\ trans b z y 
    | a ∪ b => trans a x y \/ trans b x y
    | A? => x = y /\ eval A y
    | a⋆ => step (trans a) x y
    end.



Definition valid (M : PDL) (A : form) := forall x : M, eval A x.
Notation "M ⊨ A" := (valid M A)(at level 70).

Definition tautology (A : form) := forall M, M ⊨ A.
Notation "⊨ A" := (tautology A)(at level 80).

Definition equiv A B := forall M, M ⊨ A <-> M ⊨ B.
Notation "A == B" := (equiv A B)(at level 110).

Variable (A : form).
Check (A ∧ (A → A)).

Inductive prv : form -> Prop :=
    | K a A B : prv ([a](A → B) → ([a]A → [a]B))    

    | seqE a b A : prv ([a;;b] A → [a][b]A)
    | seqI a b A : prv ([a][b] A → [a;;b]A)
    | orE a b A : prv ([a ∪ b] A → [a]A ∧ [b]A)
    | orI a b A : prv ([a]A ∧ [b]A → [a ∪ b]A)
    | starE a A : prv ([a⋆]A → (A ∧ [a][a⋆]A))
    | starI a A : prv ((A ∧ [a][a⋆]A) → [a⋆]A)
    | starInd a A : prv (A → [a]A) -> prv (A → [a⋆]A)
    | testE A B : prv ([A?]B → A → B)
    | testI A B : prv ((A → B) → [A?]B)

    | mp A B  : prv (A → B) -> prv A -> prv B
    | boxI a A : prv A -> prv ([a]A)

    | notE A : prv (((A → false) → false) → A)
    | impI A B : prv (A → (B → A))
    | impD A B C : prv ((A → (B → C)) → ((A → B) → (A → C))).

Ltac impI := apply imply_to_or; intro.


Theorem soundness (A : form) :   
    prv A -> ⊨ A.
Proof.
    intros.
    unfold tautology, valid.
    induction H; simpl; intros; try (repeat impI); intros; eauto.
    +   specialize (H0 y H1).
        case (H _ H1); intro; eauto.
        case (H2 H0).
    +   induction H0 as [z [Hx Hy]].
        apply H with z; auto.
    +   apply and_not_or; split; intro F; apply F; intros; apply H; [left|right]; auto.
    +   apply not_or_and in H as [Ha Hb].
        apply NNPP in Ha; apply NNPP in Hb.
        induction H0; eauto.
    +   intro F.
        generalize (or_to_imply (eval A0 x) (~
            (forall y : M,trans a x y -> forall y0 : M, step (trans a) y y0 -> eval A0 y0)) F); intro.
        clear F.
        apply H0; clear H0.
        -   apply H; constructor.
        -   intros; apply H.
            apply next with y; auto.
    +   apply not_or_and in H.
        induction H; apply NNPP in H; apply NNPP in H1.
        induction H0; auto.
        apply H1 with y; auto.
    +   generalize (IHprv M x); simpl in IHprv; simpl; intro.
        specialize (or_to_imply (eval A0 x) (forall y : M, trans a x y -> eval A0 y) H2 H0); intro.       
        induction H1; auto.
        apply IHstep; auto; intros.
        generalize (IHprv M y); simpl in IHprv; simpl; intro.
        specialize (or_to_imply (eval A0 y) (forall y0 : M, trans a y y0 -> eval A0 y0) H6); intro.
        apply H3 in H1.
        apply H7; auto.
    +   induction H0; subst.
        induction H; auto.
        case (H H1).
    +   simpl in IHprv1.
        specialize (IHprv2 M x).
        induction (IHprv1 M x); eauto.
        contradiction H1; auto.
    +   case H; intro.
        apply not_or_and in H0.
        induction H0.
        apply NNPP in H0; auto.
        inversion H0.
    +   induction H0.
        contradiction H0; auto.
        induction H.
        case (H H1).
        induction H; auto.
        case (H H0).
Qed.