<div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">Hello Twan,</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div>
<div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">thank you for your nice solution and for taking the time to write it.</div>
<div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">It teaches me a lot of things!</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div>
<div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">In fact, the induction on m and n was my first attempt, but for some reason I failed to finish the proof (probably I mechanically performed case analysis also on x and y in the hope to "clarify" the hypothesis but I got lost instead).</div>
</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif;font-size:small">Marco</div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">2013/10/10 Twan van Laarhoven <span dir="ltr"><<a href="mailto:twanvl@gmail.com" target="_blank">twanvl@gmail.com</a>></span><br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello Marco,<br>
<br>
<br>
I think this is easiest to prove by induction on m and n. See the attachment for my alternative proof.<br>
<br>
I just typed in the theorem, used C-c,C-c to split on m and n. The only interesting case is (suc m) (suc n). There you need induction, together with some lemmas to show that this is actually possible. To prove the lemmas, again I used case splitting together with auto to fill in the right hand side.<br>
<br>
<br>
As a remark on style, the case splitting often exposes hidden variables with irrelevant arguments. You can often clean that up quite a bit. For example your 'swap' function can be written as just<br>
<br>
swap : ∀ {m n} → Ordering m n → Ordering n m<br>
swap (less m k) = greater m k<br>
swap (equal n) = equal n<br>
swap (greater n k) = less n k<br>
<br>
<br>
Twan<div><div class="h5"><br>
<br>
On 10/10/13 00:10, Marco Maggesi wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Hello!<br>
<br>
I'm new to Agda.<br>
I wrote a proof of the following theorem<br>
(see<br>
attached file):<br>
<br>
<br>
<br>
ordering-uniqueness : {m n : ℕ} {x y : Ordering m n} → x ≡ y<br>
<br>
I'd be interested to see if there<br>
are<br>
simpler proof<br>
s of the same fact.<br>
Also general remarks about idiom and style are welcome.<br>
<br>
Thanks,<br>
Marco<br>
<br>
<br></div></div>
______________________________<u></u>_________________<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" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br>
</blockquote>
<br>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>