[Agda] matching against _::_ ?

[Andreas Abel]

You can use recursively defined vectors and let:

open import Data.Nat.Base
open import Data.Nat.Properties.Simple using (+-assoc)
open import Data.Product
open import Data.Unit

open import Function

open import Relation.Binary.PropositionalEquality using (_≡_)

infixr 1 _∷_

record V0 : Set where
   constructor []

record VS (A B : Set) : Set where
   constructor _∷_
   field head : A
         tail : B

RVec : (A : Set) (n : ℕ) → Set
RVec A zero    = V0
RVec A (suc n) = VS A (RVec A n)

postulate
   suc-assoc :  (x y z : ℕ) →
                (suc x + suc y) + suc z ≡ suc x + (suc y + suc z) →
                (x + y) + z ≡ x + (y + z)

test : (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
test a b c =
   let (a' ∷ b' ∷ c' ∷ []) = RVec _ 3 ∋ suc a ∷ suc b ∷ suc c ∷ []
       eq :  (a' + b') + c' ≡ a' + (b' + c')
       eq =  +-assoc a' b' c'
   in  suc-assoc a b c eq


On 08.06.2017 18:34, Sergei Meshveliani wrote:
> open import Relation.Binary.PropositionalEquality using (_≡_)
> open import Data.Nat.Base
> open import Data.Nat.Properties.Simple using (+-assoc)
> open import Data.Vec
> open import Function
> 
> postulate
>    suc-assoc :  (x y z : ℕ) →
>                 (suc x + suc y) + suc z ≡ suc x + (suc y + suc z) →
>                 (x + y) + z ≡ x + (y + z)
>    -- contrived
> 
> test1 : (a b c : ℕ) → (a + b) + c ≡ a + (b + c)   -- contrived
> test1 a b c =
>              let a' = suc a
>                  b' = suc b
>                  c' = suc c
> 
>                  eq :  (a' + b') + c' ≡ a' + (b' + c')
>                  eq =  +-assoc a' b' c'
>              in
>              suc-assoc a b c eq
> 
> test2 : (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
> test2 a b c =
>            case  suc a ∷ suc b ∷ suc c ∷ []  of \
>            where
>            (a' ∷ b' ∷ c' ∷ []) →
>                 	       	let eq :  (a' + b') + c' ≡ a' + (b' + c')
>                              eq =  +-assoc a' b' c'
>                          in
>                          suc-assoc a b c eq

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

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

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/