[Agda] Possible extension to pattern matching?

[Andrea Vezzosi]

Hi,

currently agda won't accept code like this:

test0 : ∀ {F : ℕ -> ℕ} -> (\ x -> suc (F x)) ≡ (\ x -> suc (suc x)) -> ℕ
test0 {.suc} refl = ?

reporting that "F x" is not the same as "suc x".

Interestingly we can actually derive "F  ≡ suc" through "cong (\ f x ->
pred (f x)) p", and in general instead of pred we can use a function like
strip

strip x (con y) = y
strip x _ = G x

to handle equations like (\x -> con (F x)) ≡ (\x -> con (G x)).

Such equations come up all the time when trying to do induction on
representations in the style of "Outrageous but Meaningful
Coincidences"[1], so it'd be nice to have native support.

It would actually be great to be able to recognize as empty things like
(\ (x : A) -> true) ≡ (\ x -> false), but that seems refutable only when
you have an element of A.


Cheers,
Andrea

[1]http://dl.acm.org/citation.cfm?id=1863497
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140227/6b0480a1/attachment.html