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

[Tristan Wibberley]

On Fri, 2008-04-18 at 00:14 +0100, Wouter Swierstra wrote:
> >  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 {}

record {} is what I was missing from my knowledge. I realised after I
sent that email that I shouldn't be giving Top : Set but rather
something that is a proof object of Top.



> > 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!

Don't worry I consider this to be play :) I wouldn't be doing it at this
time of night if it wasn't. I expect to dig holes so I can learn what
the ground looks like if there is no treasure beneath it and avoid it
later on when I'm doing something to a deadline.


...

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

Thanks for all the help.

-- 
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.