Non-constructive proof

Using Rocq
1

Dear Rocq users,

I’m currently struggling with a proof involving non-constructive reasoning. Without further ado, here is the lemma I’m trying to prove:

Lemma functional_list_choice {A} : forall (R: A -> A -> Prop) (f_list : nat -> list A),
    (forall k, f_list k <> []) ->
    (forall k v2, In v2 (f_list (S k)) -> exists v1, In v1 (f_list k) /\ R v1 v2) ->
    exists f, In (f 0) (f_list 0) /\ forall k, R (f k) (f (S k)).

This lemma essentially talks about an indexed function f_list : nat -> list A along with a relation R between elements A. The hypotheses essentially say that (1) f_list is never empty and (2) any element in f_list (S k) is in relation with a “predecessor” in f_list k. In other words, for any k, there exists a chain of elements of f_list 0, …, f_list k which respect the relation R.
What we want to prove is that there exists an infinite sequence, f, where each element f k is in f_list k, and in relation with f (S k). In other words, f is an infinite “chain” of values of A that satisfy R.

Intuitively, this chain should exist, because if it does not, it means that at some point there is either no element in f_list k (which violates the first hypothesis), or all elements in f_list k have no predecessor (which violates the second). However, I believe that there should not be a way of proving this lemma constructively: indeed, to do so, we would need to exhibit a function f which “chooses” the right sequence; however, this choice depends on looking arbitrarily far into higher indexes, and so we would not be able to prove that such a function terminates.

Therefore, what I’d like to determine is what non-constructive axiom(s) from Rocq’s standard library I need to prove this lemma, and how to apply them. I hope someone more experienced than me with non-constructive reasoning will be able to point me in the right direction. In any case, thank you for your attention :slight_smile:

Best regards,
Basile Pesin

1 Like
2

Not an expert, but this looks somewhat related to the axiom of countable choice Axiom of countable choice - Wikipedia (or some other form of the axiom of choice).

3

Following up on @Alix’s suggestion, I have modified the statement, still I cannot get to the bottom of a proof, since, AFAICT, there is nothing we can do with that fixed v1 from the existential in condition (2). Indeed, naively, referring to those conditions on f_list, I’d be tempted to say “that is not how inductive definitions work”… But I am in fact not sure what exactly you are trying to define then prove.

From Coq Require Import List.

Import ListNotations.

Lemma functional_list_choice {A} :
  forall (R : A -> A -> Prop) (f_list : nat -> list A),
    (exists f, forall k, In (f k) (f_list k)) ->  (** choice *)
    (forall k, f_list k <> []) ->
    (forall k v2, In v2 (f_list (S k)) ->
      exists v1, In v1 (f_list k) /\ R v1 v2) ->
    exists f, forall k, R (f k) (f (S k)).
Proof.
  intros R f_list [f Hf] HN HS.
  exists f; intros k.
  specialize (Hf (S k)).
  specialize (HS k (f (S k)) Hf).  (** [v1]! *)
  destruct HS as [v1 [H1 H2]].
  give_up.
Abort.
5

Hmm, not 100% sure if this works, but assuming axiom of choice and excluded middle, I sketched this out in my head.

First prove this, which is constructive.

Lemma functional_list_choice_aux {A} : forall (R: A -> A -> Prop) (f_list : nat -> list A),
    (forall k, f_list k <> []) ->
    (forall k v2, In v2 (f_list (S k)) -> exists v1, In v1 (f_list k) /\ R v1 v2) ->
    forall n, exists f, In (f 0) (f_list 0) /\ forall k, k < n -> R (f k) (f (S k)).

Therefore, by countable choice Rocq Standard Library there exists g such that for all n, such that In (g n 0) (f_list 0) /\ forall k, k < n -> R (g n k) (g n (S k)).

We know that for all n, g n 0 is an element of f_list 0. Therefore, there exists an element of f_list 0 that appears an infinite number of time in the sequence g 0 0, …, g n 0, …

Use excluded middle on P := exists x, forall k, exists n, n > k /\ g n 0 = x to prove and conclude.

6

I went along something that looks a little like what Alix is suggesting I think, using FunctionalDependentChoice_on, but it leads to having to find a R-successor above us. And naively reversing the direction in the relation we feed to the axiom is non-sensical.

From Stdlib Require Import List ClassicalFacts ChoiceFacts Program.Equality RelationClasses.

Import ListNotations.

Axiom (DC : forall A, FunctionalDependentChoice_on A).

Lemma functional_list_choice {A} : forall (R: A -> A -> Prop) (f_list : nat -> list A),
    (forall k, f_list k <> []) ->
    (forall k v2, In v2 (f_list (S k)) -> exists v1, In v1 (f_list k) /\ R v1 v2) ->
    exists f, In (f 0) (f_list 0) /\ forall k, R (f k) (f (S k)).
