[Agda] matching against _::_ ?

[Sergei Meshveliani]

On Thu, 2017-06-08 at 16:01 +0200, Andreas Abel wrote:
> The difference is that for "lemma", Agda knows
> 
>    a' = gen 0
>    b' = gen 1
> 
> but for "lemma'" it does not know this.



Please, consider this example:


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

test2  tries to gather many assignments
(three assignments in this example) into matching against a vector.
But as you write, Agda does not know that  a' = suc a, b' = suc b; ...

The goal is clear. What may be a way out?

Thanks,

------
Sergei