(*******************************************************************) (** 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.