<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">s/« which the user can then apply » /« letting the use apply them »/<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">Le 18 avr. 2020 à 17:30, Philippe de Rochambeau <<a href="mailto:phiroc@free.fr" class="">phiroc@free.fr</a>> a écrit :</div><br class="Apple-interchange-newline"><div class=""><meta http-equiv="Content-Type" content="text/html; charset=utf-8" class=""><div style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class=""><br class=""></div><div class="">Hello,</div><div class=""><br class=""></div><div class="">I am attempting to translate a Coq proof into Agda, for learning purposes (cf. <a href="https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf" class="">https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf</a>, p. 9):</div><div class=""><br class=""></div><div class=""><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo;" class=""><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">tauto₁</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">∀</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">A B C </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">:</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #4500ff" class="">Set</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">A </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> B </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> C</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">(</span><span style="font-variant-ligatures: no-common-ligatures" class="">A </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> B</span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">)</span><span style="font-variant-ligatures: no-common-ligatures" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> A </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">→</span><span style="font-variant-ligatures: no-common-ligatures" class=""> C</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(69, 0, 255);" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">tauto₁</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #535353" class="">=</span><span style="font-variant-ligatures: no-common-ligatures;" class=""> </span><span style="font-variant-ligatures: no-common-ligatures; color: #343434; background-color: #a2ff9f" class="">{ }</span><span style="font-variant-ligatures: no-common-ligatures; background-color: rgb(162, 255, 159);" class="">0</span></div></div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(69, 0, 255);" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Here’s how Coq introduces hypotheses, letting the use apply them.</div><div style="margin: 0px; font-stretch: normal; line-height: normal; font-family: Menlo; color: rgb(69, 0, 255);" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 236.23px; top: 794.986px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.849653);" class="">Coq < apply H’.</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 236.23px; top: 814.911px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.999592);" class="">1 </span><span style="left: 236.23px; top: 814.911px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.999592);" class="">subgoal</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 256.157px; top: 854.761px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.999592);" class="">A : Prop</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 256.157px; top: 874.687px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.999592);" class="">B : Prop</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 256.157px; top: 894.612px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.999592);" class="">C : Prop</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 256.157px; top: 914.537px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.999592);" class="">H : A -> B -> C</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 256.157px; top: 934.462px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.999592);" class="">H’ : A -> B</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 256.157px; top: 954.387px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.999592);" class="">HA : A</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 256.157px; top: 974.312px; font-size: 16.6043px; font-family: monospace; transform: scaleX(0.999592);" class="">============================</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><span style="left: 266.118px; top: 994.239px; font-size: 16.6043px; font-family: monospace;" class="">A</span></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">How do you do the same thing in Agda?</div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Cheers,</div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class=""><br class=""></div><div style="margin: 0px; font-stretch: normal; line-height: normal;" class="">Philippe</div></div>_______________________________________________<br class="">Agda mailing list<br class=""><a href="mailto:Agda@lists.chalmers.se" class="">Agda@lists.chalmers.se</a><br class="">https://lists.chalmers.se/mailman/listinfo/agda<br class=""></div></blockquote></div><br class=""></body></html>