Limits
A predicate saying there exists a point in the stream where a predicate is satsified.We take the unusual step of puting this inductive type in Prop even though it contains constructive information. This is because we expect this proof to only be used in proofs of termination.
Inductive LazyExists A (P:Stream A -> Prop) (x: Stream A) : Prop :=
| LazyHere : P x -> LazyExists P x
| LazyFurther : (unit -> LazyExists P (tl x)) -> LazyExists P x.
Section TakeUntil.
| LazyHere : P x -> LazyExists P x
| LazyFurther : (unit -> LazyExists P (tl x)) -> LazyExists P x.
Section TakeUntil.
takeUntil creates a list of of elements upto a the point where the predicate
P is satisfied. For efficency reasons it doesn't actually build a list, but
takes continuations for cons and nil instead. To build an actual list pass in
the const and nil constructors.
Fixpoint takeUntil (A B:Type) (P : Stream A -> bool)(s:Stream A) (ex:LazyExists P s) (cons: A -> B -> B) (nil : B) {struct ex} : B :=
(if P s as b return ((P s -> b) -> B)
then fun _ => nil
else fun (n : P s -> ⊥) => cons (hd s)
(@takeUntil A B P (tl s)
match ex with
| LazyHere H => (False_ind _ (n H))
| LazyFurther ex0 => ex0 tt
end cons nil))
(fun x => x).
Lemma takeUntil_wd : forall (A B:Type) (P : Stream A -> bool)(s:Stream A)(ex1 ex2:LazyExists P s) (cons: A -> B -> B) (nil:B),
takeUntil P ex1 cons nil = takeUntil P ex2 cons nil.
Lemma takeUntil_end : forall (A B:Type) (P:Stream A -> bool) seq (ex:LazyExists P seq) (cons:A -> B -> B) (nil : B),
P seq -> takeUntil P ex cons nil = nil.
Lemma takeUntil_step : forall (A B:Type) (P:Stream A -> bool) seq (ex:LazyExists P seq) (cons: A -> B -> B) (nil: B),
~P seq -> exists ex':(LazyExists P (tl seq)), takeUntil P ex cons nil = cons (hd seq) (takeUntil P ex' cons nil).
Lemma takeUntil_elim : forall (A B:Type) (P:Stream A -> bool) (cons: A -> B -> B) (nil: B)
(Q: Stream A -> B -> Prop),
(forall seq, P seq -> Q seq nil) ->
(forall seq x, Q (tl seq) x -> ~P seq -> Q seq (cons (hd seq) x)) ->
forall seq (ex:LazyExists P seq), Q seq (takeUntil P ex cons nil).
End TakeUntil.
Section Limit.
Variable X : MetricSpace.
(if P s as b return ((P s -> b) -> B)
then fun _ => nil
else fun (n : P s -> ⊥) => cons (hd s)
(@takeUntil A B P (tl s)
match ex with
| LazyHere H => (False_ind _ (n H))
| LazyFurther ex0 => ex0 tt
end cons nil))
(fun x => x).
Lemma takeUntil_wd : forall (A B:Type) (P : Stream A -> bool)(s:Stream A)(ex1 ex2:LazyExists P s) (cons: A -> B -> B) (nil:B),
takeUntil P ex1 cons nil = takeUntil P ex2 cons nil.
Lemma takeUntil_end : forall (A B:Type) (P:Stream A -> bool) seq (ex:LazyExists P seq) (cons:A -> B -> B) (nil : B),
P seq -> takeUntil P ex cons nil = nil.
Lemma takeUntil_step : forall (A B:Type) (P:Stream A -> bool) seq (ex:LazyExists P seq) (cons: A -> B -> B) (nil: B),
~P seq -> exists ex':(LazyExists P (tl seq)), takeUntil P ex cons nil = cons (hd seq) (takeUntil P ex' cons nil).
Lemma takeUntil_elim : forall (A B:Type) (P:Stream A -> bool) (cons: A -> B -> B) (nil: B)
(Q: Stream A -> B -> Prop),
(forall seq, P seq -> Q seq nil) ->
(forall seq x, Q (tl seq) x -> ~P seq -> Q seq (cons (hd seq) x)) ->
forall seq (ex:LazyExists P seq), Q seq (takeUntil P ex cons nil).
End TakeUntil.
Section Limit.
Variable X : MetricSpace.
This proposition says that the entire stream is within e of l
Definition NearBy (l:X)(e:QposInf) := ForAll (fun (s:Stream X) => ball_ex e (hd s) l).
Lemma NearBy_comp: forall l1 l2, st_eq l1 l2 -> forall (e1 e2:Qpos), QposEq e1 e2 -> forall s, (NearBy l1 e1 s <-> NearBy l2 e2 s).
Lemma NearBy_weak: forall l (e1 e2:Qpos), e1 <= e2 -> forall s, NearBy l e1 s -> NearBy l e2 s.
Lemma NearBy_comp: forall l1 l2, st_eq l1 l2 -> forall (e1 e2:Qpos), QposEq e1 e2 -> forall s, (NearBy l1 e1 s <-> NearBy l2 e2 s).
Lemma NearBy_weak: forall l (e1 e2:Qpos), e1 <= e2 -> forall s, NearBy l e1 s -> NearBy l e2 s.
l is the limit if for every e there exists a point where the stream is
always within e of l.
Definition Limit (s:Stream X)(l:X) := forall e, LazyExists (NearBy l e) s.
Lemma Limit_tl : forall s l, Limit s l -> Limit (tl s) l.
Lemma Limit_Str_nth_tl : forall n s l, Limit s l -> Limit (Str_nth_tl n s) l.
End Limit.
Lemma Limit_tl : forall s l, Limit s l -> Limit (tl s) l.
Lemma Limit_Str_nth_tl : forall n s l, Limit s l -> Limit (Str_nth_tl n s) l.
End Limit.