(*******************************************************************)
(** We use Coq to express proofs of the axiom of countable choice, *)
(** axiom of dependent choice and bar induction in the logic dHA^w *)
(** described in "A constructive proof of the axiom of dependent   *)
(** choice, compatible with classical logic" by Hugo Herbelin      *)
(*******************************************************************)

(******************************)
(** Axiom of countable choice *)
(******************************)

Module CountableChoice.

Parameter X : Set.
Parameter R : nat -> X -> Prop.

CoInductive P n := cons y : R n y -> P (S n) -> P n.

Definition wit {n} (a:P n) := match a with cons y _ _ => y end.
Definition prf {n} (a:P n) : R n (wit a) := match a with cons _ b _ => b end.
Definition tl n (a:P n) : P (S n) := match a with cons _ _ c => c end.

Lemma streamify : (forall n : nat, {y : X | R n y}) -> P 0.
Proof.
intros a.
generalize 0.
cofix Pc.
intro n.
destruct (a n) as (y,b).
apply (cons n y b (Pc (S n))).
Defined.

Fixpoint nth n a : P n := match n with 0 => a | S n => tl n (nth n a) end.

Theorem CountableChoice :
  (forall n : nat, {y : X | R n y}) ->
  {f : nat -> X | forall n : nat, R n (f n)}.
Proof.
intro a.
pose (b := streamify a).
exists (fun n => wit (nth n b)).
exact (fun n => prf (nth n b)).
Defined.

End CountableChoice.

(******************************)
(** Axiom of dependent choice *)
(******************************)

Module DependentChoice.

Parameter X : Set.
Parameter R : X -> X -> Prop.
Parameter x0 : X.

CoInductive P (x:X) := cons y : R x y -> P y -> P x.

Definition wit {x} (a:P x) := match a with cons y _ _ => y end.
Definition prf {x} (a:P x) : R x (wit a) := match a with cons _ b _ => b end.
Definition tl x (a:P x) : P (wit a) := match a with cons _ _ c => c end.

Fixpoint tln n (b : {x:X & P x}) : {x:X & P x} :=
  match n with 0 => b | S n => let a := tln n b in (existT _ _ (tl (projT1 a) (projT2 a))) end.

Lemma streamify : (forall x : X, {y : X | R x y}) -> P x0.
Proof.
intro a.
generalize x0.
cofix Pd.
intro x.
destruct (a x) as (y,b).
apply (cons x y b (Pd y)).
Defined.

Theorem DependentChoice :
  (forall x : X, {y : X | R x y}) ->
  {f : nat -> X | f 0 = x0 /\ (forall n : nat, R (f n) (f (S n)))}.
Proof.
intro a.
pose (b := existT (fun x => P x) x0 (streamify a)).
exists (fun n => projT1 (tln n b)).
exact (conj (refl_equal _) (fun n => prf (projT2 (tln n b)))).
Defined.

End DependentChoice.

(******************************)
(** Bar induction             *)
(******************************)

Module BarInduction.

Parameter X : Set.
Parameter B : list X -> Prop.

CoInductive P (l:list X) := cons y : B l -> P (y::l) -> P l.

Definition wit {l} (a:P l) := match a with cons y _ _ => y end.
Definition prf {l} (a:P l) : B l := match a with cons _ b _ => b end.
Definition tl l (a:P l) : P (wit a :: l) := match a with cons _ _ c => c end.

Open Scope list_scope.

Fixpoint restrict f n : list X :=
  match n with 0 => nil | S n => f n :: restrict f n end.

Fixpoint tln n (b:{l:list X & P l}) : {l:list X & P l} :=
  match n with 0 => b | S n => let a := tln n b in (existT _ _ (tl (projT1 a) (projT2 a))) end.

Theorem BarInduction : P nil -> {f : nat -> X | forall n : nat, exists l, B l /\ l = restrict f n}.
Proof.
intro a.
pose (b := existT (fun x => P x) nil a).
exists (fun n => wit (projT2 (tln n b))).
intro n.
exists (projT1 (tln n b)).
split.
exact (prf (projT2 (tln n b))).
induction n; simpl. auto. rewrite <- IHn. auto.
Defined.

End BarInduction.