[Agda] Need help completing a proof

[Philip Wadler]

Fantastic! Trust this group to find the answer quickly. Thank you very much!

But I thought rewrite was an abbreviation for using a with to match refl,
and rewrite did not work. What is the difference?

Go well, -- 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 Fri, 24 Dec 2021 at 18:23, Miëtek Bak <mietek at bak.io> wrote:

> This email was sent to you by someone outside the University.
> You should only click on links or attachments if you are certain that the
> email is genuine and the content is safe.
>
> In this case, the simplest solution seems to be using with-abstraction to
> pattern match on the result of `equation`, in order to let Agda take the
> desired equality `G ≡ H` into account.
> https://agda.readthedocs.io/en/latest/language/with-abstraction.html
>
> ```diff
> --- Example-before.lagda.md
> +++ Example-after.lagda.md
> @@ -147 +147,2 @@
> -example g h p q s t M e = {!!}
> +example g h p q s t M e with equation g h p q s t e
> +... | refl = ⟨ (M ↑ p) ↓ q , collapse g h ⟩
> ```
>
> --
> MB
>
>
> On Fri, Dec 24, 2021, at 18:03, Philip Wadler wrote:
> > I'm having trouble completing a proof, and would be grateful for help.
> > The problem arises because I need to show two values are equal, but the
> > equality of the values follows from a complex equation. In fact, it is
> > not hard to show that the equality follows from the equation, but when
> > I attempt to use the desired equality for rewriting Agda complains and
> > I can't work out what it is complaining about (or how to fix it).
> >
> > A complete example is attached. The original is more complex, I've
> > tried to boil it down to its simplest form. My apologies that the
> > simplest form is not so simple!
> >
> > Thank you for your help. Go well, -- 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/
> >
> > 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
> >
> > Attachments:
> > * Example.lagda.md
> _______________________________________________
> 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/20211224/67eeb996/attachment-0001.html>