[Agda] Hanging out with the Lean crowd

[Martin Escardo]

You may wish to check Andrej Bauer's paper
http://math.andrej.com/2016/10/10/five-stages-of-accepting-constructive-mathematics/

Martin

On 20/08/2020 23:44, mechvel at scico.botik.ru wrote:
> 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

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe