[Agda] Pattern matching on irrelevant data

[Andreas Abel]

Hi folks,

I just pushed a patch that allows one to match on an irrelevant 
argument, under the proviso that only one constructor matches.

The reason why I implemented this feature is because I want to define 
functions by recursion on a deterministic termination predicate but not 
prove that its value does not depend on the derivation of that predicate.

Please play around with this new feature and find bugs and 
inconsistencies. ;-)

Here is an example (good old division, without sized types, but 
Bove-Capretta style):

module Div where

data _≡_ {A : Set}(a : A) : A → Set where
   refl : a ≡ a

data Nat : Set where
   zero : Nat
   suc  : Nat → Nat

minus : Nat → Nat → Nat
minus  zero    m      = zero
minus (suc n)  zero   = suc n
minus (suc n) (suc m) = minus n m

{- definition we'd like to have, does not termination check
div : Nat → Nat → Nat
div zero    m = zero
div (suc n) m = suc (div (minus n m) m)
-}

-- termination predicate

data Div! (m : Nat) : Nat → Set where
   zero : Div! m zero
   suc  : ∀ {n} → Div! m (minus n m) → Div! m (suc n)

div' : (n m : Nat) → .(Div! m n) → Nat
div'  zero   m  zero   = zero
div' (suc n) m (suc N) = suc (div' (minus n m) m N)

-- irrelevance of termination argument

irrDiv! : (n m : Nat)(d d' : Div! m n) → div' n m d ≡ div' n m d'
irrDiv! n m d d' = refl

Pay attention to the last line!
We could have gotten the same result without irrelevance, but much more 
tedious.

Here is another example, involving a universe definition:
( in test/succeed/)

module TerminationOnIrrelevantArgument where

data ⊥ : Set where

data D : Set where
   empty : D
   pi    : D -> D -> D
   other : D

postulate
   app : D -> D -> D

mutual

   data Ty : D -> Set where

     Empty : Ty empty

     Pi    : (a f : D) ->
             (A : Ty a) ->
             (F : (d : D) -> .(El a A d) -> Ty (app f d)) ->
             Ty (pi a f)


   El : (a : D) -> .(A : Ty a) -> D -> Set
   El  empty    Empty         g = ⊥
   El (pi a f) (Pi .a .f A F) g = (d : D) -> .(Ad : El a A d) ->
                                  El (app f d) (F d Ad) (app g d)
   El  other   ()             g

-- Termination checking needs to look inside irrelevant arguments.
-- This only works because the termination checker is syntactic
-- and does not respect equality of irrelevant things!

-- clearly, the derivation of Ty a does not matter when computing El
cast : (a : D)(A A' : Ty a)(d : D) -> El a A d -> El a A' d
cast a A A' d x = x

Cheers,
Andreas

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

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