[Agda] Possible extension to pattern matching?

[Andreas Abel]

The unifier for the pattern matching does not do higher-order 
unification, but it does eta-contraction to make some cases work.

There is some possibility for research though...

On 27.02.2014 20:23, Andrea Vezzosi wrote:
> 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
>
>
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Depeartment of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/