[Agda] Codata and "with" matching

[Shin-Cheng Mu]

Hi,

On proving the unfold fusion theorem:

unfoldˢ-fusion : {A B C : Set} {f : B -> A × B} {h : C -> B} {g : C - 
 > A × C} ->
   (forall x -> f (h x) ≡ map-× id h (g x)) ->
     (forall x -> unfoldˢ f (h x) ∼ unfoldˢ g x)

On Sep 3, 2008, at 2:35 AM, Nils Anders Danielsson wrote:
> If the with expression is not mentioned anywhere in the context when
> you do with, then with does not have any effect on the types.

Hmm... I am still confused, but I guess your hint has something
to do with putting the with expression in the right context.
So I tried some code rearrangements.

It turns out that the proof works if I isolate the two arguments
to bisim in where clauses:

   unfoldˢ-fusion {f = f} {h = h} {g = g} fuse x ~ bisim pf1 pf2
     where pf1 : head (unfoldˢ f (h x)) ≡ head (unfoldˢ g x)
           pf1 with f (h x) | g x | fuse x
           ... | ._ | (i , j) | ≡-refl ~ ≡-refl
           pf2 : tail (unfoldˢ f (h x)) ∼ tail (unfoldˢ g x)
           pf2 with f (h x) | g x | fuse x
           ... | ._ | (i , j) | ≡-refl ~ unfoldˢ-fusion fuse j

1. If I define pf1 using "=" rather than "~", I get:

      Not implemented: mutual recursion and corecursion

    I understand that pf2 should be defined corecursively since
    it is where the (co)recursive call is made. For pf1, however,
    I thought both should be fine. Is it a rule now that all local
    definitions in a (co)recursively defined function must be
    (co)recursively defined as well?

2. Rather than isolating pf1 and pf2, I hoped to do something
    like this:

      unfoldˢ-fusion {f = f} {h = h} {g = g} fuse x
            with f (h x) | g x     | fuse x
      ...      | ._      | (i , j) | ≡-refl  ~
                 bisim {| ≡-refl |}  {| unfoldˢ-fusion fuse j |}

     However, the first interaction point has type:

     ?0 : (.Relation.Binary.Core._≡_ (head (unfoldˢ f (h x) | f (h  
x)))
          (head (unfoldˢ g x | g x)))

     Thus Agda refused to let me fill ≡-refl in. Similarly with
     the section interaction point. What made the difference?

Thanks!

sincerely,
Shin