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

[Tristan Wibberley]

On Thu, 2008-04-17 at 22:31 +0100, Wouter Swierstra wrote:
> Hi Tristan,
> 
> >> The other problem with your code is that it isn't obviously
> >> structurally recursive, and therefore doesn't termination check. This
> >> surprised me a bit. It seems ok, but maybe I'm missing something  
> >> here.
> 
> Dan Licata just pointed out that once you solve all the missing  
> proofs, the termination checker stops complaining. Phew.

That's good, but I can't see how to calculate a proof object of "even (a
or b) IsTrue" given proof objects "p : even a IsTrue" and "q : even b
IsTrue".

In the last few minutes I've tried looking at it like this (with _or_
and proof1 in a mutual block):



  (a orone) -> (b orone) -> (a or b) orone

  becomes

  (_orone a {p}) -> (_orone b {q}) -> _orone (a or b) {proof1 p q}



  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


> What about:
> 
> data Word : Nat -> Set where
>    Nil : Word 0
>    Cons : {n : Nat} -> Bit -> Word n -> Word (Succ n)
> 
> data Fin : Nat -> Set where
>    Fz : {n : Nat} -> Fin (Succ n)
>    Fs : {n : Nat} -> Fin n -> Fin (Succ n)
> 
> Octet = Word 8


> Is there any particular reason you want exactly this inductive  
> structure for the Octet type? Just curious,

I was doing it this way to experiment with things.

Does yours mean that Nil is a Word 0 and a Word 1 and a Word 2, etc...
That's nicer but I want to understand the problem I just hit first to
avoid skipping fundamental concepts.

I'll probably do it your way when I've learnt more because it is clearly
the better way.

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

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