Require Import InfSeqExt.infseq.
Require Import InfSeqExt.exteq.

(* map *)
Section sec_map.

Variable A B: Type.

CoFixpoint map (f: A->B) (s: infseq A): infseq B :=
  match s with
    | Cons x s => Cons (f x) (map f s)
  end.

Lemma map_Cons: forall (f:A->B) x s, map f (Cons x s) = Cons (f x) (map f s).
Proof using.
(* Goal: forall (s : infseq A) (_ : @True_tl A s) (_ : Q (@map A B f s)), @eventually A P s *)
intros. pattern (map f (Cons x s)). rewrite <- recons. simpl. reflexivity.
Qed.

End sec_map.

Arguments map [A B] _ _.
Arguments map_Cons [A B] _ _ _.

(* --------------------------------------------------------------------------- *)
(* Zipping two infseqs: useful for map theory *)
Section sec_zip.

Variable A B: Type.

CoFixpoint zip (sA: infseq A) (sB: infseq B) : infseq (A*B) := 
  match sA, sB with
    | Cons a sA0, Cons b sB0 => Cons (a, b) (zip sA0 sB0)
  end.

Lemma zip_Cons: forall (a:A) (b:B) sA sB, zip (Cons a sA) (Cons b sB) = Cons (a, b) (zip sA sB). 
Proof using.
(* Goal: forall (s : infseq A) (_ : @True_tl A s) (_ : Q (@map A B f s)), @eventually A P s *)
intros. pattern (zip (Cons a sA) (Cons b sB)); rewrite <- recons. simpl. reflexivity. 
Qed.

End sec_zip.

Arguments zip [A B] _ _.
Arguments zip_Cons [A B] _ _ _ _.

(* --------------------------------------------------------------------------- *)
(* map and_tl temporal logic *)

Section sec_map_modalop.

Variable A B: Type.

