Hi Thorsten, hi all
Thorsten Altenkirch wrote:
> When marking the exams, I noticed that some people proved the double
> negation of the excluded middle in an apparently very elegant way:
>
> let (---------------------------------!
> ! ex14 : Not (Not (Or A (Not A))) )
> ex14 => lam x => x (right
> x)
> (see also attached file). This is green in Epigram but I can't see how
> this should work: We assume
>
> x : Not (Or A (Not A))
>
> to show Zero, we apply x hence it remains to show Or A (Not A), we do
> this via right hence we have
> to show Not A, but x has *not* type Not A but Not (Or A (Not A))?!
>
> Is there anything wrong with my analysis? If not why does Epigram
> accept this?
I've been revisiting this bogey for obvious (at least in Nottingham)
reasons. At the time, I knew about the mysterious green shed bug, which
I put down to some cosmetic fumbling, but this was the first indicator
of a serious green error bug. I suspected the two were related, but
found neither.
It finally occurred to me how to find the green shed bug, and it turned
out to be because of a bad hack, the reason for which I've long
forgotten. Moreover, the same bug was clearly capable of causing green
suspicions generally, not just green sheds. But not green errors. So why
was this example triggering it?
Perplexed, I went ahead and replaced the bad hack with a less bad hack.
And discovered the yellow unification failure bug. The above bogus proof
only went yellow, because a unification failure wasn't propagating in
the right way. Combined with the green suspicion bug, there's your green
error!
I've fixed both the green suspicion bug and the yellow unification
failure bug, so the above 'proof' now goes brown as well it should.
Still haven't fixed the space leak...
Feel a bit silly now
Conor
PS Folks, this probably means that building a new distribution is a good
idea. I've even forgotten how we do that. Help!
