Confusion about rewrite mechanism
(too old to reply)
2018-03-29 11:28:10 UTC
Raw Message
Hi everyone!

I'm new to agda and was trying to prove some property related to Data.List.partition like this
partition-++ : ∀ {ℓ} {A : Set ℓ} {xs l r} {p} {P : A → Set p} {p : Decidable P} → (l , r) ≡ partition p xs → SomeProperty A xs (l ++ r)
And I pattern-match on xs, and encountered the problem in the [] case, I try to use rewrite and Data.Product.,-injective as follow:
partition-++ {xs = []} p rewrite ,-injectiveˡ p | ,-injectiveʳ p = ? -- no
but Agda complained about .l != [] as ,-injectiveʳ required.

And I somehow figured out a way out of it:
partition-++ {xs = []} p with ,-injectiveˡ p ... | l≡[] rewrite l≡[] | ,-injectiveʳ p = ?
In this case Agda managed to replace .l with [] and ,-injectiveʳ p type checked.

And my question is:

What's the difference between the first rewrite and the second, why the second rewriting can apply to .l inside of p while the first can't ? What role does with play here?

In this scenario what's the correct solution to this? I don't feel right about mine.