Lemma and_tl_map :
   forall (f: A->B) (P P': infseq A->Prop) (Q Q': infseq B->Prop),
   (forall s, P s -> Q (map f s)) ->
   (forall s, P' s -> Q' (map f s)) ->
   forall (s: infseq A),
   (P /\_ P') s -> (Q /\_ Q') (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P P' : forall _ : infseq A, Prop) (Q Q' : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : Q (@map A B f s)), P s) (_ : forall (s : infseq A) (_ : Q' (@map A B f s)), P' s) (s : infseq A) (_ : @and_tl B Q Q' (@map A B f s)), @and_tl A P P' s *)
unfold and_tl; intuition. 
Qed.

Lemma and_tl_map_conv :
   forall (f: A->B) (P P': infseq A->Prop) (Q Q': infseq B->Prop),
   (forall s, Q (map f s) -> P s) ->
   (forall s, Q' (map f s) -> P' s) ->
   forall (s: infseq A),
   (Q /\_ Q') (map f s) -> (P /\_ P') s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P P' : forall _ : infseq A, Prop) (Q Q' : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : Q (@map A B f s)), P s) (_ : forall (s : infseq A) (_ : Q' (@map A B f s)), P' s) (s : infseq A) (_ : @and_tl B Q Q' (@map A B f s)), @and_tl A P P' s *)
unfold and_tl; intuition. 
Qed.

Lemma or_tl_map :
   forall (f: A->B) (P P': infseq A->Prop) (Q Q': infseq B->Prop),
   (forall s, P s -> Q (map f s)) ->
   (forall s, P' s -> Q' (map f s)) ->
   forall (s: infseq A),
   (P \/_ P') s -> (Q \/_ Q') (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P P' : forall _ : infseq A, Prop) (Q Q' : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : Q (@map A B f s)), P s) (_ : forall (s : infseq A) (_ : Q' (@map A B f s)), P' s) (s : infseq A) (_ : @or_tl B Q Q' (@map A B f s)), @or_tl A P P' s *)
unfold or_tl; intuition. 
Qed.

Lemma or_tl_map_conv :
   forall (f: A->B) (P P': infseq A->Prop) (Q Q': infseq B->Prop),
   (forall s, Q (map f s) -> P s) ->
   (forall s, Q' (map f s) -> P' s) ->
   forall (s: infseq A),
   (Q \/_ Q') (map f s) -> (P \/_ P') s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P P' : forall _ : infseq A, Prop) (Q Q' : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : Q (@map A B f s)), P s) (_ : forall (s : infseq A) (_ : Q' (@map A B f s)), P' s) (s : infseq A) (_ : @or_tl B Q Q' (@map A B f s)), @or_tl A P P' s *)
unfold or_tl; intuition. 
Qed.

Lemma impl_tl_map :
   forall (f: A->B) (P P': infseq A->Prop) (Q Q': infseq B->Prop),
   (forall s, Q (map f s) -> P s) ->
   (forall s, P' s -> Q' (map f s)) ->
   forall (s: infseq A),
   (P ->_ P') s -> (Q ->_ Q') (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P P' : forall _ : infseq A, Prop) (Q Q' : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (_ : forall (s : infseq A) (_ : Q' (@map A B f s)), P' s) (s : infseq A) (_ : @impl_tl B Q Q' (@map A B f s)), @impl_tl A P P' s *)
unfold impl_tl; intuition. 
Qed.

Lemma impl_tl_map_conv :
   forall (f: A->B) (P P': infseq A->Prop) (Q Q': infseq B->Prop),
   (forall s, P s -> Q (map f s)) ->
   (forall s, Q' (map f s) -> P' s) ->
   forall (s: infseq A),
   (Q ->_ Q') (map f s) -> (P ->_ P') s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P P' : forall _ : infseq A, Prop) (Q Q' : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (_ : forall (s : infseq A) (_ : Q' (@map A B f s)), P' s) (s : infseq A) (_ : @impl_tl B Q Q' (@map A B f s)), @impl_tl A P P' s *)
unfold impl_tl; intuition. 
Qed.

Lemma not_tl_map :
   forall (f: A->B) (P : infseq A->Prop) (Q: infseq B->Prop),
   (forall s, Q (map f s) -> P s) ->
   forall (s: infseq A), (~_ P) s -> (~_ Q) (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (s : infseq A) (_ : @not_tl B Q (@map A B f s)), @not_tl A P s *)
unfold not_tl; intuition. 
Qed.

Lemma not_tl_map_conv :
   forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop),
   (forall s, P s -> Q (map f s)) ->
   forall (s: infseq A), (~_ Q) (map f s) -> (~_ P) s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (s : infseq A) (_ : @not_tl B Q (@map A B f s)), @not_tl A P s *)
unfold not_tl; intuition. 
Qed.

Lemma now_map :
   forall (f: A->B) (P: B->Prop) (s: infseq A),
   now (fun x => P (f x)) s -> now P (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : B, Prop) (s : infseq A) (_ : @now B P (@map A B f s)), @now A (fun x : A => P (f x)) s *)
intros f P (x, s) nP; assumption. 
Qed.

Lemma now_map_conv :
   forall (f: A->B) (P: B->Prop) (s: infseq A),
   now P (map f s) -> now (fun x => P (f x)) s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : B, Prop) (s : infseq A) (_ : @now B P (@map A B f s)), @now A (fun x : A => P (f x)) s *)
intros f P (x, s) nP; assumption. 
Qed.

Lemma next_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), next P s -> next Q (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (s : infseq A) (_ : @next A P s), @next B Q (@map A B f s) *)
intros f P Q PQ [x s]; apply PQ.
Qed.

Lemma next_map_conv :
   forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop),
   (forall s, Q (map f s) -> P s) ->
   forall (s: infseq A), next Q (map f s) -> next P s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : Q (@map A B f s)), P s) (s : infseq A) (_ : @next B Q (@map A B f s)), @next A P s *)
intros f P Q QP [x s]; apply QP.
Qed.

Lemma consecutive_map :
   forall (f: A->B) (P: B->B->Prop) (s: infseq A),
   consecutive (fun x y => P (f x) (f y)) s -> consecutive P (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall (_ : B) (_ : B), Prop) (s : infseq A) (_ : @consecutive B P (@map A B f s)), @consecutive A (fun x y : A => P (f x) (f y)) s *)
intros f P (x, (y, s)) nP; assumption. 
Qed.

