<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
Hi Marcus,</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
this signature looks simply a decision procedure for propositional equality between u and v, and if agda is able to figure out the proof term, I even speculate that u and v are of an inductively defined type. If that's the case, why did you involve f and g?
it might hint that it's not the signature that you might be looking for, or you are complicating a simple problem.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank"></a></b></span></span></font> </div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Marcus Christian Lehmann <lehmann@tet.tu-berlin.de><br>
<b>Sent:</b> March 14, 2019 4:09 PM<br>
<b>To:</b> Jason -Zhong Sheng- Hu; Apostolis Xekoukoulotakis<br>
<b>Cc:</b> agda list<br>
<b>Subject:</b> Re: [Agda] Case split on λ()</font>
<div> </div>
</div>
<div style="background-color:#FFFFFF">
<div class="x_moz-cite-prefix">Thank you for pointing this dead-end out.</div>
<div class="x_moz-cite-prefix"><br>
</div>
<div class="x_moz-cite-prefix">Therefore I will proceed with<br>
</div>
<div class="x_moz-cite-prefix"><br>
</div>
<div class="x_moz-cite-prefix">f : ∀ x u v → f x ≡ u → g x ≡ v → u ≡ v ⊎ u ≢ v</div>
<div class="x_moz-cite-prefix">f x u v p1 p2 = ?</div>
<div class="x_moz-cite-prefix"><br>
</div>
<div class="x_moz-cite-prefix">where proof search seems mighty enough to figure out "inj₁ refl" or "inj₂ (λ ())" for the right hand side (after case splitting on x).</div>
<div class="x_moz-cite-prefix"><br>
</div>
<div class="x_moz-cite-prefix">regards,</div>
<div class="x_moz-cite-prefix"><br>
</div>
<div class="x_moz-cite-prefix">Am 14.03.19 um 17:42 schrieb Jason -Zhong Sheng- Hu:<br>
</div>
<blockquote type="cite">
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
Hi Marcus,</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
you shouldn't expect to be able to pattern match on functions in regular type theory based on intuitionistic type theory.</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
negation is a function so it should be applied to something.<br>
</div>
<div style="font-family:Calibri,Helvetica,sans-serif; font-size:12pt; color:rgb(0,0,0)">
<br>
</div>
<div id="x_signature">
<div id="x_divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font size="3" style="font-size:12pt"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font size="3" style="font-size:12pt"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu</b></span></span></font> </div>
</div>
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="x_divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" color="#000000" style="font-size:11pt"><b>From:</b> Agda
<a class="x_moz-txt-link-rfc2396E" href="mailto:agda-bounces@lists.chalmers.se"><agda-bounces@lists.chalmers.se></a> on behalf of Marcus Christian Lehmann
<a class="x_moz-txt-link-rfc2396E" href="mailto:lehmann@tet.tu-berlin.de"><lehmann@tet.tu-berlin.de></a><br>
<b>Sent:</b> March 14, 2019 12:36 PM<br>
<b>To:</b> Apostolis Xekoukoulotakis<br>
<b>Cc:</b> agda list<br>
<b>Subject:</b> Re: [Agda] Case split on λ()</font>
<div> </div>
</div>
<div class="x_BodyFragment"><font size="2"><span style="font-size:11pt">
<div class="x_PlainText">I have attached a more complete example but it boils down to convincing
<br>
Agda that ¬ 2 ≡ 2 should be empty (following the very readable error <br>
message), e.g.<br>
<br>
```<br>
fun : ¬ (2 ≡ 2) → ⊥<br>
fun () -- Error: "¬ 2 ≡ 2 should be empty, but that's not obvious to me"<br>
```<br>
<br>
<br>
Am 14.03.19 um 09:09 schrieb Apostolis Xekoukoulotakis:<br>
> Marcus, I could not follow your example, but it seems that you are <br>
> trying to case split a function, which is not possible.<br>
><br>
> ```<br>
> open import Relation.Binary.PropositionalEquality<br>
> open import Data.Nat<br>
> open import Data.Empty<br>
> open import Relation.Nullary<br>
><br>
><br>
> fun : ¬ (2 ≡ 2) → ⊥<br>
> fun ¬x = ? -- ⊥-elim (¬x refl)<br>
><br>
> ```<br>
<br>
</div>
</span></font></div>
</blockquote>
<br>
</div>
</body>
</html>