Formalizing Desargues' theorem in Coq using ranks

ÓÖÑ Ð Þ Ò ÓÑ ØÖÝ Ø ÓÖ Ñ× Ò ÔÖÓÓ ×× ×Ø ÒØ Ð ÓÕ × ÐÐ Ò Ò º × ÑÔ × Þ Ò Ø Ð Ø Ö ØÙÖ ¸ Ø ÒÓÒ¹ Ò Ö Ý ÓÒ Ø ÓÒ× Ð × ØÓ Ø Ò Ð ÔÖÓÓ ×º ÁÒ ¹ Ø ÓÒ¸ Û Ò ÓÒ× Ö Ò Ö¹ Ñ Ò× ÓÒ׸ Ø ÑÓÙÒØ Ó Ò¹ Ò Ö Ð Ø ÓÒ× ´ º º ÔÓ ÒØ¹Ð Ò ¸ ÔÓ ÒعÔÐ Ò ¸ Ð Ò ¹ÔÐ Ò µ Ò¹ Ù ÒÙÑ ÖÓÙ× Ø Ò Ð Ð ÑÑ ×º ÁÒ Ø × Ô Ô Ö¸ Û ÔÖ × ÒØ Ò ÓÖ Ò Ð ÔÔÖÓ × ÓÒ Ø ÒÓØ ÓÒ Ó Ö Ò Û Ð¹ ÐÓÛ× ØÓ × Ö Ò Ò Ò ÒÓÒ¹ Ò Ò Ö Ð Ø ÓÒ× ×Ù × ÕÙ Ð Øݸ ÓÐÐ Ò Ö ØÝ Ò ÓÔÐ Ò Ö ØÝ ÓÑÓ Ò ÓÙ×Ðݺ ÁØ ÐÐÓÛ× ØÓ ÖÖÝ ÓÙØ ÔÖÓÓ × Ò ÑÓÖ ×Ý×Ø Ñ Ø Û Ýº ÌÓ Ú Ð¹ Ø Ø × ÔÔÖÓ ¸ Û ÓÖÑ Ð Þ Ò ÓÕ ´Ù× Ò ÓÒÐÝ Ö Ò ×µ ÓÒ Ó Ø ÙÒ Ñ ÒØ Ð Ø ÓÖ Ñ× Ó Ø ÔÖÓ Ø Ú ×Ô ¸ Ò Ñ ÐÝ × Ö Ù ×³ Ø ÓÖ Ñº Categories and Subject Descr...

• Type: Conference
• Year: 2009
• Where: SAC
• Authors: Nicolas Magaud, Julien Narboux, Pascal Schreck
• Keywords: Applied Computing, SAC 2009