[Agda] Automatic generation of trivial proofs

[Brandon Moore]

Here is a neater way of making these proofs about booleans.

The problem with "All" is that it does not compute to simpler types.
if replaced with a definition like (approximated in ascii)

all : {A : Set} {P : A -> Set} (L : List A) -> Set
all P [] = T
all P (x :: xs) = P x \x all P xs

then this would reduce when applied to a concrete list like Bins.
In fact, it reduces to a type asserting P holds over a list
to nested tuples of smaller assertions. Once everything
unfolds, each remaining assertion should be I == I or O == O.

We can build a similar goal type by taking just one function
f, and reducing the type of the assertion that (\x -> f x == f x)
for each list item. If f and g are actually equivalent, then
the fully unfolded version of this type and the previous type
will be equal.

The attached code has a function "conv" which proves
a non-reducing version of the proof type in terms of
the computational version. and a function "pf" which
unfolds a tree asserting f x == f x.



To clean things up a bit, I use (b : Bin) -> P b as
the non-reducing version of the assertion, rather than
an All type, and both (P : Bin -> Set) = P I \x P O
as the reducible version, rather than something more
general.

Brandon



      
-------------- next part --------------
A non-text attachment was scrubbed...
Name: BinProof.agda
Type: application/octet-stream
Size: 1360 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20110307/2079e1b5/BinProof.obj