Library Waterproof.Libs.Analysis.SubsequencesMetric
From Stdlib Require Import ZArith.
From Stdlib Require Import Reals.Reals.
Require Import Automation.
Require Import Libs.Analysis.MetricSpaces.
Require Import Libs.Analysis.SequencesMetric.
Require Import Notations.Common.
Require Import Notations.Reals.
Require Import Notations.Sets.
Require Import Chains.
Require Import Tactics.
Waterproof Enable Automation RealsAndIntegers.
Open Scope R_scope.
Open Scope metric_scope.
Open Scope subset_scope.
Definition is_index_sequence (n : ℕ → ℕ) :=
∀ k ∈ ℕ, (n k < n (k + 1))%nat.
Notation "'_index' 'sequence_'" := (is_index_sequence) (at level 69) : metric_scope.
Notation "'_index' 'sequence_'" := (is_index_sequence) (at level 69) : pred_for_subset_scope.
Notation "'index' 'sequence'" := (is_index_sequence) (at level 69, only parsing) : metric_scope.
Notation "'index' 'sequence'" := (is_index_sequence) (at level 69, only parsing) : pred_for_subset_scope.
Notation "n 'is' 'an' '_index' 'sequence_'" := (is_index_sequence n) (at level 69) : metric_scope.
Notation "n 'is' 'an' 'index' 'sequence'" := (is_index_sequence n) (at level 69, only parsing) : metric_scope.
Waterproof Register Expand "index" "sequence";
for is_index_sequence;
as "Definition index sequence".
The next definition captures what it means to be an index sequence.
Definition is_index_seq (n : ℕ → ℕ) :=
∀ k ∈ ℕ, (n k < n (k + 1))%nat.
Notation "a ◦ n" := (fun (k : nat) => a (n k)) (right associativity, at level 11).
Notation "a ◦ n ◦ m" := (fun (k : nat) => a (n (m k))) (right associativity).
Section my_section.
Variable X : Metric_Space.
Definition is_subsequence (b : ℕ → X) (a : ℕ → X) :=
∃ m : (ℕ → ℕ),
is_index_sequence m ∧ ∀ k ∈ ℕ,
b k = (a ◦ m) k.
Definition is_accumulation_point (p : X) (a : ℕ → X) :=
∃ m : (ℕ → ℕ),
is_index_sequence m ∧ (a ◦ m) ⟶ p.
Lemma index_sequence_property (n : ℕ → ℕ) :
is_index_sequence n ⇒
∀ k ∈ ℕ,
(n k ≥ k)%nat.
Proof.
intros.
unfold is_index_sequence in H.
unfold seal.
induction k.
specialize (H 0%nat).
unfold ge.
intro H0.
apply Nat.le_0_l.
specialize (H k).
unfold ge.
intro H1.
apply Nat.le_succ_l.
rewrite Nat.add_1_r in H.
apply (Nat.le_lt_trans k (n k)).
apply IHk; trivial.
apply H; trivial.
Qed.
Lemma index_sequence_property_automation (n : ℕ → ℕ) :
is_index_sequence n ⇒
∀ k : ℕ, (n k ≥ k)%nat.
Proof.
intros; apply index_sequence_property; auto with wp_core.
Qed.
Lemma index_seq_equiv (n : ℕ → ℕ) : is_index_seq n ⇔ is_index_sequence n.
Proof.
We show both directions.
- We need to show that is_index_seq n ⇨ is_index_sequence n.
intro.
unfold is_index_sequence.
Take k ∈ ℕ.
unfold is_index_seq in H.
We conclude that (n k < n (k + 1))%nat.
- We need to show that is_index_sequence n ⇨ is_index_seq n.
intro.
unfold is_index_seq.
Take k ∈ ℕ.
unfold is_index_sequence in H.
We conclude that (n k < n (k + 1))%nat.
Qed.
Definition is_increasing (g : ℕ → ℕ) :=
∀ k ∈ ℕ, (g k ≤ g (k + 1))%nat.
Lemma incr_loc_to_glob (g : ℕ → ℕ) :
is_increasing g
⇒ (∀ k ∈ ℕ, ∀ l ∈ ℕ, (k ≤ l)%nat ⇒ (g k ≤ g l)%nat).
Proof.
Assume that (∀ k ∈ ℕ, (g k) ≤ (g (k + 1)))%nat.
Take k ∈ ℕ.
We use induction on l.
- We first show the base case (k ≤ 0)%nat ⇨ (g k ≤ g 0)%nat.
Assume that (k ≤ 0)%nat.
It holds that (k = 0)%nat.
It suffices to show that (g k = g 0)%nat.
We conclude that (g k = g 0)%nat.
- We now show the induction step.
Take l ∈ ℕ.
Assume that ((k ≤ l) ⇨ (g k ≤ g l))%nat as (IH).
Assume that (k ≤ l + 1)%nat.
destruct (lt_eq_lt_dec k (l + 1)) as [[k_lt_Sl | k_eq_Sl] | k_gt_Sl].
+
∀ k ∈ ℕ, (n k < n (k + 1))%nat.
Notation "a ◦ n" := (fun (k : nat) => a (n k)) (right associativity, at level 11).
Notation "a ◦ n ◦ m" := (fun (k : nat) => a (n (m k))) (right associativity).
Section my_section.
Variable X : Metric_Space.
Definition is_subsequence (b : ℕ → X) (a : ℕ → X) :=
∃ m : (ℕ → ℕ),
is_index_sequence m ∧ ∀ k ∈ ℕ,
b k = (a ◦ m) k.
Definition is_accumulation_point (p : X) (a : ℕ → X) :=
∃ m : (ℕ → ℕ),
is_index_sequence m ∧ (a ◦ m) ⟶ p.
Lemma index_sequence_property (n : ℕ → ℕ) :
is_index_sequence n ⇒
∀ k ∈ ℕ,
(n k ≥ k)%nat.
Proof.
intros.
unfold is_index_sequence in H.
unfold seal.
induction k.
specialize (H 0%nat).
unfold ge.
intro H0.
apply Nat.le_0_l.
specialize (H k).
unfold ge.
intro H1.
apply Nat.le_succ_l.
rewrite Nat.add_1_r in H.
apply (Nat.le_lt_trans k (n k)).
apply IHk; trivial.
apply H; trivial.
Qed.
Lemma index_sequence_property_automation (n : ℕ → ℕ) :
is_index_sequence n ⇒
∀ k : ℕ, (n k ≥ k)%nat.
Proof.
intros; apply index_sequence_property; auto with wp_core.
Qed.
Lemma index_seq_equiv (n : ℕ → ℕ) : is_index_seq n ⇔ is_index_sequence n.
Proof.
We show both directions.
- We need to show that is_index_seq n ⇨ is_index_sequence n.
intro.
unfold is_index_sequence.
Take k ∈ ℕ.
unfold is_index_seq in H.
We conclude that (n k < n (k + 1))%nat.
- We need to show that is_index_sequence n ⇨ is_index_seq n.
intro.
unfold is_index_seq.
Take k ∈ ℕ.
unfold is_index_sequence in H.
We conclude that (n k < n (k + 1))%nat.
Qed.
Definition is_increasing (g : ℕ → ℕ) :=
∀ k ∈ ℕ, (g k ≤ g (k + 1))%nat.
Lemma incr_loc_to_glob (g : ℕ → ℕ) :
is_increasing g
⇒ (∀ k ∈ ℕ, ∀ l ∈ ℕ, (k ≤ l)%nat ⇒ (g k ≤ g l)%nat).
Proof.
Assume that (∀ k ∈ ℕ, (g k) ≤ (g (k + 1)))%nat.
Take k ∈ ℕ.
We use induction on l.
- We first show the base case (k ≤ 0)%nat ⇨ (g k ≤ g 0)%nat.
Assume that (k ≤ 0)%nat.
It holds that (k = 0)%nat.
It suffices to show that (g k = g 0)%nat.
We conclude that (g k = g 0)%nat.
- We now show the induction step.
Take l ∈ ℕ.
Assume that ((k ≤ l) ⇨ (g k ≤ g l))%nat as (IH).
Assume that (k ≤ l + 1)%nat.
destruct (lt_eq_lt_dec k (l + 1)) as [[k_lt_Sl | k_eq_Sl] | k_gt_Sl].
+
We first consider the case that .
We now consider the case . We need to show that .
Finally we consider the case . However, this case is in contradiction with .
It holds that ¬(l + 1 < k)%nat.
Contradiction.
Qed.
Lemma index_sequence_property2 (n : ℕ → ℕ) :
is_index_sequence n ⇒
∀ k1 ∈ ℕ, ∀ k2 ∈ ℕ,
(k1 ≥ k2)%nat ⇒
(n k1 ≥ n k2)%nat.
Proof.
Assume that is_index_sequence n.
Take k1, k2 ∈ ℕ; such that (k1 ≥ k2)%nat.
We need to show that (n k1 ≥ n k2)%nat.
By incr_loc_to_glob it suffices to show that is_increasing n.
We need to show that ∀ k ∈ ℕ, (n k ≤ n (k + 1))%nat.
Take k ∈ ℕ.
We conclude that (n k ≤ n (k+1))%nat.
Qed.
Lemma index_sequence_property2_automation (n : ℕ → ℕ) :
is_index_sequence n ⇒
∀ k1 : ℕ, ∀ k2 : ℕ,
(k1 ≥ k2)%nat ⇒
(n k1 ≥ n k2)%nat.
Proof.
intros; apply index_sequence_property2; auto with wp_core.
Qed.
Open Scope nat_scope.
Lemma double_is_even (n : nat) : Nat.even (2 * n) = true.
Proof.
It holds that Nat.even (2 * n) = Nat.even (0 + 2 * n).
It suffices to show that Nat.even (0 + 2*n) = true.
By Nat.even_add_mul_2 it holds that Nat.even (0 + 2*n) = Nat.even 0.
It holds that Nat.even 0 = true.
We conclude that Nat.even (0 + 2 * n) = true.
Qed.
Close Scope nat_scope.
Lemma subsequence_of_convergent_sequence (a : (ℕ → X)) (p : X) :
a ⟶ p ⇒ ∀ n _index sequence_, (a ◦ n) ⟶ p.
Proof.
Assume that a ⟶ p.
Take n index sequence.
It suffices to show that ∀ ε > 0, ∃ N1 ∈ ℕ,
(∀ k ≥ N1, (dist _ (a (n k)) p < ε)%R)%nat.
Take ε > 0.
It holds that ∃ N2 ∈ ℕ, ∀ k : ℕ, (k ≥ N2)%nat → dist _ (a k) p < ε.
Obtain such an N2. Choose N1 := N2.
* Indeed, N1 ∈ ℕ.
* We need to show that (∀ k ≥ N1, (dist(X, a(n(k)), p) < ε)%R)%nat.
Take k : ℕ; such that (k ≥ N1)%nat.
By index_sequence_property2 it holds that (n k ≥ n N1)%nat.
By index_sequence_property it holds that (n N1 ≥ N1)%nat.
assert (H3 : (n k ≥ N1)%nat) by auto with zarith.
We conclude that dist _ (a (n k)) p < ε.
Qed.
Close Scope nat_scope.
Lemma equivalent_subsequence_convergence (x y : ℕ → X) (p : X) :
is_subsequence y x ⇒ x ⟶ p ⇒ y ⟶ p.
Proof.
Assume that is_subsequence y x.
Assume that x ⟶ p.
We need to show that y ⟶ p.
It holds that ∃ m : (ℕ → ℕ), is_index_sequence m ∧ ∀ k ∈ ℕ, y k = (x ◦ m) k.
Obtain such an m. It holds that
is_index_sequence m ∧ ∀ k : ℕ, y k = (x ◦ m) k as (i).
Because (i) both is_index_sequence m and
for all k : nat, y k = x (m k) hold.
It suffices to show that ∀ ε > 0, ∃ N3 ∈ ℕ,
(∀ k ≥ N3, (dist _ (y k) p < ε)%R)%nat.
Take ε : ℝ; such that ε > 0.
It holds that ∃ K ∈ ℕ, ∀ k : ℕ, (k ≥ K)%nat → dist _ (x k) p < ε.
Obtain such a K. Choose N3 := K.
* Indeed, N3 ∈ ℕ.
* We need to show that ∀ k ≥ N3, (dist(X, y(k), p) < ε)%R%nat.
Take k : ℕ; such that (k ≥ N3)%nat.
By index_sequence_property2 it holds that (m k ≥ m K)%nat.
By index_sequence_property it holds that (m K ≥ K)%nat.
It holds that (m k ≥ K)%nat.
It holds that dist _ (x (m k)) p < ε.
It holds that y k = x (m k) as (iv).
rewrite (iv).
We conclude that dist _ (x (m k)) p < ε.
Qed.
End my_section.
Notation "b 'is' 'a' '_subsequence_' 'of' a" := (is_subsequence _ b a) (at level 69) : metric_scope.
Notation "b 'is' 'a' 'subsequence' 'of' a" := (is_subsequence _ b a) (at level 69, only parsing) : metric_scope.
Waterproof Register Expand "subsequence";
for is_subsequence;
as "Definition subsequence".
Notation "p 'is' 'an' '_accumulation' 'point_' 'of' a" := (is_accumulation_point _ p a) (at level 69) : metric_scope.
Notation "p 'is' 'an' 'accumulation' 'point' 'of' a" := (is_accumulation_point _ p a) (at level 69, only parsing) : metric_scope.
Waterproof Register Expand "accumulation" "point";
for is_accumulation_point;
as "Definition (sequential) accumulation point".
#[export] Hint Resolve index_sequence_property_automation : subsequences.
#[export] Hint Extern 1 => (unfold ge) : subsequences.
#[export] Hint Resolve double_is_even : wp_integers.
#[export] Hint Resolve index_sequence_property2_automation : subsequences.
Close Scope metric_scope.
Close Scope R_scope.
Contradiction.
Qed.
Lemma index_sequence_property2 (n : ℕ → ℕ) :
is_index_sequence n ⇒
∀ k1 ∈ ℕ, ∀ k2 ∈ ℕ,
(k1 ≥ k2)%nat ⇒
(n k1 ≥ n k2)%nat.
Proof.
Assume that is_index_sequence n.
Take k1, k2 ∈ ℕ; such that (k1 ≥ k2)%nat.
We need to show that (n k1 ≥ n k2)%nat.
By incr_loc_to_glob it suffices to show that is_increasing n.
We need to show that ∀ k ∈ ℕ, (n k ≤ n (k + 1))%nat.
Take k ∈ ℕ.
We conclude that (n k ≤ n (k+1))%nat.
Qed.
Lemma index_sequence_property2_automation (n : ℕ → ℕ) :
is_index_sequence n ⇒
∀ k1 : ℕ, ∀ k2 : ℕ,
(k1 ≥ k2)%nat ⇒
(n k1 ≥ n k2)%nat.
Proof.
intros; apply index_sequence_property2; auto with wp_core.
Qed.
Open Scope nat_scope.
Lemma double_is_even (n : nat) : Nat.even (2 * n) = true.
Proof.
It holds that Nat.even (2 * n) = Nat.even (0 + 2 * n).
It suffices to show that Nat.even (0 + 2*n) = true.
By Nat.even_add_mul_2 it holds that Nat.even (0 + 2*n) = Nat.even 0.
It holds that Nat.even 0 = true.
We conclude that Nat.even (0 + 2 * n) = true.
Qed.
Close Scope nat_scope.
Lemma subsequence_of_convergent_sequence (a : (ℕ → X)) (p : X) :
a ⟶ p ⇒ ∀ n _index sequence_, (a ◦ n) ⟶ p.
Proof.
Assume that a ⟶ p.
Take n index sequence.
It suffices to show that ∀ ε > 0, ∃ N1 ∈ ℕ,
(∀ k ≥ N1, (dist _ (a (n k)) p < ε)%R)%nat.
Take ε > 0.
It holds that ∃ N2 ∈ ℕ, ∀ k : ℕ, (k ≥ N2)%nat → dist _ (a k) p < ε.
Obtain such an N2. Choose N1 := N2.
* Indeed, N1 ∈ ℕ.
* We need to show that (∀ k ≥ N1, (dist(X, a(n(k)), p) < ε)%R)%nat.
Take k : ℕ; such that (k ≥ N1)%nat.
By index_sequence_property2 it holds that (n k ≥ n N1)%nat.
By index_sequence_property it holds that (n N1 ≥ N1)%nat.
assert (H3 : (n k ≥ N1)%nat) by auto with zarith.
We conclude that dist _ (a (n k)) p < ε.
Qed.
Close Scope nat_scope.
Lemma equivalent_subsequence_convergence (x y : ℕ → X) (p : X) :
is_subsequence y x ⇒ x ⟶ p ⇒ y ⟶ p.
Proof.
Assume that is_subsequence y x.
Assume that x ⟶ p.
We need to show that y ⟶ p.
It holds that ∃ m : (ℕ → ℕ), is_index_sequence m ∧ ∀ k ∈ ℕ, y k = (x ◦ m) k.
Obtain such an m. It holds that
is_index_sequence m ∧ ∀ k : ℕ, y k = (x ◦ m) k as (i).
Because (i) both is_index_sequence m and
for all k : nat, y k = x (m k) hold.
It suffices to show that ∀ ε > 0, ∃ N3 ∈ ℕ,
(∀ k ≥ N3, (dist _ (y k) p < ε)%R)%nat.
Take ε : ℝ; such that ε > 0.
It holds that ∃ K ∈ ℕ, ∀ k : ℕ, (k ≥ K)%nat → dist _ (x k) p < ε.
Obtain such a K. Choose N3 := K.
* Indeed, N3 ∈ ℕ.
* We need to show that ∀ k ≥ N3, (dist(X, y(k), p) < ε)%R%nat.
Take k : ℕ; such that (k ≥ N3)%nat.
By index_sequence_property2 it holds that (m k ≥ m K)%nat.
By index_sequence_property it holds that (m K ≥ K)%nat.
It holds that (m k ≥ K)%nat.
It holds that dist _ (x (m k)) p < ε.
It holds that y k = x (m k) as (iv).
rewrite (iv).
We conclude that dist _ (x (m k)) p < ε.
Qed.
End my_section.
Notation "b 'is' 'a' '_subsequence_' 'of' a" := (is_subsequence _ b a) (at level 69) : metric_scope.
Notation "b 'is' 'a' 'subsequence' 'of' a" := (is_subsequence _ b a) (at level 69, only parsing) : metric_scope.
Waterproof Register Expand "subsequence";
for is_subsequence;
as "Definition subsequence".
Notation "p 'is' 'an' '_accumulation' 'point_' 'of' a" := (is_accumulation_point _ p a) (at level 69) : metric_scope.
Notation "p 'is' 'an' 'accumulation' 'point' 'of' a" := (is_accumulation_point _ p a) (at level 69, only parsing) : metric_scope.
Waterproof Register Expand "accumulation" "point";
for is_accumulation_point;
as "Definition (sequential) accumulation point".
#[export] Hint Resolve index_sequence_property_automation : subsequences.
#[export] Hint Extern 1 => (unfold ge) : subsequences.
#[export] Hint Resolve double_is_even : wp_integers.
#[export] Hint Resolve index_sequence_property2_automation : subsequences.
Close Scope metric_scope.
Close Scope R_scope.