[Agda] Coinduction and Instance Arguments - is it possible?

[Apostolis Xekoukoulotakis]

I have a datatype (called "Bob") that tracks whether a variable has been
used or not.
I have an index datatype that points to multiple variables in the datatype
Bob without depending on the datatype "Bob" so as to not become invalid
when "Bob" changes to reflect the unavailability of a variable.

The datatype "Belongs" depends on an Index and Bob. It proves that all the
variables pointed by the index are actually available.

Every time Bob, changes, a new Belongs datatype is needed. I want this
proof to be generated by instance resolution.

I am not sure if this is possible when the index points to an infinite
number of variables, ie if we have coinductive types.

Here is the example.

-------------------------

module Test where

open import Data.Bool
open import Size

mutual

  data Bob (i : Size) : Set where
    more : Bob i → Bool → Bob i
    none : Bob i
    twoPaths : Bob i → Bob i → Bob i
    inf : Bob∞ i → Bob i

  record Bob∞ (i : Size) : Set where
    coinductive
    field
      bob : {j : Size< i} → Bob j

open Bob∞

data Bel : Set where
  bel : Bel
  nbel : Bel

mutual

  data Index (i : Size) : Set where
    here : Index i
    more : Index i → Bel → Index i
    left : Index i → Index i
    right : Index i → Index i
    inf : Index∞ i → Index i

  record Index∞ (i : Size) : Set where
    coinductive
    field
      index : {j : Size< i} → Index j

open Index∞

mutual

  data Belongs {i : Size} : Index i → Bob i → Set where
    instance
      here : ∀{b} → Belongs here (more b true)
      moreBel : ∀{ind b} → {{is : Belongs ind b}} → Belongs (more ind bel)
(more b true)
      morenBel : ∀{ind b bool} → {{is : Belongs ind b}} → Belongs (more ind
nbel) (more b bool)
      left : ∀{ind bl br} → {{is : Belongs ind bl}} → Belongs (left ind)
(twoPaths bl br)
      right : ∀{ind bl br} → {{is : Belongs ind br}} → Belongs (right ind)
(twoPaths bl br)
      inf : ∀{ind∞ bob∞} → {{is∞ : Belongs∞ ind∞ bob∞}} → Belongs (inf
ind∞) (inf bob∞)

  record Belongs∞ {i : Size} (ind∞ : Index∞ i) (bob∞ : Bob∞ i) : Set where
    coinductive
    field
      belongs : {j : Size< i} → Belongs (index ind∞) (bob bob∞)

open Belongs∞

mutual

  b : ∀{i} → Bob i
  b = more (inf b∞) true

  b∞ : ∀{i} → Bob∞ i
  bob b∞ = b


mutual

  ind : ∀{i} → Index i
  ind = more (inf ind∞) bel

  ind∞ : ∀{i} → Index∞ i
  index ind∞ = ind


data R : Set where
  r : R

test : {{bl : Belongs ind b}} → R
test = r


-- I want instance resolution to create this datatype.

mutual

  bl : {i : Size} → Belongs {i} ind b
  bl = moreBel {{inf {{bl∞}}}}

  bl∞ : {i : Size} → Belongs∞ {i} ind∞ b∞
  belongs bl∞ = bl


f : R
f = test
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180210/3dc16cbf/attachment.html>