[Agda] Do you use postulates extensively?

[Martin Escardo]

Let me go to the beginning of this thread.

I meant to answer earlier but I didn't have time.

The answer is that this heavily depends on what you want to do.

1. Suppose you want to formalize all of known mathematics, or, more 
modestly, all mathematics is currently taught in undergraduate and 
graduate degrees, or even more modestly, some existing mathematics you like.

I would suggest that, in this case, it makes a lot of sense to adopt a 
"top down" approach, and go from what we teach down to the axioms.

The formal-abstracts project seems to adopt this approach.

 
https://jiggerwit.wordpress.com/2018/04/09/formal-abstracts-a-long-term-vision/

   http://florisvandoorn.com/talks/formalabstracts2018.pdf

   https://fl60.sciencesconf.org/data/program/T_Hales_1.pdf

What you haven't proved yet is a postulate or axiom. But perhaps you 
want to formulate it as an assumption (to a module or to a 
definition/construction/theorem). Otherwise you may end up with 2000 
postulates without knowing which parts of your mathematical development 
depends on which fragment of the unformalized mathematical knowledge.

2. Suppose you want to use a proof assistant such as Agda as a helpful 
blackboard to do *new* mathematics. This is something I do often. Many 
times I start with a piece of paper and a pencil, and I work until the 
moment I need help (to do routine reductions, to test definitions before 
I find their definitive form, to test proof approaches that worked on 
paper but then reached many cases to test, or many possible induction 
hypothesis, or what-you-have in the practice of doing mathematics).

  Then the top-down approach (probably combined with a bottom-up one) 
works very well again, using holes rather than postulates as the 
preferred mechanism.

  One thing I find *very* useful is to have holes in the *formulations* 
of definitions and theorems, rather than just the proofs of theorems. In 
particular, this happens when you have a vague idea of what you want to 
prove, with perhaps a clearer idea of how you want to prove what you 
don't know yet you want to prove.

  Whenever you see 1000 lines of my Agda code, there are 5000 garbage 
lines or more needed to get them that I don't show you, just like in 
pencil-and-paper mathematics when it reaches the publication status.

  I think Agda and all proof assistants in the world need more of this 
kind of black-board / notepad support.

3. Suppose the only reason you want to use Agda (or something 
equivalent) is that you have constructive theorems. You don't care about 
formal correctness per se (you trust yourself). Then you may formalize 
your theorems so that you can run them. I do this often, particularly 
for (what I regard to be) surprising constructive results.


4. Suppose you want to experiment with non-standard axioms or axioms 
that just don't hold in type theory but are consistent (such as "all 
functions are continuous", bar induction, Markov principle, function 
extensionality, univalence, etc.). Then you may be tempted to postulate 
them. Or maybe to use them as assumptions in modules or 
definitions/constructions.

In general, mathematics (constructive or not) is *all about* going from 
assumptions to conclusions/constructions. But I don't think the 
postulate mechanism is the best one for this purpose from an engineering 
point of view of the development of mathematics. In any case, we are in 
early days, and people (developers and users) are experimenting with 
this new tool.

Martin
PS. 5. All this will be used in ways we didn't plan or anticipate, in 
any case, like with everything in science and mathematics and human 
knowedge and technology in general.




On 15/01/2019 23:56, apostolis.xekoukoulotakis at gmail.com 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.
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

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