Lemma consecutive_map_conv :
   forall (f: A->B) (P: B->B->Prop) (s: infseq A),
   consecutive P (map f s) -> consecutive (fun x y => P (f x) (f y)) s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall (_ : B) (_ : B), Prop) (s : infseq A) (_ : @consecutive B P (@map A B f s)), @consecutive A (fun x y : A => P (f x) (f y)) s *)
intros f P (x, (y, s)) nP; assumption. 
Qed.

Lemma always_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), always P s -> always Q (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (s : infseq A) (_ : @continuously A P s), @continuously B Q (@map A B f s) *)
intros f P Q PQ. cofix cf.
(* Goal: forall (s : infseq A) (_ : @always A P s), @always B Q (@map A B f s) *)
intros (x, s) a. case (always_Cons a); intros a1 a2. constructor.
- apply PQ. assumption.
(* Goal: forall _ : @now B P (@Cons B (f x) (@map A B f s)), @now A (fun x : A => P (f x)) (@Cons A x s) *)
- rewrite map_Cons; simpl. apply cf; assumption.
Qed.

Lemma always_map_conv_ext :
  forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop) (J : infseq A -> Prop),
    (forall x s, J (Cons x s) -> J s) ->
    (forall s, J s -> Q (map f s) -> P s) ->
    forall s, J s -> always Q (map f s) -> always P s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (J : forall _ : infseq A, Prop) (_ : forall (x : A) (s : infseq A) (_ : J (@Cons A x s)), J s) (_ : forall (s : infseq A) (_ : J s) (_ : Q (@map A B f s)), P s) (s : infseq A) (_ : J s) (_ : @always B Q (@map A B f s)), @always A P s *)
intros f J P Q inv JQP. cofix c.
(* Goal: forall (s : infseq A) (_ : Q s) (_ : @always B P (@map A B f s)), @always A J s *)
intros [x s] Js a.
(* Goal: @always A J (@Cons A x s) *)
rewrite map_Cons in a. case (always_Cons a); intros a1 a2. constructor.
- apply JQP. assumption.
(* Goal: Q (@map A B f s0) *)
  rewrite map_Cons; assumption.
(* Goal: forall _ : @now B P (@Cons B (f x) (@map A B f s)), @now A (fun x : A => P (f x)) (@Cons A x s) *)
- simpl. apply c.
(* Goal: Q (@map A B f s0) *)
  * apply (inv x). assumption.
(* Goal: Q (@map A B f s0) *)
  * assumption.
Qed.

Lemma always_map_conv :
   forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop),
   (forall s, Q (map f s) -> P s) ->
   forall (s: infseq A), always Q (map f s) -> always P s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : Q (@map A B f s)), P s) (s : infseq A) (_ : @always B Q (@map A B f s)), @always A P s *)
intros f P Q QP s.
(* Goal: forall _ : @always B Q (@map A B f s), @always A P s *)
apply (always_map_conv_ext f P Q True_tl); auto.
Qed.

Lemma weak_until_map :
   forall (f: A->B) (J P: infseq A->Prop) (K Q: infseq B->Prop),
   (forall s, J s -> K (map f s)) ->
   (forall s, P s -> Q (map f s)) ->
   forall (s: infseq A),
   weak_until J P s -> weak_until K Q (map f s).
Proof using.
(* Goal: forall s : infseq A, @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B s (@map A B f s)) *)
intros f J P K Q JK PQ. cofix cf.
(* Goal: forall (s : infseq A) (_ : @weak_until B K Q (@map A B f s)), @weak_until A J P s *)
intros (x, s) un. case (weak_until_Cons un); clear un.
- intro Pxs; constructor 1. apply PQ. assumption.
- intros (Jxs, un). rewrite map_Cons. constructor 2.
  * rewrite <- map_Cons. auto.
(* Goal: forall _ : @now B P (@Cons B (f x) (@map A B f s)), @now A (fun x : A => P (f x)) (@Cons A x s) *)
  * simpl. auto.
Qed.

Lemma weak_until_map_conv :
   forall (f: A->B) (J P: infseq A->Prop) (K Q: infseq B->Prop),
   (forall s, K (map f s) -> J s) ->
   (forall s, Q (map f s) -> P s) ->
   forall (s: infseq A),
   weak_until K Q (map f s) -> weak_until J P s.
