Hi Apostolis,
Instance search is not meant to construct new recursive (or corecursive)
solutions, so it is not able to automatically find your term bl unless
you've already defined it somewhere before.
However, are you sure the types 'Index' and 'Belongs' define what you want
them to mean? Usually you have one infinite datastructure (such as a
stream) and a type of *finite* indices (such as natural numbers). So I
don't think you need the 'inf' constructor for Index and Belongs. Without
these constructors, it should be possible to have instance search construct
proofs of Belongs, since then all proofs are finite.
I hope this helps.
-- Jesper
ps: A remark about terminology: you seem to be using the word 'datatype'
when you mean 'element of the datatype'.
On Sat, Feb 10, 2018 at 7:56 PM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180211/188899ed/attachment.html>