[Agda] Help with proofs

[Tristan Wibberley]

On Tue, 2008-04-29 at 11:31 +0100, Wouter Swierstra wrote:

...

> The reason this proof is annoying is that the arguments a and b are  
> Octets, but you need a proof of toNatAsUnsigned (a or b) < n - that is  
> a proof about the Nats a and b represent. It might be worth looking at  
> "Binary.agda" in the examples directory. There Conor McBride shows how  
> to define a binary successor function; you might be able to use that  
> technology to define a < function that does not depend on binary  
> numbers directly. Using that function the proof should be much easier...
> 
> Hope this helps,

Yes, thanks. It helps a lot.

I'm not bothered about making the proofs easier to write. They only ever
get written once so that bit can be as hard as anything. It is only
being able to read and understand the meat of the program's structure
that really matters in the long run (that's why I've defined the Octet
type as I have).

Though I'm forming some ideas of things that might make it easier in the
face of an intuitively defined program.

One thing, if it were possible to have something like:


fn : {a : Octet} -> {b : Octet} -> (_ : (pred (a or b)) IsTrue} ->
          Bool_which_doesn't_leak_from_"a"_or_from_"b" IsTrue
fn {allzeros} {allzeros} ()
fn all_other_cases = _

and thus use it like:

fn some_proof -- a and b remain unspecified.
              -- all I'm doing is getting a proof object of some
              -- other proposition

It would also be nice to absolutely require a function such as fn to be
used wherever a proof object is needed for a proposition having a
different form to one you already have. This is in preference from
allowing the proof objects to be the same sometimes and not others
because the rule for when it is allowed and when it isn't is difficult
to grok.

-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.