[Agda] Propositional equality for coinductive records

[Thorsten Altenkirch]

Interesting. Are there any more details about the cubical development anywhere?

Cheers,
Thorsten

From: Agda <agda-bounces at lists.chalmers.se<mailto:agda-bounces at lists.chalmers.se>> on behalf of Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis at gmail.com<mailto:apostolis.xekoukoulotakis at gmail.com>>
Date: Thursday, 23 February 2017 at 15:42
To: Jannis Limperg <jannis at limperg.de<mailto:jannis at limperg.de>>
Cc: agda list <Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>>
Subject: Re: [Agda] Propositional equality for coinductive records

You can look at the cubical branch and the cubical demos.

https://github.com/Saizan/cubical-demo/blob/master/Stream.agda#L45

You can turn a bisimulation into an equality.

On Thu, Feb 23, 2017 at 5:32 PM, Jannis Limperg <jannis at limperg.de<mailto:jannis at limperg.de>> wrote:
Dear all,

propositional equality for coinductive records is currently extremely
restricted since it is not possible (as far as I can tell) to go from
propositional equality of all fields to equality of the records. For
example, it is impossible to define `R-ext` in the following example due
to the inability to destruct `r` and `s`.


    data ? : Set where tt : ?

    data _≡_ {a} {A : Set a} (x : A) : A → Set a where
      refl : x ≡ x

    record R : Set where
      coinductive
      field force : R

    open R

    R-ext : {r s : R} → force r ≡ force s → r ≡ s
    R-ext = ?

This contrasts with Coq (and probably Agda's old coinduction) which
would allow similar equalities to be exploited.

Now, propositional equality on coinductive data is not often useful
anyway since it is too restrictive for most purposes. However, I have a
corecursive function, say `f`, for which I can prove `force (f x) ≡
force (g x)` for some simpler `g`, and being able to turn this into
`f x ≡ g x` would make it much easier to apply the equation in other
proofs. Reformulating it in terms of a bisimulation (`force r ≡ force s
→ Bisim r s`) would be possible, but much less convenient for users of `f`.

So,

- Has anyone else experienced this problem (and perhaps found a good
workaround)?
- Would it be desirable to recover this form of 'extensionality' for
coinductive records, and if so how could this be done?
- Is adding `R-ext` as an axiom dangerous?

Thanks for your consideration,
Jannis
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170224/e1d0b3eb/attachment-0001.html>