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

[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

On Wed, Sep 26, 2018 at 11:18 AM, Shin-Cheng Mu <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