[Agda] Automatic generation of trivial proofs

[Jean-Philippe Bernardy]

On Sat, Mar 5, 2011 at 9:19 PM, Christoph Herrmann
<ch at cs.st-andrews.ac.uk> wrote:
> Hi all,
>
> as you probably know, Agda is happy with a refl if it can figure out an equality just by
> evaluation. I have come across the problem to prove equations on  combinations
> of enumeration types. An example Agda script is attached in which I prove a property
> of a boolean function, using the *All* data type described in Ulf Norell's AFP'08 tutorial.
>
> Note that the "rubbish" at the right-hand side of "AutoProof" was generated
> automatically by typing Ctrl-C Ctrl-A into a goal. Agda would of course
> not provide a proof if the predicate was incorrect.

> My question: is it possible to tell Agda it does not need to pollute the program text with that
> kind of rubbish?

I assume that you are suggesting that Agda should perform the proof
search every time
it type-checks the file; effectively adding a symbol (with meaning
"please search") that would be
a valid proof. A consequence of such an addition is that type-checking
would become undecidable; and
thus the object found to the left of the colon in an Agda file would
no longer be a proof,
since it could no longer be used to easily check the validity of the
statement on the right
of the colon.

It seems that you might be interested in decidable problems only though;
for which there is ongoing work. For example, from the top of my head:
http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=385

> For some reason Agda turns just an underscore into yellow which is not
> sufficient for verification.

The underscore turns yellow because the value it stands for is not
(obviously) given
by the type-checking constraints.

Cheers,
JP.