[Agda] PLFA - Negation - Exercise Classical

[David Banas]

*Hint: what is the type of y? What is the type of the other term that you
already have? What can you derive from these two terms?  *

I can derive bottom, but how does that help me produce an A?


On Mon, Aug 24, 2020 at 7:28 PM Nicolai Kraus <nicolai.kraus at gmail.com>
wrote:

> In the second case, you have to construct a function ¬ ¬ A → A. Your
> attempt λ () can construct a function from the empty type to any other
> type. But ¬ ¬ A is in general not the empty type, so Agda complains. You
> can write λ y → ? instead, but you still need to replace '?' by the right
> expression. Hint: what is the type of y? What is the type of the other term
> that you already have? What can you derive from these two terms?
>
> Your construction of ¬¬¬-elim-inv is correct, but I don't see how to use
> it for your original exercise. I am not sure what you mean by "Agda is not
> using it". If you want Agda to use it, then you would have to tell Agda how
> to use it.
>
> Nicolai
>
>
>
> On Tue, Aug 25, 2020 at 3:13 AM David Banas <capn.freako at gmail.com> wrote:
>
>> Hi all,
>>
>> In trying the "Classical" exercise near the end of the *Negation*
>> chapter in PLFA, I'm trying to show that excluded middle implies double
>> negation elimination with:
>>
>> A⊎¬A⇒¬¬A→A : ∀ {A : Set}
>>   → A ⊎ ¬ A
>>     ---------
>>   → ¬ ¬ A → A
>> A⊎¬A⇒¬¬A→A (inj₁ a)   =  λ _ → a
>> A⊎¬A⇒¬¬A→A (inj₂ ¬A)  =  λ()
>>
>>
>> But Agda is complaining:
>>
>> ¬ (¬ A) should be empty, but that's not obvious to me
>> when checking that the expression λ () has type ¬ (¬ A) → A
>>
>>
>> I wrote a function proving that not-A implies not-//A:
>>
>> ¬¬¬-elim-inv : ∀ {A : Set}
>>   → ¬ A
>>     -------
>>   → ¬ ¬ ¬ A
>> ¬¬¬-elim-inv ¬x  =  λ f → f ¬x
>>
>>
>> And Agda is happy with that proof, but not using it when evaluating the
>> code above. And I can't quite figure out how to incorporate the proof
>> supplied by the second block of code into the evaluation of the first.
>>
>> Can anyone get me unstuck?
>>
>> Thanks!
>> -db
>>
>> _______________________________________________
>> 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/20200824/d62340d0/attachment.html>