VinaLx
2018-03-29 11:28:10 UTC
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.
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.