<div dir="ltr"><div>Dear Agda mailing list,</div><div><br></div><div>I am defining substitution on possibly open terms, and therefore need a way to generate fresh variable names. The operation</div><div><br></div><div>  fresh x xs</div><div><br></div><div>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,</div><div><br></div><div>  fresh "x" [ "x" , "x′" , "x′′" , "y" ] ≡ "x′′′"</div><div><br></div><div>To define `fresh`, I start by defining operations on identifiers and corresponding lemmas including the following:</div><div><br></div><div><div>  make : Prefix → ℕ → Id</div><div>  prefix : Id → Prefix</div><div>  suffix : Id → ℕ</div><div><br></div><div>  prefix-lemma : ∀ {p n} → prefix (make p n) ≡ p</div><div>  suffix-lemma : ∀ {p n} → suffix (make p n) ≡ n</div><div>  make-lemma : ∀ {x} → make (prefix x) (suffix x) ≡ x</div></div><div><br></div><div>Prefix is defined to be a String that does not end in a prime.<br></div><div><br></div><div>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.</div><div><br></div><div>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!</div><div><br></div><div>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`?</div><div><br></div><div>The relevant files are attached, or can be found at</div><div><br></div><div>  <a href="https://github.com/wenkokke/sf">https://github.com/wenkokke/sf</a></div><div><br></div><div>Thank you for your help! Cheers, -- P</div><div><br></div><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
</div>