[Agda] Understanding the pattern matching in proofs

[Nils Anders Danielsson]

On 2013-04-26 03:22, Amila Jayasekara wrote:
> 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
>    ....
>    ...

There is no need to use "with" in this proof. As a first step you could
write down the following six cases:

   ⊂-trans stop     stop     = ?
   ⊂-trans stop     (drop q) = ?
   ⊂-trans (drop p) (drop q) = ?
   ⊂-trans (drop p) (keep q) = ?
   ⊂-trans (keep p) (drop q) = ?
   ⊂-trans (keep p) (keep q) = ?

(You can get the job done with fewer cases.)

-- 
/NAD