<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' : (Bool × A) → Set</div><div> P' (true , a) = P a</div>
<div> P' (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' : (a : A) → ¬ All P' (list a)</div>
<div> ¬allP' a (pa ∷ ¬pa ∷ []) = ¬pa pa </div><div><br></div><div> dec : Decidable (¬_ ∘ P)</div><div> dec a with ¬all→any¬ (¬allP' 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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>