[Agda] matching against _::_ ?

[Andreas Abel]

The difference is that for "lemma", Agda knows

   a' = gen 0
   b' = gen 1

but for "lemma'" it does not know this.

On 08.06.2017 14:24, Sergei Meshveliani wrote:
> On Wed, 2017-06-07 at 23:01 +0200, Andreas Abel wrote:
>> You can use vectors:
>>
>> open import Data.Nat.Base
>> open import Data.Vec
>> open import Function
>>
>> test : ℕ
>> test = case 1 ∷ 2 ∷ 3 ∷ [] of λ where
>>     (a ∷ b ∷ c ∷ _) → a + b + c
> 
> 
> Thank you. This example works with it.
> 
> But my real example does not.
> The two lemmas below differ only in the way in which  a' and b'  are
> bound to their values. The former uses the assignment `=', the latter
> uses matching against a vector.
> Below  []' and _∷'_  are the Vec constructors.
> lemma  is type-checked, and  lemma'  is not.
> 
>    open Ring R
>    ...
>    lemma :  a + b ≈ b + a
>    lemma =  let
>               a' =  gen 0
>               b' =  gen 1
>               e  =  a' :+ b'
>               e' =  b' :+ a'
> 
>               en≡e'n :  nf e ≡ nf e'
>               en≡e'n =  PE.refl
>             in
>             value≈byNF gens e e' en≡e'n
> 
>    lemma' : a + b ≈ b + a
>    lemma' =
>           case  gen 0 ∷' gen 1 ∷' []'
>           of \
>           { (a' ∷' b' ∷' []') →
>                           let e  =  a' :+ b'
>                               e' =  b' :+ a'
> 
>                               en≡e'n :  nf e ≡ nf e'
>                               en≡e'n =  PE.refl
>                           in
>                           value≈byNF gens e e' en≡e'n
>           }
> 
> The report is
> "
> a' != b' of type Expression
> when checking that the expression PE.refl has type
> nf-comm (a' :+ b') ≡ nf-comm (b' :+ a')
> "
> 
> In lemma', the values for a' and b' occur somehow confused.
> 
> Can anyone tell, please, what is happening there?
> 
> Thanks,
>   
> ------
> Sergei
> 
> 

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