Require Import Coq.Lists.List.
Require Import Coq.Logic.ClassicalChoice.

Module Type NAT_CHOICE.

Fixpoint fisrtn_list_from_fun {A: Type} (f: nat -> A) (n: nat) : list A :=
  match n with
  | 0 => nil
  | S m => fisrtn_list_from_fun f m ++ f m :: nil
  end.

Axiom nat_stepwise_choice: forall {A: Type} (P: list A -> Prop),
  P nil ->
  (forall l, P l -> exists a, P (l ++ a :: nil)) ->
  exists f, forall n, P (fisrtn_list_from_fun f n).

End NAT_CHOICE.

Module NatChoice: NAT_CHOICE.

Section NatChoice.

Fixpoint fisrtn_list_from_fun {A: Type} (f: nat -> A) (n: nat) : list A :=
  match n with
  | 0 => nil
  | S m => fisrtn_list_from_fun f m ++ f m :: nil
  end.

Context {A: Type} (P: list A -> Prop).

Definition State: Type := {l: list A | P l}.

Hypothesis H_init: P nil.

Definition state_nil: State := exist _ nil H_init.

Section step.

Variable F: State -> A.
Hypothesis HF: forall l: State, P (proj1_sig l ++ F l :: nil).

Fixpoint step (n: nat): State := 
  match n with
  | 0 => state_nil
  | S m => exist _ _ (HF (step m))
  end.

Lemma fisrtn_list_step: forall n, fisrtn_list_from_fun (fun n0 : nat => F (step n0)) n = proj1_sig (step n).
Proof.
(* Goal: forall k : nat, P (l k) *)
  intros.
(* Goal: @eq (list A) (@fisrtn_list_from_fun A (fun n0 : nat => F (step n0)) n) (@proj1_sig (list A) (fun l : list A => P l) (step n)) *)
  induction n.
  + simpl.
(* Goal: @eq (list A) (@nil A) (@nil A) *)
    reflexivity.
  + simpl.
(* Goal: @eq (list A) (@app A (@fisrtn_list_from_fun A (fun n0 : nat => F (step n0)) n) (@cons A (F (step n)) (@nil A))) (@app A (@proj1_sig (list A) (fun l : list A => P l) (step n)) (@cons A (F (step n)) (@nil A))) *)
    f_equal; auto.
Qed.

End step.

Lemma nat_stepwise_choice:
  (forall l, P l -> exists a, P (l ++ a :: nil)) ->
  exists f, forall n, P (fisrtn_list_from_fun f n).
Proof.
(* Goal: forall k : nat, P (l k) *)
  intros.
  assert (forall (l: list A | P l), exists a : A, P (proj1_sig l ++ a :: nil)) as HH; [| clear H].
  Focus 1. {
    intros [l ?H].
    apply H; auto.
  } Unfocus.

  apply choice in HH.
  destruct HH as [f ?].

  exists (fun n => f (step f H n)).
(* Goal: forall k : nat, P (l k) *)
  intros.
  rewrite fisrtn_list_step.

  apply (proj2_sig (step f H n)).
Qed.

End NatChoice.

End NatChoice.

Export NatChoice.

Lemma nat_coinduction {A: Type}: forall (P: A -> Prop) (R: A -> A -> Prop) a0,
  P a0 ->
  (forall a, P a -> exists b, R a b /\ P b) ->
  exists l: nat -> A, l 0 = a0 /\ (forall k, R (l k) (l (S k))).
Proof.
(* Goal: forall k : nat, P (l k) *)
  intros.
  pose (Rs := 
            fix Rs (a: A) (l: list A): Prop :=
              match l with
              | nil => True
              | a0 :: l0 => P a0 /\ R a a0 /\ Rs a0 l0
              end).
(* Goal: @ex (forall _ : nat, A) (fun l : forall _ : nat, A => and (@eq A (l O) a0) (forall k : nat, R (l k) (l (S k)))) *)
  destruct (nat_stepwise_choice (Rs a0)) as [l ?].
  + simpl; auto.
  + intro l.
(* Goal: forall _ : Rs a0 l, @ex A (fun a : A => Rs a0 (@app A l (@cons A a (@nil A)))) *)
    revert a0 H.
