The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thursday, November 26, 2015 05:34:25 PM Pierre-Marie Pédrot wrote:
> On 26/11/2015 17:06, David Asher wrote:
> > But I need some additional information [ somethig like "~ (exists m,
> > m < n /\ P m)" ] in the context. Any ideas how to solve this?
> 
> If P is decidable, you can prove by induction on n that
> 
> P n -> exists m, P m /\ (forall p, p < m -> ~ P p)
> 
> I don't think that this is intuitionistically provable when P is not
> decidable though. Note that relying on such proof techniques (« let n be
> the smallest integer s.t. ... ») smells a lot like you're trying to
> reason classically.

There isn't necessarily anything wrong with reasoning classically, if the 
object is pure mathematical formalization without any intent to extract 
algorithms or run them in Coq.  Certainly, it could be an interesting 
exercise 
to see if you can prove something similar intuitionistically.  Also, 
sometimes 
thinking along those lines might result in a development which is more 
naturally provable in Coq - for example, I've recently found that proofs 
regarding filters seem more natural if you define one of the filter 
conditions as 
"∀ S, S ∈ F → Inhabited S" instead of the classically equivalent "¬ (∅ ∈ F)". 
 
However, such exercises might be "out of scope" of what you're trying to 
accomplish.
-- 
Daniel Schepler