<div dir="ltr">On Wed, Nov 13, 2013 at 12:27 PM, Jan Stolarek <span dir="ltr"><<a href="mailto:jan.stolarek@p.lodz.pl" target="_blank">jan.stolarek@p.lodz.pl</a>></span> wrote:<br><div class="gmail_extra"><div class="gmail_quote">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">[...]<br>
Now if I could apply +suc to both sides of (cong suc (+comm a b)) I would turn:<br>
suc (a + b) == suc (b + a)<br>
into:<br>
a + suc b == b + suc a<br>
which would end my proof. How can I do that?<br>
<br></blockquote><div><br></div><div>To chain proofs like that you can use transitivity:</div><div><br></div><div> trans : forall {A}{x y z : A} -> x == y -> y == z -> x == z</div><div> trans refl eq = eq</div>
<div>
<br></div><div>in fact you'll need to nest them to apply something on both sides:</div><div><br></div><div> trans (....) (trans (cong suc (+comm a b)) (....))</div><div><br></div><div>(Usually at this point the thing gets less than readable and we use the prettier syntax provided by ≡-Reasoning in Relation.Binary.PropositionalEquality from the stdlib.)</div>
<div><br></div><div>-- Andrea</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Janek<br>
_______________________________________________<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/mailman/listinfo/agda</a><br>
</blockquote></div><br></div></div>