introduced constants for true and false

Author: palmskog

infseq.v

@@ -89,8 +89,14 @@ Definition or_tl (P Q: infseq T -> Prop) : infseq T -> Prop :=
 Definition not_tl (P : infseq T -> Prop) : infseq T -> Prop := 
   fun s => ~ P s.
 
+(* constants *)
+Definition True_tl : infseq T -> Prop := fun _ => True.
+Definition False_tl : infseq T -> Prop := fun _ => False.
+
 End sec_modal_op_defn.
 
+Hint Unfold True_tl False_tl.
+
 Arguments now [T] _ _.
 Arguments next [T] _ _.
 Arguments consecutive [T] _ _.
@@ -108,6 +114,9 @@ Arguments and_tl [T] _ _ _.
 Arguments or_tl [T] _ _ _.
 Arguments not_tl [T] _ _.
 
+Arguments True_tl {T} _.
+Arguments False_tl {T} _.
+
 Notation "A ->_ B" := (impl_tl A B) (right associativity, at level 90).
 Notation "A /\_ B" := (and_tl A B) (right associativity, at level 80).
 Notation "A \/_ B" := (or_tl A B) (right associativity, at level 85).
@@ -489,8 +498,8 @@ Lemma eventually_monotonic_simple :
   (forall s, P s -> Q s) -> 
   forall s, eventually P s -> eventually Q s.
 Proof.
-intros P Q PQ s. 
-apply (eventually_monotonic P Q (fun s:infseq T => True)); auto.
+intros P Q PQ s.
+apply (eventually_monotonic P Q True_tl); auto.
 Qed.
 
 Lemma inf_often_monotonic :
@@ -669,6 +678,8 @@ unfold not_tl in Js.
 case rl; trivial.
 Qed.
 
+
+
 (* connector facts *)
 
 Lemma and_tl_comm : 

map.v

@@ -202,7 +202,7 @@ Lemma always_map_conv :
    forall (s: infseq A), always Q (map f s) -> always P s.
 Proof.
 intros f P Q QP s.
-apply (always_map_conv_ext f P Q (fun _ => True)); auto.
+apply (always_map_conv_ext f P Q True_tl); auto.
 Qed.
 
 Lemma weak_until_map :