[Agda] Proving properties about a datatype with a functional component

[Shin-Cheng Mu]

Hi,

This is a question that might be related to extensional equality,
and perhaps more. I believe that similar questions must have been
raised in other contexts, but I cannot not find solutions that
work in this case, and therefore decided to pose the question to
the list.

In a simplified form, a "responsive computation" of type A is 
either a value of type A, or a function that takes a signal
from the environment (for example, a Nat, indicating perhaps the
current time) and returns a responsive computation. This can
be modelled by the datatype:

  data RComp (A : Set) : Set where
    V : A → RComp A
    R : (ℕ → RComp A) → RComp A

I wish to prove various operations on RComp, as well as 
proving their properties. For example, we can define an 
"fmap" function for RComp:

  fmap : {A B : Set} → (A → B) → RComp A → RComp B
  fmap f (V x) = V (f x)
  fmap f (R k) = R (fmap f ∘ k)

(The definition passes termination check in Agda 2.5.4.1,
but not in, say, 2.5.2.)

One of the things I wish I can do is to prove that fmap 
is indeed a functorial map. For example, we shall have, 
for all x, fmap id x = x:

  functor1 : ∀ {A} (x : RComp A) → fmap id x ≡ x
  functor1 (V x) = refl
  functor1 (R k) = ?   -- goal: R (fmap id ∘ k) = R k

The base case (V x) is immediate. For the inductive case,
we need to prove 

  R (fmap id ∘ k) = R k

One might try either:
  
  functor1 (R k) = cong R ?                 -- goal: (fmap id ∘ k) ≡ k
  functor1 (R k) = cong (λ g → R (g ∘ k)) ? -- goal: fmap id ≡ id

Either way, extensional equality seems to start being
involved. 

I am not sure about the consequences if I postulate
extensionality. Anyway, if I do:

  postulate
    extensionality :
     {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

I can get the following to type check (where extensionality
is used to convert the recursive call to fmap id ≡ id), 

  functor1 : ∀ {A} (x : RComp A) → fmap id x ≡ x
  functor1 (V x) = refl
  functor1 {A} (R k) = cong (λ g → R (g ∘ k)) ext
    where ext : fmap {A} {A} id ≡ id
          ext = extensionality (functor1 {A})

but this fails termination check.

My question is: how would you formulate this scenario 
and prove the property above?

* Is it okay to postulate extensional equality? 
  I read about some consequences, including losing 
  canonicity, etc. Does that matter to what I want
  to prove, if they are mostly like the functorial
  property above?

* To get around the termination check, is it a 
  wrong idea to formulate RComp as an inductive type? 
  Do I need coinductive type, or the delay monad, or..?

Thank you!

(some test code is attached below)

sincerely, 
Shin
scm at iis.sinica.edu.tw


-----

module RComp where

open import Data.Nat  -- only as an example
open import Relation.Binary.PropositionalEquality

data RComp (A : Set) : Set where
  V : A → RComp A
  R : (ℕ → RComp A) → RComp A

_∘_ : {A B C : Set} → (B → C) → (A → B) → A → C
(f ∘ g) x = f (g x)

fmap : {A B : Set} → (A → B) → RComp A → RComp B
fmap f (V x) = V (f x)
fmap f (R k) = R (fmap f ∘ k)

id : {A : Set} → A → A
id x = x

postulate
  extensionality :
   {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

{-# TERMINATING #-}  -- the following fails termination check
functor1 : ∀ {A} (x : RComp A) → fmap id x ≡ x
functor1 (V x) = refl
functor1 {A} (R k) = cong (λ g → R (g ∘ k)) ext
  where ext : fmap {A} {A} id ≡ id
        ext = extensionality (functor1 {A})