Proof using.
(* Goal: forall s : infseq A, @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B s (@map A B f s)) *)
intros f J P K Q KJ QP. cofix cf.
(* Goal: forall (s : infseq A) (_ : @weak_until B K Q (@map A B f s)), @weak_until A J P s *)
intros (x, s) un.
rewrite map_Cons in un; case (weak_until_Cons un); clear un; rewrite <- map_Cons.
- intro Qxs; constructor 1. apply QP. assumption.
- intros (Kxs, un). constructor 2; simpl; auto.
Qed.

Lemma until_map :
   forall (f: A->B) (J P: infseq A->Prop) (K Q: infseq B->Prop),
   (forall s, J s -> K (map f s)) ->
   (forall s, P s -> Q (map f s)) ->
   forall (s: infseq A),
   until J P s -> until K Q (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (J P : forall _ : infseq A, Prop) (K Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : J s), K (@map A B f s)) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (s : infseq A) (_ : @until A J P s), @until B K Q (@map A B f s) *)
intros f J P K Q JK PQ s un.
(* Goal: @until B K Q (@map A B f s) *)
induction un.
- apply U0, PQ. assumption.
- rewrite map_Cons.
(* Goal: @until B K Q (@Cons B (f x) (@map A B f s)) *)
  apply U_next.
  * rewrite <- map_Cons.
(* Goal: K (@map A B f (@Cons A x s)) *)
    apply JK.
(* Goal: Q (@map A B f s0) *)
    assumption.
(* Goal: Q (@map A B f s0) *)
  * assumption.
Qed.

Lemma release_map :
   forall (f: A->B) (J P: infseq A->Prop) (K Q: infseq B->Prop),
   (forall s, J s -> K (map f s)) ->
   (forall s, P s -> Q (map f s)) ->
   forall (s: infseq A),
   release J P s -> release K Q (map f s).
Proof using.
(* Goal: forall s : infseq A, @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B s (@map A B f s)) *)
intros f J P K Q JK PQ. cofix cf.
(* Goal: forall (s : infseq A) (_ : @release B K Q (@map A B f s)), @release A J P s *)
intros (x, s) rl. case (release_Cons rl); clear rl.
(* Goal: forall (_ : P (@Cons A x s)) (_ : or (J (@Cons A x s)) (@release A J P s)), @release B K Q (@map A B f (@Cons A x s)) *)
intros Pxs orR.
(* Goal: @release B K Q (@map A B f (@Cons A x s)) *)
case orR; intro cR.
- apply R0.
(* Goal: Q (@map A B f (@Cons A x s)) *)
  * apply PQ. assumption.
(* Goal: Q (@map A B f s0) *)
  * apply JK. assumption.
- apply R_tl.
(* Goal: Q (@map A B f (@Cons A x s)) *)
  * apply PQ. assumption.
(* Goal: Q (@map A B f s0) *)
  * apply cf. assumption.
Qed.

Lemma release_map_conv :
   forall (f: A->B) (J P: infseq A->Prop) (K Q: infseq B->Prop),
   (forall s, K (map f s) -> J s) ->
   (forall s, Q (map f s) -> P s) ->
   forall (s: infseq A),
   release K Q (map f s) -> release J P s.
Proof using.
(* Goal: forall s : infseq A, @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B s (@map A B f s)) *)
intros f J P K Q KJ QP. cofix cf.
(* Goal: forall (s : infseq A) (_ : @release B K Q (@map A B f s)), @release A J P s *)
intros (x, s) rl.
rewrite map_Cons in rl; case (release_Cons rl); clear rl; rewrite <- map_Cons; intros QC orR; case orR; intro cR.
- apply R0.
(* Goal: Q (@map A B f s0) *)
  * apply QP. assumption.
(* Goal: Q (@map A B f s0) *)
  * apply KJ. assumption.
- apply R_tl.
(* Goal: Q (@map A B f s0) *)
  * apply QP. assumption.
(* Goal: Q (@map A B f s0) *)
  * apply cf. assumption.
Qed.

Lemma eventually_map :
   forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop),
   (forall s, P s -> Q (map f s)) ->
   forall s, eventually P s -> eventually Q (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (s : infseq A) (_ : @eventually A P s), @eventually B Q (@map A B f s) *)
