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`

.

looks like you need axiom of choice

Yes, I start to believe so too. I will use `ConstructiveIndefiniteDescription`

axiom, then.

Finite choice is not an axiom though. You should be able to prove that by induction on `n`

.

Why finite choice? `nat`

isn't finite type, is it?

I'm misunderstanding something, probably.

possibly because there are finitely many `i`

s less than `S n`

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)`

and since the goal is in `Prop`

, it seems you can destruct the `ex`

fine.

but I haven’t tried, so I’m probably missing something

Paolo Giarrusso - yes, that approach worked very well. Although such approach seems a bit weird, it still gets results. :)

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`

.

Can you first turn your Coq proof into words?

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.

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.

however, this often requires some creativity :-)

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.

so apologies for the shallow and generic advice; I have no time to think it through...

"use the Feynman problem-solving algorithm" :wink:

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 said:

it's not possible to make it even more "human-like"

Maybe I'm wrong... I will try that finite choice.

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. :)

Thank you all!

Lessness has marked this topic as resolved.

@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.

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`

.

especially if that step avoids using `H0`

— there’s at least no visible use.

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: Jan 29 2023 at 05:03 UTC