[Agda] Do you use postulates extensively?

[Apostolis Xekoukoulotakis]

I am not saying not to prove things but to choose the granularity of the
proof in the same way that pen&paper proofs allows us to do.
I am interested in a granularity that would make the proof acceptable in
the math community and nothing more.

It is very important to falsify propositions as fast as possible and
postulating trivialities is the way to do it.

All this assumes that you develop the theory while you use Agda.

On Thu, Jan 17, 2019 at 3:48 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Wed, 2019-01-16 at 01:56 +0200, Apostolis Xekoukoulotakis wrote:
> > Since now, I have spent days proving trivial mathematical propositions
> > without knowing if the general theory/idea is correct.
> >
> >
> > This, of course, means that the theory is developed while programming
> > in Agda. It is not developed before using Agda.
> >
> >
> > I am thinking of using postulates extensively and prove things on
> > paper instead of doing it in Agda.
> > It is less safe but much faster. Then check the validity of the main
> > Idea with the use of the postulates. Only then try to prove some of
> > the postulates that might be a bit tricky.
> >
> >
> > At least for me, proofs that do not take part in the computation of a
> > program can remain postulates.
> >
> >
> > What is your strategy? Do you use postulates extensively? In my
> > opinion this is important enough that it needs to be put in the
> > documentation. I have wasted too much time proving trivial
> > propositions and we do not have to do that.
> >
>
>
> Usually I postulate simple lemmas of which I am sure that I can prove
> them in Agda. I move fast to the final goal. If fail with this final
> goal, then one can forget of those lemmas.
> And if the goal is proved, I return to proving those lemmas in Agda.
> Formal proofs are difficult.
>
> Still setting postulates is dangerous.
> Consider the problem:
> (given a prime number  p,  find any prime number  q  greater than  p.
>
> Many people suggest:
>      Method:
>      let A = product [p' | prime p', p' <= p]
>      in  1 + A
>
> and think that  1+A  is the needed prime.
> I also thought this way, and postulated this, and continued.
> Then, I returned to a formal proof for Method.
> And discovered that I fail to prove it.
> Then I discovered a counter-example:   2*3*5*...*13 + 1
> -- something of this sort.
>
> There were more simple cases when my postulate occurred wrong.
>
> Another example of using Agda proofs.
> I "developed" a certain factorization theory for cancellative
> commutative monoids, with definitions, and so on, because it looks as
> trivial.
> To make sure that I have not mistakes there, I proved all the lemmata in
> Agda. Then I looked into the book of Jacobson, and observed there all my
> definitions and lemmas. If there was not such a book, Agda could
> essentially help.
>
> And even without proofs, dependent types are important.
> They provide an adequate programming language for representing algebraic
> classes and domains.
>
> --
> SM
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190117/fa609559/attachment.html>