intros f P Q PQ s e. induction e as [s ok | x s e induc_hyp].
- destruct s as (x, s); simpl in *. rewrite map_Cons. constructor 1.
  rewrite <- map_Cons. apply PQ. exact ok.
- rewrite map_Cons. constructor 2. exact induc_hyp.
Qed.

(* The converse seems to require much more work *)

Definition fstAB := fst (A:=A) (B:=B).

Lemma exteq_fst_zip:
  forall sA sB, exteq (map fstAB (zip sA sB)) sA.
Proof using.
(* Goal: forall s : infseq A, @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B s (@map A B f s)) *)
cofix cf. intros (a, sA) (b, sB). 
(* Goal: @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B (@Cons A x s0) (@map A B f (@Cons A x s0))) *)
rewrite zip_Cons. rewrite map_Cons. constructor. apply cf.
Qed.

Lemma exteq_zip_map :
   forall (f: A->B) (sA: infseq A) (sB: infseq B),
   always (now (fun c: A*B => let (x, y) := c in y = f x)) (zip sA sB) ->
   exteq sB (map f (map fstAB (zip sA (map f sA)))).
Proof using. 
(* Goal: forall s : infseq A, @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B s (@map A B f s)) *)
intros f. cofix cf. 
(* Goal: forall (sA : infseq A) (sB : infseq B) (_ : @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B sA sB)), @exteq B sB (@map A B f (@map (prod A B) A fstAB (@zip A B sA (@map A B f sA)))) *)
intros (a, sA) (b, sB).
(* Goal: forall _ : @now B P (@Cons B (f x) (@map A B f s)), @now A (fun x : A => P (f x)) (@Cons A x s) *)
repeat rewrite map_Cons; repeat rewrite zip_Cons; repeat rewrite map_Cons; simpl. 
(* Goal: forall _ : @now B P (@Cons B (f x) (@map A B f s)), @now A (fun x : A => P (f x)) (@Cons A x s) *)
intro al; case (always_Cons al); clear al; simpl. intros e al. case e. constructor. 
(* Goal: @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) ((cofix zip (sA : infseq A) (sB : infseq B) : infseq (prod A B) := match sA with | Cons a sA0 => match sB with | Cons b sB0 => @Cons (prod A B) (@pair A B a b) (zip sA0 sB0) end end) s0 ((cofix map (f : forall _ : A, B) (s : infseq A) : infseq B := match s with | Cons x s0 => @Cons B (f x) (map f s0) end) f s0)) *)
apply cf. exact al. 
Qed.

Lemma eventually_map_conv_aux :
   forall (f: A->B) (Q: infseq B->Prop), extensional Q ->
   forall (s: infseq A) (sB: infseq B),
   always (now (fun c: A*B => let (x, y) := c in y = f x)) (zip s sB) ->
   eventually Q sB ->
   eventually (fun sc => Q (map f (map fstAB sc))) (zip s (map f s)).
Proof using.
(* Goal: forall (f : forall _ : A, B) (Q : forall _ : infseq B, Prop) (_ : @extensional B Q) (s : infseq A) (sB : infseq B) (_ : @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B s sB)) (_ : @eventually B Q sB), @eventually (prod A B) (fun sc : infseq (prod A B) => Q (@map A B f (@map (prod A B) A fstAB sc))) (@zip A B s (@map A B f s)) *)
intros f Q extQ s sB al ev. genclear al; genclear s.
(* Goal: forall (s : infseq A) (_ : @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B s sB)), @eventually (prod A B) (fun sc : infseq (prod A B) => Q (@map A B f (@map (prod A B) A fstAB sc))) (@zip A B s (@map A B f s)) *)
induction ev as [(b, sB) QbsB | b sB ev induc_hyp].
- intros (a, sA) al.
(* Goal: Q (@map A B f s0) *)
  constructor 1. apply extQ with (Cons b sB); try assumption.
(* Goal: @exteq B (@Cons B b sB) (@map A B f (@map (prod A B) A fstAB (@zip A B (@Cons A a sA) (@map A B f (@Cons A a sA))))) *)
  apply exteq_zip_map. apply al.
