[Agda] Understanding the pattern matching in proofs

[Amila Jayasekara]

Hi All,

I am still learning Agda concepts.

I am following [1] tutorial and tried out some of the exercises in it.

It defines sublist as follows;

infix 20 _⊂_
data _⊂_ {A : Set} : List A -> List A -> Set where
stop : [] ⊂  []
drop : forall {xs y ys} -> xs ⊂  ys -> xs ⊂  y :: ys
keep : forall {x xs ys} -> xs ⊂  ys -> x :: xs  ⊂ x :: ys

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.

 ⊂-trans : {A : Set}{xs ys zs : List A} → xs ⊂ ys → ys ⊂ zs → xs ⊂ zs


  ⊂-trans stop stop = stop


  ⊂-trans p q with (drop p) (keep q)


  ... | xs ⊂ (y :: ys) | y :: ys ⊂ y :: zs = .xs ⊂ .zs
  ....
  ...

Appreciate if someone point out where I am going wrong and help me to
understand the thinking pattern.

Thank you
Regards,
Thejaka Amila

[1] http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130425/41eb3f74/attachment.html