Re: [Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...

[flicky frans]

>modulo some de Morgan and contraposition obfuscation

But isn't it possible to reduce the amount of this obfuscation in the
statement, having

open import Relation.Nullary
open import Data.Product
open import Data.Sum

lem : ∀ (P Q : Set) -> ¬ ¬ ((¬ P) ⊎ (¬ Q)) -> ¬ (P × Q)
lem P Q f p = f (λ {(inj₁ g) -> g (proj₁ p) ; (inj₂ g) -> g (proj₂ p)})

? Or am I missing something trivial?

2014-10-31 23:45 GMT+03:00, Andreas Abel <abela at chalmers.se>:
>
>
> On 31.10.14 8:05 PM, Nils Anders Danielsson wrote:
>> On 2014-10-25 17:18, Sergei Meshveliani wrote:
>>> I have been asked about a constructive proof of this theorem:
>>>
>>>    ℕ ⊆ P U Q -> (¬ isFinite P) ⊎ (¬ isFinite Q).
>>
>> Some respondents have noted things that are not provable. The following
>> statement is provable:
>>
>>    ¬ isFinite (P ∪ Q) → ¬ ¬ ((¬ isFinite P) ⊎ (¬ isFinite Q))
>>
>> See Data.Nat.InfinitelyOften in the standard library.
>
> Which is a direct consequence of the positive statement
>
>    _∪-Finite_ : ∀ {P Q} → Finite P → Finite Q → Finite (P ∪ Q)
>
> modulo some de Morgan and contraposition obfuscation.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>