[Agda] PLFA - Negation - Exercise Classical

[David Banas]

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
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200824/33cc7b88/attachment.html>