[Agda] Strangeness with corecursion

[Andreas Abel]

The workaround it to put

   {-# OPTIONS --without-K #-}

at the top of your file.

On 2019-03-03 15:01, Thorsten Altenkirch wrote:
> Just a reminder: please do not post solutions to connatural 
> multiplication! I know how to do it but my students may read this 
> mailing list.
> 
> Thorsten
> 
> *From: *"Setzer A.G." <a.g.setzer at swansea.ac.uk>
> *Date: *Sunday, 3 March 2019 at 13:58
> *To: *Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>, 
> "agda at lists.chalmers.se" <agda at lists.chalmers.se>
> *Subject: *Re: Strangeness with corecursion
> 
> Hi,
> 
> what Thorsten reported is clearly a bug.
> 
> I have the feeling it has a lot to do with the with construct.
> 
> My definition of + is as follows, using a for me more intuitive notation 
> (I borrowed some of the musical notation;
> 
> at the end of my paper with Ulrich Berger on undecidability of codata 
> types I discuss how the musical notation can be regarded with minor 
> modifications as a nice abbreviation mechanism - the following 
> definition would with such a mechanism only consist of the definition 
> of coℕand +∞)
> 
>    record coℕ∞ : Set where
>      coinductive
>      field
> ♭: coℕ
> 
> 
>    data coℕ: Set where
>      zero : coℕ
>      suc  : coℕ∞  → coℕ
> 
>    _+∞'_ : coℕ∞ → coℕ→ coℕ∞
> ♭(m +∞' n) = ♭m +∞ n
> 
>    _+∞_ : coℕ→ coℕ→ coℕ
>    zero  +∞ n  = n
>    suc m  +∞ n  = suc (m +∞' n)
> 
> The definition of * is not guarded recursive since in guarded recursion 
> one cannot apply functions to the corecursive call. One can solve this 
> by using sized types, or by unfolding the guarded recursive definition. 
> Here one needs a function plustimes n m k     which computes n + m * k
> 
> Again the suggested abbreviation mechanism would avoid the need for ∞₁' and
> 
>    _*∞₁'_ : coℕ∞ → coℕ→ coℕ∞
> ♭(m *∞₁' n) = ♭m *∞ n
> 
>    _*∞₁_ : coℕ→ coℕ→ coℕ
>    zero  *∞₁ n  = zero
>    suc m  *∞₁ n  = plustimes n m n
> 
>    plustimes' : coℕ∞ → coℕ∞ → coℕ→ coℕ∞
> ♭(plustimes'  n m k) = plustimes (♭n) m k
> 
>    plustimes : coℕ→ coℕ∞ → coℕ→ coℕ
>    plustimes zero m k = ♭(m *∞₁' k)
>    plustimes (suc n) m k = suc (plustimes' n m k)
> 
> Anton
> 
> ------------------------------------------------------------------------
> 
> *From:*Agda <agda-bounces at lists.chalmers.se> on behalf of Thorsten 
> Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk>
> *Sent:* 03 March 2019 12:16:10
> *To:* agda at lists.chalmers.se
> *Subject:* [Agda] Strangeness with corecursion
> 
> Hi,
> 
> I just set the exercise to define multiplication for conats for my 
> course on type theory. So please don’t blurt put the solution – see the 
> attached code. The following is not a solution because agda doesn’t see 
> that the definition is productive (even though it is):
> 
> prd∞ (m *∞ n) with prd∞ m
> 
> prd∞ (m *∞ n) | (just pm) = prd∞ (n +∞ (pm *∞ n))
> 
> prd∞ (m *∞ n) | nothing   = nothing
> 
> but after the following change
> 
> prd∞ (m *∞ n) with prd∞ m
> 
> prd∞ (m *∞ n) | (just pm) with (pm *∞ n)
> 
> prd∞ (m *∞ n) | (just pm) | x = prd∞ (n +∞ x)
> 
> prd∞ (m *∞ n) | nothing   = nothing
> 
> agda seems to accept is. Actually even if +∞ is not contractive.
> 
> Is this a known bug? Otherwise can somebody remind e how to report this?
> 
> Cheers,
> 
> Thorsten
> 
> 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 contact the sender and delete the email and
> 
> attachment.
> 
> Any views or opinions expressed by the author of this email do not
> 
> necessarily reflect the views of the University of Nottingham. Email
> 
> communications with the University of Nottingham may be monitored
> 
> where permitted by law.
> 
> 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 contact the sender and delete the email and
> attachment.
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>