[Agda] about `abstract'

[Ulf Norell]

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. In
> > this case you might be writing a function on vectors and needing to
> > product a Vec A n from a Vec A (n + 0). That's easy to do given +0,
> > but if it is abstract your function won't evaluate (at compile time,
> > at run-time there's no problem).
>
>
> Please, what precisely is the example?
> Is it to program, say
>
>   f : Vec Bool (2 + 0) → Vec Bool 2
> and
>   bi-f : Bijective f
> ?
> I thought that (Vec A m) and (Vec A n) are considered as different
> domains, but it it possible to program a provable bijection
>

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 ++[].

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