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

(* --------------------------------------------------------------------------- *)
(* Infinite subsequences *)

Section sec_subseq.

Variable T: Type.

(* suff s s'  means  s is a suffix of s' *)
Inductive suff (s : infseq T) : infseq T -> Prop :=
  | sp_eq : suff s s
  | sp_next : forall x s0, suff s s0 -> suff s (Cons x s0).

(* simple but not the most useful -- useless indeed *)
CoInductive subseq : infseq T -> infseq T -> Prop :=
  | Subseq : forall s s0 s1,
             suff s1 s0 -> subseq s (tl s1) -> subseq (Cons (hd s1) s) s0.

CoInductive subseqs' : infseq (infseq T) -> infseq T -> Prop :=
  | Subseqs' : forall si s0 s1,
             suff s1 s0 -> subseqs' si (tl s1) -> subseqs' (Cons s1 si) s0. 

CoInductive subseqs : infseq (infseq T) -> infseq T -> Prop :=
  | Subseqs : forall si s,
             suff (hd si) s -> subseqs (tl si) (tl (hd si)) -> subseqs si s. 

Lemma subseqs_subseqs' : forall si s, subseqs si s -> subseqs' si s.
Proof using.
(* Goal: forall (si : infseq (infseq T)) (s : infseq T) (_ : subseqs' si s), subseqs si s *)
cofix subsub. 
(* Goal: forall (si : infseq (infseq T)) (s : infseq T) (_ : subseqs' si s), subseqs si s *)
intros si s su. case su; clear su si s.
(* Goal: forall (si : infseq (infseq T)) (s : infseq T) (_ : suff (@hd (infseq T) si) s) (_ : subseqs (@tl (infseq T) si) (@tl T (@hd (infseq T) si))), subseqs' si s *)
intros (s1, si) s0. simpl. intros su sb. constructor.
- assumption.
- apply subsub. assumption.
Qed.

Lemma subseqs'_subseqs : forall si s, subseqs' si s -> subseqs si s.
(* Goal: forall (si : infseq (infseq T)) (s : infseq T) (_ : subseqs' si s), subseqs si s *)
cofix subsub.
(* Goal: forall (si : infseq (infseq T)) (s : infseq T) (_ : subseqs' si s), subseqs si s *)
intros si s su. case su; clear su si s.
(* Goal: forall (_ : suff (@hd (infseq T) (@Cons (infseq T) s1 si)) s0) (_ : subseqs (@tl (infseq T) (@Cons (infseq T) s1 si)) (@tl T (@hd (infseq T) (@Cons (infseq T) s1 si)))), subseqs' (@Cons (infseq T) s1 si) s0 *)
intros si s0 s1 su sb. constructor; simpl.
- assumption. 
- apply subsub. assumption. 
Qed.

(* Relating inf subseq to infinitely often *)

(* In the next lemma, always1 is bit overkill, but is just what is needed below *)
Lemma subseqs_eventually : 
  forall P si s, subseqs si s -> always1 P si -> eventually P s.
Proof using.
(* Goal: forall (P : forall _ : infseq T, Prop) (si : infseq (infseq T)) (s : infseq T) (_ : subseqs si s) (_ : @always1 (infseq T) P si), @eventually T P s *)
intros P si s su. destruct su as [si s sf _].
(* Goal: forall _ : @always1 (infseq T) P si, @eventually T P s *)
induction sf as [ | x s0 _ Hrec]; intro a. 
(* Goal: forall (_ : suff (@hd (infseq T) (@Cons (infseq T) s1 si)) s0) (_ : subseqs (@tl (infseq T) (@Cons (infseq T) s1 si)) (@tl T (@hd (infseq T) (@Cons (infseq T) s1 si)))), subseqs' (@Cons (infseq T) s1 si) s0 *)
- constructor 1. case a; simpl. intros; assumption.
- constructor 2. apply Hrec. apply a.
Qed.

Lemma subseqs_tl : forall si s, subseqs si (tl s) -> subseqs si s. 
Proof using.
(* Goal: forall (si : infseq (infseq T)) (s : infseq T) (_ : subseqs si (@tl T s)), subseqs si s *)
intros si (x, s) su. simpl in su.
(* Goal: forall _ : @always1 (infseq T) P si, @always T (@eventually T P) (@tl T s) *)
case su. clear su si s; intros si s sf su.
(* Goal: mem x (@Cons T y s') *)
constructor.
- constructor 2. exact sf.
- exact su.
Qed.

Theorem subseq_inf_often :
  forall P si s, subseqs si s -> always1 P si -> inf_often P s.
Proof using.
(* Goal: forall (P : forall _ : infseq T, Prop) (si : infseq (infseq T)) (s : infseq T) (_ : subseqs si s) (_ : @always1 (infseq T) P si), @inf_often T P s *)
intros P. red. cofix sio.
(* Goal: forall (si : infseq (infseq T)) (s : infseq T) (_ : subseqs si s) (_ : @always1 (infseq T) P si), @always T (@eventually T P) s *)
intros si s su a.
(* Goal: mem x (@Cons T y s') *)
constructor.
- apply subseqs_eventually with si; assumption.
- genclear a. case su. 
  clear su si s; intros (s0, si) s sf su a; simpl in * |- * . 
(* Goal: @always T (@eventually T P) (@tl T s) *)
  apply (sio si); clear sio.
(* Goal: forall (_ : suff (@hd (infseq T) (@Cons (infseq T) s1 si)) s0) (_ : subseqs (@tl (infseq T) (@Cons (infseq T) s1 si)) (@tl T (@hd (infseq T) (@Cons (infseq T) s1 si)))), subseqs' (@Cons (infseq T) s1 si) s0 *)
  * induction sf; simpl.
(* Goal: subseqs si (@tl T s0) *)
(* Goal: subseqs si s1 *)
    trivial. 
    apply subseqs_tl. assumption (* induction hyp *). 
  * change (always1 P (tl (Cons s0 si))). case a; simpl; trivial. 
Qed.

(* Conversely : TODO *)

Inductive ex_suff (P: infseq T -> Prop) (s' : infseq T) : Prop :=
  Esp : forall s, suff s s' -> P s -> ex_suff P s'.

Theorem eventually_suff :
   forall P s', eventually P s' -> ex_suff P s'.
Proof using.
(* Goal: forall (P : forall _ : infseq T, Prop) (s' : infseq T) (_ : @eventually T P s'), ex_suff P s' *)
intros P s ev. induction ev.   
- exists s; [ constructor | assumption]. 
- destruct IHev. exists s0. 
(* Goal: mem x s' *)
  * constructor; assumption.
(* Goal: mem x s' *)
  * assumption.
Qed.

(* Extensional version *)

Inductive suff_exteq (s : infseq T) : infseq T -> Prop :=
  | sb_eq : forall s', exteq s s' -> suff_exteq s s'
  | sb_next : forall x s', suff_exteq s s' -> suff_exteq s (Cons x s').

Inductive suffb (x : T) (s : infseq T) : infseq T -> Prop :=
  | sp_eqb : forall s', exteq (Cons x s) s' -> suffb x s s'
  | sp_nextb : forall y s', suffb x s s' -> suffb x s (Cons y s').

CoInductive subseqb : infseq T -> infseq T -> Prop :=
  | Subseqb : forall x s s', suffb x s s' -> subseqb s s' -> subseqb (Cons x s) s'.

Inductive mem (x : T) : infseq T -> Prop :=
  | mem0 : forall s, mem x (Cons x s)
  | mem_next : forall y s, mem x s -> mem x (Cons y s).

Lemma subseqb_included : forall x s, mem x s -> forall s', subseqb s s' -> mem x s'.
Proof using.
(* Goal: forall (x : T) (s : infseq T) (_ : mem x s) (s' : infseq T) (_ : subseqb s s'), mem x s' *)
induction 1 as [| y s M IHmem].
- inversion_clear 1 as [a b c ssp _]. induction ssp as [s' ssp | ].
(* Goal: mem x (@Cons T y s') *)
  inversion_clear ssp. constructor.
(* Goal: mem x (@Cons T y s') *)
  constructor. assumption.
- inversion_clear 1. apply IHmem; assumption.
Qed.

End sec_subseq. 
