Modal mu calculus in Coq

modal_mu.v

Require Import Coq.Classes.SetoidClass.

Program Instance Iff1Setoid{A:Type} : Setoid (A->Prop) := {|
  equiv := fun P Q => forall x, P x <-> Q x
|}.
Next Obligation.
  split.
  - intros P x; reflexivity.
  - intros P Q H x; symmetry; exact (H x).
  - intros P Q R H0 H1 x; transitivity (Q x); [exact (H0 x)|exact (H1 x)].
Qed.

Class Monotone{A:Type}(P:(A->Prop)->A->Prop) := {
  monotonicity :
    forall(Q R:A->Prop),
      (forall x, Q x -> R x) -> (forall x, P Q x -> P R x)
}.
Class Antitone{A:Type}(P:(A->Prop)->A->Prop) := {
  antitonicity :
    forall(Q R:A->Prop),
      (forall x, Q x -> R x) -> (forall x, P R x -> P Q x)
}.
Instance MonotoneRefl{A:Type} : Monotone (fun P:A->Prop => P).
Proof.
  constructor.
  intros Q R H; exact H.
Qed.

Instance const_monotone{A:Type} (P:A->Prop) : Monotone (fun _ => P).
Proof.
  constructor.
  intros S T m x H; exact H.
Qed.

Instance const_antitone{A:Type} (P:A->Prop) : Antitone (fun _ => P).
Proof.
  constructor.
  intros S T m x H; exact H.
Qed.

Instance composite_monotone{A:Type} (P Q:(A->Prop)->A->Prop) :
  Monotone P -> Monotone Q -> Monotone (fun X => P (Q X)).
Proof.
  intros [pm] [qm]; constructor.
  intros S T m; apply pm, qm, m.
Qed.

Instance composite_antitone{A:Type} (P Q:(A->Prop)->A->Prop) :
  Monotone P -> Antitone Q -> Antitone (fun X => P (Q X)).
Proof.
  intros [pm] [qm]; constructor.
  intros S T m; apply pm, qm, m.
Qed.

Definition and1{A:Type} (P Q:A->Prop) (x:A) := P x /\ Q x.
Definition or1{A:Type} (P Q:A->Prop) (x:A) := P x \/ Q x.
Definition not1{A:Type} (P:A->Prop) (x:A) := ~P x.
Definition impl1{A:Type} (P Q:A->Prop) (x:A) := P x -> Q x.
Definition True1{A:Type} (x:A) := True.
Definition False1{A:Type} (x:A) := False.

Notation "x /1\ y" := (and1 x y) (at level 80, right associativity).
Notation "x \1/ y" := (or1 x y) (at level 85, right associativity).
Notation "~1 x" := (not1 x) (at level 75, right associativity).
Notation "x -1> y" := (impl1 x y) (at level 100, right associativity).

Definition diamond{A:Type} (R:A->A->Prop) (P:A->Prop) : A->Prop :=
  fun x => exists y, R x y /\ P y.
Definition box{A:Type} (R:A->A->Prop) (P:A->Prop) : A->Prop :=
  fun x => forall y, R x y -> P y.

Instance and1_monotone{A:Type} (P Q:(A->Prop)->A->Prop):
  Monotone P -> Monotone Q -> Monotone (fun X => P X /1\ Q X).
Proof.
  intros [pm] [qm]; constructor.
  intros S T m x [HP HQ].
  split; [apply (pm _ _ m _ HP)|apply (qm _ _ m _ HQ)].
Qed.
Instance and1_antitone{A:Type} (P Q:(A->Prop)->A->Prop):
  Antitone P -> Antitone Q -> Antitone (fun X => P X /1\ Q X).
Proof.
  intros [pm] [qm]; constructor.
  intros S T m x [HP HQ].
  split; [apply (pm _ _ m _ HP)|apply (qm _ _ m _ HQ)].
Qed.
Instance or1_monotone{A:Type} (P Q:(A->Prop)->A->Prop):
  Monotone P -> Monotone Q -> Monotone (fun X => P X \1/ Q X).