- intros (a, sA). repeat rewrite map_Cons. repeat rewrite zip_Cons.
(* Goal: forall _ : @now B P (@Cons B (f x) (@map A B f s)), @now A (fun x : A => P (f x)) (@Cons A x s) *)
  intro al. case (always_Cons al); simpl. clear al; intros e al. 
(* Goal: @eventually (prod A B) (fun sc : infseq (prod A B) => Q (@map A B f (@map (prod A B) A fstAB sc))) (@Cons (prod A B) (@pair A B a (f a)) (@zip A B sA (@map A B f sA))) *)
  constructor 2. apply induc_hyp. exact al. 
Qed.

Lemma eventually_map_conv_ext :
   forall (f: A->B) (P: infseq A->Prop) (Q: infseq B->Prop) (J : infseq A -> Prop),
   extensional P -> extensional Q -> extensional J ->
   (forall x s, J (Cons x s) -> J s) ->
   (forall s, J s -> Q (map f s) -> eventually P s) ->
   forall s, J s -> eventually Q (map f s) -> eventually P s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (J : forall _ : infseq A, Prop) (_ : @extensional A P) (_ : @extensional B Q) (_ : @extensional A J) (_ : forall (x : A) (s : infseq A) (_ : J (@Cons A x s)), J s) (_ : forall (s : infseq A) (_ : J s) (_ : Q (@map A B f s)), @eventually A P s) (s : infseq A) (_ : J s) (_ : @eventually B Q (@map A B f s)), @eventually A P s *)
intros f P Q J extP extQ extJ inv QP s Js ev.
(* Goal: @eventually A P s *)
revert Js.
assert (efst: J (map fstAB (zip s (map f s))) -> eventually P (map fstAB (zip s (map f s)))).
- assert (evzip : eventually (fun sc => Q (map f (map fstAB sc))) (zip s (map f s))).
  * clear extP QP P.
     assert (alzip : (always (now (fun c : A * B => let (x, y) := c in y = f x)) (zip s (map f s)))).
(* Goal: forall s : infseq A, @always (prod A B) (@now (prod A B) (fun c : prod A B => let (x, y) := c in @eq B y (f x))) (@zip A B s (@map A B f s)) *)
     + clear ev extQ. generalize s. cofix cf. intros (x, s0). constructor.
(* Goal: forall _ : @now B P (@Cons B (f x) (@map A B f s)), @now A (fun x : A => P (f x)) (@Cons A x s) *)
       -- simpl. reflexivity.
(* Goal: forall _ : @now B P (@Cons B (f x) (@map A B f s)), @now A (fun x : A => P (f x)) (@Cons A x s) *)
       -- simpl. apply cf.
     + apply (eventually_map_conv_aux f Q extQ s (map f s) alzip ev).
  * clear ev. induction evzip as [((a, b), sAB) QabsAB | c sAB _ induc_hyp].
    + intros Js.
(* Goal: Q (@map A B f s0) *)
      apply QP; assumption.
    + intros Js.
(* Goal: @eventually A P (@map (prod A B) A fstAB (@Cons (prod A B) c sAB)) *)
      rewrite map_Cons.
(* Goal: @eventually A P (@Cons A x s) *)
      apply E_next.
(* Goal: @eventually A P (@map (prod A B) A fstAB sAB) *)
      apply induc_hyp.
(* Goal: J (@map (prod A B) A fstAB sAB) *)
      rewrite map_Cons in Js.
(* Goal: J (@map (prod A B) A fstAB sAB) *)
      apply (inv (fstAB c)).
(* Goal: Q (@map A B f s0) *)
      assumption.
- intros Js.
(* Goal: @eventually A P s *)
  assert (emJ: J (map fstAB (zip s (map f s)))).
  * unfold extensional in extJ.
(* Goal: J (@map (prod A B) A fstAB (@zip A B s (@map A B f s))) *)
    apply (extJ s).
    + apply exteq_sym. apply exteq_fst_zip.
(* Goal: Q (@map A B f s0) *)
    + assumption.
  * apply efst in emJ.
(* Goal: @eventually A P s *)
    genclear emJ.
(* Goal: forall _ : @eventually A P (@map (prod A B) A fstAB (@zip A B s (@map A B f s))), @eventually A P s *)
    apply extensional_eventually.
    + exact extP.
    + apply exteq_fst_zip.
