<div dir="ltr"><div dir="ltr"><div>Yep, Agda has such a feature: it's called dependent pattern matching.</div><div style="margin-left:40px"><span style="font-family:monospace,monospace"><br></span></div><div style="margin-left:40px"><span style="font-family:monospace,monospace">inversionEven : {n : ℕ} -> even (suc (suc n)) -> even n<br>inversionEven (evenSS x) = x</span></div><div style="margin-left:40px"><span style="font-family:monospace,monospace"><br></span></div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Feb 19, 2019 at 6:17 PM Pierre Lescanne (en) <<a href="mailto:pierre.lescanne@ens-lyon.fr">pierre.lescanne@ens-lyon.fr</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 bgcolor="#FFFFFF">
Assuming a predicate <i>even</i><br>
<p><b>data even : ℕ -> Set where</b><b><br>
</b><b> even0 : even zero</b><b><br>
</b><b> even1 : even (suc zero)</b><b><br>
</b><b> evenSS : {n : ℕ} -> even n -> even (suc (suc n))</b></p>
<p>I would like to prove:</p>
<p><b>inversionEven : {n : ℕ} -> even (suc (suc n)) -> even n</b></p>
<p>In Coq, I could use <br>
</p>
<ul>
<li>either a command <i>inversion</i></li>
<li>or a somewhat direct proof<i> </i>that applies even_ind. </li>
</ul>
<p>Are there similar features in Agda ?<br>
</p>
<pre class="gmail-m_1628939666156285212moz-signature" cols="72">--
Cheers
---------------------------
Pierre Lescanne (Emeritus Professor)
LIP / École normale supérieure de Lyon
46 allée d'Italie
69364 LYON Cedex 07, France
tél: +33 6 85 70 94 31
<a class="gmail-m_1628939666156285212moz-txt-link-freetext" href="http://perso.ens-lyon.fr/pierre.lescanne/" target="_blank">http://perso.ens-lyon.fr/pierre.lescanne/</a>
---------------------------
</pre>
</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>