[Agda] `search' format

[Sergei Meshveliani]

On Sat, 2017-04-29 at 17:26 +0200, Andreas Abel wrote:
> 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}
> 


I see, thank you.
I thought of the partition  prefix, found, suffix  
to be explicitly returned together with a proof for
prefix ++ (found ∷ suffix) ≡ xs.

Anyway, these parts can be somehow `extracted' from  FirstMatch.
Meanwhile I use Found and Search (shown below),
and I thought of whether Standard library has anything close to this.
Because this is not nice to reinvent an item of Standard.

I have come to this because I use the partition   prefix, found, suffix
to arrange a termination proof for recursion with a list. Because each
prefix and suffix  has a smaller length than  xs.
 
Regards,

------
Sergei



> 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
> >
> 
>