(* Goal: forall (a0 : A) (_ : P a0) (_ : Rs a0 l), @ex A (fun a : A => Rs a0 (@app A l (@cons A a (@nil A)))) *)
    induction l.
(* Goal: forall k : nat, P (l k) *)
    - simpl; intros.
(* Goal: @ex A (fun a : A => and (P a) (and (R a0 a) True)) *)
      destruct (H0 a0 H) as [a1 [? ?]].
(* Goal: @ex A (fun a1 : A => and (P a) (and (R a0 a) (Rs a (@app A l (@cons A a1 (@nil A)))))) *)
      exists a1; auto.
    - simpl; intros ? ? [? [? ?]].
(* Goal: @ex A (fun a1 : A => and (P a) (and (R a0 a) (Rs a (@app A l (@cons A a1 (@nil A)))))) *)
      specialize (IHl _ H1 H3).
(* Goal: @ex A (fun a1 : A => and (P a) (and (R a0 a) (Rs a (@app A l (@cons A a1 (@nil A)))))) *)
      destruct IHl as [a1 ?].
(* Goal: @ex A (fun a1 : A => and (P a) (and (R a0 a) (Rs a (@app A l (@cons A a1 (@nil A)))))) *)
      exists a1; auto.
  + exists (fun n => match n with 0 => a0 | S n => l n end).
(* Goal: and (@eq A (l O) a0) (and (forall k : nat, R (l k) (l (S k))) (forall k : nat, P (l k))) *)
    split; auto.
(* Goal: forall k : nat, P (l k) *)
    intros.
(* Goal: R match k with | O => a0 | S n => l n end (l k) *)
    specialize (H1 (S k)).
(* Goal: R match k with | O => a0 | S n => l n end (l k) *)
    destruct k; [simpl in H1; tauto |].
(* Goal: Rs a (@app A l0 (@cons A (l k) (@cons A (l (S k)) (@nil A)))) *)
    simpl in H1.
    rewrite <- app_assoc in H1; simpl in H1.
(* Goal: R (l k) (l (S k)) *)
    clear H H0.
(* Goal: forall k : nat, P (l k) *)
    revert a0 H1; induction (fisrtn_list_from_fun l k); intros.
    - simpl in H1.
(* Goal: R (l k) (l (S k)) *)
      tauto.
    - apply (IHl0 a); clear IHl0.
(* Goal: Rs a (@app A l0 (@cons A (l k) (@cons A (l (S k)) (@nil A)))) *)
      simpl in H1.
(* Goal: R (l k) (l (S k)) *)
      simpl; tauto.
Qed.

Lemma nat_coinduction' {A: Type}: forall (P: A -> Prop) (R: A -> A -> Prop) a0,
  P a0 ->
  (forall a, P a -> exists b, R a b /\ P b) ->
  exists l: nat -> A, l 0 = a0 /\ (forall k, R (l k) (l (S k))) /\ (forall k, P (l k)).
Proof.
(* Goal: forall k : nat, P (l k) *)
  intros.
(* Goal: @ex (forall _ : nat, A) (fun l : forall _ : nat, A => and (@eq A (l O) a0) (and (forall k : nat, R (l k) (l (S k))) (forall k : nat, P (l k)))) *)
  pose (R' := fun (a b: A) => R a b /\ P b).
  
(* Goal: @ex (forall _ : nat, A) (fun l : forall _ : nat, A => and (@eq A (l O) a0) (and (forall k : nat, R (l k) (l (S k))) (forall k : nat, P (l k)))) *)
  destruct (nat_coinduction P R' a0 H) as [l [? ?]].
  + simpl; unfold R'; firstorder.
  + exists l.
(* Goal: and (@eq A (l O) a0) (and (forall k : nat, R (l k) (l (S k))) (forall k : nat, P (l k))) *)
    split; auto.
(* Goal: and (forall k : nat, R (l k) (l (S k))) (forall k : nat, P (l k)) *)
    split; [subst R'; firstorder |].
(* Goal: forall k : nat, P (l k) *)
    intros.
(* Goal: P (l k) *)
    destruct k; [subst; auto |].
(* Goal: P (l (S k)) *)
    specialize (H2 k).
(* Goal: P (l (S k)) *)
    destruct H2; auto.
Qed.
