[Agda] Help with proofs

[Tristan Wibberley]

Hi all,

How should I go about implementing proofs 2 and 3 in the below? I've
struggled with this for a week hitting dead-end after dead-end.

module octet where

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}
{-# BUILTIN SUC succ    #-}
{-# BUILTIN ZERO zero   #-}

_+_ : Nat -> Nat -> Nat
zero + b = b
(succ a) + b = a + (succ b)

data Bool : Set where
  True : Bool
  False : Bool

data Bottom : Set where
record Top : Set where

_IsTrue : Bool -> Set
True IsTrue = Top
False IsTrue = Bottom

_IsFalse : Bool -> Set
True IsFalse = Bottom
False IsFalse = Top

_&&_ : Bool -> Bool -> Bool
False && False = False
False && True = False
True && False = False
True && True = True

_<_ : Nat -> Nat -> Bool
zero < zero = False
(succ a) < zero = False
zero < (succ b) = True
(succ a) < (succ b) = a < b 

pred : (a : Nat) -> {_ : (0 < a) IsTrue} -> Nat
pred 0 {}
pred (succ a) {_} = a

-- Interesting stuff starts here
mutual
  -- allzeros is an octet (00000000b)
  -- x orone is an octet if bit0 is clear (x = nnnnnnn0b)
  -- x shifted is an octet if bit7 is clear and at least one bit is set
  --     (eg x = 01nnnnnnb, 001nnnnnb, 011nnnnnb, etc)
  data Octet : Set where
    allzeros : Octet
    _orone : (o : Octet) -> {_ : (lsbclear o) IsTrue} -> Octet
    _shifted : (o : Octet) ->
               {_ : (msbclear o) IsTrue} ->
               {_ : (nonzero o) IsTrue} -> 
               Octet

  toNatAsUnsigned : Octet -> Nat
  toNatAsUnsigned allzeros = 0
  toNatAsUnsigned (a orone) = succ (toNatAsUnsigned a)
  toNatAsUnsigned (a shifted) = (toNatAsUnsigned a) + (toNatAsUnsigned
a)

  maxplusone : Nat
  maxplusone = 256

  msbvalue : Nat
  msbvalue = 128

  nonzero : Octet -> Bool
  nonzero allzeros = False
  nonzero (_ orone) = True
  nonzero (a shifted) = True

  lsbclear : Octet -> Bool
  lsbclear allzeros = True
  lsbclear (_ orone) = False
  lsbclear (_ shifted) = True

  msbclear : Octet -> Bool
  msbclear o = (toNatAsUnsigned o) < msbvalue

_istrue : (a : Bool) -> {_ : a IsTrue} -> a IsTrue
_istrue False {}
_istrue True {p} = p

mutual
  _or_ : Octet -> Octet -> Octet
  allzeros or b = b
  (_orone a {p}) or allzeros  = _orone a {p}
  (_orone a {p}) or c@(_ shifted) =
              _orone (a or c) {proof1 p ((lsbclear c) istrue)}
  (_orone a {p}) or (_orone b {q}) =
              _orone (a or b) {proof1 p q}
  (_shifted a {p} {q}) or allzeros = _shifted a {p} {q}
  a@(_ shifted) or (_orone b {r}) =
              _orone (a or b) {proof1 ((lsbclear a) istrue) r}
  (_shifted a {p} {q}) or (_shifted b {r} {s}) =
              _shifted (a or b) {proof2 p r} {proof3 q s}

  proof1 : {a : Octet} -> {b : Octet} ->
           (_ : lsbclear a IsTrue) -> (_ : lsbclear b IsTrue) -> 
           lsbclear (a or b) IsTrue
  proof1 {allzeros} {allzeros} _ _ = _ 
  proof1 {_ orone} {_} () _
  proof1 {_} {_ orone} _ ()
  proof1 {_ shifted} {_ shifted} _ _ = _
  proof1 {allzeros} {_ shifted} _ _ = _
  proof1 {_ shifted} {allzeros} _ _ = _ 

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

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


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