[Agda] about `abstract'

[Ulf Norell]

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)

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160303/f44b4a3c/attachment.html