[Agda] not-all -> any-not

[Jesper Cockx]

¬all→any¬ is not provable without assuming P is decidable: in order to
define it, we would have to decide for which x in xs we have ¬ (P x), but
this is not possible in general.
If it were provable, we could decide ¬ P for arbitrary P as below:

    postulate ¬all→any¬ : {A : Set} {P : A → Set} {xs : List A} →
                      (¬ All P xs) → Any (¬_ ∘ P) xs

    postulate A : Set
    postulate P : A → Set

    P' : (Bool × A) → Set
    P' (true , a)  = P a
    P' (false , a) = ¬ P a

    list : A → List (Bool × A)
    list a = (true , a) ∷ (false , a) ∷ []

    ¬allP' : (a : A) → ¬ All P' (list a)
    ¬allP' a (pa ∷ ¬pa ∷ []) = ¬pa pa

    dec : Decidable (¬_ ∘ P)
    dec a with ¬all→any¬ (¬allP' a)
    dec a | here ¬pa  = yes ¬pa
    dec a | there (here ¬¬pa) = no ¬¬pa
    dec a | there (there ())

Best,
Jesper


On Thu, Oct 24, 2013 at 7:54 PM, Sergei Meshveliani <mechvel at botik.ru>wrote:

> People,
> I write
>
>   ¬all→any¬ : {A : Set} {P : A → Set} {P? : Decidable P} {xs : List A} →
>                                       (¬ All P xs) → (Any (¬_ ∘ P) xs)
>
> and think:  is this provable without using  Decidable ?
>
> I tried a singleton list for a counter example. But here is the proof:
>
>  ¬all→P1 : {A : Set} {P : A → Set} {x : A} → (¬ All P (x ∷ [])) → ¬ P x
>  ¬all→P1 ¬all-x Px =  ¬all-x (Px ∷a []a)
>
> ([]a, _∷a_  imported from  Data.List.All  as renamed [], _∷_).
>
> May be   x ∷ y ∷ []   is a counter example?
>
>
> And  ¬all→any¬  I implement as
>
>   ¬all→any¬              {xs = []}     ¬all[]     =  ⊥-elim $ ¬all[] []a
>
>   ¬all→any¬ {P = P} {P? = P?} {xs = x ∷ ys} ¬all-x:ys  with P? x
>   ...      |
>              no ¬Px = here ¬Px
>   ...      | yes Px =
>                  there $ ¬all→any¬ {P = P} {P? = P?} {xs = ys} ¬all-ys
>                               where
>                               ¬all-ys : ¬ All P ys
>                               ¬all-ys all-ys = ¬all-x:ys (Px ∷a all-ys)
>
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131024/f42dc390/attachment.html