Qed.

Lemma eventually_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, eventually Q (map f s) -> eventually P s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : @extensional A P) (_ : @extensional B Q) (_ : forall (s : infseq A) (_ : Q (@map A B f s)), P s) (s : infseq A) (_ : @eventually B Q (@map A B f s)), @eventually A P s *)
intros f P Q extP extQ QP s.
(* Goal: @weak_until B K Q (@map A B f s) *)
apply eventually_map_conv_ext with (J := True_tl); auto.
- apply extensional_True_tl.
(* Goal: forall (s : infseq A) (_ : @True_tl A s) (_ : Q (@map A B f s)), @eventually A P s *)
- intros. apply E0. apply QP. assumption.
Qed.

Lemma eventually_map_monotonic :
   forall (f: A->B) (P Q J: infseq A->Prop) (K : infseq B -> Prop),
   (forall x s, J (Cons x s) -> J s) ->
   (forall x s, K (map f (Cons x s)) -> K (map f s)) ->
   (forall s, J s -> K (map f s) -> Q s -> P s) ->
   forall s, J s -> K (map f s) -> eventually Q s -> eventually P s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P Q J : forall _ : infseq A, Prop) (K : forall _ : infseq B, Prop) (_ : forall (x : A) (s : infseq A) (_ : J (@Cons A x s)), J s) (_ : forall (x : A) (s : infseq A) (_ : K (@map A B f (@Cons A x s))), K (@map A B f s)) (_ : forall (s : infseq A) (_ : J s) (_ : K (@map A B f s)) (_ : Q s), P s) (s : infseq A) (_ : J s) (_ : K (@map A B f s)) (_ : @eventually A Q s), @eventually A P s *)
intros f P Q J K Jinv Kinv JKQP s invJ invK ev.
(* Goal: @eventually A P s *)
induction ev as [s Qs | x s ev IHev].
- apply E0.
(* Goal: Q (@map A B f s0) *)
  apply JKQP; assumption.
- apply E_next.
(* Goal: @eventually A P s *)
  apply IHev.
(* Goal: Q (@map A B f s0) *)
  * apply (Jinv x); assumption.
(* Goal: Q (@map A B f s0) *)
  * apply (Kinv x); assumption.
Qed.

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), inf_often P s -> inf_often Q (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (s : infseq A) (_ : @continuously A P s), @continuously B Q (@map A B f s) *)
intros f P Q PQ.
(* Goal: Q (@map A B f s0) *)
apply always_map; apply eventually_map; assumption.
Qed.

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), inf_often Q (map f s) -> inf_often P s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : @extensional A P) (_ : @extensional B Q) (_ : forall (s : infseq A) (_ : Q (@map A B f s)), P s) (s : infseq A) (_ : @continuously B Q (@map A B f s)), @continuously A P s *)
intros f P Q eP eQ QP.
(* Goal: forall (s : infseq A) (_ : @inf_often B Q (@map A B f s)), @inf_often A P s *)
apply always_map_conv; apply eventually_map_conv; trivial.
Qed.

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), continuously P s -> continuously Q (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : forall (s : infseq A) (_ : P s), Q (@map A B f s)) (s : infseq A) (_ : @continuously A P s), @continuously B Q (@map A B f s) *)
intros f P Q PQ.
(* Goal: Q (@map A B f s0) *)
apply eventually_map; apply always_map; assumption.
Qed.

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), continuously Q (map f s) -> continuously P s.
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : infseq A, Prop) (Q : forall _ : infseq B, Prop) (_ : @extensional A P) (_ : @extensional B Q) (_ : forall (s : infseq A) (_ : Q (@map A B f s)), P s) (s : infseq A) (_ : @continuously B Q (@map A B f s)), @continuously A P s *)
intros f P Q eP eQ QP.
(* Goal: forall _ : @eventually B (@now B P) (@map A B f s), @eventually A (@now A (fun x : A => P (f x))) s *)
apply eventually_map_conv.
- apply extensional_always; assumption.
- apply extensional_always; assumption.
- apply always_map_conv; assumption.
Qed.

(* Some corollaries *)

