[Agda] PLFA - Negation - Exercise Classical

[Philip Wadler]

Thank you to the list for dealing with PLFA questions!

I'm happy for this to continue, but if the list is not happy, there is an
alternative mailing list available:
    plfa-interest at inf.ed.ac.uk
    http://lists.inf.ed.ac.uk/mailman/listinfo/plfa-interest

Go well, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/



On Tue, 25 Aug 2020 at 04:39, David Banas <capn.freako at gmail.com> wrote:

> Oh, of course, by defining (and then using) *absurd*:
>
> absurd : ∀ {A : Set}
>   → ⊥
>     --
>   → A
> absurd ()
>
> A⊎¬A⇒¬¬A→A : ∀ {A : Set}
>   → A ⊎ ¬ A
>     ---------
>   → ¬ ¬ A → A
> A⊎¬A⇒¬¬A→A (inj₁ a)   =  λ _ → a
> A⊎¬A⇒¬¬A→A (inj₂ ¬A)  =  λ y → absurd (y ¬A)
>
>
>
> On Mon, Aug 24, 2020 at 8:14 PM David Banas <capn.freako at gmail.com> wrote:
>
>> *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
>>>>
>>> _______________________________________________
> 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/20200825/413ca7cd/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200825/413ca7cd/attachment.ksh>