[Agda] The joys and sorrows of abstraction

[Ulf Norell]

In your case the reason the proof fails without `abstract` is that the
`rewrite` doesn't trigger.
Here's a simpler example exhibiting the same behaviour:

module _ where

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

module WithAbstract where

  abstract
    f : Nat → Nat
    f zero    = zero
    f (suc n) = suc (f n)

    lem : ∀ n → f n ≡ n
    lem zero    = refl
    lem (suc n) rewrite lem n = refl

  thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
  thm m n rewrite lem (suc m) = refl
  -- Works.

module WithoutAbstract where

  f : Nat → Nat
  f zero    = zero
  f (suc n) = suc (f n)

  lem : ∀ n → f n ≡ n
  lem zero    = refl
  lem (suc n) rewrite lem n = refl

  thm : ∀ m n → f (suc m) + n ≡ suc (m + n)
  thm m n rewrite lem (suc m) = refl
  -- Fails since rewrite doesn't trigger:
  --   lem (suc m)  : suc (f m)     ≡ suc m
  --   goal         : suc (f m + n) ≡ suc (m + n)

In general I think it's optimistic to expect tactics (of which rewrite is
an example) to be stable under substitution.

/ Ulf


On Wed, May 16, 2018 at 9:24 PM, Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> Thanks, Martin. So which fragment do you recommend? Cheers, -- P
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
> On 16 May 2018 at 16:03, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>
>>
>>
>> On 16/05/18 20:37, Philip Wadler wrote:
>>
>>> Thanks for following up. It is the latter case. But I don't understand
>>> why it should be ok for that to fail. Removing abstract should just replace
>>> some abstract terms by their concretions, which have already been type
>>> checked. Everything that was provably equal before should still be equal,
>>> so why is it ok for the proof of equality to now fail? Doesn't this violate
>>> stability under substitution? Cheers, -- P
>>>
>>
>> It is because of things such as this that I prefer to restrict my usage
>> of Agda to a fragment corresponding to a well-understood type theory.
>>
>> This may be limiting in terms of expressivity, conciseness, and
>> efficiency, but at least one can tell whether something is a bug or not,
>> rather than a bug or a feature.
>>
>> :-)
>> Martin
>>
>>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180516/3815dff9/attachment.html>