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

[Martin Escardo]

If you abstract from your particular application, the type you are 
considering is that of countably branching trees with leaves in A, which 
arises also in many other applications, either literally or in the form 
of a variation (e.g. labels also in the internal nodes).

One often can get away by considering the relation f ~ g on functions 
defined by f x = g x for all x. The price to pay is that it is not 
automatic that in this case P f -> P g for an arbitrary property P. But 
you will be able to prove this in many specific examples of P that arise 
in your work (I have used this often).

In this way you can get away without function extensionality in many 
cases. However, this doesn't always work or, even when it works, can be 
very inconvenient and "nonmodular".

HoTT/UF is an extension of dependent type theories which addresses 
precisely the problem of extensionality of equality (not only for 
functions, but more generally for types, in the form of univalence).

You can either consistently postulate functional extensionality (but you 
will lose computational content sometimes), or else try the new "Cubical 
Agda", which has extensionality that computes. Unfortunately, at the 
moment this is not very well documented, as it is fairly recent work, 
and hence only the experts know how to use it.

https://agda.readthedocs.io/en/latest/language/cubical.html

Chuangjie Xu has an example of a computation that gets stuck with 
function extensionality, producing a fairly large term (I think 300 
lines), but that computes the number zero when rendered in Cubical Agda.

http://www.cs.bham.ac.uk/~mhe/chuangjie-xu-thesis-cubical/html/index.html

The experiment that computes zero (the modulus of uniform continuity of 
a constant function) is here

http://www.cs.bham.ac.uk/~mhe/chuangjie-xu-thesis-cubical/html/UsingFunext.ModellingUC.ComputationExperiments.html

Martin

On 26/09/18 10:18, scm at iis.sinica.edu.tw wrote:
> 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})
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe