Apostolis Xekoukoulotakis

2018-02-10 18:56:14 UTC

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

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