Proof.
  intros [pm] [qm]; constructor.
  intros S T m x [HP|HQ].
  - left; apply (pm _ _ m _ HP).
  - right; apply (qm _ _ m _ HQ).
Qed.
Instance or1_antitone{A:Type} (P Q:(A->Prop)->A->Prop):
  Antitone P -> Antitone Q -> Antitone (fun X => P X \1/ Q X).
Proof.
  intros [pm] [qm]; constructor.
  intros S T m x [HP|HQ].
  - left; apply (pm _ _ m _ HP).
  - right; apply (qm _ _ m _ HQ).
Qed.
Instance not1_monotone{A:Type} (P:(A->Prop)->A->Prop):
  Antitone P -> Monotone (fun X => ~1 (P X)).
Proof.
  intros [pm]; constructor.
  intros S T m x H HP.
  apply H, (pm _ _ m _ HP).
Qed.
Instance not1_antitone{A:Type} (P:(A->Prop)->A->Prop):
  Monotone P -> Antitone (fun X => ~1 (P X)).
Proof.
  intros [pm]; constructor.
  intros S T m x H HP.
  apply H, (pm _ _ m _ HP).
Qed.
Instance impl1_monotone{A:Type} (P Q:(A->Prop)->A->Prop):
  Antitone P -> Monotone Q -> Monotone (fun X => P X -1> Q X).
Proof.
  intros [pm] [qm]; constructor.
  intros S T m x H HP.
  apply (qm _ _ m), H, (pm _ _ m), HP.
Qed.
Instance impl1_antitone{A:Type} (P Q:(A->Prop)->A->Prop):
  Monotone P -> Antitone Q -> Antitone (fun X => P X -1> Q X).
Proof.
  intros [pm] [qm]; constructor.
  intros S T m x H HP.
  apply (qm _ _ m), H, (pm _ _ m), HP.
Qed.

Instance diamond_monotone{A:Type} (R:A->A->Prop) (P:(A->Prop)->A->Prop):
  Monotone P -> Monotone (fun X => diamond R (P X)).
Proof.
  intros [pm]; constructor.
  intros S T m x [y [Hy H]].
  exists y; split; [exact Hy|].
  apply (pm _ _ m), H.
Qed.
Instance diamond_antitone{A:Type} (R:A->A->Prop) (P:(A->Prop)->A->Prop):
  Antitone P -> Antitone (fun X => diamond R (P X)).
Proof.
  intros [pm]; constructor.
  intros S T m x [y [Hy H]].
  exists y; split; [exact Hy|].
  apply (pm _ _ m), H.
Qed.
Instance box_monotone{A:Type} (R:A->A->Prop) (P:(A->Prop)->A->Prop):
  Monotone P -> Monotone (fun X => box R (P X)).
Proof.
  intros [pm]; constructor.
  intros S T m x H y Hy.
  apply (pm _ _ m), (H y Hy).
Qed.
Instance box_antitone{A:Type} (R:A->A->Prop) (P:(A->Prop)->A->Prop):
  Antitone P -> Antitone (fun X => box R (P X)).
Proof.
  intros [pm]; constructor.
  intros S T m x H y Hy.
  apply (pm _ _ m), (H y Hy).
Qed.

Ltac intro_box :=
  match goal with
  | [ |- @box _ ?R _ ?x ] =>
      let y := fresh "y" in
      let Hy := fresh "H" in
      intros y Hy;
      repeat match goal with
      | [ HH : @box _ R _ x |- _ ] =>
          specialize (HH y Hy)
      end;
      clear dependent x;
      rename y into x
  end.

Ltac elim_diamond H :=
  match type of H with
  | @diamond _ ?R _ ?x =>
      let y := fresh "y" in
      let Hy := fresh "H" in
      destruct H as [y [Hy H]];
      repeat match goal with
      | [ HH : @box _ R _ x |- _ ] =>
          specialize (HH y Hy)
      end;
      match goal with
      | [ |- @diamond _ R _ x ] =>
          exists y; split; [exact Hy|]
      end;
      clear dependent x;
      rename y into x
  end.

