more inf_often and continuously lemmas

Author: palmskog

classical.v

@@ -54,6 +54,27 @@ apply E_next.
 assumption.
 Qed.
 
+Lemma not_continously_inf_often_not :
+  forall (P : infseq T -> Prop) (s : infseq T),
+  ~ continuously P s -> inf_often (~_ P) s.
+Proof.
+intros P.
+cofix c.
+intros [x s] cnyP.
+apply Always.
+  unfold continuously in cnyP.
+  apply not_eventually_always_not in cnyP.
+  apply always_now in cnyP.
+  unfold not_tl in cnyP.
+  apply not_always_eventually_not in cnyP.
+  assumption.
+apply c.
+intros cnynP.
+contradict cnyP.
+apply E_next.
+assumption.
+Qed.
+
 Lemma not_tl_and_tl_or_tl :
   forall (P Q : infseq T -> Prop) (s : infseq T),
   (~_ (P /\_ Q)) s -> ((~_ P) \/_ (~_ Q)) s.
@@ -67,4 +88,5 @@ End sec_classical.
 Implicit Arguments not_eventually_not_always [T P s].
 Implicit Arguments not_always_eventually_not [T P s].
 Implicit Arguments not_inf_often_continuously_not [T P s].
+Implicit Arguments not_continously_inf_often_not [T P s].
 Implicit Arguments not_tl_and_tl_or_tl [T P Q s].

infseq.v

@@ -381,30 +381,6 @@ Qed.
 
 (* not_tl inside operators *)
 
-Lemma continuously_not_inf_often : 
-  forall (P : infseq T -> Prop) (s : infseq T),
-  continuously (~_ P) s -> ~ inf_often P s.
-Proof.
-intros P s cnyP.
-induction cnyP.
-  destruct s as [e s].
-  intros ifP.
-  apply always_now in ifP.
-  induction ifP.
-    destruct s0 as [e0 s0].
-    apply always_now in H.
-    unfold not_tl in H.
-    contradict H.
-    trivial.
-  apply always_invar in H.
-  contradict IHifP.
-  trivial.
-intro ioP.
-apply always_invar in ioP.
-contradict IHcnyP.
-trivial.
-Qed.
-
 Lemma not_eventually_always_not :
   forall (P : infseq T -> Prop) (s : infseq T),
   ~ eventually P s <-> always (~_ P) s.
@@ -493,6 +469,52 @@ apply always_invar in alP.
 assumption.
 Qed.
 
