<div dir="ltr"><div>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.</div><div>I am interested in a granularity that would make the proof acceptable in the math community and nothing more.</div><div><br></div><div>It is very important to falsify propositions as fast as possible and postulating trivialities is the way to do it.</div><div><br></div><div>All this assumes that you develop the theory while you use Agda.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 17, 2019 at 3:48 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Wed, 2019-01-16 at 01:56 +0200, Apostolis Xekoukoulotakis wrote:<br>
> Since now, I have spent days proving trivial mathematical propositions<br>
> without knowing if the general theory/idea is correct.<br>
> <br>
> <br>
> This, of course, means that the theory is developed while programming<br>
> in Agda. It is not developed before using Agda.<br>
> <br>
> <br>
> I am thinking of using postulates extensively and prove things on<br>
> paper instead of doing it in Agda.<br>
> It is less safe but much faster. Then check the validity of the main<br>
> Idea with the use of the postulates. Only then try to prove some of<br>
> the postulates that might be a bit tricky.<br>
> <br>
> <br>
> At least for me, proofs that do not take part in the computation of a<br>
> program can remain postulates.<br>
> <br>
> <br>
> What is your strategy? Do you use postulates extensively? In my<br>
> opinion this is important enough that it needs to be put in the<br>
> documentation. I have wasted too much time proving trivial<br>
> propositions and we do not have to do that.<br>
> <br>
<br>
<br>
Usually I postulate simple lemmas of which I am sure that I can prove<br>
them in Agda. I move fast to the final goal. If fail with this final<br>
goal, then one can forget of those lemmas.<br>
And if the goal is proved, I return to proving those lemmas in Agda.  <br>
Formal proofs are difficult.<br>
<br>
Still setting postulates is dangerous.<br>
Consider the problem:<br>
(given a prime number  p,  find any prime number  q  greater than  p.<br>
<br>
Many people suggest:<br>
     Method:<br>
     let A = product [p' | prime p', p' <= p]<br>
     in  1 + A <br>
<br>
and think that  1+A  is the needed prime.<br>
I also thought this way, and postulated this, and continued.<br>
Then, I returned to a formal proof for Method.<br>
And discovered that I fail to prove it.<br>
Then I discovered a counter-example:   2*3*5*...*13 + 1<br>
-- something of this sort.<br>
<br>
There were more simple cases when my postulate occurred wrong. <br>
<br>
Another example of using Agda proofs.<br>
I "developed" a certain factorization theory for cancellative<br>
commutative monoids, with definitions, and so on, because it looks as<br>
trivial.<br>
To make sure that I have not mistakes there, I proved all the lemmata in<br>
Agda. Then I looked into the book of Jacobson, and observed there all my<br>
definitions and lemmas. If there was not such a book, Agda could<br>
essentially help.<br>
<br>
And even without proofs, dependent types are important.<br>
They provide an adequate programming language for representing algebraic<br>
classes and domains. <br>
<br>
--<br>
SM<br>
<br>
<br>
<br>
</blockquote></div>