[Agda] matching against _::_ ?

[Sandro Stucki]

On Thu, Jun 8, 2017 at 6:34 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> 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?

I'm not sure I understand your question correctly, but if you're just
trying collect multiple let-definitions in one line, using products
instead of vectors/lists might help:

-------------------------------------------------------------------
-- ...
open import Data.Product using (_,_; _,′_)

-- ...
test2 : (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
test2 a b c =
            let a' , b' , c' = 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

-------------------------------------------------------------------

You can avoid the use of _,′_ by defining your own (non-dependent) product type.

I hope this helps
/Sandro


> Thanks,
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda