[Agda] using `abstract'

[Andrea Vezzosi]

On Mon, Oct 5, 2015 at 2:41 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> People,
>
> I am trying to understand of whether the `abstract' construct can be
> sensibly used in application.
>
> 1. Last 2 years I complained several times on that `abstract' is allowed
> almost nowhere in my program.
> But today the situation is changed!
> I have tried to put `abstract' to many proofs, and it is type-checked.
> I am not sure, but the impression is that mainly it is allowed now
> (in Agda 2.4.2.4).
>
> 2. I have reported an example of ``abstract case ...'' which probably
> presents a bug.
>
> 3. I wrote earlier that many proofs can be put under `abstract', and
> that this will hopefully reduce the type check cost.
>
> May be this will reduce the cost.
> But I need to understand: what possibilities will be lost?
>
> Consider an example:
>
>   abstract
>     lemma : ∀ {m n : ℕ} → m ∸ n ≡ 0 → m ≤ n
>     lemma {0}     {_}     _     =  z≤n
>     lemma {suc m} {0}     ()
>     lemma {suc m} {suc n} m∸n≡0 =  s≤s $ lemma {m} {n} m∸n≡0
>
> What important possibilities are lost by putting it under `abstract' ?
>
> For example: let
>                   2∸4=0 : 2 ∸ 4 ≡ 0.
> Then,
>       p = (lemma 2∸4=0)  : 2 ≤ 4,
>
> and this is achieved by using `lemma' as abstract.
> Here  p  occurs an _unknown value_ of type  2 ≤ 4.
> Right?

Yeah, in the sense that all you know is that it's built with lemma.

> If `lemma' is not under `abstract', then the program can analyze what
> precisely the construction of  p  is,  for example, how many  s≤s  has
> it in its value.
> Right?

Yes

> In what scopes/modules `abstract' will has its effect in applying this
> `lemma' ?

I don't understand the question

> Can it really happen that a client function will not be satisfied with
> this particular abstracted `lemma' ?

In this case you can prove that all the elements of type  2 ≤ 4 are
equal up to propositional equality, so it should be fine.

> If such clients have sense, then consider the following suggestion.
>

This suggestion is very close to something you can do already, by
defining lemma not under abstract and then define

abstract
   lemma' = lemma

and use lemma' where you would use (abstract lemma).

you can also provide an abstract proof that lemma and lemma' are
propositionally equal.

> 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.
>
> Is it true that `abstract' needs to be a way of applying a function
> and not a way if declaring it?
>
> Can somebody, please, explain the subject?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda