[Agda] Termination not being proven

[Will Sonnex]

Hi Dan,

Thanks for the response; annoying that Agda's termination checker
can't figure this one out.

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

I've hit another problem though and I thought I'd share it to see if
anyone had any insight. Here's my code-base:

insort : Nat → List Nat → List Nat
insort n [] = n ∷ []
insort n (x ∷ xs) with inspect (n <= x)
... | True with-≡ _ = n ∷ (x ∷ xs)
... | False with-≡ _ = x ∷ (insort n xs)

sorted : List Nat → Bool
sorted [] = True
sorted (_ ∷ []) = True
sorted (x ∷ (y ∷ ys)) with inspect (x <= y)
... | True with-≡ _ = sorted (y ∷ ys)
... | False with-≡ _ = False

con : {A : Set} → False ≡ True → A
con ()

prop : {x : Nat} {y : Nat} {ys : List Nat}
  → x <= y ≡ True → sorted (insort x (y ∷ ys)) ≡ sorted (y ∷ ys)
prop {x} {y} {ys} φ with inspect (x <= y)
... | True with-≡ _ = refl
... | False with-≡ φ' = con (trans φ' φ)

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?

Anyway my real problem is that I would like to solve this by breaking
the normalisation step up like so:

prop : {x : Nat} {y : Nat} {ys : List Nat}
  → x <= y ≡ True → sorted (insort x (y ∷ ys)) ≡ sorted (y ∷ ys)
prop {x} {y} {ys} φ with inspect (x <= y)
... | True with-≡ _ = prop'
  where
  prop' : sorted (x ∷ (y ∷ ys)) ≡ sorted (y ∷ ys)
  prop' = refl
... | False with-≡ φ' = con (trans φ' φ)

But Agda seems to forget the outer pattern match when it moves into
the "where" definitions, so the "refl" doesn't work any more. This is
almost a deal-breaker for my proof output, since my proof system
remembers all previous pattern matches implicitly within its
sub-proofs. I have a way around it, whereby I re-pattern match and
then close all the invalid branches with the earlier inspected
equivalences, but it is messy (in my proof output I would have to
re-do this every time I use an outer pattern match in an inner
sub-proof):

prop : {x : Nat} {y : Nat} {ys : List Nat}
  → x <= y ≡ True → sorted (insort x (y ∷ ys)) ≡ sorted (y ∷ ys)
prop {x} {y} {ys} φ with inspect (x <= y)
... | True with-≡ _ = prop'
  where
  prop' : sorted (x ∷ (y ∷ ys)) ≡ sorted (y ∷ ys)
  prop' with inspect (x <= y)
  ... | True with-≡ _ = refl
  ... | False with-≡ φ' = con (trans φ' φ)
... | False with-≡ φ' = con (trans φ' φ)


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


Cheers,

Will



On 27 February 2011 21:21, Dan Licata <drl at cs.cmu.edu> wrote:
> Hi Will,
>
> I think the problem is with the 'with'.  The 'with' gets compiled as a
> helper function, and I think what is happening is that both y and ys are
> getting passed as separate arguments to the helper function, so Agda
> loses sight of the fact that, when you put them back together, what you
> get is something smaller than the input.
>
> For example, if you rewrite it as follows:
>
>  sorted' : List Nat -> Bool
>  sorted' [] = True
>  sorted' (x :: t) with t
>  ... | [] = True
>  ... | y :: xs with lte x y
>  ...              | True = sorted' t
>  ...              | False = False
>
> (sorry for switching notation to my library)
>
> then it termination-checks.
>
> The nicest way to write it is to define _andalso_ : Bool -> Bool -> Bool
> and then avoid using a 'with' at all:
>
>  sorted'' : List Nat -> Bool
>  sorted'' [] = True
>  sorted'' (x :: []) = True
>  sorted'' (x :: y :: xs) = lte x y andalso sorted'' (y :: xs)
>
> In this version Agda spots what you want it to.
>
> Make sense?
> -Dan
>
> On Feb27, Will Sonnex wrote:
>> I have a structurally recursive function which checks whether a list
>> is sorted, but Agda tells me it cannot prove termination:
>>
>> _<=_ : ℕ → ℕ → Bool
>> zero <= _ = true
>> suc x <= zero = false
>> suc x <= suc y = x <= y
>>
>> sorted : List ℕ → Bool
>> sorted [] = true
>> sorted (_ ∷ []) = true
>> sorted (x ∷ (y ∷ ys)) with x <= y
>> ... | true = sorted (y ∷ ys)
>> ... | false = false
>>
>>
>> It seems strange to me that Agda can show "xs ≺ x :: xs" but not "y ::
>> ys ≺ x :: (y :: ys)", since the former is a more general case of the
>> latter.
>>
>>
>