ltl.v

Require Import Relations.

Set Implicit Arguments.

Section LTL.
  Variable State : Type.
  
  (* Traces *)
  CoInductive Trace : Type :=
    | Cons : State -> Trace -> Trace.
  
  Definition head (trace : Trace) :=
    match trace with Cons head tail => head end.
  
  Definition tail (trace : Trace) :=
    match trace with Cons head tail => tail end.
  
  (* Formulas *)
  Definition TraceFormula := Trace -> Prop.
  Definition StateFormula := State -> Prop.
  
  (* Operators *)
  Definition next (F : TraceFormula) : TraceFormula :=
    fun trace => F (tail trace).
  
  Definition and (F : TraceFormula) (G : TraceFormula) : TraceFormula :=
    fun trace => (F trace) /\ (G trace).
  
  Definition or (F : TraceFormula) (G : TraceFormula) : TraceFormula :=
    fun trace => (F trace) \/ (G trace).
  
  Definition equiv (F : TraceFormula) (G : TraceFormula) : TraceFormula :=
    fun trace => (F trace) <-> (G trace).
  
  Definition not (F : TraceFormula) : TraceFormula :=
    fun trace => (F trace) -> False.
  
  Definition implies (F : TraceFormula) (G : TraceFormula) : TraceFormula :=
    fun trace => (F trace) -> (G trace).
  
  CoInductive globally (F : TraceFormula) : Trace -> Prop :=
    | globally_I trace: F trace -> globally F (tail trace) -> globally F trace.
  
  Inductive eventually (F : TraceFormula) : Trace -> Prop :=
    | eventually_B trace: F trace -> eventually F trace
    | eventually_S trace: eventually F (tail trace) -> eventually F trace.
  
  Inductive until (F : TraceFormula) (G : TraceFormula) : Trace -> Prop :=
    | until_B trace: G trace -> until F G trace
    | until_S trace: F trace -> until F G (tail trace) -> until F G trace.
End LTL.