[Agda] wishlist/some help wanted

[Tristan Wibberley]

Hi all,

I've got 4 problems/issues below.

1) flipor has to have every case listed on its own or it won't
typecheck. Is there a way to say "in all other cases"? Magic With almost
does it, but doesn't work when there are predicates.

2) flipor must be called with the two Bools as flipor {true} {false} p.
Is there a way to have it deduce the bools from the proof object (I know
flipor isn't needed here, but in more complex cases, it is - I think).

3) secondofatrueor (second of a true or) doesn't pass the termination
checker.

4) It seems that sometimes for some proof object "p" proving a predicate
"P", when "P => Q", "p" is also a proof object of "Q", yet other times
it isn't. Is it possible to add a feature where the programmer always
has to write a proof strategy from P to Q and it will always be used
without having to use its name if agda has a proof of P and needs a
proof of Q. Perhaps these implications could be used automatically when
the source inhabits the same type as the target and that type is
inhabited only by one proof object, such as with "True" below.

Can anybody help me with them - if there is no solution currently is
there anything that can be done to make them solvable in the future in
terms of feature additions?


module logic where

data Bool : Set where
  true : Bool
  false : Bool

_||_ : Bool -> Bool -> Bool
_||_ true _      = true
_||_ _ true      = true
_||_ false false = false

_&&_ : Bool -> Bool -> Bool
_&&_ false _   = false
_&&_ _ false   = false
_&&_ true true = true

!_ : Bool -> Bool
!_ false = true
!_ true  = false

data False : Set where
record True : Set where

_istrue : Bool -> Set
_istrue true = True
_istrue false = False

flipor : {a : Bool} -> {b : Bool} ->
         (_ : (a || b) istrue) ->
         (b || a) istrue
flipor {false} {false} ()
flipor {_} {_} _ = _
-- flipor {true}  {false} _  = _
-- flipor {false} {true}  _  = _
-- flipor {true}  {true}  _  = _

secondofatrueor : (a : Bool) -> (b : Bool) ->
                  {_ : (a || b) istrue} ->
                  Bool
secondofatrueor false false {}
secondofatrueor true false     = false
secondofatrueor false true {p} = !(secondofatrueor true false
                                     {flipor {- {true} {false} -} p})
secondofatrueor true true      = true

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