[Agda] PLFA - Negation - Exercise Classical

[Nicolai Kraus]

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/20200825/d070ff71/attachment.html>