[Agda] about `abstract'

[Sergei Meshveliani]

On Thu, 2016-03-03 at 13:38 +0100, Ulf Norell wrote:
> 
> 
> On Thu, Mar 3, 2016 at 1:12 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         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  ?
> 
> 
> How about
> 
> 
>   castVec-∷ : ∀ {m n} (eq : m ≡ n) x (xs : Vec A m) →
>                  castVec (cong suc eq) (x ∷ xs) ≡ x ∷ castVec eq xs
>   castVec-∷ refl _ _ = refl

>   ++[] : ∀ {n} (xs : Vec A n) → castVec (+0 n) (xs ++ []) ≡ xs
>   ++[] [] = refl
>   ++[] (_∷_ {n} x xs) rewrite castVec-∷ (+0 n) x (xs ++ []) = 
>                                               cong (x ∷_) (++[] xs)
> 

It is type-checked. Thank you.

------
Sergei