<div dir="ltr"><div><span style="font-family:arial,sans-serif;font-size:13px">¬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 </span>¬ (P x), but this is not possible in general.</div>


<div><span style="font-family:arial,sans-serif;font-size:13px">If it were provable, we could decide </span>¬ P for arbitrary P as below:<br></div><div><br></div><div><div>    postulate ¬all→any¬ : {A : Set} {P : A → Set} {xs : List A} →</div>


<div>                      (¬ All P xs) → Any (¬_ ∘ P) xs</div><div><br></div><div>    postulate A : Set</div><div>    postulate P : A → Set</div><div><br></div><div>    P&#39; : (Bool × A) → Set</div><div>    P&#39; (true , a)  = P a</div>


<div>    P&#39; (false , a) = ¬ P a</div><div><br></div><div>    list : A → List (Bool × A)</div><div>    list a = (true , a) ∷ (false , a) ∷ []</div><div><br></div><div>    ¬allP&#39; : (a : A) → ¬ All P&#39; (list a)</div>


<div>    ¬allP&#39; a (pa ∷ ¬pa ∷ []) = ¬pa pa </div><div><br></div><div>    dec : Decidable (¬_ ∘ P)</div><div>    dec a with ¬all→any¬ (¬allP&#39; a)</div><div>    dec a | here ¬pa  = yes ¬pa</div><div>    dec a | there (here ¬¬pa) = no ¬¬pa</div>


<div>    dec a | there (there ())</div></div><div><br></div><div>Best,</div><div>Jesper</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Oct 24, 2013 at 7:54 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
I write<br>
<br>
  ¬all→any¬ : {A : Set} {P : A → Set} {P? : Decidable P} {xs : List A} →<br>
                                      (¬ All P xs) → (Any (¬_ ∘ P) xs)<br>
<br>
and think:  is this provable without using  Decidable ?<br>
<br>
I tried a singleton list for a counter example. But here is the proof:<br>
<br>
 ¬all→P1 : {A : Set} {P : A → Set} {x : A} → (¬ All P (x ∷ [])) → ¬ P x<br>
 ¬all→P1 ¬all-x Px =  ¬all-x (Px ∷a []a)<br>
<br>
([]a, _∷a_  imported from  Data.List.All  as renamed [], _∷_).<br>
<br>
May be   x ∷ y ∷ []   is a counter example?<br>
<br>
<br>
And  ¬all→any¬  I implement as<br>
<br>
  ¬all→any¬              {xs = []}     ¬all[]     =  ⊥-elim $ ¬all[] []a<br>
<br>
  ¬all→any¬ {P = P} {P? = P?} {xs = x ∷ ys} ¬all-x:ys  with P? x<br>
  ...      |<br>
             no ¬Px = here ¬Px<br>
  ...      | yes Px =<br>
                 there $ ¬all→any¬ {P = P} {P? = P?} {xs = ys} ¬all-ys<br>
                              where<br>
                              ¬all-ys : ¬ All P ys<br>
                              ¬all-ys all-ys = ¬all-x:ys (Px ∷a all-ys)<br>
<br>
<br>
Thank you in advance for explanation,<br>
<br>
------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>