Lessness (Apr 04 2021 at 20:59): Lessness (Apr 04 2021 at 20:59):I'm trying to construct nested segments (last definition), but I've got a problem.
The goal doesn't simplify to expected m <= x <= M... it probably means a defined function ns wrongly in some way, but I can't wrap my brain around it and find the mistake.
I will be thankful for any help.
Require Import Reals Lra Utf8 Lia Classical IndefiniteDescription.
Open Scope R.
Set Implicit Arguments.
Axiom classic_sumbool: ∀ (P: Prop), {P} + {¬ P}.
Definition set A := A → Prop.
Definition subset A (X Y: set A) := ∀ x, X x → Y x.
Definition sequence_of A := nat → A.
Definition Rle_pair := { p: R * R | fst p <= snd p }.
Coercion Rle_pair_proj1 (p: Rle_pair) := proj1_sig p.
Definition segment (p: Rle_pair): set R := match p: R * R with (a, b) => λ x, a <= x <= b end.
Tactic Notation "transparent" "assert" "(" ident(H) ":" open_constr(type) ")" :=
refine (let H := (_ : type) in _).
Definition nested_segments :=
{ ns: nat → Rle_pair | ∀ i, subset (segment (ns (S i))) (segment (ns i)) }.
Definition nested_segments_proj1 (ns: nested_segments) := proj1_sig ns.
Coercion nested_segments_proj1: nested_segments >-> Funclass.
Definition sequence := sequence_of R.
Definition normal_subsequence := { s: nat → nat | ∀ i, (s i < s (S i))%nat }.
Definition normal_subsequence_proj1 (s: normal_subsequence) := proj1_sig s.
Coercion normal_subsequence_proj1: normal_subsequence >-> Funclass.
Definition normal_subsequence_of (xn: sequence) (s: normal_subsequence): sequence := λ i, xn (s i).
Definition finite_elements A (P: A → Prop) (s: sequence_of A) :=
∃ (L: list nat), ∀ n, P (s n) → List.In n L.
Definition infinite_elements A (P: A → Prop) (s: sequence_of A) :=
∃ (sub: normal_subsequence), ∀ n, P (s (sub n)).
Theorem finite_and_infinite A (P: A → Prop) (s: sequence_of A):
finite_elements P s ↔ ¬ infinite_elements P s.
Proof.
Admitted.
Theorem finite_or_infinite A (P: A → Prop) (s: sequence_of A):
{ finite_elements P s } + { infinite_elements P s }.
Proof.
destruct (classic_sumbool (finite_elements P s)); auto.
right. rewrite finite_and_infinite in n. tauto.
Qed.
Definition sequence_bounded (s: sequence) := ∃ m M, ∀ i, m <= s i <= M.
Definition construction (s: sequence) (H: sequence_bounded s): nested_segments.
Proof.
unfold sequence_bounded in *. apply constructive_indefinite_description in H.
destruct H as [m H]. apply constructive_indefinite_description in H.
destruct H as [M H].
transparent assert (id: normal_subsequence). Unshelve.
2:{ exists (λ i, i). intro. abstract lia. }
assert (infinite_elements (λ n, m <= s n <= M) (λ i, i)).
{ simpl. unfold infinite_elements. exists id. exact H. }
transparent assert (ns: (nat → Rle_pair)). Unshelve.
2:{ intro n.
assert (m <= M). { pose (H O). abstract lra. }
revert s m M H H0 H1. induction n.
+ intros. exists (m, M). simpl. auto.
+ intros. destruct (finite_or_infinite (λ n, m <= s n <= (m + M) / 2) (λ i, i)),
(finite_or_infinite (λ n, (m + M) / 2 <= s n <= M) (λ i, i)).
- exfalso. unfold finite_elements in *. destruct f as [L1 H2], f0 as [L2 H3].
assert (finite_elements (λ n, m <= s n <= M) (λ i, i)).
{ exists (app L1 L2). intros. assert (m <= s n0 <= (m + M) / 2 ∨ (m + M) / 2 <= s n0 <= M) by abstract lra.
apply List.in_or_app. destruct H5; [left|right]; eauto. }
rewrite finite_and_infinite in H4. eauto.
- exists ((m + M) / 2, M). simpl. abstract lra.
- exists (m, (m + M) / 2). simpl. abstract lra.
- exists (m, (m + M) / 2). simpl. abstract lra. }
exists ns. intros ? ? ?. unfold ns in *. simpl in *.
destruct (finite_or_infinite (λ n, m <= s n <= (m + M) / 2) (λ i, i)),
(finite_or_infinite (λ n, (m + M) / 2 <= s n <= M) (λ i, i)).
+ exfalso. assert (finite_elements (λ n, m <= s n <= M) (λ i, i)).
{ destruct f as [L1 H3], f0 as [L2 H4]. exists (app L1 L2). intros.
assert (m <= s n <= (m + M) / 2 ∨ (m + M) / 2 <= s n <= M) by lra.
apply List.in_or_app. destruct H5; [left|right]; eauto. }
apply finite_and_infinite in H2. eauto.
+ unfold segment in H1. simpl in *.
Admitted.
It is unclear what you want to achieve. Since your definition contains axioms, it will not be executable. So it doesn't matter that much what specific nested_segemnts you construct, since you anyway can't compute it. You can prove that there exists a nested_sequence by using the trivial nested sequence where all segments match the bounds you have as hypothesis, but this would except for the bounds be entirely unrelated to your sequence s.
It might be possible to make some partial use of your specific definition by unfolding it just to the axioms, but this won't be very practical. It would make more sense to define what specific properties your nested_segments shall have, e.g. how it is connected to your sequence s, and then prove that a nested_sequence with this property exists.
Lessness (Apr 08 2021 at 17:09):Thank you!
It would make more sense to define what specific properties your nested_segments shall have, e.g. how it is connected to your sequence s, and then prove that a nested_sequence with this property exists.
Yes, that makes much more sense than me using axioms etc.
One problem I have is that I need to prove that specific nested segment sequence exists (with given properties, "exists (ns: nested_segments), ..."). As nested segments are based on function nat -> Rle_pair which is defined recursively (in the proof of Bolzano-Weierstrass theorem), I see no other way than to construct this function. (By "intro; induction n; etc.")
But it seems that I can't make the use of hypotheses in the form "exists x, ..." because they can't be destructed when 'proving' goal of Rle_pair (for the given natural number). That's the reason why I'm stuck now.
Jasper Hugunin (Apr 08 2021 at 17:31):When you want to prove that something exists with certain properties, and you may want to use that thing later to define a piece of data (not just say that it exists), you probably want to use {x | P x} instead of exists x, P x. That says "I have an x with these properties, and here it is", while exists x, P x says something more like "An x exists, but I don't care at all what it is." The two are very similar, but the first lets you get x out to define data.
Lessness (Apr 11 2021 at 12:28):Thank you! :)
That and fixing some other newbie errors helped.
Last updated: Oct 04 2023 at 19:01 UTC