Proof.
  intros * NE PRED.

  (* We are going to work over elements of a whose level is identified *)
  set (X := {n : nat & {a : A & In a (f_list n)}}).
 
  (* We need the initial point *)
  destruct (f_list 0) as [| a0 ?] eqn:eq; [now apply NE in eq | assert (IN0: In a0 (f_list 0)) by (rewrite eq; now left); clear eq].
  pose (existT _ 0 (existT _ a0 IN0): X) as x0.

  pose proof (DC X (fun '(existT _ n (existT _ a _)) '(existT _ m (existT _ b _)) => m = S n /\ R a b)).
  unshelve edestruct H as [f [EQ Hf]].
  (* Our starting point, we already constructed it *)
  - exact x0.
  (* All elements of X have somebody related by R.
    Alas! We need to pick somebody *above* us, and there isn't such a candidate alwas! *)
  - intros [n [a INa]].
    specialize (PRED (S n)).
    admit.
  (* But if we could, it would work! *)
  - exists (fun k => projT1 (projT2 (f k))).
    split.
    + destruct (f 0) as [n [x IN]].
      subst x0; cbn in *.
      dependent induction EQ; left; reflexivity.
    + intros k.
      specialize (Hf k).
      destruct (f k) as [k' [ak INk]], (f (S k)) as [k''' [ak' INk']]; apply Hf.
Admitted.

So I felt like the goal would be to first work on proving that there is an infinite ascending R-chain, i.e., something like:

Section WithParam.

  Axiom (DC : forall A, FunctionalDependentChoice_on A).
  Axiom (EM : excluded_middle).
  Variable A : Type.
  Variable R : A -> A -> Prop.
  Variable f_list : nat -> list A.

  CoInductive upward_chain_R : nat -> A -> Prop :=
  | going_up n a b (INn : In b (f_list (S n))) (HR : R a b) (Hrec : upward_chain_R (S n) b) : upward_chain_R n a.

  Lemma reverse_the_graph :
    (forall k v2, In v2 (f_list (S k)) -> exists v1, In v1 (f_list k) /\ R v1 v2) ->
    (exists a, In a (f_list 0) /\ upward_chain_R 0 a).
 Proof.
(* Something something classically by absurd??? Intuitively, if it's False, then each element at level 0 has only a finite upward chain. But starting from any height, we can build by induction a downward chain all the way to 0. Hence if we pick their max + 1, we have a contradiction *)
 Admitted

And if we managed to have that, we should be able to add this predicate to our type X to carefully guide our axiom of choice to precisely pick this chain rather than randomly.

But it also vaguely feel like the whole difficulty of what you want to prove is in this auxiliary lemma that exhibit that there exists the infinite chain of interest (by Koenig lemma, as pointed out by a colleague).

EDIT: I’m very interested in the solution though now, it’s one of these problem that made me feel stupid trying and failing at it, I feel invested now!

1 Like
7

Thank you for the proposition ! I did try a really similar approach using countable choice. Unfortunately where I get stuck is that there is no guarantee that g n1 k and g n2 k correspond for two different n1 and n2. I am not sure if I understand if your last two paragraphs solve this issue ?

8

Thank you for your interest ! I tried something similar. One issue is that what you would like to do is build the upward chain by coinduction, but you cannot since the conclusion is of the form exists ..., which is inductive. Also I am not sure how I would extract the nat -> A function from the upward chain.

9

So for the latter, my reasoning is: if we can exhibit an a0 at level 0 that satisfies this coinductive predicate, then the aborted attempt that I posted just above should work by taking X roughly to be {n : nat & { a : A & In a (f_list n) /\ reachable_from a0 n} as the coinductive predicate tells us how to pick the element above us and related by R (where reachable_from is the inductive that you imagine that moves level one by one through R).

As to how to prove the coinductive predicate, then indeed I do not suggest to prove it by coinduction, but rather by the absurd as sketched in my previous message. The first thing would be to prove that if an element is not in the predicate, then there’s a bound such that any R upward-chain starting from it is of length at most this bound, then showing that for any bound, we can create one by starting from this level and going downward, and hence concluding by taking the max of the bounds for all elements in the level 0. But that’s all speculative of course, I haven’t tried.

10

My first remark would be that finiteness (enforced by using lists) is critical in the proof. Indeed, if you replace non empty lists with non empty predicates then the result is actually false:

Require Import List Arith Lia.

Import ListNotations.

Section finite_is_critical.

  Hypothesis functional_choice_not_finite : forall A (R: A -> A -> Prop) (P : nat -> A -> Prop),
    (forall k, exists a, P k a) ->
    (forall k v2, P (S k) v2 -> exists v1, P k v1 /\ R v1 v2) ->
    exists f, P 0 (f 0) /\ forall k, R (f k) (f (S k)).

  Theorem absurd_functional_choice_not_finite : False.
  Proof.
    destruct (functional_choice_not_finite nat (fun x y => x = S y) (fun _ _ => True))
      as (f & H1 & H2); eauto.
    assert (forall n, f n = f 0 - n) as Hf.
    + intros n; induction n as [ | n IHn ].
      * lia.
      * rewrite H2 in IHn; lia.
    + generalize (H2 (f 0)).
      rewrite Hf; lia.
  Qed.

End finite_is_critical.

Hence this makes me think about König’s lemma to establish the proof: Every finitely branching tree which is infinite has an infinite branch. Notice that this is non-constructive form of König’s lemma, but the contrapositive form, called the FAN theorem, can be constructivelly established under some mild assumptions.

I will investigate this a bit more.

11

Here’s what might be a (overly classical?) proof sketch:

Let S (k, a) (k', b) be R a b /\ In a (f_list k) /\ In b (f_list k') /\ k' = S k.

Let P x be the proposition “the set of y such that x~S^*~y is infinite”.

For any given k, at least one a exists such that P(k,a). Indeed otherwise there is a maximum k' such that (k,a)~S^*~(k',b). Then we can use (1) to get some (k'+1,b') to which we can repeatedly apply (2) to come back to some (k,a'), contradiction.

For any x\in P there exists only finitely many successors through S, so there exists at least one y\in P such that x~S~y.

On this sig P, we can apply FunctionalDependentChoice to conclude, it seems.

12

The best I can do is to prove your lemma with the axioms of excluded middle (XM) and König’s lemma (KL) in the following forms:

Require Import List Arith Lia.

Import ListNotations.

Inductive rel_seq {X} (R : X -> X -> Prop) : list X -> Prop :=
  | seq_zero : rel_seq R []
  | seq_one x : rel_seq R [x]
  | seq_more l x y : R x y -> rel_seq R (l++[x]) -> rel_seq R (l++[x;y]).

Definition finite {X} (P : X -> Prop) := exists l, forall x, P x <-> In x l.

Axiom Konigs_lemma : 
    forall X (R : X -> X -> Prop) (HR : forall x, finite (R x)) (x : X),
       (forall n, exists l, rel_seq R (x::l) /\ n <= length l)
    -> (exists f, f 0 = x /\ forall n, R (f n) (f (S n))).

Axiom xm : forall A : Prop, A \/ ~ A.

(** a good amount of interesting proofs *)

Check functional_list_choice.
Print Assumptions functional_list_choice.

(** outputs

functional_list_choice
     : forall (A : Type) (R : A -> A -> Prop) (f_list : nat -> list A),
       (forall k : nat, f_list k <> []) ->
       (forall (k : nat) (v2 : A),
        In v2 (f_list (S k)) -> exists v1 : A, In v1 (f_list k) /\ R v1 v2) ->
       exists f : nat -> A,
         In (f 0) (f_list 0) /\ (forall k : nat, R (f k) (f (S k)))
Axioms: xm, Konigs_lemma 

*)

König’s lemma (KL) states that if a relation R is finitely branching and, starting from x, has R-sequences of unbounded size, then there is a nat-indexed R-sequence starting from x.

Assuming X can be totally sorted you only need XM and unique choice to prove KL, otherwise dependent choice is also required to establish KL.

[EDIT] I needed to edit that post because I am new user, limited to 3 replies, but here is a complete proof assuming XM and KL:

Require Import List Arith Lia.

Import ListNotations.

Fact list_snoc2_eq X l (x y : X) : l++[x;y] = (l++[x])++[y].
Proof. now rewrite <- app_assoc. Qed.

Inductive rel_seq {X} (R : X -> X -> Prop) : list X -> Prop :=
  | seq_zero : rel_seq R []
  | seq_one x : rel_seq R [x]
  | seq_more l x y : R x y -> rel_seq R (l++[x]) -> rel_seq R (l++[x;y]).

Local Fact rel_seq_inv_rec X R l :
     @rel_seq X R l 
  -> forall m x y, l = m++[x;y] -> R x y /\ rel_seq R (m++[x]).
Proof.
  destruct 1.
  + now intros [].
  + now intros [ | ? [] ].
  + intros m u v.
    rewrite !list_snoc2_eq.
    intros ([]%app_inj_tail & ?)%app_inj_tail; now subst m u v.
Qed.

Fact rel_seq_inv X R l x y :
   @rel_seq X R (l++[x;y]) <-> R x y /\ rel_seq R (l++[x]).
Proof.
  split.
  + intros H; now apply rel_seq_inv_rec with (1 := H).
  + intros []; now constructor 3.
Qed.

Inductive choice_seq {X} (P : nat -> X -> Prop) : list X -> Prop :=
  | choice_seq_nil : choice_seq P []
  | choice_seq_cons x l : P (length l) x -> choice_seq P l -> choice_seq P (l++[x]).

Local Fact choice_seq_inv_rec X P l :
     @choice_seq X P l
  -> forall m x, l = m++[x] -> P (length m) x /\ choice_seq P m.
Proof.
  destruct 1.
  + now intros [].
  + intros m y (<- & <-)%app_inj_tail; auto.
Qed.

Fact choice_seq_inv X P l x :
  @choice_seq X P (l++[x]) <-> P (length l) x /\ choice_seq P l.
Proof.
  split.
  + intros H; now apply choice_seq_inv_rec with (1 := H).
  + intros []; now constructor.
Qed.

Section list_prod.

  Variables (X Y Z : Type) (f : X -> Y -> Z).

  Definition list_prod l m := flat_map (fun x => map (f x) m) l.

  Fact list_prod_spec l m c : In c (list_prod l m) <-> exists x y, c = f x y /\ In x l /\ In y m.
  Proof.
    unfold list_prod.
    rewrite in_flat_map; split.
    + intros (? & ? & (? & [])%in_map_iff); eauto.
    + intros (x & ? & -> & []).
      exists x; split; auto.
      apply in_map_iff; eauto.
  Qed.

End list_prod.

Arguments list_prod {_ _ _}.

Definition finite {X} (P : X -> Prop) := exists l, forall x, P x <-> In x l.

Axiom XM : forall A : Prop, A \/ ~ A. 

(** Notice that this critically depends on xm, or at least P being (weakly) decidable *)
Fact finite_anti__XM X P Q : (forall x : X, P x -> Q x) -> finite Q -> finite P.
Proof.
  intros HPQ (l & Hl).
  cut (forall x, P x -> In x l).
  2: intros ? ?; now apply Hl, HPQ.
  clear Q HPQ Hl.
  induction l as [ | x l IHl ] in P |- *; intros HP.
  + exists []; split; simpl.
    * now intros H%HP.
    * easy.
  + destruct (XM (P x)) as [ Hx | Hx ].
    * destruct (IHl (fun y => P y /\ In y l)) as (m & Hm).
      - tauto.
      - exists (x::m).
        intros; simpl; rewrite <- Hm; split.
        ++ intros H; destruct (HP _ H) as [ <- | ]; auto.
        ++ intros [ <- | [] ]; auto. 
    * apply IHl.
      intros y Hy.
      destruct (HP _ Hy) as [ -> | ]; now auto.
Qed.

Axiom Konigs_lemma : 
    forall X (R : X -> X -> Prop) (HR : forall x, finite (R x)) (x : X),
       (forall n, exists l, rel_seq R (x::l) /\ n <= length l)
    -> (exists f, f 0 = x /\ forall n, R (f n) (f (S n))).

Section functional_list_choice.

  Variables (A : Type) (R: A -> A -> Prop) (f_list : nat -> list A)
            (f0 : forall k, f_list k <> [])
            (f1 : forall k v2, In v2 (f_list (S k)) -> exists v1, In v1 (f_list k) /\ R v1 v2).

  Let P n x := In x (f_list n).

  Local Fact unbounded n x : P n x -> exists l, rel_seq R (l++[x]) /\ choice_seq P (l++[x]) /\ length l = n.
  Proof.
    induction n as [ | n IHn ] in x |- *.
    + exists []; repeat split; auto. 
      * constructor 2.
      * constructor; simpl; auto; constructor.
    + intros G0.
      destruct f1 with (1 := G0) as (y & (l & H1 & H2 & H3)%IHn & H4).
      exists (l++[y]); repeat split; auto.
      * rewrite <- app_assoc; simpl.
        now constructor.
      * constructor; auto.
        rewrite length_app, H3; simpl.
        replace (n+1) with (S n); auto; lia.
      * rewrite length_app; simpl; lia.
  Qed.

  Let T (x y : option (nat * A)) :=
    match x, y with
    | None, Some (i,y)       => i = 0 /\ In y (f_list 0)
    | Some (i,x), Some (j,y) => j = S i /\ In x (f_list i) /\ In y (f_list j) /\ R x y
    | _, _ => False
    end.

  Local Fact T_fin x : finite (T x).
  Proof.
    destruct x as [ (i,x) | ]; simpl.
    + cut (finite (fun y => match y with | Some (n,y) => n = S i /\ In y (f_list n) | None => False end)).
      * apply finite_anti__XM; intros [ [] | ]; simpl; tauto.
      * exists (list_prod (fun n a => Some (n,a)) [S i] (f_list (S i))).
        intros [ (j,y) | ]; rewrite list_prod_spec; split.
        - intros (-> & ?); exists (S i), y; simpl; auto.
        - intros (? & ? & [=] & [ <- | [] ] & ?); subst; auto.
        - tauto.
        - now intros (? & ? & ? & _).
    + exists (list_prod (fun n a => Some (n,a)) [0] (f_list 0)).
      intros [ (j,y) | ]; rewrite list_prod_spec; split; simpl.
      - intros (-> & ?); exists 0, y; auto.
      - intros (? & ? & [=] & [ <- | [] ] & ?); subst; auto.
      - tauto.
      - now intros (? & ? & ? & _).
  Qed.

  Fixpoint iseq (l : list A) n :=
    match l with
    | []   => []
    | a::l => Some (n,a) :: iseq l (S n)
    end.

  Fact iseq_length l n : length (iseq l n) = length l.
  Proof. induction l in n |- *; simpl; auto. Qed.

  Fact iseq_app l m n : iseq (l++m) n = iseq l n ++ iseq m (length l + n).
  Proof.
    induction l as [ | x l IHl ] in n |- *; simpl; f_equal; auto.
    rewrite IHl; do 2 f_equal; lia.
  Qed.

  Fact iseq_S l x : iseq (l++[x]) 0 = iseq l 0 ++ [Some (length l,x)].
  Proof. rewrite iseq_app; simpl; do 4 f_equal; lia. Qed.

  Fact rel_seq_R__T l : rel_seq R l -> choice_seq P l -> rel_seq T (None::iseq l 0).
  Proof.
    induction 1 as [ | | l x y H1 H2 IH2 ].
    + simpl; constructor.
    + simpl; intros E.
      constructor 3 with (l := []).
      * red; split; auto.
        apply choice_seq_inv with (l := []) in E as (E & _).
        exact E.
      * simpl; constructor.
    + rewrite list_snoc2_eq.
      intros (H3 & H4)%choice_seq_inv.
      rewrite !iseq_S, <- list_snoc2_eq.
      constructor 3 with (l := _::_).
      * repeat split; auto.
        - rewrite length_app; simpl; lia.
        - apply choice_seq_inv in H4.
          apply H4.
      * simpl; rewrite <- iseq_S; auto.
  Qed.

  Local Lemma from_Konig : exists f, f 0 = None /\ forall n, T (f n) (f (S n)).
  Proof.
    apply Konigs_lemma.
    + apply T_fin.
    + intros n.
      specialize (f0 n).
      case_eq (f_list n); [ easy | ].
      intros x m Hm.
      destruct (unbounded n x) as (l & H1 & H2 & H3).
      1: red; rewrite Hm; simpl; auto.
      exists (iseq (l++[x]) 0); split.
      * apply rel_seq_R__T; auto.
      * rewrite iseq_length, length_app, H3; lia.
  Qed.

  Lemma functional_list_choice : exists f, In (f 0) (f_list 0) /\ forall k, R (f k) (f (S k)).
  Proof.
    destruct from_Konig as (f & H1 & H2).
    assert (forall n, { x | f (S n) = Some (n,x)}) as G.
    1:{ intros n; induction n as [ | n (x & Hx) ].
        + generalize (H2 0).
          rewrite H1.
          destruct (f 1) as [ (i,x) | ]; simpl; try easy.
          intros (-> & _); eauto.
        + generalize (H2 (S n)).
          rewrite Hx.
          destruct (f (S (S n))) as [ (i,y) | ]; simpl; try easy.
          intros (-> & _); eauto. }
    exists (fun n => proj1_sig (G n)); split.
    + destruct (G 0) as (x & Hx); simpl.
      generalize (H2 1).
      rewrite Hx.
      destruct (G 1) as (y & ->).
      simpl; tauto.
    + intros n.
      generalize (H2 (S n)).
      destruct (G n) as (x & ->).
      destruct (G (S n)) as (y & ->); simpl; tauto.
  Qed.

End functional_list_choice.

Check functional_list_choice.
Print Assumptions functional_list_choice.
3 Likes
13

The looks like the proof of König’s lemma indeed with “under an infinite sub-tree” as an invariant.

14

Here is an unfinished proof, but it should be feasible to tie the knot.

From Coq Require Import Lists.List Lia PeanoNat.
From Coq Require Import ClassicalFacts ChoiceFacts.
From Coq Require Import Logic.Classical_Pred_Type.

Import ListNotations.

Axiom (FDC : forall A, FunctionalDependentChoice_on A).
Axiom (FCC : forall A, FunctionalCountableChoice_on A).
Axiom (EM: excluded_middle).

Lemma functional_list_choice {A} : forall (R: A -> A -> Prop) (f_list : nat -> list A),
    (forall k, f_list k <> []) ->
    (forall k v2, In v2 (f_list (S k)) -> exists v1, In v1 (f_list k) /\ R v1 v2) ->
    exists f, In (f 0) (f_list 0) /\ forall k, R (f k) (f (S k)).
Proof.
  intros * NE PRED.

  pose proof (NE 1) as NE1.
  destruct (f_list 1) as [|a]; [congruence|clear NE1 l].

  assert (NEk: forall k, In (hd a (f_list k)) (f_list k)).
  { intro k. pose proof (NE k); destruct (f_list k); [congruence|].
    left. reflexivity. }

  assert (G: forall n x, In x (f_list n) -> exists f, f n = x /\ forall k, (k < n)%nat -> In (f k) (f_list k) /\ R (f k) (f (S k))).
  { induction n; intros x Hx.
    - exists (fun k => x). split; [reflexivity|]. intros; lia.
    - pose proof (PRED _ _ Hx) as Hx'.
      destruct Hx' as (v1 & Hv1 & HRv1).
      pose proof (IHn _ Hv1) as Hv1'.
      destruct Hv1' as (f & Hv1' & Hf).
      exists (fun k => if Nat.eq_dec k (S n) then x else f k).
      destruct (Nat.eq_dec _ _) as [_|]; [|congruence].
      split; [reflexivity|]. intros k Hk.
      destruct (Nat.eq_dec k (S n)) as [|_]; [lia|].
      assert (k = n \/ k < n)%nat as [->|Hk'] by lia.
      + destruct (Nat.eq_dec _ _) as [_|]; [|congruence].
        rewrite Hv1'. split; assumption.
      + destruct (Nat.eq_dec _ _) as [|_]; [lia|].
        apply Hf; assumption. }

  destruct (FCC (nat -> A) (fun n f => In (f n) (f_list n) /\ (forall k : nat, k < n -> In (f k) (f_list k) /\ R (f k) (f (S k))))) as (g & Hg).
  { intros n. pose proof (G n _ (NEk n)) as (f & Hf1 & Hf2).
    exists f; split; auto. rewrite Hf1; apply NEk. }

  assert (Hg_in: forall n k, (k <= n)%nat -> In (g n k) (f_list k)).
  { intros. assert (k < n \/ n = k) as [Hlt|<-] by lia.
    - destruct (Hg n) as (_ & Hgn). apply Hgn. assumption.
    - apply (proj1 (Hg n)). }

  destruct (EM (exists x0, forall k, exists n, n > k /\ g n 0 = x0)) as [HEX|HNEX].
  2:{ exfalso.
      assert (HFN: forall (x: A), exists (k: nat), forall (n: nat), (n > k)%nat -> (g n 0 <> x)).
      { pose proof (not_ex_all_not _ _ HNEX) as HA.
        intro x. specialize (HA x). cbn in HA.
        destruct (not_all_ex_not _ _ HA) as [k Hk].
        exists k. pose proof (not_ex_all_not _ _ Hk) as HB.
        intros n. specialize (HB n). cbn in HB.
        apply Classical_Prop.not_and_or in HB.
        tauto. }
      assert (HF': exists k, forall x, In x (f_list 0) -> forall n, n > k -> g n 0 <> x).
      { induction (f_list 0).
        - exists O. intros x Hx. apply in_nil in Hx; elim Hx.
        - destruct (HFN a0) as (k0 & Hk0).
          destruct IHl as (kl & Hkl).
          exists (max k0 kl). intros x Hx n Hn.
          apply in_inv in Hx. destruct Hx as [->|Hx].
          + apply Hk0; lia.
          + apply Hkl; auto; lia. }
      destruct HF' as (k & HF').
      apply (HF' (g (k + 1) 0) (Hg_in (k + 1)%nat 0 ltac:(lia)) (k + 1) ltac:(lia)).
      reflexivity. }
  destruct HEX as (x0 & Hx0).
  destruct (FCC nat (fun n k => n < k /\ g k 0 = x0)) as (idx1 & Hidx1).
  { intro n. destruct (Hx0 n) as (k & ? & ?). exists k; split; auto; lia. }

  (* Basically RR should say that there exists a subsequence of [g] that agrees on its first (length l1) elements. and we can extract a new subsequence that agrees on its first (length l1) + 1 elements *)
  set (RR := fun (l1 l2: list A) => exists xn, l2 = l1 ++ [xn] /\ True).
  assert (exists prefixn, prefixn 0 = [x0] /\ (forall n, RR (prefixn n) (prefixn (S n)))) as (f & Hf0 & HfS).
  { apply FDC. admit. }

  exists (fun n => nth_default a (f n) n). split.
  { rewrite Hf0. cbn.
    destruct (Hx0 0) as (? & (? & <-)).
    apply Hg_in; lia. }
  (* Use HfS to conclude *)

Admitted.

Basically, I proved that there is a subsequence such that forall n : nat, n < idx1 n /\ g (idx1 n) 0 = x0. i.e. they all agree on the first element, you can repeat that reasoning a finite number of times to build a subsequence that agrees on its first n elements, and axiom of choice can conclude. I’m guessing this is kind of like reproving König’s lemma from reading the other answers, though I wasn’t aware of it.

15

Hi ! Thank you very much. This looks great :slight_smile: I need a bit of time to understand and digest the proof. I would also like to be able to prove Konig’s lemma from the axioms you cite (choice and XM), but I will try to do so by myself :slight_smile:

1 Like
16

If I understand correctly, I would need to complete the True in the definition of RR with something that relates l1 and l2 with g ? In that case, I’m a bit worried that the hypothesis of FDC on the next line would not be provable, since it quantifies universally on l1 without any relation with the rest of the context…

17

You are right, a stronger axiom of choice was needed, though here is a complete proof using only excluded middle and some flavours of axiom of choice.

From Coq Require Import Lists.List Lia PeanoNat.
From Coq Require Import ClassicalFacts ChoiceFacts.
From Coq Require Import Logic.Classical_Pred_Type.

Import ListNotations.

Axiom (DFC : DependentFunctionalChoice).
Axiom (FCC : FunctionalCountableChoice).
Axiom (EM : excluded_middle).

Lemma functional_list_choice {A} : forall (R: A -> A -> Prop) (f_list : nat -> list A),
    (forall k, f_list k <> []) ->
    (forall k v2, In v2 (f_list (S k)) -> exists v1, In v1 (f_list k) /\ R v1 v2) ->
    exists f, In (f 0) (f_list 0) /\ forall k, R (f k) (f (S k)).
Proof.
  intros * NE PRED.

  pose proof (NE 1) as NE1.
  destruct (f_list 1) as [|a]; [congruence|clear NE1 l].

  assert (NEk: forall k, In (hd a (f_list k)) (f_list k)).
  { intro k. pose proof (NE k); destruct (f_list k); [congruence|].
    left. reflexivity. }

  assert (G: forall n x, In x (f_list n) -> exists f, f n = x /\ forall k, (k < n)%nat -> In (f k) (f_list k) /\ R (f k) (f (S k))).
  { induction n; intros x Hx.
    - exists (fun k => x). split; [reflexivity|]. intros; lia.
    - pose proof (PRED _ _ Hx) as Hx'.
      destruct Hx' as (v1 & Hv1 & HRv1).
      pose proof (IHn _ Hv1) as Hv1'.
      destruct Hv1' as (f & Hv1' & Hf).
      exists (fun k => if Nat.eq_dec k (S n) then x else f k).
      destruct (Nat.eq_dec _ _) as [_|]; [|congruence].
      split; [reflexivity|]. intros k Hk.
      destruct (Nat.eq_dec k (S n)) as [|_]; [lia|].
      assert (k = n \/ k < n)%nat as [->|Hk'] by lia.
      + destruct (Nat.eq_dec _ _) as [_|]; [|congruence].
        rewrite Hv1'. split; assumption.
      + destruct (Nat.eq_dec _ _) as [|_]; [lia|].
        apply Hf; assumption. }

  destruct (FCC (nat -> A) (fun n f => In (f n) (f_list n) /\ (forall k : nat, k < n -> In (f k) (f_list k) /\ R (f k) (f (S k))))) as (g & Hg).
  { intros n. pose proof (G n _ (NEk n)) as (f & Hf1 & Hf2).
    exists f; split; auto. rewrite Hf1; apply NEk. }

  assert (Hg_in: forall n k, (k <= n)%nat -> In (g n k) (f_list k)).
  { intros. assert (k < n \/ n = k) as [Hlt|<-] by lia.
    - destruct (Hg n) as (_ & Hgn). apply Hgn. assumption.
    - apply (proj1 (Hg n)). }

  destruct (EM (exists x0, forall k, exists n, n > k /\ g n 0 = x0)) as [HEX|HNEX].
  2:{ exfalso.
      assert (HFN: forall (x: A), exists (k: nat), forall (n: nat), (n > k)%nat -> (g n 0 <> x)).
      { pose proof (not_ex_all_not _ _ HNEX) as HA.
        intro x. specialize (HA x). cbn in HA.
        destruct (not_all_ex_not _ _ HA) as [k Hk].
        exists k. pose proof (not_ex_all_not _ _ Hk) as HB.
        intros n. specialize (HB n). cbn in HB.
        apply Classical_Prop.not_and_or in HB.
        tauto. }
      assert (HF': exists k, forall x, In x (f_list 0) -> forall n, n > k -> g n 0 <> x).
      { induction (f_list 0).
        - exists O. intros x Hx. apply in_nil in Hx; elim Hx.
        - destruct (HFN a0) as (k0 & Hk0).
          destruct IHl as (kl & Hkl).
          exists (max k0 kl). intros x Hx n Hn.
          apply in_inv in Hx. destruct Hx as [->|Hx].
          + apply Hk0; lia.
          + apply Hkl; auto; lia. }
      destruct HF' as (k & HF').
      apply (HF' (g (k + 1) 0) (Hg_in (k + 1)%nat 0 ltac:(lia)) (k + 1) ltac:(lia)).
      reflexivity. }
  destruct HEX as (x0 & Hx0).
  destruct (DFC nat (fun _ => nat) (fun x y => x < y /\ g y 0 = x0)) as (next0 & Hnext0).
  { intro n. destruct (Hx0 n) as (k & ? & ?). exists k; split; auto; lia. }

  set (idx1 := fun n => Nat.iter (S n) next0 0).

  assert (Hidx1: (forall i j, i < j -> idx1 i < idx1 j) /\ (forall i, g (idx1 i) 0 = x0)).
  { split.
    - induction j; intro Hlt; [lia|].
      assert (i = j \/ i < j) as [->|Hijlt] by lia.
      + unfold idx1.  rewrite (Nat.iter_succ (S _)).
        apply Hnext0.
      + transitivity (idx1 j); [apply IHj; auto|].
        unfold idx1.  rewrite (Nat.iter_succ (S _)).
        apply Hnext0.
    - intros; destruct i; apply Hnext0. }

  (* Basically RR should say that there exists a subsequence of [g] that agrees on its first (length l1) elements. and we can extract a new subsequence that agrees on its first (length l1) + 1 elements *)
  set (l_ok := fun (l: list A) => let n := length l in exists idx, (forall i j, i < j -> idx i < idx j) /\ (forall k i, i < n -> g (idx k) i = nth_default a l i) /\ (forall i, S i < n -> R (nth_default a l i) (nth_default a l (S i)))).

  set (RR := fun (l1 l2: list A) => (exists xn, l2 = l1 ++ [xn]) /\ l_ok l1 /\ l_ok l2).
  assert (exists prefixn, prefixn 0 = [x0] /\ (forall n, RR (prefixn n) (prefixn (S n)))) as (f & Hf0 & HfS).
  { destruct (DFC {l : list A | l_ok l} (fun l1 => {l2 : list A | (exists xn, l2 = proj1_sig l1 ++ [xn]) /\ l_ok l2}) (fun l1 l2 => RR (proj1_sig l1) (proj1_sig l2))) as (f & Hf).
    { intros ln. destruct ln as (ln & Hln). cbn.
      destruct Hln as (idxn & Hidxn).
      destruct Hidxn as (idxn_ascending & idxn_prefix & idxn_rels).
      assert (idxn_mono: forall i, i <= idxn i).
      { induction i; [lia|].
        pose proof (idxn_ascending i (S i) ltac:(lia)). lia. }
      set (N := length ln).
      destruct (EM (exists xN, forall k, exists n, (idxn n) > idxn k /\ g (idxn n) N = xN)) as [HEX|HNEX].
      2:{ exfalso.
          assert (HFN: forall (xN: A), exists (k: nat), forall (n: nat), (idxn n > idxn k)%nat -> (g (idxn n) N <> xN)).
          { pose proof (not_ex_all_not _ _ HNEX) as HA.
            intro x. specialize (HA x). cbn in HA.
            destruct (not_all_ex_not _ _ HA) as [k Hk].
            exists k. pose proof (not_ex_all_not _ _ Hk) as HB.
            intros n. specialize (HB n). cbn in HB.
            apply Classical_Prop.not_and_or in HB.
            tauto. }
          assert (HF': exists k, forall x, In x (f_list N) -> forall n, idxn n > idxn k -> g (idxn n) N <> x).
          { induction (f_list N).
            - exists O. intros x Hx. apply in_nil in Hx; elim Hx.
            - destruct (HFN a0) as (k0 & Hk0).
              destruct IHl as (kl & Hkl).
              exists (max k0 kl). intros x Hx n Hn.
              apply in_inv in Hx. destruct Hx as [->|Hx].
              + apply Hk0. apply (Arith_base.gt_le_trans_stt _ _ _ Hn).
                assert (k0 >= kl \/ k0 < kl) as [D|D] by lia; [rewrite Nat.max_l by lia|rewrite Nat.max_r by lia]; [lia|].
                pose proof (idxn_ascending _ _ D); lia.
              + apply Hkl; auto.
                apply (Arith_base.gt_le_trans_stt _ _ _ Hn).
                assert (k0 >= kl \/ k0 < kl) as [D|D] by lia; [rewrite Nat.max_l by lia|rewrite Nat.max_r by lia]; [|lia].
                assert (k0 = kl \/ kl < k0) as [->|D'] by lia; [reflexivity|].
                pose proof (idxn_ascending _ _ D'); lia. }
          destruct HF' as (k & HF').
          assert (E: N <= idxn (Init.Nat.max (k + 1) (N + 1))).
          { assert (k >= N \/ k <= N) as [?|?] by lia.
            - rewrite Nat.max_l by lia.
              transitivity (k + 1); [|apply idxn_mono]; lia.
            - rewrite Nat.max_r by lia.
              transitivity (N + 1); [|apply idxn_mono]; lia. }
          pose proof (Hg_in (idxn (max (k + 1) (N + 1))) N E) as HIn.
          apply (HF' _ HIn (Init.Nat.max (k + 1) (N + 1))); [|reflexivity].
          pose proof (idxn_ascending k ((Init.Nat.max (k + 1) (N + 1))) ltac:(lia)). lia. }
      destruct HEX as (xN & HxN).
      destruct (DFC nat (fun _ => nat) (fun x y => idxn x < idxn y /\ g (idxn y) N = xN)) as (nextN & HnextN).
      { intro n. destruct (HxN n) as (k & ? & ?). exists k; split; auto; lia. }

      set (idxN := fun n => idxn (Nat.iter (S n) nextN 0)).

      assert (HlN: l_ok (ln ++ [xN])).
      { exists idxN. split.
        { unfold idxN. induction j; [lia|]; intros.
          rewrite (Nat.iter_succ (S j)).
          assert (i = j \/ i < j) as [->|] by lia.
          - apply HnextN.
          - transitivity (idxn (Nat.iter (S j) nextN 0)); [apply IHj|apply HnextN]; auto. }
        assert (length (ln ++ [xN]) = S N) as -> by (rewrite length_app; cbn; lia).
        split.
        { intros. rewrite nth_default_eq.
          assert (i < N \/ i = N) as [| ->] by lia.
          - rewrite app_nth1 by assumption. unfold idxN.
            rewrite idxn_prefix by assumption. apply nth_default_eq.
          - rewrite app_nth2 by lia.
            rewrite Nat.sub_diag. cbn.
            unfold idxN. rewrite Nat.iter_succ.
            apply HnextN. }
        intros. do 2 rewrite nth_default_eq.
        assert (S i < N \/ i = (N - 1)) as [| ->] by lia.
        - do 2 rewrite app_nth1 by lia.
          do 2 rewrite <- nth_default_eq.
          apply idxn_rels; assumption.
        - assert (S (N - 1) = N) as -> by lia.
          rewrite (@app_nth1 _ _ _ _ (N - 1)) by lia.
          rewrite app_nth2 by lia. rewrite Nat.sub_diag.
          cbn. destruct (HxN N) as (N0 & Hn0 & <-).
          rewrite <- nth_default_eq.
          rewrite <- (idxn_prefix N0 (N - 1) ltac:(lia)).
          pose proof (proj2 (proj2 (Hg (idxn N0)) (N - 1) ltac:(pose proof (idxn_mono N); lia)))as Q.
          replace (S (N - 1)) with N in Q by lia. apply Q. }

      assert (HlN': (exists xn, ln ++ [xN] = ln ++ [xn]) /\ l_ok (ln ++ [xN])).
      { split. exists xN. reflexivity. assumption. }

      exists (exist _ (ln ++ [xN]) HlN'). cbn.
      split; [eexists; reflexivity|].
      split; auto.
      exists idxn. auto. }
    (* fn apply f n times to [x0] *)
    assert (Hl0: l_ok [x0]).
    { red. exists idx1. intros; split; [apply Hidx1|].
      cbn [length]. split; [|intros; lia].
      intros k i Hi; assert (i = 0)%nat as -> by lia. apply Hidx1. }
    set (fn := fix fn n := match n with
                           | O => exist _ [x0] Hl0
                           | S n' => exist _ (proj1_sig (f (fn n'))) (proj2 (proj2_sig (f (fn n'))))
                           end).
    exists (fun n => proj1_sig (fn n)).
    split; [reflexivity|].
    cbn [fn proj1_sig]. intros; apply Hf. }

  exists (fun n => nth_default a (f n) n). split.
  { rewrite Hf0. cbn.
    destruct (Hx0 0) as (? & (? & <-)).
    apply Hg_in; lia. }

  assert (Hlen_f: forall n, length (f n) = S n).
  { induction n; [rewrite Hf0; reflexivity|].
    destruct (HfS n) as ((xn & Hxn) & Hl1 & Hl2).
    rewrite Hxn. rewrite length_app, IHn. cbn. lia. }

  intro k. destruct (HfS k) as ((xn & Hxn) & Hl1 & Hl2).
  rewrite (nth_default_eq k).
  rewrite <- (app_nth1 (f k) [xn]) by (rewrite Hlen_f; lia).
  rewrite <- Hxn, <- nth_default_eq.
  destruct Hl2 as (_ & _ & _ & W).
  apply W. rewrite Hlen_f. lia.
Qed.

(* Print Assumptions functional_list_choice. *)

(* Axioms: *)
(* Classical_Prop.classic : forall P : Prop, P \/ ~ P *)
(* FCC : FunctionalCountableChoice *)
(* EM : excluded_middle *)
(* DFC : DependentFunctionalChoice *)
2 Likes
18

Thank you, that looks great ! Actually, since FDC implies FCC, and EM is the same as Classical_Prop.classic, we can reduce the number of axioms to 2.
I need a bit of time to digest and understand the proof, but I was wondering if you thought if your proof is essentially similar to the one of @DmxLarchey which uses König’s lemma ? In that case, would that mean that the proof of König’s lemma is “hidden” somewhere in your proof script ?
In any case, thank you again for your work, I would definitely not have found the solution by myself :slight_smile:

19

I’m not familiar enough with König’s lemma to be certain, but I would assume so.

The essence of my proof is as follows.

We call an element of f_list 0 a root, and we say that an element of f_list n is at level n, then it’s easy to show that for all elements at level n, there exists a path down to a root, where a path of length n is defined as an enumeration f: nat -> A such that for all i <= n, f i is at level i and for all i<n, R (f i) (f (S i)).

There exists an enumeration g: nat -> path such that g n is a path of length n (I think this could be proved constructively, but I used choice).

Since there is a finite number of roots, by infinite pigeonhole principle, there exists a subsequence of paths that all have the same root (this needs excluded middle and choice).

This very much is the setting for using König’s lemma now if one has it, you have an infinite tree (for all n, there exists a path of length greater than n), and all branchings are finite since there is a finite number of elements that can be at level n.

So I’m guessing this is where I ended up proving it.

2 Likes
20

The lemma that showd that there is a R-path of arbitrary length from level n to level 0, is called unbounded in the code I posted. This is proved constructively, by induction on n. But finite paths are coded using lists (satisfying rel_seq for respecting R and choice_seq for respecting f_list) instead of finite prefixes of maps nat -> A.

21

For the sake of completeness, here is a proof of König’s lemma assuming excluded middle and dependent choice:

Require Import List Arith Lia Utf8.

Import ListNotations.

Definition finite {X} (P : X → Prop) :=  ∃l, ∀x, P x ↔ In x l.

Section forall_exists_finite.

  Variables (X : Type) (Q : X → nat → Prop).

  Local Lemma forall_exists_list l : 
      (∀x, In x l → ∃n, Q x n)
    → ∃m, ∀x, In x l → ∃n, n ≤ m ∧ Q x n.
  Proof.
    induction l as [ | x l IHl ]; intros Hl.
    + exists 0; simpl; tauto.
    + destruct (Hl x) as (n & Hn); simpl; auto.
      destruct IHl as (m & Hm).
      * intros; apply Hl; simpl; auto.
      * exists (n+m).
        intros ? [ <- | (k & [])%Hm ].
        - exists n; split; auto; lia.
        - exists k; split; auto; lia.
  Qed.

  Theorem forall_exists_finite_bound (P : X → Prop) :
      finite P
    → (∀x, P x → ∃n, Q x n)
    → ∃m, ∀x, P x → ∃n, n ≤ m ∧ Q x n.
  Proof.
    intros (l & Hl) H.
    destruct forall_exists_list with (l := l) as (n & Hn).
    + intros ? ?%Hl; auto.
    + exists n; intros ? ?%Hl; auto.
  Qed.

End forall_exists_finite.

Inductive rel_seq {X} (R : X → X → Prop) : list X → Prop :=
  | rel_seq_zero : rel_seq R []
  | rel_seq_one x : rel_seq R [x]
  | rel_seq_more l x y : R x y → rel_seq R (l++[x]) → rel_seq R (l++[x;y]).
  
#[local] Hint Constructors rel_seq : core.

Fact rel_seq_head_inv X (R : X → X → Prop) l :
    rel_seq R l
  → match l with 
    | []      => True
    | [_]     => True
    | x::y::l => R x y ∧ rel_seq R (y::l)
    end.
Proof.
  induction 1 as [ | x | [ | ? [] ] ]; simpl in *; auto; split; tauto || eauto.
  + constructor 3 with (l := []); simpl; auto.
  + constructor 3 with (l := _::_); simpl; tauto.
Qed.

Axiom dc : ∀ X (R : X → X → Prop),
        (∀x, ∃y, R x y) 
       → ∀x, ∃ρ, ρ 0 = x ∧ ∀n, R (ρ n) (ρ (S n)).

Fact dc_sigma X (Q : X → Prop) (R : X → X → Prop) :
    (∀x, Q x → ∃y, Q y ∧ R x y)
   → ∀x, Q x → ∃ρ, ρ 0 = x ∧ (∀n, Q (ρ n) ∧ R (ρ n) (ρ (S n))).
Proof.
  generalize (dc {x | Q x} (λ u v, R (proj1_sig u) (proj1_sig v))).
  intros DC H x Hx.
  destruct DC with (x := exist _ x Hx) as (rho & H1 & H2).
  + intros (y & Hy).
    destruct (H _ Hy) as (z & Hz & H1).
    exists (exist _ z Hz); now simpl.
  + exists (fun n => proj1_sig (rho n)); split.
    * now rewrite H1.
    * intros n; split; auto.
      apply (proj2_sig _).
Qed.

Axiom xm : ∀ A : Prop, A ∨ ¬ A.

Section Konigs_lemma.

  Variables (X : Type) 
            (R : X → X → Prop)
            (HR : ∀x, finite (R x)).

  (** bounded means that R-sequences starting at x have a bounded length *) 
  Let bounded x := ∃n, ∀l, rel_seq R (x::l) → length l < n.

  (** bounded is "hereditary" for R. Does not depend on XM *)
  Local Fact bounded_R x : (∀y, R x y → bounded y) → bounded x.
  Proof. 
    intros Hx.
    destruct forall_exists_finite_bound
      with (1 := HR x) (2 := Hx)
      as (m & Hm).
    exists (1+m).
    intros [ | y l ] Hl; simpl; [ lia | ].
    apply rel_seq_head_inv in Hl as ((n & H1 & H2)%Hm & H3).
    apply H2 in H3; lia.
  Qed.

  (* This simulates "reasonning by absurd" using xm *)
  Tactic Notation "absurd" "as" ident(C) :=
  match goal with |- ?c => destruct (xm c) as [ | C ]; [ trivial | exfalso ] end.

  (** unbounded means that there are arbitrary long R-sequences starting at x *)
  Let unbounded x := ∀n, ∃l, rel_seq R (x::l) ∧ n ≤ length l.

  (** This is the contrapositive of bounded_R, and it depends XM.
      It states that unbounded is an invariant for R *)
  Local Lemma unbounded_R__XM x : unbounded x → ∃y, unbounded y ∧ R x y.
  Proof.
    intros Hx.
    absurd as C1.
    destruct (bounded_R x) as (n & Hn).
    + intros y Hy.
      absurd as C2.
      destruct C1; exists y; split; auto.
      intros n.
      absurd as C3.
      destruct C2.
      exists n.
      intros l Hl.
      destruct (le_lt_dec n (length l)); auto.
      destruct C3; eauto.
    + destruct (Hx n) as (l & ?%Hn & ?); lia.
  Qed.

  (** We apply DC to the unbounded invariant *)
  Theorem Konigs_lemma x :
      (∀n, ∃l, rel_seq R (x :: l) ∧ n ≤ length l)
    → ∃ρ, ρ 0 = x ∧ ∀n, R (ρ n) (ρ (S n)).
  Proof.
    intros Hx.
    destruct dc_sigma
      with (Q := unbounded) (R := R) (x := x)
      as (rho & H1 & H2); auto.
    + apply unbounded_R__XM.
    + exists rho; split; auto.
      intro; apply H2.
  Qed.

End Konigs_lemma.

Check Konigs_lemma.
Print Assumptions Konigs_lemma.
2 Likes