## Stream: Coq users

### Topic: Do i need to use some kind of AOC (axiom of choice) here?

#### Lessness (Apr 03 2021 at 19:28):

I'm trying to prove the theorem `finite_and_infinite`. Do I need to use some kind of axiom of choice (for example, the `constructive_indefinite_description` from https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.IndefiniteDescription.html)?

Also, if someone can help me with proving the theorem, I would be very thankful. :)

``````Require Import Classical List Lia.

Definition sequence_of A := nat -> A.
Definition normal_subsequence := { sub: nat -> nat | forall i, sub i < sub (S i) }.
Definition normal_subsequence_of A (s: sequence_of A) (sub: normal_subsequence): sequence_of A :=
fun n => s (proj1_sig sub n).

Definition finite_elements A (P: A -> Prop) (s: sequence_of A) :=
exists (L: list nat), forall n, P (s n) -> In n L.

Definition infinite_elements A (P: A -> Prop) (s: sequence_of A) :=
exists (sub: normal_subsequence), forall n, P (s (proj1_sig sub n)).

Theorem nats_not_in_the_list (L: list nat): exists n, forall i, (n < i)%nat -> List.In i L -> False.
Proof.
pose (proj1 (List.list_max_le L (List.list_max L)) (le_n _)).
rewrite List.Forall_forall in f.
exists (List.list_max L). intros.
apply f in H0. lia.
Qed.

Theorem finite_and_infinite A (P: A -> Prop) (s: sequence_of A):
finite_elements A P s <-> ~ infinite_elements A P s.
Proof.
split; intros.
+ intro. unfold finite_elements, infinite_elements in *.
destruct H as [L H]. destruct H0 as [sub H0].
destruct (nats_not_in_the_list L).
assert (forall i, i <= proj1_sig sub i)%nat.
{ intros. induction i. lia. destruct sub. simpl in *. pose (l i). lia. }
unfold normal_subsequence_of in H0.
assert (forall n, List.In (proj1_sig sub n) L).
{ intros. apply H. eauto. }
pose (H1 (proj1_sig sub (S x))). apply f.
- pose (H2 (S x)). lia.
- eauto.
``````

#### Lessness (Apr 03 2021 at 20:08):

Yess!! I did it. Using the axiom `constructive_indefinite_description`.

``````Tactic Notation "transparent" "assert" "(" ident(H) ":" open_constr(type) ")" :=
refine (let H := (_ : type) in _).

Theorem finite_and_infinite A (P: A -> Prop) (s: sequence_of A):
finite_elements A P s <-> ~ infinite_elements A P s.
Proof.
split; intros.
+ intro. unfold finite_elements, infinite_elements in *.
destruct H as [L H]. destruct H0 as [sub H0].
destruct (nats_not_in_the_list L).
assert (forall i, i <= proj1_sig sub i)%nat.
{ intros. induction i. lia. destruct sub. simpl in *. pose (l i). lia. }
unfold normal_subsequence_of in H0.
assert (forall n, List.In (proj1_sig sub n) L).
{ intros. apply H. eauto. }
pose (H1 (proj1_sig sub (S x))). apply f.
- pose (H2 (S x)). lia.
- eauto.
+ unfold finite_elements, infinite_elements in *. simpl.
assert (~ (forall L: list nat, exists n: nat, P (s n) /\ ~ In n L)).
{ intro. apply H. clear H. apply functional_choice in H0. destruct H0 as [f H0].
transparent assert (function: (nat -> nat)). Unshelve.
2: { intro n. induction n.
+ exact (f nil).
+ exact (f (seq 0 (S IHn))). }
transparent assert (sub: normal_subsequence). Unshelve.
2: { exists function. intros. induction i.
+ abstract (destruct (H0 (seq 0 (S (f nil)))) as [H1 H2]; rewrite in_seq in H2; simpl in *; lia).
+ abstract (destruct (H0 (seq 0 (S (f (seq O (S (function i))))))) as [H1 H2];
rewrite in_seq in H2; simpl in *; lia). }
exists sub. intro. unfold sub. simpl. destruct n.
+ simpl. apply H0.
+ simpl. apply H0. }
apply not_all_not_ex. intro. apply H0. intros. apply not_all_not_ex. intro. apply (H1 L).
intro. pose proof (H2 n). tauto.
Qed.
``````

Last updated: Jan 28 2023 at 06:30 UTC