[Agda] PLFA - Negation - Exercise Classical

Philip Wadler wadler at inf.ed.ac.uk
Tue Aug 25 11:39:43 CEST 2020


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>


More information about the Agda mailing list