[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
***@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})

[Andrea Vezzosi]

You can get functor1 to termination check like this:

functor1 : ∀ {A} (x : RComp A) → fmap id x ≡ x
functor1 (V x) = refl
functor1 {A} (R k) = cong R (extensionality (\ x → functor1 (k x)))

Now the recursive call is on (k x) which is recognized as smaller than (R k).

The consequence of postulating extensionality is that if you "subst"
with such an equality proof it will be stuck like that.
(Though you might still be able to generalize your goal and pattern
match the equality proof away).

If you are using Agda mostly to verify properties of simply-typed
programs then this should be less of a problem, because you won't have
to reason about how your proofs compute.

Cheers,
Andrea

Post by 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
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 : {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,
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
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
postulate
{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
-----
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
{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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by 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
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 : {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,
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
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
postulate
{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
-----
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
{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
https://lists.chalmers.se/mailman/listinfo/agda