On the Formalization of the Modal μ-Calculus in the Calculus of Inductive Constructionsに載ってたコードが古かったので新しいものに書き換えた

MuCalculus.v

Parameter Act var : Set.

Axiom var_nat : exists srj : var -> nat, forall n, exists x, srj x = n.

Inductive o : Set := 
    | ff : o 
    | Not : o -> o 
    | Imp : o -> o -> o 
    | Box : Act -> o -> o 
    | Var : var -> o 
    | mu : (var -> o) -> o.


Notation "⊥" := ff.
Notation "¬ e" := (Not e)(at level 10).
Notation "[ a ] e" :=(Box a e)(at level 20).
Notation "e1 → e2" := (Imp e1 e2) (at level 50).



Fixpoint isin (x : var) (f : o) : Prop :=
    match f with 
    | ff => False 
    | Not f' => isin x f' 
    | Imp f1 f2 => isin x f1 \/ isin x f2 
    | Box a f' => isin x f' 
    | Var y => x = y
    | mu F => forall y, isin x (F y) 
    end. 

Fixpoint notin (x : var) (f : o) : Prop :=
    match f with
    | ff => True 
    | Not f' => notin x f' 
    | Imp f1 f2 => notin x f1 /\ notin x f2 
    | Box a f' => notin x f' 
    | Var y => x <> y
    | mu F => forall y, x <> y -> notin x (F y) 
    end.


Fixpoint posin (x : var) (f : o) : Prop :=
    match f with 
    | ff => True 
    | Not f' => negin x f' 
    | Imp f1 f2 => negin x f1 /\ posin x f2 
    | Box a f' => posin x f' 
    | Var y => True
    | mu F => forall y, x <> y -> posin x (F y) 
    end

with  negin (x : var) (f : o) : Prop :=
    match f with 
    | ff => True 
    | Not f' => posin x f' 
    | Imp f1 f2 => posin x f1 /\ negin x f2 
    | Box a f' => negin x f' 
    | Var y => x <> y
    | mu F => forall y, x <> y -> negin x (F y) 
    end.

Fixpoint iswf (f : o) : Prop :=
    match f with 
    | ff => True 
    | Not f' => iswf f' 
    | Imp f1 f2 => iswf f1 /\ iswf f2 
    | Box a f' => iswf f' 
    | Var y => True 
    | mu F => forall x, iswf (F x) /\ (notin x (mu F) -> posin x (F x))
    end.

Record wfo : Set := {
    prp :> o;
    cond : iswf prp;
}.

Lemma neverempty (x : var) : 
    exists y,  x <>y.
    induction var_nat as [f Hf].
    generalize (Hf (f x + 1));  intro Hy.
    induction Hy as [y Hy].
    exists y; intro F; subst.
    induction (f y); simpl in *; inversion Hy; auto.
Qed.    

Require Import Nat Lia Omega.

Lemma separation x y f :
    notin x f -> isin y f -> x <> y.
Proof.
    induction f; simpl; subst; auto.
    +   intros [Hf1 Hf2] H.
        induction H; eauto.
    +   intros; subst; auto.
    +   rename o0 into f; intros.
        induction var_nat as [g Hg].
        pose (n := g y + g x).
        generalize (Hg (n +1)); intro Hxy.
        induction Hxy as [xy gxy].
        apply H with xy; eauto.
        apply H0. intro F; subst. lia.
Qed.

Lemma notin_posin_negin (x:var)(A :o) :
    notin x A  -> posin x A  /\ negin x A.
Proof.
    induction A; simpl; intros; auto.
    +   apply IHA in H.
        induction H; split; auto.
    +   induction H as [H1 H2]; apply IHA1 in H1; apply IHA2 in H2.
        induction H1; induction H2; repeat split; auto.
    +   rename o0 into f; split; intros; apply H0 in H1; apply H in H1; apply H1.
Qed.

Lemma notin_posin (x : var) (A : o): 
    notin x A -> posin x A.
Proof.
    intro; apply notin_posin_negin; auto.
Qed.        

Lemma notin_negin (x : var) (A : o): 
    notin x A -> negin x A.
Proof. 
    intro; apply notin_posin_negin; auto.
Qed.      


Parameter bind : var -> o -> Prop.
Reserved Notation "f1 ⊴  f2" (at level 30).
Notation "x ↦ f" := (bind x f)(at level 30).

Section Expansion.



