[Agda] Termination not being proven

[Nils Anders Danielsson]

On 2011-02-28 16:43, Will Sonnex wrote:
> I'm currently trying to develop an Agda output for an automated
> theorem prover I've been working on for Haskell programs
> (http://www.doc.ic.ac.uk/~ws506/tryzeno), so I've elected to just
> split my proof output and program mapping into separate files and only
> termination-check the proofs, since I might have to work with
> non-terminating definitions anyway (is this sound? I think so...).

No. Your programs could contain arbitrary ill-founded code:

   inhabited : {A : Set} → A
   inhabited = inhabited

Using inhabited one can prove anything (which fits in Set).

If you want to ensure soundness, then you need to represent partial
functions in some "safe" way, for instance by introducing a term
representation for a partial language, or by using the partiality monad.

> My "refl" on the first branch of "prop" complains that it cannot match
> sorted (x :: (y :: ys)) to sorted (y :: ys). I can see where the
> problem is here I think, in that it beta-normalises the inner term
> "insort x (y ∷ ys)" to "x :: (y :: ys)" but then doesn't retry
> normalising the outer one, maybe a bug?

No. The with construct is just fancy syntactic sugar which expands into
a helper function. If you want to understand how with works, then I
think it would be a useful exercise to write the helper functions
associated with your code manually.

> But Agda seems to forget the outer pattern match when it moves into
> the "where" definitions, so the "refl" doesn't work any more.

The only way in which Agda "remembers" a pattern match is if some
unification happens as a result of the match.

> Wondered if anyone had any insight. Should I submit a feature request
> for pattern matches to stay in scope inside inner definitions?

http://code.google.com/p/agda/issues/detail?id=239

-- 
/NAD