[Agda] Possible extension to pattern matching?

[Adam Gundry]

Hi Andrea,


On 27/02/14 19: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".

You might be interested in this discussion on the Agda issue tracker,
along similar lines:

http://code.google.com/p/agda/issues/detail?id=738


> 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.

(Amusingly my motivation in that issue was to extend the same paper.)


> 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.

Right, if A is uninhabited then the functions are trivially
extensionally equal, so we need to decide type inhabitation...


> Cheers,
> Andrea
> 
> [1]http://dl.acm.org/citation.cfm?id=1863497


All the best,

Adam

-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/