[Agda] Understanding the pattern matching in proofs

[Amila Jayasekara]

Dear Nils,

Thanks for the reply. Actually I got the problem solved by pattern matching
as you mentioned. My complete solution is;

  -- Transitivity


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


  ⊆-trans stop stop = stop


  ⊆-trans stop (drop q) = drop q

  ⊆-trans p (drop q) = drop (⊆-trans p q)


  ⊆-trans (keep p) (keep q) = keep (⊆-trans p q)


  ⊆-trans (drop p) (keep q) = drop (⊆-trans p q)

Thanks
Amila


On Mon, Apr 29, 2013 at 5:36 AM, Nils Anders Danielsson <nad at cse.gu.se>wrote:

> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130429/d6eee551/attachment.html