MuCal.v

From Autosubst Require Import Autosubst.
Require Import Ensembles.
Require Import Finite_sets.
Require Import Classical.

Set Implicit Arguments.
Unset Strict Implicit.


Notation sets := Ensemble.
Notation "∅" := Empty_set.
Notation "x ∈ X" := (In _ X x)(at level 50).
Notation "A ∩ B" := (Intersection _ A B)(at level 40).
Notation "A ∪ B" := (Union _ A B)(at level 40).
Notation "A ⊂ B" := (Included _ A B)(at level 30).
Notation "A // B" := (Setminus _ A B)(at level 40).
(* Notation "¬ A" := (Complement _ A)(at level 40). *)
Notation "[ S => P ]" := (fun S => P).
Notation extension := Extensionality_Ensembles.



Inductive varp := Varp : nat -> varp.

Inductive form  : Type :=
    | Var : var -> form
    | Fls : form
    | Or : form -> form -> form 
    | Not : form -> form    
    | Box : prog -> form -> form 
    | Mu : {bind form} -> form


with prog :=
    | atom : varp -> prog
    | seq : prog -> prog -> prog
    | orp : prog -> prog -> prog
    | star : prog -> prog 
    | test : form -> prog.


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 > A" := (Dia a A)(right associativity, at level 201, format "< a >. A"). *)
Notation "A ?" := (test A) (at level 1,format "A ?").
Notation  "¬ A" := (Not A)(at level 60).
Infix "∨" := Or (at level 70).

Definition And A B := ¬ (¬ A ∨ ¬ B).
Definition Tru := ¬ Fls.
Definition Imp A B :=  (¬ A) ∨ B.
Infix "∧" := And (at level 70).
Infix "→" := Imp (at level 80, right associativity).


Instance Ids_forms : Ids form. derive. Defined.
Instance Rename_forms : Rename form. derive. Defined.
Instance Subst_forms : Subst form. derive. Defined.
Instance SubstLemmas_form : SubstLemmas form. derive. Qed.

Infix "∘" := scomp (at level 56, left associativity) : subst_scope.
Notation "s ∙ sigma" := (scons s sigma) (at level 55, sigma at level 56, right associativity) : subst_scope.
Notation "⇑ σ" := (up σ)(at level 30).




Module Model.


Parameter state : Set.
Parameter trans : state -> varp -> state -> Prop.
Definition Env := var -> state -> Prop.
Parameter valuation : Env.

Inductive step {S : Type} (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.

Definition cons (X : state -> Prop) (f : Env) : Env :=
    fun n => match n with | O => X | S n' => f n' end.


Fixpoint eval (f : Env) (A : form) (x : state) : Prop :=
    match A with 
    | Var a => valuation a x
    | Fls => False
    | ¬ A => ~ (eval f A x)
    | L ∨ R => eval f L x \/ eval f R x
    | [a]A => forall y, evalt f a x y -> eval f A y
    | Mu A' => forall X, (eval (cons X f) A') ⊂ X -> x ∈ X 
    end


with evalt (f : Env )(p : prog) (x y : state) : Prop :=
    match p with 
    | atom a => trans x a y
    | a ;; b => exists z, evalt f a x z /\ evalt f b z y 
    | a + b => evalt f a x y \/ evalt f b x y
    | A? => x = y /\ eval f A y
    | a⋆ => step (evalt f a) x y
    end.

Theorem mu_subst A f :
    (Mu A).[f] = Mu (A.[⇑ f]).
Proof.
    asimpl; auto.
Qed.



Definition sat s f := forall e, s ∈ eval e f.
Notation "s |= f" := (sat s f)(at level 50).

Definition valid f := forall s, s |= f.
Notation "|= f" := (valid f) (at level 30).


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)

    | muA A : prv (A.[Mu A ∙ ids] → Mu A)
    | muI A B : prv (A.[B ∙ ids] → B) -> prv (Mu A → B)

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

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