Inductive expto : o -> o -> Prop :=
    | expto_rflx Φ : Φ ⊴ Φ 
    | expto_btrns x Φ Ψ :
        x ↦ Φ -> Φ ⊴ Ψ -> (Var x) ⊴ Ψ
    | expto_Not Φ Ψ :
        Φ ⊴ Ψ -> (¬ Φ) ⊴ (¬ Ψ)
    | expto_Imp Φ1 Ψ1 Φ2 Ψ2 :
        Φ1 ⊴ Ψ1 -> Φ2 ⊴ Ψ2 -> (Φ1 → Φ2) ⊴ (Ψ1 → Ψ2)
    | expto_Box Φ Ψ a :
        Φ ⊴ Ψ -> [a]Φ ⊴ [a]Ψ
    | expto_mu f g : 
        (forall x, f x ⊴ g x) -> mu f ⊴ mu g
    where "f1 ⊴ f2" := (expto f1 f2).

Hint Constructors expto : core.


Lemma expto_bind x Φ :
    x ↦ Φ -> (Var x) ⊴ Φ.
Proof.
    induction Φ; intro; eapply expto_btrns; eauto.
Qed.

Lemma expto_trns Φ Ψ ξ :
    Φ ⊴ Ψ -> Ψ ⊴ ξ -> Φ ⊴ ξ.
Proof.    
    intro H. generalize ξ.
    induction H; intros; eauto; clear H;
    try match goal with
    | [H : _ ⊴ _ |- _] => inversion H; subst; auto
    end.
Qed.

End Expansion.

Notation "f1 ⊴  f2" := (expto f1 f2)(at level 30).





Inductive olist : Set :=
    | nil : olist
    | cons : o -> olist -> olist.

Fixpoint Boxlist (a : Act) (l : olist) : olist :=
    match l with 
    | nil => nil 
    | cons Φ l' => cons (Box a Φ) (Boxlist a l')
    end.



Parameter U : Set.
Parameter T : U -> o -> Prop.

Fixpoint Sequent (w : U) (Φ : o) (l : olist) :=
        match l with 
        | nil => T w Φ
        | cons Φ' l' => T w Φ' -> Sequent w Φ l' 
        end.
Section Proof_Rules.



Variable Φ Ψ ξ : o.
Variable w : U.

Axiom Not_I :
    (T w Φ -> T w ⊥) -> T w (¬ Φ).

Axiom Not_E : iswf Φ -> 
    T w Φ -> T w (¬ Φ) -> T w ⊥.

Axiom RAA : 
    (T w (¬ Φ) -> T w ⊥)  -> T w Φ.

Axiom Imp_I : 
    (T w Φ -> T w Ψ) -> T w (Φ → Ψ).

Axiom Imp_E : iswf Φ ->
    T w (Φ → Ψ) -> T w Φ -> T w Ψ.

Axiom Sc : forall (G : olist) (a : Act),
    (forall w', Sequent w' Φ G) -> Sequent w ([a]Φ) (Boxlist a G).

Axiom expto_R :
    Φ ⊴ Ψ -> T w Φ -> T w Ψ.

Axiom expto_L : 
    Φ ⊴ Ψ -> T w Ψ -> T w Φ.

Axiom mu_I : forall (F : var -> o),
     (forall z, z ↦ mu F -> T w (F z)) -> T w (mu F).

Axiom mu_E : forall (F : var -> o), iswf Φ ->
    (forall z, notin z (mu F) -> z ↦ Φ -> (forall w', T w' (F z) -> T w' Φ)) ->
    T w (mu F) -> T w Φ.



Lemma ff_E : (T w ⊥) -> (T w Φ).
Proof.
    intro F. apply RAA; auto.
Qed.

Lemma K (a : Act) : 
    (forall w' : U, T w' Ψ -> T w' Φ) -> 
    T w ([a]Ψ) -> T w ([a]Φ).
Proof.
    intros.
    generalize (Sc (cons Ψ nil) a); simpl. intro; eauto.
Qed.

End Proof_Rules.

Goal forall (Φ : wfo) (w : U),
    T w Φ <-> T w (mu (fun x => ¬ Φ → Var x)).
Proof.
    intros. generalize (cond Φ); intro.
    split; intro.
    +   apply mu_I; intros.
        apply Imp_I; intro.        
        generalize (Not_E Φ w H H0 H2); intro F.
        apply ff_E; auto.
    +   apply mu_E with ((fun x : var => ¬ Φ → Var x)); auto; intros.
        apply RAA; intro.
        assert (iswf (¬ Φ)) by (simpl; auto).
        generalize (Imp_E (¬ Φ) (Var z) w' H5 H3 H4); intro.
        eapply Not_E with Φ; auto.
        apply expto_R with (Var z); auto.
        eapply expto_btrns with Φ; auto.
        apply expto_rflx.
Qed.