Mefresa.Behaviour.LTL

This module is a contribution from Coq d'Art book

Require Import List.

Require Export Mefresa.Behaviour.CoInductionLib.

Section LTL.

Set Implicit Arguments.

Definition satisfies (A:Type) (l:LList A) (P:LList A -> Prop) : Prop := P l.
Hint Unfold satisfies: llists.

Notation "t '|=' p" := (satisfies t p) (at level 3, left associativity).

Inductive Atomic (A:Type) (At:A -> Prop) : LList A -> Prop :=
    Atomic_intro : forall (a:A) (l:LList A), At a -> Atomic At (LCons a l).

Hint Resolve Atomic_intro: llists.

Inductive Next (A:Type) (P:LList A -> Prop) : LList A -> Prop :=
    Next_intro : forall (a:A) (l:LList A), P l -> Next P (LCons a l).

Hint Resolve Next_intro: llists.

Lemma Next_example (X:Type) (a b:X) : satisfies (LCons a (forever b)) (Next (Atomic (eq b))).
Proof.
    rewrite (forever_unfold b); auto with llists.
Qed.

Inductive Eventually (A:Type) (P:LList A -> Prop) : LList A -> Prop :=
  | Eventually_here :
      forall (a:A) (l:LList A), P (LCons a l) -> Eventually P (LCons a l)
  | Eventually_further :
      forall (a:A) (l:LList A), Eventually P l -> Eventually P (LCons a l).

Hint Resolve Eventually_here Eventually_further: llists.

Lemma Eventually_of_LAppend (A:Type):
  forall (P:LList A -> Prop) (u v:LList A),
    Finite u ->
    satisfies v (Eventually P) -> satisfies (LAppend u v) (Eventually P).
Proof.
  unfold satisfies in |- *; simple induction 1; intros;
   autorewrite with llists using auto with llists.
Qed.

CoInductive Always (A:Type) (P:LList A -> Prop) : LList A -> Prop :=
  Always_LCons :
    forall (a:A) (l:LList A),
      P (LCons a l) -> Always P l -> Always P (LCons a l).

Hint Resolve Always_LCons: llists.

Lemma Always_Infinite (A:Type):
  forall (P:LList A -> Prop) (l:LList A),
      satisfies l (Always P) -> Infinite l.
Proof.
  intro P; cofix H.
  simple destruct l.
  intro H0; inversion H0.
  intros a0 l0 H0; split.
  apply H; auto.
  inversion H0; auto.
Qed.

Definition F_Infinite (A:Type) (P:LList A -> Prop) : LList A -> Prop :=
   Always (Eventually P).

Definition F_Infinite_2_Eventually (A:Type): forall (P:LList A -> Prop) l, F_Infinite P l-> Eventually P l.
  intros P l.
  case l.
  inversion 1.
  inversion 1.
   assumption.
Defined.

Section A_Proof_with_F_Infinite.

   Variables (A : Type) (a b c : A).

   Let w : LList A := LCons a (LCons b LNil).

   Let w_omega := omega w.

   Let P (l:LList A) : Prop := l = w_omega \/ l = LCons b w_omega.

  Remark P_F_Infinite :
   forall l:LList A, P l -> satisfies l (F_Infinite (Atomic (eq a))).
  Proof.
   unfold F_Infinite in |- *.
   cofix.
   intro l; simple destruct 1.
   intro eg; rewrite eg.
   unfold w_omega in |- *; rewrite omega_of_Finite.
   unfold w in |- *.
   autorewrite with llists using auto with llists.
   split.
   auto with llists.
   apply P_F_Infinite.
   unfold P in |- *; auto.
   unfold w in |- *; auto with llists.
   intro eg; rewrite eg.
   unfold w_omega in |- *; rewrite omega_of_Finite.
   unfold w in |- *.
   rewrite LAppend_LCons.
   split.
   auto with llists.
   apply P_F_Infinite.
   unfold P in |- *; left.
   rewrite <- LAppend_LCons.
   rewrite <- omega_of_Finite.
   trivial.
   auto with llists.
   unfold w in |- *; auto with llists.
  Qed.

  Lemma omega_F_Infinite : satisfies w_omega (F_Infinite (Atomic (eq a))).
  Proof.
   apply P_F_Infinite.
   unfold P in |- *; left.
   trivial.
  Qed.

End A_Proof_with_F_Infinite.

Theorem F_Infinite_cons :
  forall (A:Type) (P:LList A -> Prop) (a:A) (l:LList A),
    satisfies l (F_Infinite P) -> satisfies (LCons a l) (F_Infinite P).
Proof.
  split.
  inversion H.
  right.
  auto.
  assumption.
Qed.

Theorem F_Infinite_consR :
forall (A:Type) (P:LList A -> Prop) (a:A) (l:LList A),
   satisfies (LCons a l) (F_Infinite P) -> satisfies l (F_Infinite P).
Proof.
  inversion 1.
  assumption.
Qed.

Definition G_Infinite (A:Type) (P:LList A -> Prop) : LList A -> Prop :=
   Eventually (Always P).

Lemma always_a (A:Type) (a:A): satisfies (forever a) (Always (Atomic (eq a))).
Proof.
  unfold satisfies in |- *; cofix H.
  rewrite (forever_unfold a).
  auto with llists.
Qed.

Lemma LAppend_G_Infinite (A:Type) :
  forall (u v:LList A) (P:LList A -> Prop),
    Finite u ->
    satisfies v (G_Infinite P) ->
    satisfies (LAppend u v) (G_Infinite P).
Proof.
  simple induction 1.
  autorewrite with llists using auto.
  intros; autorewrite with llists using auto.
  unfold G_Infinite in |- *; auto with llists.
  right.
  apply H1.
  auto.
Qed.

Lemma LAppend_G_Infinite_R (A:Type) :
  forall (u v:LList A) (P:LList A -> Prop),
    Finite u ->
    satisfies (LAppend u v) (G_Infinite P) ->
    satisfies v (G_Infinite P).
Proof.
  simple induction 1.
  autorewrite with llists using auto.
  intros; autorewrite with llists using auto.
  rewrite LAppend_LCons in H2.
  inversion_clear H2.
  apply H1.
  inversion_clear H3.
  generalize H4; case (LAppend l v).
  intro H5; inversion H5.
  left.
  auto.
  auto.
Qed.

End LTL.

Hint Unfold satisfies: llists.
Hint Resolve Always_LCons: llists.
Hint Resolve Eventually_here Eventually_further: llists.
Hint Resolve Next_intro: llists.
Hint Resolve Atomic_intro: llists.