Lessness (Oct 26 2021 at 18:54): Lessness (Oct 26 2021 at 18:54):How should I approach in such situation? Big thanks for any hints.
1 subgoal
n : nat
s : sequence (R ^ S n)
a : extendedR ^ S n
eps : epsilon
H0 : ∀ (i : nat) (H : (i < S n)%nat), ∃ n0 : nat, ∀ n1 : nat, (n1 > n0)%nat → extendedR_neighbourhood (element a H) eps (element (s n1) H)
______________________________________(1/1)
∃ n0 : nat, ∀ n1 : nat, (n1 > n0)%nat → ∀ (i : nat) (H : (i < S n)%nat), extendedR_neighbourhood (element a H) eps (element (s n1) H)
As far as I can see, I should somehow collect all corresponding natural numbers for each i that's less than S n and calculate max of them all. But that seems not possible because H0 contains ex, not a sig.
Gaëtan Gilbert (Oct 26 2021 at 19:48):looks like you need axiom of choice
Lessness (Oct 26 2021 at 19:50):Yes, I start to believe so too. I will use ConstructiveIndefiniteDescription axiom, then.
Pierre-Marie Pédrot (Oct 26 2021 at 19:55):Finite choice is not an axiom though. You should be able to prove that by induction on n.
Lessness (Oct 26 2021 at 20:54):Why finite choice? nat isn't finite type, is it?
I'm misunderstanding something, probably.
Paolo Giarrusso (Oct 26 2021 at 20:59):possibly because there are finitely many is less than S n
Paolo Giarrusso (Oct 26 2021 at 21:01):so if n is 0, the max is 0, and in the inductive case, you can pick the max of the n from the induction hypothesis and that from H0 n ltac:(lia)
Paolo Giarrusso (Oct 26 2021 at 21:02):and since the goal is in Prop, it seems you can destruct the ex fine.
Paolo Giarrusso (Oct 26 2021 at 21:02):but I haven’t tried, so I’m probably missing something
Lessness (Oct 26 2021 at 22:13):Paolo Giarrusso - yes, that approach worked very well. Although such approach seems a bit weird, it still gets results. :)
Lessness (Nov 24 2021 at 19:59):Is there a "human way" to prove this helper lemma? Like, calculating max of all corresponding nats or smth.
I managed to prove it using induction on n, but it's a bit unsatisfying in some way (although still nice)... as I want to reproduce "human" proof.
Theorem sequence_limit_element_limits_aux {n} (P: ∀ i (H: (i < S n)%nat) (k: nat), Prop)
(H0: ∀ i (H: (i < S n)%nat) k1 k2, (k1 <= k2)%nat → P i H k1 → P i H k2):
(∀ i (H: (i < S n)%nat), ∃ m, P i H m) →
(∃ m, ∀ i (H: (i < S n)%nat), P i H m).
Proof.
induction n.
+ intros. destruct (H _ (le_n 1)) as [m H1]. exists m. intros. assert (i = 0)%nat by lia. subst.
replace (le_n 1) with H2 in H1 by (apply ProofIrrelevance). auto.
+ intros. pose (λ i (H: (i < S n)%nat) k, P i (le_S _ _ H) k) as P'.
pose proof (IHn P').
assert (∀ i (H: (i < S n)%nat) k1 k2, (k1 <= k2)%nat → P' i H k1 → P' i H k2).
{ unfold P'. intros. apply (H0 _ (le_S _ _ H2) _ _ H3 H4). }
pose proof (H1 H2).
assert (∀ i (H: (i < S n)%nat), ∃ m, P' i H m).
{ intros. apply (H _ (le_S _ _ H4)). }
pose proof (H3 H4).
destruct H5 as [N1 H5]. destruct (H _ (le_n (S (S n)))) as [N2 H6].
clear H. exists (max N1 N2). intros.
inversion H; subst.
- pose proof (H0 _ H). eapply H7. assert (N2 <= max N1 N2)%nat by lia. eauto.
replace (le_n _) with H in H6 by apply ProofIrrelevance. auto.
- pose proof (H0 _ H). eapply H7. assert (N1 <= max N1 N2)%nat by lia. eauto.
pose proof (H5 _ H8). unfold P' in H9.
replace (le_S _ _ _) with H in H9 by apply ProofIrrelevance. auto.
Qed.
Any hints how to make "human" proof of theorem sequence_limit_element_limits_aux?
Something like this:
1) prove that there exists (L: list nat), some_property L. Still thinking about this part...
2) prove that list_max L satisfies property forall i (H: i < S n), P i H m.
Paolo Giarrusso (Nov 27 2021 at 14:49):Can you first turn your Coq proof into words?
Lessness (Nov 27 2021 at 15:04):It goes something like this:
1) collect all numbers less than S n in list;
2) make another list of corresponding numbers (taken from forall i H, exists m, P i H m), name it L;
3) calculate max element of list L, name it M;
4) forall i < S n, the corresponding number from L is less or equal than M, therefore for all of them P i H M.
Probably it's possible to make it using some axiom of choice, but I want to make the proof without it and still make the proof "human"-ish as much as possible.
Paolo Giarrusso (Nov 27 2021 at 15:51):I’m not sure what “humanish” means (except that humans don’t use H6 as a name), but a general strategy I’d say try to isolate steps into a reusable building block… for instance, Pierre-Marie suggested finite choice as a potential lemma to use.
Paolo Giarrusso (Nov 27 2021 at 15:51):however, this often requires some creativity :-)
Paolo Giarrusso (Nov 27 2021 at 16:09):By which I mean, I can't think of any other block that can be extracted, and I'm not even sure how exactly to use finite choice.
Paolo Giarrusso (Nov 27 2021 at 16:10):so apologies for the shallow and generic advice; I have no time to think it through...
Karl Palmskog (Nov 27 2021 at 16:12):"use the Feynman problem-solving algorithm" :wink:
Lessness (Nov 27 2021 at 16:12):I managed to make the proof I wanted (there exists a list and we take list_max of it) and believe that it's not possible to make it even more "human-like" (as I understand it, sorry for bad explaining of the idea).
Theorem sequence_limit_element_limits_aux' {n} (P: ∀ i (H: (i < S n)%nat) (k: nat), Prop)
(H0: ∀ i (H: (i < S n)%nat) k1 k2, (k1 <= k2)%nat → P i H k1 → P i H k2):
(∀ i (H: (i < S n)%nat), ∃ m, P i H m) →
(∃ m, ∀ i (H: (i < S n)%nat), P i H m).
Proof.
intros.
assert (∃ L, (∀ i (H: (i < S n)%nat), ∃ x, In x L ∧ P i H x)).
{ induction n.
+ assert (0 < 1)%nat by apply le_n. destruct (H _ H1) as [m H2].
exists (m :: nil). intros. exists m. intuition.
inversion H3.
- subst. replace H3 with H1 by apply ProofIrrelevance. auto.
- inversion H5.
+ pose (λ i (H: (i < S n)%nat) m, P i (le_S _ _ H) m) as P'.
assert (∀ (i : nat) (H : (i < S n)%nat) (k1 k2 : nat), k1 ≤ k2 → P' i H k1 → P' i H k2).
{ intros. unfold P' in *. eapply H0. exact H2. auto. }
assert (∀ (i : nat) (H : (i < S n)%nat), ∃ m : nat, P' i H m).
{ intros. destruct (H _ (le_S _ _ H2)) as [m H3]. exists m. auto. }
destruct (IHn P' H1 H2) as [L H3]. unfold P' in H3.
destruct (H _ (le_n _)) as [m H4].
exists (L ++ m :: nil). intros. inversion H5.
- subst. exists m. intuition. replace (le_n _) with H5 in H4 by apply ProofIrrelevance. auto.
- clear H6. destruct (H3 _ H7) as [x [H8 H9]].
exists x. intuition. replace (le_S _ _ _) with H5 in H9 by apply ProofIrrelevance. auto. }
destruct H1 as [L H1]. exists (list_max L). intros. destruct (H1 _ H2) as [x [H3 H4]].
assert (x <= list_max L)%nat.
{ Search list_max. pose proof (proj1 (list_max_le L (list_max L)) (le_n (list_max L))).
rewrite Forall_forall in H5. eauto. }
eauto.
Qed.
Apologies for posting in the wrong thread... :cold_sweat:
Lessness (Nov 27 2021 at 16:34):Lessness said:
it's not possible to make it even more "human-like"
Maybe I'm wrong... I will try that finite choice.
Lessness (Nov 27 2021 at 17:37):I believe finite choice shouldn't be working here, because of ∀ i (H: (i < S n)%nat), ∃ m, P i H m) which is about existence of nat (which is not finite), not fin.
Anyway, I changed my mind a bit and will use IndefiniteDescription axiom, to get proof that's maximally similar to human proof. Even if it is not necessary. And proofs without this choice axiom will stay as nice memories and gained experience. :)
Lessness (Nov 27 2021 at 17:37):Thank you all!
Notification Bot (Nov 27 2021 at 17:38):Lessness has marked this topic as resolved.
Paolo Giarrusso (Nov 27 2021 at 17:45):@Lessness AFAICT, the “finite” in “finite choice” doesn’t care about the type of what exists, but about how long the search is — and the domain for i is finite here.
Paolo Giarrusso (Nov 27 2021 at 17:49):since fin n ~= { i | i < n }, it seems the axiom of finite choice is almost equivalent to the step you’re carrying out in your first assert.
Paolo Giarrusso (Nov 27 2021 at 17:51):especially if that step avoids using H0 — there’s at least no visible use.
Paolo Giarrusso (Nov 27 2021 at 17:54):with some massaging, that step is basically going from \forall (i : Fin (S n), \exists m : nat, Q i m to \exists mf : Fin (S n) -> nat, \forall (i : Fin (S n)), Q i (mf i)`; this \forall / \exists swap _is_ a constructively provable version of the axiom of choice.
Last updated: Oct 13 2024 at 01:02 UTC