[Agda] Problem with inductively defined type having (simulated) partial constructors

[Wouter Swierstra]

>  proof1 : {a : Octet} -> {b : Octet} ->
>           (_ : even a IsTrue) -> (_ : even b IsTrue) ->
>           even (a or b) IsTrue
>  proof1 {allzeros} {allzeros} p q = ???
>  proof1 {_ orone} {_} p q = ???
>  proof1 {_} {_ orone} p q = ???
>  proof1 {_ shifted} {_shifted} p q = ???
>
> I can't figure an expression to put in each of these clauses that
> produces Top or Bottom : Set instead of : Set1

So in the first set of question marks, you have to give a proof that  
"even (allzeros or allzeros) IsTrue". By definition of _or_ this is  
the same as a proof of "even allZeros IsTrue". Now by definition of  
even, this is the same as a proof of "True IsTrue" - which is easy:

>  proof1 {allzeros} {allzeros} p q = record {}


In some cases, you will need to use your proof arguments to rule out  
impossible branches. For example, what should the right-hand side be  
in this branch:

>  proof1 {_orone a {p}} {b} q1 q2 = ?

We seem stuck: we need to show that "(a orone) or allzeros" is even,  
which it isn't. Fortunately, this branch is impossible: there's no way  
to provide the q1 argument that proves "a orone" is even. In Agda you  
can write:

>  proof1 {_orone a {p}} {b} () q2

where the "()" means "no argument can ever have this type, so I'm not  
going to bother writing the right-hand side". There's a symmetric case  
if the second argument is "b orone". The other cases are all pretty  
easy. I hope you get the idea.

> I was doing it this way to experiment with things.

Sure - that's the best way to learn. It just appears that you've dug  
yourself into a bit of a hole - please don't think that Agda is all  
hard work and no play!

The way I suggested allows you to write down the type of an n-bit  
word. Nil is a word without bits; you can make a word of size (n + 1)  
from a bit and a word of size n.

> Although constructing an Octet from "allzeros", "shift" and "set bit  
> 0"
> is also nice in a way.

Here's a different way to set things up, that is a bit closer to what  
you're trying to do:

data Word' : Nat -> Bool -> Set where
   Zero : Word' 0 False
   Shift : {n : Nat} -> {b : Bool} -> Word' n b -> Word' (Succ k) False
   OrOne : {n : Nat} -> Word' n False -> Word' n True

Now the type "Word' n b" represents a binary word of with (n + 1) bits  
with the rightmost bit set to b. It's slightly different from your  
data type. Instead of having "allzeros" produce an all-zero vector and  
have shift check that you don't go out of bounds, this representation  
starts with an empty bitvector and uses shift to make longer vectors.

If you use this definition of Word', you should be able to define this  
function, without having to do any proofs:

or : forall {n b1 b2} -> Word' n b1 -> Word' n b2 -> Word' n (bor b1 b2)

where bor is the Boolean or function.

Sorry if this doesn't make any sense, it's getting quite late. Best of  
luck,

   Wouter