Unset Elimination Schemes.
Inductive lfp{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} (x:A) : Prop :=
  | lfp_intro (Q:A->Prop) (LE : forall y, Q y -> lfp P y) (IN : P Q x) : lfp P x.
Set Elimination Schemes.

Definition lfp_ind{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} (P0:A->Prop)
  (f : forall (x : A), P (lfp P) x -> P P0 x -> P0 x) :=
  fix F(x:A) (l:lfp P x) : P0 x :=
  match l with
  | lfp_intro _ _ Q LE IN =>
      f x (monotonicity _ _ LE _ IN)
        (monotonicity _ _ (fun y q => F y (LE y q)) _ IN)
  end.

CoInductive gfp{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} (x:A) : Prop :=
  | gfp_intro (Q:A->Prop) (LE : forall y, Q y -> gfp P y) (IN : P Q x) : gfp P x.

Definition gfp_coind{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} (P0:A->Prop)
  (f : forall (x : A), P0 x -> P P0 x) :=
  cofix F(x:A) (p:P0 x) : gfp P x :=
  gfp_intro P x P0 (fun y H => F y H) (f x p).

Notation "'mu' x .. y , p" := (lfp (fun x => .. (lfp (fun y => p)) ..))
  (at level 200, x binder, right associativity,
   format "'[' 'mu'  '/  ' x  ..  y ,  '/  ' p ']'")
  : type_scope.
Notation "'nu' x .. y , p" := (gfp (fun x => .. (gfp (fun y => p)) ..))
  (at level 200, x binder, right associativity,
   format "'[' 'nu'  '/  ' x  ..  y ,  '/  ' p ']'")
  : type_scope.

Theorem lfp_unfold{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} :
  lfp P == P (lfp P).
Proof.
  intros x.
  split.
  - intros [Q LE IN].
    apply (monotonicity _ _ LE), IN.
  - intros H.
    exists (lfp P); [auto|]; exact H.
Qed.

Theorem gfp_unfold{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} :
  gfp P == P (gfp P).
Proof.
  intros x.
  split.
  - intros [Q LE IN].
    apply (monotonicity _ _ LE), IN.
  - intros H.
    exists (gfp P); [auto|]; exact H.
Qed.

Theorem lfp_accum{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} (Q:A->Prop) :
  (forall x, lfp (fun X => P (Q /1\ X)) x -> Q x) -> (forall x, lfp P x -> Q x).
Proof.
  intros H x Hx.
  apply H.
  induction Hx as [x _ IHx].
  apply lfp_unfold.
  revert x IHx; apply monotonicity; intros x IHx.
  split; [apply H, IHx|exact IHx].
Qed.

Theorem gfp_accum{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} (Q:A->Prop) :
  (forall x, Q x -> gfp (fun X => P (Q \1/ X)) x) -> (forall x, Q x -> gfp P x).
Proof.
  intros H x Hx.
  apply H in Hx.
  revert x Hx; apply gfp_coind; intros x CIHx.
  apply gfp_unfold in CIHx.
  revert x CIHx; apply monotonicity; intros x CIHx.
  destruct CIHx as [CIHx|CIHx]; [apply H, CIHx|exact CIHx].
Qed.

Theorem lfp_accum'{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} (Q:A->Prop) :
  (forall x, P (lfp (fun X => Q /1\ P X)) x -> Q x) -> (forall x, lfp P x -> Q x).
Proof.
  intros H x Hx.
  apply H.
  induction Hx as [x _ IHx].
  revert x IHx; apply monotonicity; intros x IHx.
  apply lfp_unfold.
  split; [apply H, IHx|exact IHx].
Qed.

Theorem gfp_accum'{A:Type} (P:(A->Prop)->A->Prop) {PM:Monotone P} (Q:A->Prop) :
  (forall x, Q x -> P (gfp (fun X => Q \1/ P X)) x) -> (forall x, Q x -> gfp P x).
Proof.
  intros H x Hx.
  apply H in Hx.
  revert x Hx; apply gfp_coind; intros x CIHx.
  revert x CIHx; apply monotonicity; intros x CIHx.
  apply gfp_unfold in CIHx.
  destruct CIHx as [CIHx|CIHx]; [apply H, CIHx|exact CIHx].
