case or with [Re: [Agda] Re: Issue 897 in agda: unnatural space behavoir of the checker]

[Andreas Abel]

On 19.09.2013 14:34, Nils Anders Danielsson wrote:
> On 2013-09-17 15:09, Sergei Meshveliani wrote:
>> But I need a general understanding:  when to use `with' and when to
>> use `case'.

My strategy would be to use case wherever possible, and with only when 
case does not work since you need to abstract the discriminant (the 
thing you case over) in the goal.

Below is the classic example: filter can be defined with case, but 
filterCreatesSublist needs with in order to abstract (f x) in the goal.

module Filter where

open import Function
open import Data.Bool
open import Data.List using (List; []; _∷_)

filter : {A : Set}(f : A → Bool)(as : List A) → List A
filter f [] = []
filter f (x ∷ xs) = case (f x) of λ
   { true → x ∷ filter f xs
   ; false → filter f xs
   }

data _⊂_ {A : Set} : (xs ys : List A) → Set where
   done : ∀ {xs}      → xs ⊂ xs
   keep : ∀ x {xs ys} → xs ⊂ ys → (x ∷ xs) ⊂ (x ∷ ys)
   skip : ∀ x {xs ys} → xs ⊂ ys →       xs ⊂ (x ∷ ys)

filterCreatesSublist : ∀ {A}(f : A → Bool)(xs : List A) → filter f xs ⊂ xs
filterCreatesSublist f [] = done
-- filterCreatesSublist f (x ∷ xs) = ?
-- goal mentions (f x) which we need to abstract
-- to make the case of (f x) reduce
filterCreatesSublist f (x ∷ xs) with (f x)
... | true  = keep x (filterCreatesSublist f xs)
... | false = skip x (filterCreatesSublist f xs)



-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/