<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 -> List A -> Set where</div><div>stop : [] ⊂ []</div><div>drop : forall {xs y ys} -> xs ⊂ ys -> xs ⊂ y :: ys</div>
<div>keep : forall {x xs ys} -> xs ⊂ ys -> 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>