The fan “theorem”

Published on Nov. 22nd, 2008 on https://speleologic.livejournal.com/1273.html

The #fan theorem is a theorem of Brouwer's original intuitionistic analysis, which follows from the principle of bar induction. In a classical setting it is also a theorem, thanks to the principle of excluded middle.

In constructive type theory it is not a theorem (yet), although by adding a principle of bar induction we can formally prove it. (see http://www.brics.dk/RS/98/39/BRICS-RS-98-39.ps.gz )

My interest in the fan theorem comes from some specific places where it appears, like the completeness theorem of Wim Veldman or giving type-theoretical explanation to backtracking. Hence I am interested in specific instances of it and their computational contents.

I was wondering what is the problem with the general formulation however and that is why I tried to express it in #Coq, for the particular fan Cantor space. It boils down to giving a proof of the following:

B : (nat –> option bool) –> Prop bB : forall a : nat –> bool, exists l : nat, B (IS a l) mB : forall (a : nat –> bool) (l : nat), B (IS a l) –> B (IS a (S l)) ============================ exists n : nat, forall a : nat –> bool, B (IS a n)