How do you make use of a proof of absurdity in Agda for an absurd pattern?

Question

I'm trying to write my own version of foldr1, which takes a non-empty Vec A n (with proof n ≡ zero → ⊥), and a binary operation A → A → A and returns a value of type A. That is:

foldr1 : {A : Set} {n : ℕ} (n ≡ zero → ⊥) → (A → A → A) → Vec A n → A

The issue is, trying to apply the absurd pattern to the case foldr1 p binop [] () the complier says:

Cannot eliminate type A with pattern () (did you supply too many arguments?)

Since the compiler can't deduce absurdity on it's own, I'd like to be able to provide the proof manually, doing something like: foldr1 p binop [] (p refl) where refl : n \equiv zero, but the compiler does not like that syntax.

Is there a way to provide the proof of absurdity manually in Agda to construct absurd patterns? If not, how can I get the compiler to deduce that what I have written is indeed an absurd pattern? My code is something like:

open import Data.Vec
open import Data.Nat
open import Relation.Binary.PropositionalEquality 

data ⊥ : Set where

binfold₁ : {n : ℕ} → {A : Set} → (n ≡ zero → ⊥) → Vec A n → (A → A → A) → A 
binfold₁ p [] _⊗_ ()
binfold₁ p (x ∷ v) _⊗_ = ?

gallais gallais · Accepted Answer · 2017-03-22T17:19:02

You can either define ⊥-elim : {A : Set} → ⊥ → A or use the empty type defined in Data.Empty that already defines it:

open import Data.Vec
open import Data.Nat
open import Data.Empty
open import Relation.Binary.PropositionalEquality 

binfold₁ : {n : ℕ} → {A : Set} → (n ≡ zero → ⊥) → Vec A n → (A → A → A) → A 
binfold₁ p []      _⊗_ = ⊥-elim (p refl)
binfold₁ p (x ∷ v) _⊗_ = {!!}

But you can also pick another type where, instead of asking for a proof n ≡ zero → ⊥, you ask for a vector of type Vec A (suc n):

binfold₁' : {n : ℕ} → {A : Set} → Vec A (suc n) → (A → A → A) → A 
binfold₁' (x ∷ v) _⊗_ = {!!}

How do you make use of a proof of absurdity in Agda for an absurd pattern?

1 Answers