+Lemma continuously_not_inf_often :
+  forall (P : infseq T -> Prop) (s : infseq T),
+  continuously (~_ P) s -> ~ inf_often P s.
+Proof.
+intros P s cnyP.
+induction cnyP.
+  destruct s as [e s].
+  intros ifP.
+  apply always_now in ifP.
+  induction ifP.
+    destruct s0 as [e0 s0].
+    apply always_now in H.
+    unfold not_tl in H.
+    contradict H.
+    trivial.
+  apply always_invar in H.
+  contradict IHifP.
+  trivial.
+intro ioP.
+apply always_invar in ioP.
+contradict IHcnyP.
+trivial.
+Qed.
+
+Lemma inf_often_not_continuously :
+  forall (P : infseq T -> Prop) (s : infseq T),
+  inf_often (~_ P) s -> ~ continuously P s.
+Proof.
+intros P s ioP cnyP.
+induction cnyP.
+  destruct s as [x s].
+  apply always_now in ioP.
+  induction ioP.
+    destruct s0 as [x' s0].
+    apply always_now in H.
+    unfold not_tl in H0.
+    contradict H0.
+    assumption.
+  apply always_invar in H.
+  contradict IHioP.
+  assumption.
+apply inf_often_invar in ioP.
+contradict IHcnyP.
+assumption.
+Qed.
+
 (* connector facts *)
 
 Lemma and_tl_comm : 
@@ -572,11 +594,12 @@ Implicit Arguments eventually_monotonic_simple [T P Q s].
 Implicit Arguments inf_often_monotonic [T P Q s].
 Implicit Arguments continuously_monotonic [T P Q s].
 
-Implicit Arguments continuously_not_inf_often [T P s].
 Implicit Arguments not_eventually_always_not [T P s].
 Implicit Arguments eventually_not_always [T P s].
 Implicit Arguments until_always_not_always [T J P s].
 Implicit Arguments always_not_eventually_not [T P s].
+Implicit Arguments continuously_not_inf_often [T P s].
+Implicit Arguments inf_often_not_continuously [T P s].
 
 Implicit Arguments and_tl_comm [T P Q s].
 Implicit Arguments and_tl_assoc [T P Q R s].

map.v

@@ -12,10 +12,12 @@ CoFixpoint map (f: A->B) (s: infseq A): infseq B :=
   end.
 
 Lemma map_Cons: forall (f:A->B) x s, map f (Cons x s) = Cons (f x) (map f s).
+Proof.
 intros. pattern (map f (Cons x s)). rewrite <- recons. simpl. reflexivity.
 Qed.
 
-End sec_map. 
+End sec_map.
+
 Implicit Arguments map [A B].
 Implicit Arguments map_Cons [A B].
 
@@ -41,7 +43,7 @@ Implicit Arguments zip [A B].
 Implicit Arguments zip_Cons [A B].
 
 (* --------------------------------------------------------------------------- *)
-(* map and_tl  temporal logic *)
+(* map and_tl temporal logic *)
 
 Section sec_map_modalop.
 
@@ -293,45 +295,45 @@ genclear efst. apply extensional_eventually.
   apply exteq_fst_zip.
 Qed.
 
-Lemma continuously_map :
+Lemma inf_often_map :
    forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop),
    (forall s, P s -> Q (map f s)) ->
-   forall (s: infseq A), continuously P s -> continuously Q (map f s).
+   forall (s: infseq A), inf_often P s -> inf_often Q (map f s).
 Proof.
 intros f P Q PQ.
-apply eventually_map; apply always_map; assumption.
+apply always_map; apply eventually_map; assumption.
 Qed.
 
-Lemma continuously_map_conv :
+Lemma inf_often_map_conv :
    forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop),
    extensional P -> extensional Q -> 
    (forall s, Q (map f s) -> P s) ->
-   forall (s: infseq A), continuously Q (map f s) -> continuously P s.
+   forall (s: infseq A), inf_often Q (map f s) -> inf_often P s.
 Proof.
 intros f P Q eP eQ QP.
-apply eventually_map_conv.
-- apply extensional_always; assumption.
-- apply extensional_always; assumption.
-- apply always_map_conv; assumption.
+apply always_map_conv; apply eventually_map_conv; trivial.
 Qed.
 
-Lemma inf_often_map :
+Lemma continuously_map :
    forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop),
    (forall s, P s -> Q (map f s)) ->
-   forall (s: infseq A), inf_often P s -> inf_often Q (map f s).
+   forall (s: infseq A), continuously P s -> continuously Q (map f s).
 Proof.
 intros f P Q PQ.
-apply always_map; apply eventually_map; assumption.
+apply eventually_map; apply always_map; assumption.
 Qed.
 
-Lemma inf_often_map_conv :
+Lemma continuously_map_conv :
    forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop),
    extensional P -> extensional Q -> 
    (forall s, Q (map f s) -> P s) ->
-   forall (s: infseq A), inf_often Q (map f s) -> inf_often P s.
+   forall (s: infseq A), continuously Q (map f s) -> continuously P s.
 Proof.
 intros f P Q eP eQ QP.
-apply always_map_conv; apply eventually_map_conv; trivial.
+apply eventually_map_conv.
+- apply extensional_always; assumption.
+- apply extensional_always; assumption.
+- apply always_map_conv; assumption.
 Qed.
 
 (* Some corollaries *)