[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-21 00:28, Jesper Cockx wrote:
> On Thu, Aug 20, 2020 at 10:29 PM <mechvel at scico.botik.ru> wrote:
> 
>> Probably the majority of people keep in mind a bit another thing:
>> a possibility to use a non-constructive proof, when failed to
>> provide
>> a constructive one.
>> 
>> Does Agda support such a possibility?
> 
> Everything you do in Agda is constructive by default, but you can
> always use `postulate` to add any non-constructive principle you want.
> It will not (or at least, should not) break Agda in any way, except
> that you (obviously) lose canonicity, i.e. you may have a `b : Bool`
> that does not evaluate to `true` or `false`.

I knew of the `postulate' possibility for using non-constructive proofs,
but never tried it, doubt about the effects that may occur in practice.
The constructive area is too large in computer algebra methods, one can
program many years and never exit from it.


>> I cannot imagine: what can be wrong in this discourse.
>> In what way can it be possible the result R different from (1) and
>> (2).
>> How may it look this R ?
>> The result of (1) or (2) exists in nature independently on whether
>> we
>> have shown
>> some witness or not.
>> ?
> 
> There is nothing inherently wrong with either constructive or
> non-constructive mathematics, which one you use depends on what job
> you want to use it for. In particular, the meaning of the word
> 'exists' is not the same in constructive and non-constructive
> mathematics.

Of course it is different. But in what way?
Thus, in the above example with a `singular' even number:
a singular number either exists in Nat (among 2,4,6...) or does not 
exist
(i.e. the procedure F terminates or does not).

In constructive philosophy, how can it look the third possibility in 
this example?


> What can be annoying are the people who are convinced
> non-constructive mathematics is the right tool for *every* job.

Last 8 years I program proofs in Agda for algorithms in algebra.
Initially Agda is chosen not for constructivism but for
dependent types + functionality + laziness.
I viewed dependent types as a tool for a better domain representation, 
without relation
to constructivism.
And all of these proofs occur constructive, so far, because
(a) this is default in Agda, and one needs an effort and a particular 
reason to
     go beyond this,
(b) it occurs sufficient, so far.

But may there be any reason for using constructive proofs besides (a) 
and (b) ?
I think, it is like in the following example.
(I) One can prove non-constructively that a number  n  is not prime.
(II) But a constructive proof provides an algorithm that returns an 
non-trivial divisor
      m  for  n.
Evidently, (I) + (II) is strictly better than (I).

I think, this example shows that it may have sense to search specially 
for
a constructive proof. Evidently, this is so in many cases, but not in 
all cases.

?

--
SM