[Agda] Do you use postulates extensively?

[Sergei Meshveliani]

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