Lemma eventually_now_map :
   forall (f: A->B) (P: B->Prop) (s: infseq A),
   eventually (now (fun x => P (f x))) s -> eventually (now P) (map f s).
Proof using.
(* Goal: forall (f : forall _ : A, B) (P : forall _ : B, Prop) (s : infseq A) (_ : @eventually A (@now A (fun x : A => P (f x))) s), @eventually B (@now B P) (@map A B f s) *)
intros f P. apply eventually_map. apply now_map.
Qed.

Lemma eventually_now_map_conv :
   forall (f: A->B) (P: B->Prop) (s: infseq A),
   eventually (now P) (map f s) -> eventually (now (fun x => P (f x))) s.
Proof using.
(* Goal: forall _ : @eventually B (@now B P) (@map A B f s), @eventually A (@now A (fun x : A => P (f x))) s *)
intros f P s. apply eventually_map_conv.
- apply extensional_now. 
- apply extensional_now. 
(* Goal: forall _ : @now B P (@Cons B (f x) (@map A B f s)), @now A (fun x : A => P (f x)) (@Cons A x s) *)
- clear s. intros (x, s). repeat rewrite map_Cons. simpl. trivial.
Qed.

Lemma eventually_map_now_eq :
  forall (f: A -> B) a s, eventually (now (eq a)) s -> 
  eventually (now (eq (f a))) (map f s).
Proof using.
(* Goal: forall (s : infseq A) (_ : @eventually A (@now A (@eq A a)) s), @eventually B (@now B (@eq B (f a))) (@map A B f s) *)
intros f a. apply eventually_map.
(* Goal: @now B (@eq B (f a)) (@map A B f s) *)
intros s noa. apply now_map.
(* Goal: @now A (fun x : A => @eq B (f a) (f x)) s *)
genclear noa. monotony. apply f_equal.
Qed.

End sec_map_modalop. 

Arguments and_tl_map [A B f P P' Q Q'] _ _ [s] _.
Arguments and_tl_map_conv [A B f P P' Q Q'] _ _ [s] _.
Arguments or_tl_map [A B f P P' Q Q'] _ _ [s] _.
Arguments or_tl_map_conv [A B f P P' Q Q'] _ _ [s] _.
Arguments impl_tl_map [A B f P P' Q Q'] _ _ [s] _ _.
Arguments impl_tl_map_conv [A B f P P' Q Q'] _ _ [s] _ _.
Arguments not_tl_map [A B f P Q] _ [s] _ _.
Arguments not_tl_map_conv [A B f P Q] _ [s] _ _.
Arguments now_map [A B f P s] _.
Arguments now_map_conv [A B f P s] _.
Arguments next_map [A B f P Q] _ [s] _.
Arguments next_map_conv [A B f P Q] _ [s] _.
Arguments consecutive_map [A B f P s] _.
Arguments consecutive_map_conv [A B f P s] _.
Arguments always_map [A B f P Q] _ [s] _.
Arguments always_map_conv_ext [A B f P Q J] _ _ [s] _ _.
Arguments always_map_conv [A B f P Q] _ [s] _.
Arguments weak_until_map [A B f J P K Q] _ _ [s] _.
Arguments weak_until_map_conv [A B f J P K Q] _ _ [s] _.
Arguments until_map [A B f J P K Q] _ _ [s] _.
Arguments release_map [A B f J P K Q] _ _ [s] _.
Arguments release_map_conv [A B f J P K Q] _ _ [s] _.
Arguments eventually_map [A B f P Q] _ [s] _.
Arguments eventually_map_conv_ext [A B f P Q J] _ _ _ _ _ [s] _ _.
Arguments eventually_map_conv [A B f P Q] _ _ _ [s] _.
Arguments eventually_map_monotonic [A B f P Q] _ _ _ _ _ [s] _ _ _.
Arguments inf_often_map [A B f P Q] _ [s] _.
Arguments inf_often_map_conv [A B f P Q] _ _ _ [s] _.
Arguments continuously_map [A B f P Q] _ [s] _.
Arguments continuously_map_conv [A B f P Q] _ _ _ [s] _.
Arguments eventually_now_map [A B f P s] _.
Arguments eventually_now_map_conv [A B f P s] _.
Arguments eventually_map_now_eq [A B f a s] _.
