Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Reasoning about equalities of equalities

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Reasoning about equalities of equalities


Chronological Thread 
    < Chronological >      < Thread >
  • From: Talia Ringer <tringer AT cs.washington.edu>
  • To: Coq-Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Reasoning about equalities of equalities
  • Date: Sun, 24 May 2020 20:30:05 -0700
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-wr1-f52.google.com
  • Ironport-phdr: 9a23:wtGkQhDmbFsRFeo7yaGWUyQJP3N1i/DPJgcQr6AfoPdwSPT5osbcNUDSrc9gkEXOFd2Cra4d1qyP6vGrBz1IyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLN/IA+roQnMssQajopvJ6IswRbVv3VEfPhby3l1LlyJhRb84cmw/J9n8ytOvv8q6tBNX6bncakmVLJUFDspPXw7683trhnDUBCA5mAAXWUMkxpHGBbK4RfnVZrsqCT6t+592C6HPc3qSL0/RDqv47t3RBLulSwKMSMy/mPKhcxqlK9UrxKvqRJ8zYDJfo+aKOFzcbnBcd4AX2dNQtpdWi5HD4ihb4UPFe0BPeNAoofjvVQOqRq+ChOxD+3zyz9IgHD20rMg0+88FgzGwBYgH9MIsHTbstr1LrwfXvyuzKXSwzTMdehW2Tf86IjOfRAhvfaMXbRqfcXP1EYvChrIg1ONooPqIz2bzP4Cs3SH7+V+T+KvjXYqpg5trjWryMoihYfHiIwRx1zY6yl03Zo4K9KlREN/fNOqEIZcui6EOoZ5Xs4vTW5ltSQ0x7AHupO2YTUGxZYmyhPZdveJcJCI7wr9WOqNJTp0nnFodbKlixqs70Ss1/fwW8mq3FtMsyFLiMPDtmoX2BzW8sWHSuVy/kOm2TuX0gDc8OBEIUQtmavVMZ4t36c8lpQTvEjdBCP2l0L2jKiZdkUg5Oek8fjoYrLjppOENo90jB/xMrg2l8ChHeg1NhICUmub9OimyrHv41D1TK9Kg/EoiqXZtYrVJcUfpq63GQ9V1YMj5g6jDze80dQYm3YHI0xfeB+ck4fpIEvCIf7iAvekg1SskTFrx//aPr3mBJXBNGbMn6r8fbpl8U5T1BIzzcxD55JTErwOPPXzWlbouNPECh85Lhe7zv38CNR904MeQXiADrWYMKPUq1+I5/ggL/OCZI8P637BLK0O4OerpnskkxdJdq6wmJATdXqQH/J8Ikzfb2C60fkbFmJfggM6TeWislyEXjNJLyKuRaM66TwhIIm9S5jKXYCshrOd2yH9E5FLMDMVQmuQGGvlIt3XE8wHbzifd5c4z240EIO5Qopk7imA8Q/3z709c7jR8ywc8I35jZ17ureVmhY1+jh5Sc+a1jPVFjAmriYzXzYzmZtHjwl4w1aH37J/hqUJR9dIoexASQc7M5HAyOo8BtzvCFuYIoW5DW2+S9DjOgkfC8oryoZfMU1mXcqrlRDC2SW2BLlTmrCWVsQ5
Hi all,

What are some of your favorite lemmas (in a world with zero axioms beyond CIC) for reasoning about equalities between proofs of equalities? I feel like my brain breaks when the answer isn't one of eq_refl or UIP_dec. Does anyone have some good pointers for useful facts about equality proofs?

Talia

Archive powered by MHonArc 2.6.19+.

Top of Page