[Agda] Help with proofs

[Wouter Swierstra]

Hi Tristan,

proof3 is pretty easy. You can just pattern match on the implicit  
octets, killing off impossible branches:

  proof3 : {a : Octet} -> {b : Octet} ->
           (_ : nonzero a IsTrue) -> (_ : nonzero b IsTrue) ->
           nonzero (a or b) IsTrue
  proof3 {allzeros} () _
  proof3  {x orone} {allzeros} p q = record {}
  proof3  {x orone} {y orone} p q = record {}
  proof3  {x orone} {y shifted} p q = record {}
  proof3  {x shifted} {allzeros} p q = record {}
  proof3  {x shifted} {y orone} p q = record {}
  proof3  {x shifted} {y shifted} p q = record {}

It's kind of annoying that you need to write out all the patterns  
explicitly, even if the right-hand side is the same for all the  
branches. The reason for this is that it isn't clear that "nonzero (a  
or b) IsTrue" - even if it is true for any choice of constructor for a  
or b (except allzeros and allzeros, of course). Once you have a  
constructor, this can trigger a step of beta reduction in the "or"  
function, and the proof becomes trivial.

>  proof2 : {a : Octet} -> {b : Octet} ->
>           (_ : (msbclear a) IsTrue) ->
>           (_ : (msbclear b) IsTrue) ->
>           (msbclear (a or b)) IsTrue
>  proof2 _ _ = _ -- what here?

This one is much harder, I think. First of all, you may want to  
generalise it to:

proof2 :  {a : Octet} -> {b : Octet} -> {n : Nat} ->
>           ((toNatAsUnsigned a) < n) IsTrue ->
>           ((toNatAsUnsigned b) < n) IsTrue ->
>           (toNatAsUnsigned (a or b) < n) IsTrue

As you'll need to make recursive calls to proof, where the upper bound  
isn't 128, but 127 for example.

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,

   Wouter