[Agda] `search' format

[Andreas Abel]

It looks like you want to find the first element that satisfies P.

I'd do this with an inductive predicate for the result:

open import Data.List
open import Data.List.Any
open import Data.List.All

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Unary

data FirstMatch {A : Set} (P : A → Set) : List A → Set where
   here  : ∀{x xs} (p : P x) → FirstMatch P (x ∷ xs)
   there : ∀{x xs} (¬p : ¬ (P x)) (ps : FirstMatch P xs)
         → FirstMatch P (x ∷ xs)

findFirst : ∀{A : Set}{P : A → Set} (f : Decidable P)
   → Decidable (FirstMatch P)
findFirst f [] = no λ()
findFirst f (x ∷ xs) with f x
findFirst f (x ∷ xs) | yes p = yes (here p)
findFirst f (x ∷ xs) | no ¬p with findFirst f xs
findFirst f (x ∷ xs) | no ¬p | yes p = yes (there ¬p p)
findFirst f (x ∷ xs) | no ¬p | no ¬q = no
   λ{ (here p) → ¬p p ; (there _ q) → ¬q q}


On 28.04.2017 22:21, Sergei Meshveliani wrote:
> Can people tell, please,
>
> what may be a sensible general format for searching in a list?
>
> I consider this one:
>
>   search : ∀ {p} {P : A → Set p} → (P? : Decidable P) → (xs : List A) →
>
>                                          Found P? xs  ⊎  All (¬_ ∘ P) xs
>
> where Found is defined as
>
>   record Found {p} {P : A → Set p} (P? : Decidable P) (xs : List A) :
>                                                                  Set _
>          where
>          field  prefix   : List A
>                 found    : A
>                 suffix   : List A
>                 ¬prefix  : All (¬_ ∘ P) prefix
>                 P-found  : P found
>                 concatEq : prefix ++ (found ∷ suffix) ≡ xs
>
> I think this expresses completely the axioms for searching in a list.
>
> Has Standard library something similar?
>
> (I am sorry if the list answered to this long ago, I just do not
> recall).
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/