[Agda] A proof of omniscience in Agda

[Vincent Siles]

Dear all,
I did a quick (and very dirty) translation of Martin's files into Coq
(I don't trust Agda yet :p)
and it went perfectly well. I wanted to avoid Prop so I redefined
everything but the definition of
bool and nat.

You can have a look at [1] if you are interested. Be aware that I did
a direct translation of his code into Coq
so it is ugly and somehow difficult to read. I'll rewrite it in a
better "Coq" way after TYPES.


Cheers,
Vincent

[1]: http://www.cse.chalmers.se/~siles/coq/LPO.v

2011/9/4 Martin Escardo <m.escardo at cs.bham.ac.uk>:
> Dear Hank,
>
> Thanks for pointing out that my opportunities of employment are not
> nil if the funding policies proceed in the direction they seem to be
> going.
>
> More seriously:
>
> On 03/09/11 16:04, Peter Hancock wrote:
>>
>> Have you really debauched the set of natural numbers, or just made
>> some other set of other things?(Smiley.)
>
> This is a fair question. I have three answers.
>
> Firstly, in the current Agda files I do embed ℕ into ℕ∞ so that only
> one new element, namely ∞, arises, dutifully formally proved (not
> because I wanted to justify this to people who might ask, but because
> it is needed for the proof of the theorem (twice: once directly, and
> once indirectly in the density theorem).
>
> Secondly, in the accompanying paper cited in the Agda files I do
> mention that another way of seeing ℕ∞ is as a co-inductive definition
> using 0 and successor, in which you hence get the new point ∞ in the
> usual well known way (as an infinite piling of successor
> functions). (The first way of adding the point is that of traditional
> constructive mathematics.)
>
> Thirdly, I could have written the Agda proof using the co-inductive
> definition, and in fact this is a nice exercise for people in this
> list trying to understand how Agda works. The reason I didn't do that
> is that there will be a next installment of the Agda proof, showing
> that plenty of other subsets of the Cantor space are omniscient. For
> this generalized setting, it is more convenient to have ℕ∞ in the way
> I currently defined it.
>
> Anyway, I sense that you were only joking and that you didn't really
> intend me to answer this.
>
> Best wishes,
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>