Qed.

Instance lfp_monotone{A:Type} (R:A->A->Prop) (P:(A->Prop)->(A->Prop)->A->Prop)
  {PM : forall X, Monotone (P X)} :
  (forall Y, Monotone (fun X => P X Y)) -> Monotone (fun X => lfp (P X)).
Proof.
  intros PM'; constructor.
  intros S T m x H.
  induction H as [x _ IHx].
  apply lfp_unfold.
  revert x IHx; apply (@monotonicity _ _ (PM' _)), m.
Qed.
Instance lfp_antitone{A:Type} (R:A->A->Prop) (P:(A->Prop)->(A->Prop)->A->Prop)
  {PM : forall X, Monotone (P X)} :
  (forall Y, Antitone (fun X => P X Y)) -> Antitone (fun X => lfp (P X)).
Proof.
  intros PM'; constructor.
  intros S T m x H.
  induction H as [x _ IHx].
  apply lfp_unfold.
  revert x IHx; apply (@antitonicity _ _ (PM' _)), m.
Qed.
Instance gfp_monotone{A:Type} (R:A->A->Prop) (P:(A->Prop)->(A->Prop)->A->Prop)
  {PM : forall X, Monotone (P X)} :
  (forall Y, Monotone (fun X => P X Y)) -> Monotone (fun X => gfp (P X)).
Proof.
  intros PM'; constructor.
  intros S T m x H.
  revert x H; apply gfp_coind; intros x CIHx.
  apply gfp_unfold in CIHx.
  revert x CIHx; apply (@monotonicity _ _ (PM' _)), m.
Qed.
Instance gfp_antitone{A:Type} (R:A->A->Prop) (P:(A->Prop)->(A->Prop)->A->Prop)
  {PM : forall X, Monotone (P X)} :
  (forall Y, Antitone (fun X => P X Y)) -> Antitone (fun X => gfp (P X)).
Proof.
  intros PM'; constructor.
  intros S T m x H.
  revert x H; apply gfp_coind; intros x CIHx.
  apply gfp_unfold in CIHx.
  revert x CIHx; apply (@antitonicity _ _ (PM' _)), m.
Qed.

Goal forall{A:Type} (R:A->A->Prop) (X Y:A->Prop),
  forall x, box R (X /1\ Y) x <-> (box R X /1\ box R Y) x.
Proof.
  intros A R X Y x.
  split.
  - intros H.
    split.
    + intro_box.
      destruct H as [H _].
      exact H.
    + intro_box.
      destruct H as [_ H].
      exact H.
  - intros [H0 H1].
    intro_box.
    split; [exact H0|exact H1].
Qed.

Goal forall{A:Type} (R:A->A->Prop) (X Y:A->Prop),
  forall x, diamond R (X \1/ Y) x <-> (diamond R X \1/ diamond R Y) x.
Proof.
  intros A R X Y x.
  split.
  - intros H.
    destruct H as [y [Hy [H|H]]]; [left|right]; exists y; (split; [exact Hy|]); exact H.
  - intros [H0|H1].
    + elim_diamond H0.
      left.
      exact H0.
    + elim_diamond H1.
      right.
      exact H1.
Qed.


Goal forall{A:Type} (R:A->A->Prop) (P:(A->Prop)->(A->Prop)) {PM:Monotone P} (x:A),
  (mu X, P X) x -> (nu X, P X) x.
Proof.
  intros A R P PM x H.
  induction H as [x _ H].
  apply gfp_unfold.
  revert x H; apply monotonicity; intros x H.
  exact H.
Qed.

Goal forall{A:Type} (R:A->A->Prop) (x:A),
  (nu X, diamond R True1 /1\ box R X) x -> (nu X, diamond R X) x.
Proof.
  intros A R x H.
  revert x H; apply gfp_coind; intros x H.
  apply gfp_unfold in H.
  destruct H as [H0 H1].
  elim_diamond H0.
  exact H1.
Qed.