<div dir="ltr">Hi All,<div><br></div><div style>I am still learning Agda concepts.</div><div style><br></div><div style>I am following [1] tutorial and tried out some of the exercises in it.</div><div style><br></div><div style>
It defines sublist as follows;</div><div style><br></div><div style><div>infix 20 _⊂_</div><div>data _⊂_ {A : Set} : List A -&gt; List A -&gt; Set where</div><div>stop : [] ⊂  []</div><div>drop : forall {xs y ys} -&gt; xs ⊂  ys -&gt; xs ⊂  y :: ys</div>
<div>keep : forall {x xs ys} -&gt; xs ⊂  ys -&gt; x :: xs  ⊂ x :: ys</div></div><div style><br></div><div style>I need to prove \sub is transitive. So I understand that in the transitive function I have to pattern match on stop, drop and keep cases. But I am having difficulty relating pattern matching with my proof.</div>
<div style><br></div><div style><div> ⊂-trans : {A : Set}{xs ys zs : List A} → xs ⊂ ys → ys ⊂ zs → xs ⊂ zs                                                                                        </div><div>  ⊂-trans stop stop = stop                                                                                                                                    </div>
<div>  ⊂-trans p q with (drop p) (keep q)                                                                                                                          </div><div>  ... | xs ⊂ (y :: ys) | y :: ys ⊂ y :: zs = .xs ⊂ .zs </div>
<div>  ....</div><div>  ...</div><div><br></div><div style>Appreciate if someone point out where I am going wrong and help me to understand the thinking pattern.</div><div style><br></div><div style>Thank you</div><div style>
Regards,</div><div style>Thejaka Amila</div></div><div style><br></div><div style>[1] <a href="http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf">http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf</a></div>
</div>