standard equivalence for release

Author: palmskog

classical.v

@@ -64,6 +64,37 @@ contradict alP.
 assumption.
 Qed.
 
+Lemma not_until_release : 
+  forall (J P : infseq T -> Prop) (s : infseq T),
+  ~ until (~_ J) (~_ P) s -> release J P s.
+Proof.
+intros J P.
+cofix c.
+intros s.
+case (classic (J s)).
+  intros Js un.
+  destruct s as [x s].
+  apply R0; trivial.
+  case (classic (P (Cons x s))); trivial.
+  intros Ps.
+  contradict un.
+  apply U0.
+  apply Ps.  
+intros Js un.
+destruct s as [x s].
+apply R_tl.
+  case (classic (P (Cons x s))); trivial.
+  intros Ps.
+  contradict un.
+  apply U0.
+  apply Ps.
+simpl.
+apply c.
+intros unn.
+contradict un.
+apply U_next; trivial.
+Qed.
+
 Lemma not_inf_often_continuously_not : 
   forall (P : infseq T -> Prop) (s : infseq T),
   ~ inf_often P s -> continuously (~_ P) s.
@@ -112,6 +143,7 @@ End sec_classical.
 Arguments weak_until_until_or_always [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] _.
 Arguments not_inf_often_continuously_not [T P s] _.
 Arguments not_continously_inf_often_not [T P s] _.
 Arguments not_tl_and_tl_or_tl [T P Q s] _.

infseq.v

@@ -651,6 +651,24 @@ contradict IHcnyP.
 assumption.
 Qed.
 
+Lemma release_not_until : 
+  forall (J P : infseq T -> Prop) (s : infseq T),
+  release J P s -> ~ until (~_ J) (~_ P) s.
+Proof.
+intros J P s rl un.
+induction un as [s Ps |x s Js IHun IH].
+  destruct s as [x s].
+  unfold not_tl in Ps.
+  apply release_Cons in rl.
+  destruct rl as [Psr rl].
+  contradict Ps.
+  assumption.
+apply release_Cons in rl.
+destruct rl as [Ps rl].
+unfold not_tl in Js.
+case rl; trivial.
+Qed.
+
 (* connector facts *)
 
 Lemma and_tl_comm : 
@@ -745,6 +763,7 @@ Arguments weak_until_always_not_always [T J P s] _ _.
 Arguments always_not_eventually_not [T P s] _ _.
 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 and_tl_comm [T P Q s].
 Arguments and_tl_assoc [T P Q R s].
@@ -755,14 +774,20 @@ Arguments not_tl_or_tl_and_tl [T P Q s] _ _.
 
 Ltac monotony := 
   match goal with 
-     | [ |- now ?P ?s -> now ?Q ?s ] => apply now_monotonic
-     | [ |- next ?P ?s -> next ?Q ?s ] => apply next_monotonic
+     | [ |- now ?P ?s -> now ?Q ?s ] =>
+       apply now_monotonic
+     | [ |- next ?P ?s -> next ?Q ?s ] =>
+       apply next_monotonic
      | [ |- consecutive ?P ?s -> consecutive ?Q ?s ] =>
        apply consecutive_monotonic
-     | [ |- always ?P ?s -> always ?Q ?s ] => apply always_monotonic
-     | [ |- weak_until ?J ?P ?s -> weak_until ?K ?Q ?s ] => apply weak_until_monotonic
-     | [ |- until ?J ?P ?s -> until ?K ?Q ?s ] => apply until_monotonic
-     | [ |- release ?J ?P ?s -> release ?K ?Q ?s ] => apply release_monotonic
+     | [ |- always ?P ?s -> always ?Q ?s ] =>
+       apply always_monotonic
+     | [ |- weak_until ?J ?P ?s -> weak_until ?K ?Q ?s ] =>
+       apply weak_until_monotonic
+     | [ |- until ?J ?P ?s -> until ?K ?Q ?s ] =>
+       apply until_monotonic
+     | [ |- release ?J ?P ?s -> release ?K ?Q ?s ] =>
+       apply release_monotonic
      | [ |- ?J ?s -> eventually ?P ?s -> eventually ?Q ?s ] =>
        apply eventually_monotonic
      | [ |- continuously ?P ?s -> continuously ?Q ?s ] =>