[Agda] Do you use postulates extensively?

[Apostolis Xekoukoulotakis]

Mathematics has used informal proofs for thousands of years, and this is
why we made progress because the cost of a formal proof is enormous.
Why then use agda? Because types can guide the implementation of parts that
are important or are part of the computational path.

The question then is to find the correct strategy:
A) Informally prove a proposition and put explicitly the postulate
assumptions in the type. Have a secondary proposition without those
assumptions. This is the one to be used by the other proofs.
B) One could use type variables to imitate the traditional informal way of
proving. ("Because of theorem1.1 , lemma2.4 etc.")
C) Avoid proofs inside the types as much as possible, use abstraction if
the proof is used in the arguments and existential quantification if it is
used in the type of the result.

The question then becomes how to limit the effects of a failure of a proof
of a proposition. Will the effects cascade to the all the remaining proofs?
Many times ,
the failure can be local and mitigated with a fix. In others, the effect is
catastrophic.

For example, Shinichi Mochizuki's proof of the abc conjecture could be
wrong because of the incorrectness of a corollary. Given that the theory is
thousands of pages and many years of work, this will certainly be a
catastrophic failure if one is not able to replace that proposition with
something else.

Is the cascading effect of a wrong agda proposition bigger than in an
informal mathematical setting? What are your strategies in mitigating it
assuming that you use postulates?

On Wed, Jan 16, 2019 at 12:49 PM Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> On 16/01/2019 00.56, Apostolis Xekoukoulotakis wrote:
> > Do you use postulates extensively?
>
> No, but I can imagine that this depends on what you are working on. If
> your subject of study depends on a lot of prior, very solid work, then
> it might make sense to use postulates.
>
> When I prove something under an assumption that cannot be proven (say,
> "assuming equality of functions is extensional…") I have found it useful
> to state the assumption explicitly rather than using postulates. This
> makes it easy to track exactly what parts of the development depend on
> what assumptions.
>
> --
> /NAD
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190116/b781156e/attachment.html>