<div dir="ltr">Oh, of course, by defining (and then using) <font face="monospace"><b>absurd</b></font>:<div><br></div><blockquote style="margin:0 0 0 40px;border:none;padding:0px"><div><font face="monospace">absurd : ∀ {A : Set}</font></div><div><font face="monospace"> → ⊥</font></div><div><font face="monospace"> --</font></div><div><font face="monospace"> → A</font></div><div><font face="monospace">absurd ()</font></div><div><font face="monospace"><br></font></div><div><font face="monospace">A⊎¬A⇒¬¬A→A : ∀ {A : Set}</font></div><div><font face="monospace"> → A ⊎ ¬ A</font></div><div><font face="monospace"> ---------</font></div><div><font face="monospace"> → ¬ ¬ A → A</font></div><div><font face="monospace">A⊎¬A⇒¬¬A→A (inj₁ a) = λ _ → a</font></div><div><font face="monospace">A⊎¬A⇒¬¬A→A (inj₂ ¬A) = λ y → absurd (y ¬A)</font></div></blockquote><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Aug 24, 2020 at 8:14 PM David Banas <<a href="mailto:capn.freako@gmail.com">capn.freako@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><i>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><div><br></div><div>I can derive bottom, but how does that help me produce an A?</div><div> <br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, Aug 24, 2020 at 7:28 PM Nicolai Kraus <<a href="mailto:nicolai.kraus@gmail.com" target="_blank">nicolai.kraus@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">In the second case, you have to construct a function ¬ ¬ A → A. Your attempt <span style="font-family:monospace">λ () can construct a function from the empty type to any other type. But</span> ¬ ¬ 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? <div><br></div><div>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.</div><div><br></div><div>Nicolai</div><div><br><div><br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Aug 25, 2020 at 3:13 AM David Banas <<a href="mailto:capn.freako@gmail.com" target="_blank">capn.freako@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hi all,<div><br></div><div>In trying the "Classical" exercise near the end of the <i>Negation</i> chapter in PLFA, I'm trying to show that excluded middle implies double negation elimination with:</div><div><br></div><blockquote style="margin:0px 0px 0px 40px;border:none;padding:0px"><div><font face="monospace">A⊎¬A⇒¬¬A→A : ∀ {A : Set}</font></div><div><font face="monospace"> → A ⊎ ¬ A</font></div><div><font face="monospace"> ---------</font></div><div><font face="monospace"> → ¬ ¬ A → A</font></div><div><font face="monospace">A⊎¬A⇒¬¬A→A (inj₁ a) = λ _ → a</font></div><div><font face="monospace">A⊎¬A⇒¬¬A→A (inj₂ ¬A) = λ()</font></div></blockquote><div><br></div><div>But Agda is complaining:</div><div><br></div><blockquote style="margin:0px 0px 0px 40px;border:none;padding:0px"><div><font face="monospace">¬ (¬ A) should be empty, but that's not obvious to me</font></div><div><font face="monospace">when checking that the expression λ () has type ¬ (¬ A) → A</font></div></blockquote><div><br></div><div>I wrote a function proving that not-A implies not-//A:</div><div><br></div><blockquote style="margin:0px 0px 0px 40px;border:none;padding:0px"><div><font face="monospace">¬¬¬-elim-inv : ∀ {A : Set}</font></div><div><font face="monospace"> → ¬ A</font></div><div><font face="monospace"> -------</font></div><div><font face="monospace"> → ¬ ¬ ¬ A</font></div><div><font face="monospace">¬¬¬-elim-inv ¬x = λ f → f ¬x</font></div></blockquote><div><br></div><div>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.</div><div><br></div><div>Can anyone get me unstuck?</div><div><br></div><div>Thanks!</div><div>-db</div><div><br></div></div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</blockquote></div>
</blockquote></div>