Require Import InfSeqExt.infseq.
Require Import Classical.

Section sec_classical.

Variable T : Type.

Lemma weak_until_until_or_always :
  forall (J P : infseq T -> Prop) (s : infseq T),
    weak_until J P s -> until J P s \/ always J s.
Proof using.
(* Goal: forall (J P : forall _ : infseq T, Prop) (s : infseq T) (_ : @weak_until T J P s), or (@until T J P s) (@always T J s) *)
intros J P s.
(* Goal: forall _ : @weak_until T J P s, or (@until T J P s) (@always T J s) *)
case (classic (eventually P s)).
- intros evP wu.
(* Goal: or (@until T J P s) (@always T J s) *)
  left.
(* Goal: @until T J P s *)
  induction evP.
  * apply U0. assumption.
  * apply weak_until_Cons in wu.
(* Goal: @until T J P (@Cons T x s) *)
    case wu.
    + intros PC.
(* Goal: @until T J P s *)
      apply U0. assumption.
    + intros [Js wu'].
(* Goal: @until T J P (@Cons T x s) *)
      apply U_next; trivial.
(* Goal: @until T J P s *)
      apply IHevP.
(* Goal: @eventually T (@always T P) s *)
      assumption.
- intros evP wu.
(* Goal: or (@until T J P s) (@always T J s) *)
  right.
(* Goal: @always T J s *)
  apply not_eventually_always_not in evP.
(* Goal: @always T J s *)
  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 using.
(* Goal: forall (J P : forall _ : infseq T, Prop) (s : infseq T) (_ : not (@until T (@not_tl T J) (@not_tl T P) s)), @release T J P s *)
intros J P.
(* Goal: forall (s : infseq T) (_ : not (@continuously T P s)), @inf_often T (@not_tl T P) s *)
cofix c.
(* Goal: forall (s : infseq T) (_ : not (@until T (@not_tl T J) (@not_tl T P) s)), @release T J P s *)
intros s.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
case (classic (P s)).
- intros Ps un.
(* Goal: False *)
  contradict un.
(* Goal: @until T J P s *)
  apply U0.
(* Goal: @eventually T (@always T P) s *)
  assumption.
- intros Ps.
(* Goal: forall _ : not (@until T (@and_tl T J (@not_tl T P)) (@and_tl T (@not_tl T J) (@not_tl T P)) s), @weak_until T J P s *)
  case (classic (J s)); destruct s as [x s].
  * intros Js un.
(* Goal: @weak_until T (@and_tl T J (@not_tl T P)) (@and_tl T (@not_tl T J) (@not_tl T P)) (@Cons T x s) *)
    apply W_tl.
    + unfold and_tl, not_tl.
(* Goal: @and_tl T (@not_tl T J) (@not_tl T P) (@Cons T x s) *)
      split; trivial.
    + simpl.
(* Goal: @always T (@eventually T (@not_tl T P)) (@tl T (@Cons T x s)) *)
      apply c.
(* Goal: not (@until T J P s) *)
      intros unn.
(* Goal: False *)
      contradict un.
(* Goal: @until T J P (@Cons T x s) *)
      apply U_next; trivial.
  * intros Js un.
(* Goal: @weak_until T J P s *)
    apply W0.
(* Goal: @and_tl T (@not_tl T J) (@not_tl T P) (@Cons T x s) *)
    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 using.
(* Goal: forall (J P : forall _ : infseq T, Prop) (s : infseq T) (_ : not (@weak_until T J P s)), @until T (@and_tl T J (@not_tl T P)) (@and_tl T (@not_tl T J) (@not_tl T P)) s *)
intros J P s wun.
(* Goal: @until T (@and_tl T J (@not_tl T P)) (@and_tl T (@not_tl T J) (@not_tl T P)) s *)
case (classic (until (J /\_ ~_ P) (~_ J /\_ ~_ P) s)); trivial.
(* Goal: forall _ : not (@until T J P s), @until T J P s *)
intros un.
(* Goal: @until T (@and_tl T J (@not_tl T P)) (@and_tl T (@not_tl T J) (@not_tl T P)) s *)
contradict wun.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
revert s un.
(* Goal: forall (s : infseq T) (_ : not (@continuously T P s)), @inf_often T (@not_tl T P) s *)
cofix c.
(* Goal: forall (s : infseq T) (_ : not (@until T (@not_tl T J) (@not_tl T P) s)), @release T J P s *)
intros s.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
case (classic (P s)).
- intros Ps un.
(* Goal: @weak_until T J P s *)
  apply W0.
(* Goal: @eventually T (@always T P) s *)
  assumption.
- intros Ps.
(* Goal: forall _ : not (@until T (@and_tl T J (@not_tl T P)) (@and_tl T (@not_tl T J) (@not_tl T P)) s), @weak_until T J P s *)
  case (classic (J s)); destruct s as [x s].
  * intros Js un.
(* Goal: @weak_until T J P (@Cons T x s) *)
    apply W_tl; trivial.
(* Goal: @release T (@not_tl T J) (@not_tl T P) (@tl T (@Cons T x s)) *)
    simpl.
(* Goal: @always T (@eventually T (@not_tl T P)) (@tl T (@Cons T x s)) *)
    apply c.
(* Goal: not (@until T J P s) *)
    intros unn.
(* Goal: False *)
    contradict un.
(* Goal: @until T J P (@Cons T x s) *)
    apply U_next; trivial.
(* Goal: @and_tl T (@not_tl T J) (@not_tl T P) (@Cons T x s) *)
    split; trivial.
  * intros Js un.
(* Goal: False *)
    contradict un.
(* Goal: @until T J P s *)
    apply U0.
(* Goal: @and_tl T (@not_tl T J) (@not_tl T P) (@Cons T x s) *)
    split; trivial.
Qed.

Lemma not_eventually_not_always : 
  forall (P : infseq T -> Prop) (s : infseq T),
  ~ eventually (~_ P) s -> always P s.
Proof using.
(* Goal: forall (P : forall _ : infseq T, Prop) (s : infseq T) (_ : not (@continuously T P s)), @inf_often T (@not_tl T P) s *)
intros P.
(* Goal: forall (s : infseq T) (_ : not (@continuously T P s)), @inf_often T (@not_tl T P) s *)
cofix c.
(* Goal: forall (s : infseq T) (_ : not (@eventually T (@not_tl T P) s)), @always T P s *)
intro s.
(* Goal: forall _ : not (@eventually T (@not_tl T P) s), @always T P s *)
destruct s as [e s].
(* Goal: forall _ : not (@eventually T (@not_tl T P) (@Cons T e s)), @always T P (@Cons T e s) *)
intros evnP.
(* Goal: @inf_often T (@not_tl T P) (@Cons T x s) *)
apply Always.
- case (classic (P (Cons e s))); trivial.
(* Goal: forall _ : not (P (@Cons T e s)), P (@Cons T e s) *)
  intros orP.
(* Goal: P (@Cons T e s) *)
  apply (E0 _ (~_ P)) in orP.
(* Goal: False *)
  contradict evnP.
(* Goal: @eventually T (@always T P) s *)
  assumption.
- apply c.
(* Goal: @release T (@not_tl T J) (@not_tl T P) (@tl T (@Cons T x s)) *)
  simpl.
(* Goal: forall _ : not (@eventually T (@not_tl T P) s), @eventually T (@not_tl T P) s *)
  intros evP.
(* Goal: False *)
  contradict evnP.
(* Goal: @continuously T P (@Cons T x s) *)
  apply E_next.
(* Goal: @eventually T (@always T P) s *)
  assumption.
Qed.

Lemma not_always_eventually_not : 
  forall (P : infseq T -> Prop) (s : infseq T),
  ~ always P s -> eventually (~_ P) s.
Proof using.
(* Goal: forall (P : forall _ : infseq T, Prop) (s : infseq T) (_ : not (@always T P s)), @eventually T (@not_tl T P) s *)
intros P s alP.
(* Goal: @eventually T (@not_tl T P) s *)
case (classic ((eventually (~_ P)) s)); trivial.
(* Goal: forall _ : not (@eventually T (@not_tl T P) s), @eventually T (@not_tl T P) s *)
intros evP.
(* Goal: @eventually T (@not_tl T P) s *)
apply not_eventually_not_always in evP.
(* Goal: @eventually T (@not_tl T P) s *)
contradict alP.
(* Goal: @eventually T (@always T P) s *)
assumption.
Qed.

Lemma not_until_release : 
  forall (J P : infseq T -> Prop) (s : infseq T),
  ~ until (~_ J) (~_ P) s -> release J P s.
Proof using.
(* Goal: forall (J P : forall _ : infseq T, Prop) (s : infseq T) (_ : not (@until T (@not_tl T J) (@not_tl T P) s)), @release T J P s *)
intros J P.
(* Goal: forall (s : infseq T) (_ : not (@continuously T P s)), @inf_often T (@not_tl T P) s *)
cofix c.
(* Goal: forall (s : infseq T) (_ : not (@until T (@not_tl T J) (@not_tl T P) s)), @release T J P s *)
intros s.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
case (classic (J s)).
- intros Js un.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
  destruct s as [x s].
(* Goal: @release T J P (@Cons T x s) *)
  apply R0; trivial.
(* Goal: P (@Cons T x s) *)
  case (classic (P (Cons x s))); trivial.
(* Goal: forall _ : not (P s), @release T (@not_tl T J) (@not_tl T P) s *)
  intros Ps.
(* Goal: False *)
  contradict un.
(* Goal: @until T J P s *)
  apply U0.
(* Goal: @not_tl T P (@Cons T x s) *)
  apply Ps.
- intros Js un.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
  destruct s as [x s].
(* Goal: @release T J P (@Cons T x s) *)
  apply R_tl.
  * case (classic (P (Cons x s))); trivial.
(* Goal: forall _ : not (P s), @release T (@not_tl T J) (@not_tl T P) s *)
    intros Ps.
(* Goal: False *)
    contradict un.
(* Goal: @until T J P s *)
    apply U0.
(* Goal: @not_tl T P (@Cons T x s) *)
    apply Ps.
  * simpl.
(* Goal: @always T (@eventually T (@not_tl T P)) (@tl T (@Cons T x s)) *)
    apply c.
(* Goal: not (@until T J P s) *)
    intros unn.
(* Goal: False *)
    contradict un.
(* Goal: @until T J P (@Cons T x s) *)
    apply U_next; trivial.
Qed.

Lemma not_release_until :
  forall (J P : infseq T -> Prop) (s : infseq T),
  ~ release (~_ J) (~_ P) s -> until J P s.
Proof using.
(* Goal: forall (J P : forall _ : infseq T, Prop) (s : infseq T) (_ : not (@release T (@not_tl T J) (@not_tl T P) s)), @until T J P s *)
intros J P s rl.
(* Goal: @until T J P s *)
case (classic (until J P s)); trivial.
(* Goal: forall _ : not (@until T J P s), @until T J P s *)
intros un.
(* Goal: @until T J P s *)
contradict rl.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
revert s un.
(* Goal: forall (s : infseq T) (_ : not (@continuously T P s)), @inf_often T (@not_tl T P) s *)
cofix c.
(* Goal: forall (s : infseq T) (_ : not (@until T J P s)), @release T (@not_tl T J) (@not_tl T P) s *)
intros s un.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
case (classic (P s)).
- intros Ps.
(* Goal: False *)
  contradict un.
(* Goal: @until T J P s *)
  apply U0.
(* Goal: @eventually T (@always T P) s *)
  assumption.
- intros Ps.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
  case (classic (J s)).
  * intros Js.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
    destruct s as [x s].
(* Goal: @release T (@not_tl T J) (@not_tl T P) (@Cons T x s) *)
    apply R_tl; trivial.
(* Goal: @release T (@not_tl T J) (@not_tl T P) (@tl T (@Cons T x s)) *)
    simpl.
(* Goal: @always T (@eventually T (@not_tl T P)) (@tl T (@Cons T x s)) *)
    apply c.
(* Goal: not (@until T J P s) *)
    intros unn.
(* Goal: False *)
    contradict un.
(* Goal: @until T J P (@Cons T x s) *)
    apply U_next; trivial.
  * intros Js.
(* Goal: @release T (@not_tl T J) (@not_tl T P) s *)
    destruct s as [x s].
(* Goal: @eventually T (@always T P) s *)
    apply R0; unfold not_tl; assumption.
Qed.

Lemma not_inf_often_continuously_not : 
  forall (P : infseq T -> Prop) (s : infseq T),
  ~ inf_often P s -> continuously (~_ P) s.
Proof using.
(* Goal: forall (P : forall _ : infseq T, Prop) (s : infseq T) (_ : not (@inf_often T P s)), @continuously T (@not_tl T P) s *)
intros P s ioP.
(* Goal: @continuously T (@not_tl T P) s *)
apply not_always_eventually_not in ioP.
(* Goal: @continuously T (@not_tl T P) s *)
induction ioP.
- apply not_eventually_always_not in H.
(* Goal: @continuously T (@not_tl T P) s *)
  apply E0.
(* Goal: @eventually T (@always T P) s *)
  assumption.
- apply E_next.
(* Goal: @eventually T (@always T P) s *)
  assumption.
Qed.

Lemma not_continously_inf_often_not :
  forall (P : infseq T -> Prop) (s : infseq T),
  ~ continuously P s -> inf_often (~_ P) s.
Proof using.
(* Goal: forall (P : forall _ : infseq T, Prop) (s : infseq T) (_ : not (@continuously T P s)), @inf_often T (@not_tl T P) s *)
intros P.
(* Goal: forall (s : infseq T) (_ : not (@continuously T P s)), @inf_often T (@not_tl T P) s *)
cofix c.
(* Goal: forall (s : infseq T) (_ : not (@continuously T P s)), @inf_often T (@not_tl T P) s *)
intros [x s] cnyP.
(* Goal: @inf_often T (@not_tl T P) (@Cons T x s) *)
apply Always.
- unfold continuously in cnyP.
(* Goal: @eventually T (@not_tl T P) (@Cons T x s) *)
  apply not_eventually_always_not in cnyP.
(* Goal: @eventually T (@not_tl T P) (@Cons T x s) *)
  apply always_now in cnyP.
(* Goal: @eventually T (@not_tl T P) (@Cons T x s) *)
  unfold not_tl in cnyP.
(* Goal: @eventually T (@not_tl T P) (@Cons T x s) *)
  apply not_always_eventually_not in cnyP.
(* Goal: @eventually T (@always T P) s *)
  assumption.
- apply c.
(* Goal: not (@continuously T P (@tl T (@Cons T x s))) *)
  intros cnynP.
(* Goal: False *)
  contradict cnyP.
(* Goal: @continuously T P (@Cons T x s) *)
  apply E_next.
(* Goal: @eventually T (@always T P) s *)
  assumption.
Qed.

Lemma not_tl_and_tl_or_tl :
  forall (P Q : infseq T -> Prop) (s : infseq T),
  (~_ (P /\_ Q)) s -> ((~_ P) \/_ (~_ Q)) s.
Proof using.
(* Goal: forall (P Q : forall _ : infseq T, Prop) (s : infseq T) (_ : @not_tl T (@and_tl T P Q) s), @or_tl T (@not_tl T P) (@not_tl T Q) s *)
intros P Q s; unfold not_tl, and_tl, or_tl.
(* Goal: forall _ : not (and (P s) (Q s)), or (not (P s)) (not (Q s)) *)
apply not_and_or.
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] _.
Arguments not_release_until [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] _.
