[Agda] PLFA - Negation - Exercise Classical

[David Banas]

Oh, gosh! I didn't even think to wonder if there might be a more
appropriate venue for my PLFA-related questions.
My sincerest apologies to anyone, who found that inappropriate. :(
And my sincerest thanks to those who responded. :)

-db


On Tue, Aug 25, 2020 at 2:40 AM Philip Wadler <wadler at inf.ed.ac.uk> wrote:

> 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
>>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200825/3137130a/attachment.html>