From stdpp Require Import prelude.
From Coq Require Import Streams Sorted.
From VLSM.Lib Require Import Preamble StreamExtras SortedLists.
From VLSM.Lib Require Import ListExtras StdppExtras NeList.
From Coq Require Import Streams Sorted.
From VLSM.Lib Require Import Preamble StreamExtras SortedLists.
From VLSM.Lib Require Import ListExtras StdppExtras NeList.
Utility: Stream Filters
P and a stream s, a stream of naturals ns
determines a filtering_subsequence for P on s if it corresponds to
the list of positions in ss where P holds, increasingly ordered.
Definition filtering_subsequence
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ns : Stream nat)
: Prop
:= (forall i, i < hd ns -> ~ P (Str_nth i s)) /\
ForAll2 (fun m n => P (Str_nth m s) /\ m < n /\ forall i, m < i < n -> ~ P (Str_nth i s)) ns.
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ns : Stream nat)
: Prop
:= (forall i, i < hd ns -> ~ P (Str_nth i s)) /\
ForAll2 (fun m n => P (Str_nth m s) /\ m < n /\ forall i, m < i < n -> ~ P (Str_nth i s)) ns.
A more intuitive statement of the filtering_subsequence property.
See FilteringSubsequence_iff for the equivalence result.
Record FilteringSubsequence
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ns : Stream nat)
: Prop :=
{
fs_monotone : monotone_nat_stream_prop ns;
fs_is_filter : forall n, P (Str_nth n s) <-> exists k, n = Str_nth k ns;
}.
Lemma filtering_subsequence_sorted
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ns : Stream nat)
(Hfs : filtering_subsequence P s ns)
: ForAll2 lt ns.
Proof.
destruct Hfs as [_ Hfs].
revert Hfs; apply ForAll2_subsumption.
by intros a b H; apply H.
Qed.
Lemma filtering_subsequence_prefix_sorted
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ns : Stream nat)
(Hfs : filtering_subsequence P s ns)
: forall n, LocallySorted lt (stream_prefix ns n).
Proof.
intro n. apply LocallySorted_ForAll2.
apply stream_prefix_ForAll2.
by apply filtering_subsequence_sorted in Hfs.
Qed.
Lemma filtering_subsequence_iff
{A : Type}
(P Q : A -> Prop)
(HPQ : forall a, P a <-> Q a)
(s : Stream A)
(ss : Stream nat)
: filtering_subsequence P s ss <-> filtering_subsequence Q s ss.
Proof.
unfold filtering_subsequence.
rewrite !ForAll2_forall.
by setoid_rewrite <- HPQ.
Qed.
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ns : Stream nat)
: Prop :=
{
fs_monotone : monotone_nat_stream_prop ns;
fs_is_filter : forall n, P (Str_nth n s) <-> exists k, n = Str_nth k ns;
}.
Lemma filtering_subsequence_sorted
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ns : Stream nat)
(Hfs : filtering_subsequence P s ns)
: ForAll2 lt ns.
Proof.
destruct Hfs as [_ Hfs].
revert Hfs; apply ForAll2_subsumption.
by intros a b H; apply H.
Qed.
Lemma filtering_subsequence_prefix_sorted
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ns : Stream nat)
(Hfs : filtering_subsequence P s ns)
: forall n, LocallySorted lt (stream_prefix ns n).
Proof.
intro n. apply LocallySorted_ForAll2.
apply stream_prefix_ForAll2.
by apply filtering_subsequence_sorted in Hfs.
Qed.
Lemma filtering_subsequence_iff
{A : Type}
(P Q : A -> Prop)
(HPQ : forall a, P a <-> Q a)
(s : Stream A)
(ss : Stream nat)
: filtering_subsequence P s ss <-> filtering_subsequence Q s ss.
Proof.
unfold filtering_subsequence.
rewrite !ForAll2_forall.
by setoid_rewrite <- HPQ.
Qed.
Each element in a filtering_subsequence is a position in the base
stream for which the predicate holds.
Lemma filtering_subsequence_witness
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(k : nat)
: P (Str_nth (Str_nth k ss) s).
Proof.
destruct Hfs as [_ Hfs].
by rewrite ForAll2_forall in Hfs; apply Hfs.
Qed.
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(k : nat)
: P (Str_nth (Str_nth k ss) s).
Proof.
destruct Hfs as [_ Hfs].
by rewrite ForAll2_forall in Hfs; apply Hfs.
Qed.
For each position in the base stream for which the predicate holds is
present in the filtering_subsequence.
Lemma filtering_subsequence_witness_rev
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(n : nat)
(Hn : P (Str_nth n s))
: exists k, n = Str_nth k ss.
Proof.
apply filtering_subsequence_sorted in Hfs as Hss_sorted.
apply monotone_nat_stream_prop_from_successor in Hss_sorted.
apply monotone_nat_stream_find with (n := n) in Hss_sorted.
destruct Hss_sorted as [Hlt | [k Hk]].
- by destruct Hfs as [Hfs _]; elim (Hfs n).
- destruct Hk as [Heq | Hk]; subst; [by exists k |].
exfalso. apply proj2 in Hfs.
rewrite ForAll2_forall in Hfs.
specialize (Hfs k) as [_ [_ Hfs]].
by elim (Hfs n).
Qed.
Lemma FilteringSubsequence_iff
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ss : Stream nat)
: FilteringSubsequence P s ss <-> filtering_subsequence P s ss.
Proof.
split.
- intros []; split.
+ setoid_rewrite fs_is_filter0.
intros i Hi [? ->].
apply (fs_monotone0 x 0) in Hi.
by lia.
+ apply ForAll2_forall; intros n; split_and!.
* by apply fs_is_filter0; eexists.
* by apply (fs_monotone0 n (S n)); lia.
* setoid_rewrite fs_is_filter0.
intros i [Hni Hni'] [? ->].
by apply fs_monotone0 in Hni, Hni'; lia.
- constructor.
+ by eapply monotone_nat_stream_prop_from_successor, filtering_subsequence_sorted.
+ split; [by apply filtering_subsequence_witness_rev |].
by intros [? ->]; apply filtering_subsequence_witness.
Qed.
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(n : nat)
(Hn : P (Str_nth n s))
: exists k, n = Str_nth k ss.
Proof.
apply filtering_subsequence_sorted in Hfs as Hss_sorted.
apply monotone_nat_stream_prop_from_successor in Hss_sorted.
apply monotone_nat_stream_find with (n := n) in Hss_sorted.
destruct Hss_sorted as [Hlt | [k Hk]].
- by destruct Hfs as [Hfs _]; elim (Hfs n).
- destruct Hk as [Heq | Hk]; subst; [by exists k |].
exfalso. apply proj2 in Hfs.
rewrite ForAll2_forall in Hfs.
specialize (Hfs k) as [_ [_ Hfs]].
by elim (Hfs n).
Qed.
Lemma FilteringSubsequence_iff
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ss : Stream nat)
: FilteringSubsequence P s ss <-> filtering_subsequence P s ss.
Proof.
split.
- intros []; split.
+ setoid_rewrite fs_is_filter0.
intros i Hi [? ->].
apply (fs_monotone0 x 0) in Hi.
by lia.
+ apply ForAll2_forall; intros n; split_and!.
* by apply fs_is_filter0; eexists.
* by apply (fs_monotone0 n (S n)); lia.
* setoid_rewrite fs_is_filter0.
intros i [Hni Hni'] [? ->].
by apply fs_monotone0 in Hni, Hni'; lia.
- constructor.
+ by eapply monotone_nat_stream_prop_from_successor, filtering_subsequence_sorted.
+ split; [by apply filtering_subsequence_witness_rev |].
by intros [? ->]; apply filtering_subsequence_witness.
Qed.
Prefixes of the filtering subsequence expressed as filters.
Lemma filtering_subsequence_prefix_is_filter
{A : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
: forall (k : nat),
stream_prefix ss (S k) =
filter (fun i => P (Str_nth i s)) (stream_prefix nat_sequence (S (Str_nth k ss))).
Proof.
intro k.
apply (@set_equality_predicate _ lt _).
- by apply filtering_subsequence_prefix_sorted with P s.
- apply LocallySorted_filter.
+ by typeclasses eauto.
+ by apply nat_sequence_prefix_sorted.
- unfold ListSetExtras.set_eq, subseteq, list_subseteq.
setoid_rewrite elem_of_list_filter.
setoid_rewrite elem_of_stream_prefix.
setoid_rewrite nat_sequence_nth.
split; intros.
+ destruct H as [i [Hi Ha]].
subst.
split; [by apply filtering_subsequence_witness |].
eexists; split; [| done].
destruct (decide (i = k)); [subst; lia |].
cut (Str_nth i ss < Str_nth k ss); [lia |].
apply ForAll2_transitive_lookup; [by typeclasses eauto | | lia].
by apply filtering_subsequence_sorted in Hfs.
+ destruct H as [Hpa [_a [Hlt H_a]]].
subst _a.
destruct (filtering_subsequence_witness_rev _ _ _ Hfs _ Hpa) as [k' ->].
exists k'.
split; [| done].
apply filtering_subsequence_sorted in Hfs.
apply monotone_nat_stream_prop_from_successor in Hfs.
specialize (monotone_nat_stream_rev _ Hfs k' k) as Hle.
by lia.
Qed.
Lemma filtering_subsequence_prefix_length
{A : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(m : nat)
: length (filter P (stream_prefix s (S (Str_nth m ss)))) = S m.
Proof.
specialize (filtering_subsequence_prefix_is_filter _ _ _ Hfs m) as Hfilter.
apply f_equal with (f := length) in Hfilter.
rewrite stream_prefix_length in Hfilter.
rewrite! stream_prefix_S, filter_app in Hfilter.
unfold filter at 2 in Hfilter. simpl in Hfilter.
rewrite nat_sequence_nth in Hfilter.
rewrite stream_prefix_S, filter_app.
unfold filter at 2. simpl.
specialize (filtering_subsequence_witness _ _ _ Hfs m) as Hm.
rewrite decide_True in Hfilter by done.
rewrite decide_True by done.
rewrite app_length, Nat.add_comm in Hfilter. simpl in Hfilter.
rewrite app_length, Nat.add_comm. simpl.
rewrite Hfilter.
f_equal.
clear -Hfs.
generalize (Str_nth m ss).
induction n; [done |].
rewrite !stream_prefix_S, !filter_app, !app_length, IHn.
f_equal. rewrite nat_sequence_nth.
by cbn; case_decide.
Qed.
Lemma filtering_subsequence_prefix_is_filter_last
{A : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(n : nat)
(Hn : P (Str_nth n s))
: Str_nth (length (filter P (stream_prefix s n))) ss = n.
Proof.
specialize (filtering_subsequence_witness_rev _ _ _ Hfs _ Hn) as [k Heqn].
replace (length _) with k; [by subst |].
specialize (filtering_subsequence_prefix_length _ _ _ Hfs k) as Hlength.
rewrite! stream_prefix_S, filter_app in Hlength.
unfold filter at 2 in Hlength. simpl in Hlength.
rewrite decide_True in Hlength by (subst; done).
rewrite app_length, Nat.add_comm in Hlength. simpl in Hlength.
by inversion Hlength; subst.
Qed.
{A : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
: forall (k : nat),
stream_prefix ss (S k) =
filter (fun i => P (Str_nth i s)) (stream_prefix nat_sequence (S (Str_nth k ss))).
Proof.
intro k.
apply (@set_equality_predicate _ lt _).
- by apply filtering_subsequence_prefix_sorted with P s.
- apply LocallySorted_filter.
+ by typeclasses eauto.
+ by apply nat_sequence_prefix_sorted.
- unfold ListSetExtras.set_eq, subseteq, list_subseteq.
setoid_rewrite elem_of_list_filter.
setoid_rewrite elem_of_stream_prefix.
setoid_rewrite nat_sequence_nth.
split; intros.
+ destruct H as [i [Hi Ha]].
subst.
split; [by apply filtering_subsequence_witness |].
eexists; split; [| done].
destruct (decide (i = k)); [subst; lia |].
cut (Str_nth i ss < Str_nth k ss); [lia |].
apply ForAll2_transitive_lookup; [by typeclasses eauto | | lia].
by apply filtering_subsequence_sorted in Hfs.
+ destruct H as [Hpa [_a [Hlt H_a]]].
subst _a.
destruct (filtering_subsequence_witness_rev _ _ _ Hfs _ Hpa) as [k' ->].
exists k'.
split; [| done].
apply filtering_subsequence_sorted in Hfs.
apply monotone_nat_stream_prop_from_successor in Hfs.
specialize (monotone_nat_stream_rev _ Hfs k' k) as Hle.
by lia.
Qed.
Lemma filtering_subsequence_prefix_length
{A : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(m : nat)
: length (filter P (stream_prefix s (S (Str_nth m ss)))) = S m.
Proof.
specialize (filtering_subsequence_prefix_is_filter _ _ _ Hfs m) as Hfilter.
apply f_equal with (f := length) in Hfilter.
rewrite stream_prefix_length in Hfilter.
rewrite! stream_prefix_S, filter_app in Hfilter.
unfold filter at 2 in Hfilter. simpl in Hfilter.
rewrite nat_sequence_nth in Hfilter.
rewrite stream_prefix_S, filter_app.
unfold filter at 2. simpl.
specialize (filtering_subsequence_witness _ _ _ Hfs m) as Hm.
rewrite decide_True in Hfilter by done.
rewrite decide_True by done.
rewrite app_length, Nat.add_comm in Hfilter. simpl in Hfilter.
rewrite app_length, Nat.add_comm. simpl.
rewrite Hfilter.
f_equal.
clear -Hfs.
generalize (Str_nth m ss).
induction n; [done |].
rewrite !stream_prefix_S, !filter_app, !app_length, IHn.
f_equal. rewrite nat_sequence_nth.
by cbn; case_decide.
Qed.
Lemma filtering_subsequence_prefix_is_filter_last
{A : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(n : nat)
(Hn : P (Str_nth n s))
: Str_nth (length (filter P (stream_prefix s n))) ss = n.
Proof.
specialize (filtering_subsequence_witness_rev _ _ _ Hfs _ Hn) as [k Heqn].
replace (length _) with k; [by subst |].
specialize (filtering_subsequence_prefix_length _ _ _ Hfs k) as Hlength.
rewrite! stream_prefix_S, filter_app in Hlength.
unfold filter at 2 in Hlength. simpl in Hlength.
rewrite decide_True in Hlength by (subst; done).
rewrite app_length, Nat.add_comm in Hlength. simpl in Hlength.
by inversion Hlength; subst.
Qed.
Given a filtering_subsequence for property
P over a stream s and
a function f transforming elements with property P, we can define the
filtering of s by P mapped through the function f.
Definition filtering_subsequence_stream_filter_map
{A B : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(f : dsig P -> B)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
: Stream B
:= map (fun k => f (dexist _ (filtering_subsequence_witness P s ss Hfs k))) nat_sequence.
{A B : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(f : dsig P -> B)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
: Stream B
:= map (fun k => f (dexist _ (filtering_subsequence_witness P s ss Hfs k))) nat_sequence.
Connecting prefixes of filtering_subsequence_stream_filter_map with
list_filter_maps on prefixes.
Lemma fitering_subsequence_stream_filter_map_prefix
{A B : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(f : dsig P -> B)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(n : nat)
(pre_filter_map := list_filter_map P f (stream_prefix s n))
(m := length pre_filter_map)
: stream_prefix (filtering_subsequence_stream_filter_map P f s ss Hfs) m = pre_filter_map.
Proof.
subst m pre_filter_map.
induction n; [done |].
rewrite stream_prefix_S, list_filter_map_app, app_length.
remember (list_filter_map P f [Str_nth n s]) as lst.
unfold list_filter_map in Heqlst.
rewrite filter_annotate_unroll in Heqlst. simpl in Heqlst.
case_decide; subst lst; simpl; [| by rewrite Nat.add_comm, app_nil_r].
replace (length (list_filter_map P f (stream_prefix s n)) + 1)
with (S (length (list_filter_map P f (stream_prefix s n))))
by lia.
rewrite stream_prefix_S.
rewrite IHn.
f_equal. f_equal.
unfold filtering_subsequence_stream_filter_map.
rewrite Str_nth_map.
f_equal. apply dsig_eq.
simpl. rewrite nat_sequence_nth.
f_equal.
unfold list_filter_map.
rewrite map_length. rewrite filter_annotate_length.
by apply filtering_subsequence_prefix_is_filter_last.
Qed.
Program Definition fitering_subsequence_stream_filter_map_prefix_ex
{A B : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(f : dsig P -> B)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(m : nat)
: {n : nat |
stream_prefix (filtering_subsequence_stream_filter_map P f s ss Hfs) m =
list_filter_map P f (stream_prefix s n)}
:=
match m with
| 0 => exist _ 0 _
| S m => exist _ (S (Str_nth m ss)) _
end.
Next Obligation.
Proof. done. Qed.
Next Obligation.
Proof.
intros. subst.
specialize (fitering_subsequence_stream_filter_map_prefix P f _ _ Hfs (S (Str_nth m ss))) as Heq.
remember (S m) as Sm.
simpl in *.
rewrite <- Heq.
f_equal.
unfold list_filter_map.
rewrite map_length. rewrite filter_annotate_length.
symmetry. subst.
by apply filtering_subsequence_prefix_length.
Qed.
Lemma stream_filter_Forall
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ss : Stream nat)
(s' := stream_subsequence s ss)
(Hfs : filtering_subsequence P s ss)
: ForAll1 P s'.
Proof.
apply ForAll1_forall.
intro n.
unfold s'.
unfold stream_subsequence.
rewrite Str_nth_map.
by apply filtering_subsequence_witness.
Qed.
{A B : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(f : dsig P -> B)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(n : nat)
(pre_filter_map := list_filter_map P f (stream_prefix s n))
(m := length pre_filter_map)
: stream_prefix (filtering_subsequence_stream_filter_map P f s ss Hfs) m = pre_filter_map.
Proof.
subst m pre_filter_map.
induction n; [done |].
rewrite stream_prefix_S, list_filter_map_app, app_length.
remember (list_filter_map P f [Str_nth n s]) as lst.
unfold list_filter_map in Heqlst.
rewrite filter_annotate_unroll in Heqlst. simpl in Heqlst.
case_decide; subst lst; simpl; [| by rewrite Nat.add_comm, app_nil_r].
replace (length (list_filter_map P f (stream_prefix s n)) + 1)
with (S (length (list_filter_map P f (stream_prefix s n))))
by lia.
rewrite stream_prefix_S.
rewrite IHn.
f_equal. f_equal.
unfold filtering_subsequence_stream_filter_map.
rewrite Str_nth_map.
f_equal. apply dsig_eq.
simpl. rewrite nat_sequence_nth.
f_equal.
unfold list_filter_map.
rewrite map_length. rewrite filter_annotate_length.
by apply filtering_subsequence_prefix_is_filter_last.
Qed.
Program Definition fitering_subsequence_stream_filter_map_prefix_ex
{A B : Type}
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
(f : dsig P -> B)
(s : Stream A)
(ss : Stream nat)
(Hfs : filtering_subsequence P s ss)
(m : nat)
: {n : nat |
stream_prefix (filtering_subsequence_stream_filter_map P f s ss Hfs) m =
list_filter_map P f (stream_prefix s n)}
:=
match m with
| 0 => exist _ 0 _
| S m => exist _ (S (Str_nth m ss)) _
end.
Next Obligation.
Proof. done. Qed.
Next Obligation.
Proof.
intros. subst.
specialize (fitering_subsequence_stream_filter_map_prefix P f _ _ Hfs (S (Str_nth m ss))) as Heq.
remember (S m) as Sm.
simpl in *.
rewrite <- Heq.
f_equal.
unfold list_filter_map.
rewrite map_length. rewrite filter_annotate_length.
symmetry. subst.
by apply filtering_subsequence_prefix_length.
Qed.
Lemma stream_filter_Forall
{A : Type}
(P : A -> Prop)
(s : Stream A)
(ss : Stream nat)
(s' := stream_subsequence s ss)
(Hfs : filtering_subsequence P s ss)
: ForAll1 P s'.
Proof.
apply ForAll1_forall.
intro n.
unfold s'.
unfold stream_subsequence.
rewrite Str_nth_map.
by apply filtering_subsequence_witness.
Qed.
Obtaining filtering_sequences for streams
Section sec_stream_filter_positions.
Context
[A : Type]
(P : A -> Prop)
{Pdec : forall a, Decision (P a)}
.
Given a stream
The definition iterates looking for the first position in which
s and a proof that there exists an element of s for
which P holds, computes the first position of s in which P holds
(shifted by the given argument n) and the remainder of s after that
position.
P holds,
termination being ensured by the fact that Exists1 is inductive.
Fixpoint stream_filter_fst_pos
(s : Stream A)
(Hev : Exists1 P s)
(n : nat)
{struct Hev}
: nat * Stream A.
Proof.
refine
(match decide (P (hd s)) with
| left p => (n, tl s)
| right _ =>
stream_filter_fst_pos (tl s) _ (S n)
end).
by destruct Hev.
Defined.
Lemma stream_filter_fst_pos_characterization
(s : Stream A)
(Hev : Exists1 P s)
(n : nat)
: exists k,
stream_filter_fst_pos s Hev n = (n + k, Str_nth_tl (S k) s) /\
P (Str_nth k s) /\ (forall i, i < k -> ~ P (Str_nth i s)).
Proof.
revert s Hev n.
fix H 2.
intros.
destruct Hev; simpl.
- destruct (decide _); [| done].
by exists 0; split_and!; f_equal; [lia | | lia].
- destruct (decide _); simpl.
+ by exists 0; split_and!; f_equal; [lia | | lia].
+ specialize (H (tl s) Hev (S n)) as (k & Heq & Hp & Hnp).
exists (S k). rewrite Heq.
split; [f_equal; lia |].
split; [done |].
intros. destruct i; [done |].
by apply Hnp; lia.
Qed.
Lemma stream_filter_fst_pos_infinitely_often
(s : Stream A)
(Hev : Exists1 P s)
(n : nat)
: InfinitelyOften P s -> InfinitelyOften P (stream_filter_fst_pos s Hev n).2.
Proof.
destruct (stream_filter_fst_pos_characterization s Hev n) as (k & -> & _).
by apply InfinitelyOften_nth_tl.
Qed.
Lemma stream_filter_fst_pos_le
(s : Stream A)
(Hev : Exists1 P s)
(n : nat)
: n <= (stream_filter_fst_pos s Hev n).1.
Proof.
destruct (stream_filter_fst_pos_characterization s Hev n) as (k & -> & _).
by cbn; lia.
Qed.
Lemma stream_filter_fst_pos_nth_tl_has_property
(s : Stream A)
(n : nat)
(sn := Str_nth_tl n s)
(Hev : Exists1 P sn)
(fpair := stream_filter_fst_pos (Str_nth_tl n s) Hev n)
: P (Str_nth fpair.1 s) /\
forall i, n <= i < fpair.1 -> ~ P (Str_nth i s).
Proof.
specialize (stream_filter_fst_pos_characterization sn Hev n)
as [k [Heq [Hp Hnp]]].
subst sn fpair.
rewrite Heq.
clear -Hp Hnp. rewrite Str_nth_plus, Nat.add_comm in Hp.
split; [done |].
intros i [Hlt_i Hilt].
apply stdpp_nat_le_sum in Hlt_i as [i' ->].
rewrite Nat.add_comm, <- Str_nth_plus.
by apply Hnp; cbn in *; lia.
Qed.
(s : Stream A)
(Hev : Exists1 P s)
(n : nat)
{struct Hev}
: nat * Stream A.
Proof.
refine
(match decide (P (hd s)) with
| left p => (n, tl s)
| right _ =>
stream_filter_fst_pos (tl s) _ (S n)
end).
by destruct Hev.
Defined.
Lemma stream_filter_fst_pos_characterization
(s : Stream A)
(Hev : Exists1 P s)
(n : nat)
: exists k,
stream_filter_fst_pos s Hev n = (n + k, Str_nth_tl (S k) s) /\
P (Str_nth k s) /\ (forall i, i < k -> ~ P (Str_nth i s)).
Proof.
revert s Hev n.
fix H 2.
intros.
destruct Hev; simpl.
- destruct (decide _); [| done].
by exists 0; split_and!; f_equal; [lia | | lia].
- destruct (decide _); simpl.
+ by exists 0; split_and!; f_equal; [lia | | lia].
+ specialize (H (tl s) Hev (S n)) as (k & Heq & Hp & Hnp).
exists (S k). rewrite Heq.
split; [f_equal; lia |].
split; [done |].
intros. destruct i; [done |].
by apply Hnp; lia.
Qed.
Lemma stream_filter_fst_pos_infinitely_often
(s : Stream A)
(Hev : Exists1 P s)
(n : nat)
: InfinitelyOften P s -> InfinitelyOften P (stream_filter_fst_pos s Hev n).2.
Proof.
destruct (stream_filter_fst_pos_characterization s Hev n) as (k & -> & _).
by apply InfinitelyOften_nth_tl.
Qed.
Lemma stream_filter_fst_pos_le
(s : Stream A)
(Hev : Exists1 P s)
(n : nat)
: n <= (stream_filter_fst_pos s Hev n).1.
Proof.
destruct (stream_filter_fst_pos_characterization s Hev n) as (k & -> & _).
by cbn; lia.
Qed.
Lemma stream_filter_fst_pos_nth_tl_has_property
(s : Stream A)
(n : nat)
(sn := Str_nth_tl n s)
(Hev : Exists1 P sn)
(fpair := stream_filter_fst_pos (Str_nth_tl n s) Hev n)
: P (Str_nth fpair.1 s) /\
forall i, n <= i < fpair.1 -> ~ P (Str_nth i s).
Proof.
specialize (stream_filter_fst_pos_characterization sn Hev n)
as [k [Heq [Hp Hnp]]].
subst sn fpair.
rewrite Heq.
clear -Hp Hnp. rewrite Str_nth_plus, Nat.add_comm in Hp.
split; [done |].
intros i [Hlt_i Hilt].
apply stdpp_nat_le_sum in Hlt_i as [i' ->].
rewrite Nat.add_comm, <- Str_nth_plus.
by apply Hnp; cbn in *; lia.
Qed.
Given as stream
s for which predicate P holds InfinitelyOften
produces the streams of all its position at which P holds in a strictly
increasing order (shifted by the given argument n).
CoFixpoint stream_filter_positions
(s : Stream A) (Hinf : InfinitelyOften P s) (n : nat) : Stream nat :=
let fpair := stream_filter_fst_pos _ (fHere _ _ Hinf) n in
Cons fpair.1 (stream_filter_positions fpair.2
(stream_filter_fst_pos_infinitely_often _ (fHere _ _ Hinf) n Hinf) (S fpair.1)).
Lemma stream_filter_positions_unroll (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat)
(fpair := stream_filter_fst_pos _ (fHere _ _ Hinf) n)
: stream_filter_positions s Hinf n =
Cons fpair.1 (stream_filter_positions fpair.2
(stream_filter_fst_pos_infinitely_often _ (fHere _ _ Hinf) n Hinf) (S fpair.1)).
Proof.
by rewrite <- recons at 1.
Qed.
Lemma stream_filter_positions_Str_nth_tl
(s : Stream A) (Hinf : InfinitelyOften P s) (n0 : nat) (n : nat)
: exists kn (Hinf' : InfinitelyOften P (Str_nth_tl (S kn) s)),
Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn) (stream_filter_positions (Str_nth_tl (S kn) s) Hinf' (S (n0 + kn))) /\
P (Str_nth kn s).
Proof.
induction n.
- simpl. rewrite (stream_filter_positions_unroll s Hinf n0).
specialize
(stream_filter_fst_pos_characterization s (fHere _ s Hinf) n0)
as [k [Heq [Hp _]]].
assert (Hk : (stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).1 = n0 + k).
{ by rewrite Heq. }
assert (Htl : (stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).2 = Str_nth_tl (S k) s).
{ by rewrite Heq. }
exists k.
by rewrite Hk; cbn in *; rewrite <- Htl; eauto.
- replace
(Str_nth_tl (S n) (stream_filter_positions s Hinf n0))
with (tl (Str_nth_tl n (stream_filter_positions s Hinf n0)))
by apply tl_nth_tl.
destruct IHn as [kn [Hinfn [Hsn Hpn]]].
rewrite Hsn.
simpl. rewrite (stream_filter_positions_unroll (Str_nth_tl kn (tl s)) Hinfn (S (n0 + kn))).
specialize
(stream_filter_fst_pos_characterization (Str_nth_tl kn (tl s)) (fHere _ _ Hinfn) (S (n0 + kn)))
as [k [Heq [Hp _]]].
exists (S (k + kn)).
cbn in Heq.
apply (f_equal fst) in Heq as Hk; rewrite Hk.
apply (f_equal snd) in Heq as Htl.
simpl in Htl |- *.
rewrite tl_nth_tl, Str_nth_tl_plus in Htl.
rewrite Str_nth_plus in Hp.
rewrite <- Htl.
by replace (n0 + S (k + kn)) with (S (n0 + kn + k)) by lia; eauto.
Qed.
Lemma stream_filter_positions_monotone
(s : Stream A) (Hinf : InfinitelyOften P s) (n : nat)
: monotone_nat_stream_prop (stream_filter_positions s Hinf n).
Proof.
apply monotone_nat_stream_prop_from_successor.
revert s Hinf n.
cofix H.
intros.
constructor; simpl; [| by apply H].
by apply stream_filter_fst_pos_le.
Qed.
(s : Stream A) (Hinf : InfinitelyOften P s) (n : nat) : Stream nat :=
let fpair := stream_filter_fst_pos _ (fHere _ _ Hinf) n in
Cons fpair.1 (stream_filter_positions fpair.2
(stream_filter_fst_pos_infinitely_often _ (fHere _ _ Hinf) n Hinf) (S fpair.1)).
Lemma stream_filter_positions_unroll (s : Stream A) (Hinf : InfinitelyOften P s) (n : nat)
(fpair := stream_filter_fst_pos _ (fHere _ _ Hinf) n)
: stream_filter_positions s Hinf n =
Cons fpair.1 (stream_filter_positions fpair.2
(stream_filter_fst_pos_infinitely_often _ (fHere _ _ Hinf) n Hinf) (S fpair.1)).
Proof.
by rewrite <- recons at 1.
Qed.
Lemma stream_filter_positions_Str_nth_tl
(s : Stream A) (Hinf : InfinitelyOften P s) (n0 : nat) (n : nat)
: exists kn (Hinf' : InfinitelyOften P (Str_nth_tl (S kn) s)),
Str_nth_tl n (stream_filter_positions s Hinf n0) =
Cons (n0 + kn) (stream_filter_positions (Str_nth_tl (S kn) s) Hinf' (S (n0 + kn))) /\
P (Str_nth kn s).
Proof.
induction n.
- simpl. rewrite (stream_filter_positions_unroll s Hinf n0).
specialize
(stream_filter_fst_pos_characterization s (fHere _ s Hinf) n0)
as [k [Heq [Hp _]]].
assert (Hk : (stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).1 = n0 + k).
{ by rewrite Heq. }
assert (Htl : (stream_filter_fst_pos s (fHere (Exists1 P) s Hinf) n0).2 = Str_nth_tl (S k) s).
{ by rewrite Heq. }
exists k.
by rewrite Hk; cbn in *; rewrite <- Htl; eauto.
- replace
(Str_nth_tl (S n) (stream_filter_positions s Hinf n0))
with (tl (Str_nth_tl n (stream_filter_positions s Hinf n0)))
by apply tl_nth_tl.
destruct IHn as [kn [Hinfn [Hsn Hpn]]].
rewrite Hsn.
simpl. rewrite (stream_filter_positions_unroll (Str_nth_tl kn (tl s)) Hinfn (S (n0 + kn))).
specialize
(stream_filter_fst_pos_characterization (Str_nth_tl kn (tl s)) (fHere _ _ Hinfn) (S (n0 + kn)))
as [k [Heq [Hp _]]].
exists (S (k + kn)).
cbn in Heq.
apply (f_equal fst) in Heq as Hk; rewrite Hk.
apply (f_equal snd) in Heq as Htl.
simpl in Htl |- *.
rewrite tl_nth_tl, Str_nth_tl_plus in Htl.
rewrite Str_nth_plus in Hp.
rewrite <- Htl.
by replace (n0 + S (k + kn)) with (S (n0 + kn + k)) by lia; eauto.
Qed.
Lemma stream_filter_positions_monotone
(s : Stream A) (Hinf : InfinitelyOften P s) (n : nat)
: monotone_nat_stream_prop (stream_filter_positions s Hinf n).
Proof.
apply monotone_nat_stream_prop_from_successor.
revert s Hinf n.
cofix H.
intros.
constructor; simpl; [| by apply H].
by apply stream_filter_fst_pos_le.
Qed.
stream_filter_positions produces a filtering_sequence.
Lemma stream_filter_positions_filtering_subsequence
(s : Stream A) (Hinf : InfinitelyOften P s)
: filtering_subsequence P s (stream_filter_positions s Hinf 0).
Proof.
split.
- specialize (stream_filter_fst_pos_characterization s (fHere (Exists1 P) s Hinf) 0)
as [k [Heq [Hpk Hnp]]].
simpl in Heq.
by rewrite stream_filter_positions_unroll; cbn; rewrite Heq.
- apply ForAll2_forall.
intro n.
specialize (stream_filter_positions_Str_nth_tl s Hinf 0 n) as Hnth_tl.
simpl in Hnth_tl.
remember (stream_filter_positions s Hinf 0).
destruct Hnth_tl as [kn [Hnth_inf [Hnth Hnth_p]]].
unfold Str_nth. simpl. rewrite <- tl_nth_tl.
rewrite stream_filter_positions_unroll in Hnth.
specialize (stream_filter_fst_pos_characterization
(Str_nth_tl kn (tl s)) (fHere _ _ Hnth_inf) (S kn))
as [k [Heq [Hpk Hnp]]].
rewrite Hnth; simpl.
split; [done |].
rewrite Heq. simpl.
split; [lia |].
intros i [Hle Hlt].
apply stdpp_nat_le_sum in Hle as [k' ->].
rewrite Nat.add_comm, <- Str_nth_tl_plus. simpl.
by apply Hnp; lia.
Qed.
(s : Stream A) (Hinf : InfinitelyOften P s)
: filtering_subsequence P s (stream_filter_positions s Hinf 0).
Proof.
split.
- specialize (stream_filter_fst_pos_characterization s (fHere (Exists1 P) s Hinf) 0)
as [k [Heq [Hpk Hnp]]].
simpl in Heq.
by rewrite stream_filter_positions_unroll; cbn; rewrite Heq.
- apply ForAll2_forall.
intro n.
specialize (stream_filter_positions_Str_nth_tl s Hinf 0 n) as Hnth_tl.
simpl in Hnth_tl.
remember (stream_filter_positions s Hinf 0).
destruct Hnth_tl as [kn [Hnth_inf [Hnth Hnth_p]]].
unfold Str_nth. simpl. rewrite <- tl_nth_tl.
rewrite stream_filter_positions_unroll in Hnth.
specialize (stream_filter_fst_pos_characterization
(Str_nth_tl kn (tl s)) (fHere _ _ Hnth_inf) (S kn))
as [k [Heq [Hpk Hnp]]].
rewrite Hnth; simpl.
split; [done |].
rewrite Heq. simpl.
split; [lia |].
intros i [Hle Hlt].
apply stdpp_nat_le_sum in Hle as [k' ->].
rewrite Nat.add_comm, <- Str_nth_tl_plus. simpl.
by apply Hnp; lia.
Qed.
A restatement of filtering_subsequence_stream_filter_map based on the
InfinitelyOften predicate, using the stream_filter_positions_filtering_subsequence.
Definition stream_filter_map
[B : Type]
(f : dsig P -> B)
(s : Stream A)
(Hinf : InfinitelyOften P s)
: Stream B :=
filtering_subsequence_stream_filter_map P f _ _
(stream_filter_positions_filtering_subsequence s Hinf).
[B : Type]
(f : dsig P -> B)
(s : Stream A)
(Hinf : InfinitelyOften P s)
: Stream B :=
filtering_subsequence_stream_filter_map P f _ _
(stream_filter_positions_filtering_subsequence s Hinf).
Stream filtering is obtained as a specialization of stream_filter_map.
Definition stream_filter
(s : Stream A)
(Hinf : InfinitelyOften P s)
: Stream A :=
stream_filter_map proj1_sig s Hinf.
End sec_stream_filter_positions.
Section sec_stream_map_option.
(s : Stream A)
(Hinf : InfinitelyOften P s)
: Stream A :=
stream_filter_map proj1_sig s Hinf.
End sec_stream_filter_positions.
Section sec_stream_map_option.
Mapping a partial function on a stream
f which is InfinitelyOften defined on the
elements of a stream s, we can define the stream of the defined mapped
values of s through f as a particular stream_filter_map.
Context
[A B : Type]
(f : A -> option B)
(P : A -> Prop := is_Some ∘ f)
(s : Stream A)
.
Definition stream_map_option
(Hinf : InfinitelyOften P s)
: Stream B :=
stream_filter_map P (fun k : dsig P => is_Some_proj (proj2_dsig k)) s Hinf.
Lemma stream_map_option_prefix
(Hinf : InfinitelyOften P s)
(n : nat)
(map_opt_pre := omap f (stream_prefix s n))
(m := length map_opt_pre)
: stream_prefix (stream_map_option Hinf) m = map_opt_pre.
Proof.
subst map_opt_pre m.
rewrite !(omap_as_filter f (stream_prefix s n)).
by apply fitering_subsequence_stream_filter_map_prefix.
Qed.
Program Definition stream_map_option_prefix_ex
(Hinf : InfinitelyOften P s)
(Hfs := stream_filter_positions_filtering_subsequence _ _ Hinf)
(k : nat)
: { n | stream_prefix (stream_map_option Hinf) k = omap f (stream_prefix s n)} :=
let (n, Heq) := (fitering_subsequence_stream_filter_map_prefix_ex P
(fun k => is_Some_proj (proj2_dsig k)) _ _ Hfs k)
in exist _ n _.
Next Obligation.
Proof.
by intros; cbn; rewrite !omap_as_filter.
Qed.
Definition bounded_stream_map_option
(Hfin : FinitelyManyBound P s)
: list B :=
omap f (stream_prefix s (` Hfin)).
End sec_stream_map_option.
Section sec_stream_concat_map.
Mapping a function expanding elements to lists of elements on a stream
f which InfinitelyOften produces non-empty lists from
the elements of a stream s, we can define the stream obtained by
concatenating the values of s through f.
Context
[A B : Type]
(f : A -> list B)
(FNonEmpty : A -> Prop := fun a => f a <> [])
(s : Stream A)
.
Definition stream_concat_map
(Hinf : InfinitelyOften FNonEmpty s)
: Stream B :=
stream_concat (stream_filter_map FNonEmpty (list_function_restriction f) s Hinf).
Lemma stream_concat_map_prefix
(Hinf : InfinitelyOften FNonEmpty s)
(n : nat)
(mbind_prefix := mbind f (stream_prefix s n))
(m := length mbind_prefix)
: stream_prefix (stream_concat_map Hinf) m = mbind_prefix.
Proof.
subst mbind_prefix m; unfold stream_concat_map.
cut (mjoin
(List.map ne_list_to_list
(list_filter_map (fun a : A => f a <> []) (list_function_restriction f)
(stream_prefix s n))) = mbind f (stream_prefix s n)).
{
intros <-.
by erewrite stream_concat_prefix;
unfold stream_filter_map;
rewrite fitering_subsequence_stream_filter_map_prefix.
}
by apply list_filter_map_mbind.
Qed.
Program Definition stream_concat_map_ex_prefix
(Hinf : InfinitelyOften FNonEmpty s)
(Hfs := stream_filter_positions_filtering_subsequence _ _ Hinf)
(k : nat)
: {n : nat |
stream_prefix (stream_concat_map Hinf) k
`prefix_of`
mbind f (stream_prefix s n)}
:=
let (n, Heq) :=
(fitering_subsequence_stream_filter_map_prefix_ex
FNonEmpty (list_function_restriction f) _ _ Hfs k)
in exist _ n _.
Next Obligation.
Proof.
cbn; intros Hinf k n Heq.
rewrite <- (stream_concat_map_prefix Hinf).
apply stream_prefix_of.
rewrite <- list_filter_map_mbind.
replace k
with (length (list_filter_map FNonEmpty (list_function_restriction f) (stream_prefix s n)))
by (rewrite <- Heq; apply stream_prefix_length).
by apply ne_list_concat_min_length.
Qed.
Program Definition stream_concat_map_ex_min_prefix
`{EqDecision B}
(Hinf : InfinitelyOften FNonEmpty s)
(k : nat)
(Ppre := fun m =>
stream_prefix (stream_concat_map Hinf) k
`prefix_of`
mbind f (stream_prefix s m))
: {n : nat | minimal_among le Ppre n}
:=
let (n, Hpre) := stream_concat_map_ex_prefix Hinf k in
exist _ (find_least_among Ppre n) _.
Next Obligation.
Proof.
by intros; apply find_least_among_is_minimal.
Qed.
Definition bounded_stream_concat_map
(Hfin : FinitelyManyBound FNonEmpty s)
: list B :=
mbind f (stream_prefix s (` Hfin)).
End sec_stream_concat_map.
For a totally defined function, stream_map_option corresponds to the
regular map on streams.
Lemma stream_map_option_EqSt [A B : Type] (f : A -> B)
: forall s (Hinf : InfinitelyOften (is_Some ∘ (Some ∘ f)) s),
EqSt (map f s) (stream_map_option (Some ∘ f) s Hinf).
Proof.
intros. apply EqSt_stream_prefix. intro n.
destruct n; [done |].
rewrite <- stream_prefix_map.
pose (stream_map_option_prefix_ex (Some ∘ f) s Hinf (S n)) as Hrew.
rewrite (proj2_sig Hrew).
replace (` Hrew) with (S n); [done |].
simpl. f_equal. clear.
cut
(forall k, Streams.Str_nth n
(stream_filter_positions (is_Some ∘ (Some ∘ f)) s Hinf k) = k + n).
{ intros Hk. specialize (Hk 0). simpl in Hk. congruence. }
revert s Hinf.
assert (Hfirst : forall s Hinf k,
(stream_filter_fst_pos (is_Some ∘ (Some ∘ f)) s (fHere _ _ Hinf) k).1 = k).
{
intros.
edestruct stream_filter_fst_pos_characterization as (_k & -> & _ & H_k); cbn.
destruct _k; [lia |].
by exfalso; apply (H_k 0); [lia | eexists].
}
induction n; intros; rewrite stream_filter_positions_unroll; unfold Streams.Str_nth; simpl.
- by rewrite Hfirst; lia.
- unfold Streams.Str_nth in IHn.
by rewrite IHn, Hfirst; lia.
Qed.
: forall s (Hinf : InfinitelyOften (is_Some ∘ (Some ∘ f)) s),
EqSt (map f s) (stream_map_option (Some ∘ f) s Hinf).
Proof.
intros. apply EqSt_stream_prefix. intro n.
destruct n; [done |].
rewrite <- stream_prefix_map.
pose (stream_map_option_prefix_ex (Some ∘ f) s Hinf (S n)) as Hrew.
rewrite (proj2_sig Hrew).
replace (` Hrew) with (S n); [done |].
simpl. f_equal. clear.
cut
(forall k, Streams.Str_nth n
(stream_filter_positions (is_Some ∘ (Some ∘ f)) s Hinf k) = k + n).
{ intros Hk. specialize (Hk 0). simpl in Hk. congruence. }
revert s Hinf.
assert (Hfirst : forall s Hinf k,
(stream_filter_fst_pos (is_Some ∘ (Some ∘ f)) s (fHere _ _ Hinf) k).1 = k).
{
intros.
edestruct stream_filter_fst_pos_characterization as (_k & -> & _ & H_k); cbn.
destruct _k; [lia |].
by exfalso; apply (H_k 0); [lia | eexists].
}
induction n; intros; rewrite stream_filter_positions_unroll; unfold Streams.Str_nth; simpl.
- by rewrite Hfirst; lia.
- unfold Streams.Str_nth in IHn.
by rewrite IHn, Hfirst; lia.
Qed.