<div dir="ltr"><div>Hi Apostolis,<br><br>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.<br><br></div><div>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.<br><br></div><div>I hope this helps.<br><br>-- Jesper<br></div><div><br><br></div>ps: A remark about terminology: you seem to be using the word 'datatype' when you mean 'element of the datatype'.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Feb 10, 2018 at 7:56 PM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div>I have a datatype (called "Bob") that tracks whether a variable has been used or not.<br></div>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.<br><br></div>The datatype "Belongs" depends on an Index and Bob. It proves that all the variables pointed by the index are actually available.<br><br></div>Every time Bob, changes, a new Belongs datatype is needed. I want this proof to be generated by instance resolution.<br><br></div>I am not sure if this is possible when the index points to an infinite number of variables, ie if we have coinductive types. <br><br></div>Here is the example.<br><br>-------------------------<br><br>module Test where<br><br>open import Data.Bool<br>open import Size<br><br>mutual<br><br> data Bob (i : Size) : Set where<br> more : Bob i → Bool → Bob i<br> none : Bob i<br> twoPaths : Bob i → Bob i → Bob i<br> inf : Bob∞ i → Bob i<br><br> record Bob∞ (i : Size) : Set where<br> coinductive<br> field<br> bob : {j : Size< i} → Bob j <br><br>open Bob∞<br><br>data Bel : Set where<br> bel : Bel<br> nbel : Bel<br> <br>mutual<br><br> data Index (i : Size) : Set where<br> here : Index i<br> more : Index i → Bel → Index i<br> left : Index i → Index i<br> right : Index i → Index i<br> inf : Index∞ i → Index i<br> <br> record Index∞ (i : Size) : Set where<br> coinductive<br> field<br> index : {j : Size< i} → Index j<br><br>open Index∞<br><br>mutual<br><br> data Belongs {i : Size} : Index i → Bob i → Set where<br> instance<br> here : ∀{b} → Belongs here (more b true)<br> moreBel : ∀{ind b} → {{is : Belongs ind b}} → Belongs (more ind bel) (more b true)<br> morenBel : ∀{ind b bool} → {{is : Belongs ind b}} → Belongs (more ind nbel) (more b bool)<br> left : ∀{ind bl br} → {{is : Belongs ind bl}} → Belongs (left ind) (twoPaths bl br)<br> right : ∀{ind bl br} → {{is : Belongs ind br}} → Belongs (right ind) (twoPaths bl br)<br> inf : ∀{ind∞ bob∞} → {{is∞ : Belongs∞ ind∞ bob∞}} → Belongs (inf ind∞) (inf bob∞)<br><br> record Belongs∞ {i : Size} (ind∞ : Index∞ i) (bob∞ : Bob∞ i) : Set where<br> coinductive<br> field<br> belongs : {j : Size< i} → Belongs (index ind∞) (bob bob∞)<br><br>open Belongs∞<br><br>mutual<br><br> b : ∀{i} → Bob i<br> b = more (inf b∞) true<br><br> b∞ : ∀{i} → Bob∞ i<br> bob b∞ = b<br><br><br>mutual<br><br> ind : ∀{i} → Index i<br> ind = more (inf ind∞) bel<br><br> ind∞ : ∀{i} → Index∞ i<br> index ind∞ = ind<br><br><br>data R : Set where<br> r : R<br><br>test : {{bl : Belongs ind b}} → R<br>test = r<br><br><br>-- I want instance resolution to create this datatype.<br><br>mutual<br><br> bl : {i : Size} → Belongs {i} ind b<br> bl = moreBel {{inf {{bl∞}}}}<br><br> bl∞ : {i : Size} → Belongs∞ {i} ind∞ b∞<br> belongs bl∞ = bl <br><br><br>f : R<br>f = test<br><br></div>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>