[Agda] wishlist/some help wanted

[Nils Anders Danielsson]

On Sat, Apr 26, 2008 at 10:31 PM, Tristan Wibberley
<tristan at wibberley.org> wrote:

>  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"?

If a function is defined using wildcards, then the wildcards often
have to be expanded when you want to prove something about the
function, because otherwise the function does not evaluate in the type
of the proof. (Your situation is similar.)

There were plans to change the semantics of pattern matching so that
these wildcards were implicitly expanded (i.e. to expand catch-all
cases in case trees, using information obtained from the completeness
checker). This would take care of your problem here. I don't know what
the current status of these plans are, though.

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

Agda only instantiates things for you when there is a unique solution.
It uses unification to accomplish this. In the simplest setting you
can only unify two things if one is a variable, or both are
applications of the same constructor to unifiable things (*). In
particular, a function application is (almost) never unifiable with
another one. Just because you know that f x = f y does not mean that
x = y, for instance.

If you want things to be automatically inferred, then you should make
sure that unification can do the inference.

(*) Agda is a bit more clever than this. I don't think anyone has
written down a simple explanation of how unification works in Agda,
but you can read Ulf's thesis for a technical, not entirely up-to-date
description.

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

This is because nothing gets structurally smaller in the recursive
call. There are many ways to handle this problem:

* Use an eliminator which captures the recursion structure which you
  have in mind (untested code):

  elimT<F : {a : Set}
            (P : a -> Set) ->
            P true ->
            (P true -> P false) ->
            (b : Bool) -> P b
  elimT<F P t f true  = t
  elimT<F P t f false = f t

* Use a type which ensures that the recursive call is on a
  structurally smaller argument:

  data Bool : Set where
    true  : Bool
    false : (b : Bool) -> b ≡ true -> Bool

  (This is more of a hack, at least in this case.)

* The sledge-hammer approach: Use well-founded induction, or "Ana's
  method". Unnecessary in this case.

* Rewrite your algorithm so that it becomes structurally recursive.
  Not always easy, but can be pleasant if it works.

In this case I would recommend you to get rid of the recursive call
entirely.

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

I don't follow you here. Can you give an example?

-- 
/NAD