[Agda] about `abstract'

[Sergei Meshveliani]

On Wed, 2016-03-02 at 16:14 +0100, Ulf Norell wrote:
> 
> 
> On Mon, Feb 29, 2016 at 9:31 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         On Mon, 2016-02-29 at 19:40 +0100, Ulf Norell wrote:
>         >
>         > On Mon, Feb 29, 2016 at 2:27 PM, Sergei Meshveliani
>         <mechvel at botik.ru>
>         > wrote:
>         >
>         >         2. The given proof for  two+0  is constructed only
>         from the
>         >         signature of
>         >            +0.  Hence  +0  can be placed under
>         `abstract' (for this
>         >         example).
>         >
>         >         Also I expect that the implementation part for  +0
>         will not
>         >         be used
>         >         anywhere in type-checking any future client
>         function, the type
>         >         checker
>         >         will be satisfied with the signature of  +0.
>         >
>         >         Can you imagine the necessity of using the
>         implementation
>         >         rules for 0+
>         >         in type checking something?
>         >
>         >
>         > There are certainly cases where you need equality proofs  
>         > to reduce. 
>         > []


> Here's a concrete example:
> 
> open import Data.Nat
> open import Data.Vec
> open import Relation.Binary.PropositionalEquality
> 
> abstract
>   +0 : ∀ n → n + 0 ≡ n
>   +0 zero    = refl
>   +0 (suc n) = cong suc (+0 n)

> module _ {a} {A : Set a} where

>   castVec : ∀ {m n} → m ≡ n → Vec A m → Vec A n
>   castVec refl xs = xs

>   ++[] : ∀ {n} (xs : Vec A n) → castVec (+0 n) (xs ++ []) ≡ xs
>   ++[] [] = ?  -- castVec (+0 0) [] ≡ []  cannot be proven with refl
>   ++[] (x ∷ xs) = ?  -- similar problems
> 
> 
> Since +0 is abstract, castVec doesn't evaluate so you can't prove this
> formulation of ++[].
> 

And what proof is possible when `abstract' is removed?
I do not find such, so far:

  ++[] : ∀ {n} (xs : Vec A n) → castVec (+0 n) (xs ++ []) ≡ xs
  ++[] {_}     []       = refl
  ++[] {suc n} (x ∷ xs) = goal
       	    where
            eq : castVec (+0 n) (xs ++ []) ≡ xs
            eq = ++[] xs

            goal :  castVec (cong suc (+0 n)) ((x ∷ xs) ++ []) ≡  x ∷ xs
        
            goal = ?   -- refl             ?
                       -- cong (_∷_ x) eq  ?
   
Thanks,

------
Sergei