branching on the left vs branching on the right (agda bubble sort part 3)

I gave a definition of onepass, the inner loop of my Agda bubblesort implementation, in an earlier post.

That wasn't the first implementation that I tried.

Instead, first I wrote it like this, in a way that uses with expressions. The difference is that the version I wrote uses an if construct that is manually defined. Agda seems to prefer doing case analysis / branching using with, which makes it seem as if you're getting a new parameter to pattern match on - in the below example, the results of y ≤? y which is either yes _ or no _.

onepass : {n : ℕ}→ Vec ℕ n → Vec ℕ n
  onepass {zero} [] = []
  onepass {suc zero} (y :: []) = y :: []
  onepass {suc (suc n)} (y :: (y' :: y0)) with y ≤? y'
  ... | yes _ = y :: (onepass {suc n} (y' :: y0))
  ... | no _ = y' :: (onepass {suc n} (y :: y0))

For comparison, here's the definition in my first post:

onepass {suc (suc n)} (y :: (y' :: y0)) = if y ≤? y' then        
                                        y :: (onepass {suc n} (y' :: y0))     
                                   else y' :: (onepass {suc n} (y :: y0))  

The two implementations do the same thing at runtime - they swap the first two elements of the list and recurse. But their compile-time behaviour is different.

The with-based version doesn't pass the termination checker. The if-based one does.

The with-based version with with the proofs that I gave in part 2. The if based version doesn't.

So I pretty much am forced to choose: I can use the with-based definition, and turn off the termination checker in the Agda compiler. Or not. Either way seems pretty lame. In order to proof all this stuff, I have to turn off the termination checker which is a key part of checking the proofs that I'm writing.

I don't really understand what is going on inside Agda to make the first version not work. But that's what I actually use in practice (with termination checking turned off) - perhaps I can investigate a bit more later. But for now, I want to continue working on a proof (albeit not termination checked) that bubblesort actually sorts...