[Agda] The joys and sorrows of abstraction

[Philip Wadler]

Dear Agda mailing list,

I am defining substitution on possibly open terms, and therefore need a way
to generate fresh variable names. The operation

  fresh x xs

returns a name that is similar to x but does not appear in the list xs,
where similar means that it may have extra primes at the end. For example,

  fresh "x" [ "x" , "x′" , "x′′" , "y" ] ≡ "x′′′"

To define `fresh`, I start by defining operations on identifiers and
corresponding lemmas including the following:

  make : Prefix → ℕ → Id
  prefix : Id → Prefix
  suffix : Id → ℕ

  prefix-lemma : ∀ {p n} → prefix (make p n) ≡ p
  suffix-lemma : ∀ {p n} → suffix (make p n) ≡ n
  make-lemma : ∀ {x} → make (prefix x) (suffix x) ≡ x

Prefix is defined to be a String that does not end in a prime.

The definitions of make, prefix, and suffix are quite involved, so in order
to prevent them expanding to unreadable length in proofs I have made them
and the corresponding lemmas abstract. Doing so, the proof was fairly easy
to complete. However, because the definitions are abstract, Agda cannot
actually compute fresh variables as in the example above.

That's ok. Having completed the proofs with readable terms, I should be
able to now remove the abstract declaration. Since everything typechecked
before, revealing the definition bodies should preserve types. But in fact,
Agda now complains about one of the key proofs!

Is there any way to *both* be able to compute fresh names *and* retain my
related proofs, in particular, the proof that `fresh x xs` generates a name
not in `xs`?

The relevant files are attached, or can be found at

  https://github.com/wenkokke/sf

Thank you for your help! 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/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180515/0cc31d6a/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: FreshId.lagda
Type: application/octet-stream
Size: 4437 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180515/0cc31d6a/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Collections.lagda
Type: application/octet-stream
Size: 6501 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180515/0cc31d6a/attachment-0001.obj>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180515/0cc31d6a/attachment.ksh>