[Agda] using `abstract'

[Martin Escardo]

On 05/10/15 13:41, Sergei Meshveliani wrote:
> 4. Suppose that the Language allows ``applying as abstract''
>    and also ``applying as concrete''
>    -- instead of declaring a function being `abstract'.
> 
> For example:
> 
>     p =  lemma 2∸4=0
>     <do something with  p>
> 
>     p' = (abstract lemma) 2∸4=0
>     <do something with  p'>
> 
> The word `abstract' is not in the declaration of `lemma', but it is set
> at the place where `lemma' is applied.
> The first call of `lemma' applies the concrete version, and the second
> call applies the abstract version.
> 
> This is on the user program decision: where the abstract version is
> sufficient and where is not. It depends on the situation, on the meaning
> of the program fragment.

You can actually implement "abstract lemma" in Agda as it is. I will
write "Abstract lemma" instead:

\begin{code}

module abstractor where

open import Agda.Primitive using (Level ; lzero ; lsuc ; _⊔_)

Abstract : {i : Level} {X : Set i} → X → X
Abstract {i} {X} x = y
 where
  abstract
   y : X
   y = x

\end{code}

Silly example to try to demonstrate this:

\begin{code}

data _≡_ {i : Level}{X : Set i} : X → X → Set i where
 refl : {x : X} → x ≡ x

data ℕ : Set where
 zero : ℕ
 succ : ℕ → ℕ

example : succ zero ≡ Abstract(succ zero)
example = ?

\end{code}

The proof "refl" is not accepted in the example.

Martin