added weak_until-until duality, fixed associativity level of not_tl

Author: palmskog

classical.v

@@ -29,6 +29,65 @@ apply not_eventually_always_not in evP.
 apply weak_until_always_not_always in wu; trivial.
 Qed.
 
+Lemma not_until_weak_until :
+  forall (J P : infseq T -> Prop) (s : infseq T),
+    ~ until J P s -> weak_until (J /\_ ~_ P) (~_ J /\_ ~_ P) s.
+Proof.
+intros J P.
+cofix c.
+intros s.
+case (classic (P s)).
+  intros Ps un.
+  contradict un.
+  apply U0.
+  assumption.
+intros Ps.
+case (classic (J s)); destruct s as [x s].
+  intros Js un.
+  apply W_tl.
+    unfold and_tl, not_tl.
+    split; trivial.
+  simpl.
+  apply c.
+  intros unn.
+  contradict un.
+  apply U_next; trivial.
+intros Js un.
+apply W0.
+split; trivial.
+Qed.
+
+Lemma not_weak_until_until :
+  forall (J P : infseq T -> Prop) (s : infseq T),
+    ~ weak_until J P s -> until (J /\_ ~_ P) (~_ J /\_ ~_ P) s.
+Proof.
+intros J P s wun.
+case (classic (until (J /\_ ~_ P) (~_ J /\_ ~_ P) s)); trivial.
+intros un.
+contradict wun.
+revert s un.
+cofix c.
+intros s.
+case (classic (P s)).
+  intros Ps un.
+  apply W0.
+  assumption.
+intros Ps.
+case (classic (J s)); destruct s as [x s].
+  intros Js un.
+  apply W_tl; trivial.
+  simpl.
+  apply c.
+  intros unn.
+  contradict un.
+  apply U_next; trivial.
+  split; trivial.
+intros Js un.
+contradict un.
+apply U0.
+split; trivial.
+Qed.
+
 Lemma not_eventually_not_always : 
   forall (P : infseq T -> Prop) (s : infseq T),
   ~ eventually (~_ P) s -> always P s.
@@ -172,6 +231,8 @@ Qed.
 End sec_classical.
 
 Arguments weak_until_until_or_always [T J P s] _.
+Arguments not_until_weak_until [T J P s] _.
+Arguments not_weak_until_until [T J P s] _.
 Arguments not_eventually_not_always [T P s] _.
 Arguments not_always_eventually_not [T P s] _.
 Arguments not_until_release [T J P s] _.

infseq.v

@@ -120,7 +120,7 @@ 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).
-Notation "~_ A" := (not_tl A) (right associativity, at level 90).
+Notation "~_ A" := (not_tl A) (right associativity, at level 75).
 
 Section sec_modal_op_lemmas.
 
@@ -735,6 +735,54 @@ contradict Js.
 assumption.
 Qed.
 
+Lemma weak_until_not_until :
+  forall (J P : infseq T -> Prop) (s : infseq T),
+    weak_until (J /\_ ~_ P) (~_ J /\_ ~_ P) s -> ~ until J P s.
+Proof.
+intros J P s wu un.
+induction un.
+  destruct s as [x s].
+  apply weak_until_Cons in wu.
+  case wu; unfold not_tl, and_tl.
+    intros [Js Ps].
+    contradict Ps.
+    assumption.
+  intros [[Js Ps] wun].
+  contradict Ps.
+  assumption.
+apply weak_until_Cons in wu.
+case wu.
+  unfold not_tl, and_tl.
+  intros [Js Ps].
+  contradict Js.
+  assumption.
+intros [[Js Ps] wun].
+contradict IHun.
+assumption.
+Qed.
+
+Lemma until_not_weak_until :
+  forall (J P : infseq T -> Prop) (s : infseq T),
+    until (J /\_ ~_ P) (~_ J /\_ ~_ P) s -> ~ weak_until J P s.
+Proof.
+intros J P s un wun.
+induction un as [s JPs | x s JPs IHun IH]; unfold not_tl, and_tl in JPs; destruct JPs as [Js Ps].
+  destruct s as [x s].
+  apply weak_until_Cons in wun.
+  case wun; trivial.
+  intros [JCs wu].
+  contradict Js.
+  assumption.
+apply weak_until_Cons in wun.
+case wun.
+  intros PCs.
+  contradict Ps.
+  assumption.
+intros [JCs wu].
+contradict IH.
+assumption.
+Qed.
+
 (* connector facts *)
 
 Lemma and_tl_comm : 
@@ -834,6 +882,8 @@ Arguments continuously_not_inf_often [T P s] _ _.
 Arguments inf_often_not_continuously [T P s] _ _.
 Arguments release_not_until [T J P s] _ _.
 Arguments until_not_release [T J P s] _ _.
+Arguments weak_until_not_until [T J P s] _ _.
+Arguments until_not_weak_until [T J P s] _ _.
 
 Arguments and_tl_comm [T P Q s].
 Arguments and_tl_assoc [T P Q R s].