[Agda] Do you use postulates extensively?

Sat Jan 19 15:55:09 CET 2019

If I use many postulates, they can't be put as assumptions in the type. I
will try to only use postulates when they are trivial or are not in an
important path of the theory.
And we'll see if it works.

> 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.

With refinement , I do something similar.
Here you know what you want to prove but you do not know how to prove it.
You have a degree of freedom that you can use to determine the refining
protocol.
For example, to prove that a number is factored by 3, you can choose to
have numbers that are factored by 6.

On Fri, Jan 18, 2019 at 9:44 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190119/452df3a3/attachment.html>