2

In answer to this question Assisting Agda's termination checker the recursion is proven to be well-founded.

Given the function defined like so (and everything else like in Vitus's answer there):

f : ℕ → ℕ
f n = go _ (<-wf n)
  where
  go : ∀ n → Acc n → ℕ
  go zero    _       = 0
  go (suc n) (acc a) = go ⌊ n /2⌋ (a _ (s≤s (/2-less _)))

I cannot see how to prove f n == f ⌊ n /2⌋. (My actual problem has a different function, but the problem seems to boil down to the same thing)

My understanding is that go gets Acc n computed in different ways. I suppose, f n can be shown to pass Acc ⌊ n /2⌋ computed by a _ (s≤s (/2-less _)), and f ⌊ n /2⌋ passes Acc ⌊ n /2⌋ computed by <-wf ⌊ n /2⌋, so they cannot be seen identical.

It seems to me proof-irrelevance must be used somehow, to say that it's enough to just have an instance of Acc n, no matter how computed - but any way I try to use it, it seems to contaminate everything with restrictions (eg pattern matching doesn't work, or irrelevant function cannot be applied, etc).

Community
  • 1
  • 1
Sassa NF
  • 5,306
  • 15
  • 22
  • 2
    Proof irrelevance gets you nowhere, I'm afraid. The restrictions you face are there precisely because irrelevant stuff cannot affect the computation (so no pattern matching, etc). Indeed, `Acc` is quite crucial for the computation. That being said, these proofs are very hard - and that's even when you know the internals. The only advice I currently have is to take a look at the proofs here: http://agda.github.io/agda-stdlib/html/Induction.Nat.html – Vitus Oct 16 '14 at 22:09
  • @Vitus thank you! To start with, I wasn't sure whether I am missing some trick, so that's already a good advice. – Sassa NF Oct 16 '14 at 22:12

0 Answers0