coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Reasoning about equalities of equalities

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Talia Ringer <tringer AT cs.washington.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Reasoning about equalities of equalities
Date: Mon, 25 May 2020 11:33:59 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f181.google.com
Ironport-phdr: 9a23:a5Jt8xzA6Yi91E3XCy+O+j09IxM/srCxBDY+r6Qd0uoWL/ad9pjvdHbS+e9qxAeQG9mCtrQd0bKd4/+ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTqwbalvIBmosQnducobjIl/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTlkzkMOSIn/27Li8xwlKNbrwynpxxj2I7ffYWZOONjcq/BYd8WQGxMVdtTWSNcGIOxd4UBAeofM+hFrIfypVUOoxyxCgawC+3i0SNIi33s0KEmyektDR/K0Qo9FNwOqnTUq9D1Ob8cXeC3y6nIyzTDb/BI1jf59ofHbAssof6JXb1qcMrRzVMjGB/CjlWVp4DuIjSY1uYKs2id7upgVvygi2o5pA5vuTWvycIshZPIhoIR0FzL6SJ5wIMsKNC+VUV0bsKqHoFKuCGGK4t5XNkiQ2dwtSs41rAIuYO2cScExpg6yBDRZfKKfpWH7x//W+icJSp0iX17db6ihhu/70euxO3yW8e70ltEoSpLnNbMuH0RyhDe7NWMRPV6/kekwzmP1gbT5/lLIUA1iarbK4MhzaUqmpUPtkTDGyn7k1j1gq+Obkgo5PSk5uD9brjlppKQLZJ4hwDiPqg0h8CyAvk0PhAQU2Wa5eiwybju8VD9TbpWi/A7najUvIzGKckeuKK2GAFV3Zsm5hu9ADqr3s8XkHwcI11bdhKHgY3kO1/QL/35A/qyhkqjnyp2yP/aOLDqH4/DIWLZkLj7eLZw805cxxQ3zdBY/59UD6sOIPP3WkPordzYEgI1PxW6w+r6C9hxy5kSWW2IAq+eP6PStUGH6vgzLOmLYY8ZoDf9K/476P7ylXI1h0MRcK2z0ZYUaH20BOlqLkSFbXb2n9sMEnoGshI7TOPwiV2CVTBTZ2y1X6I5/jw7CoWmDYHCRoCunrOB2Dm0EYNNa2BJD1CDC3bod4GeV/gQbyKSJ9dtkiYYWri5V48hyRauuRfmxLpgN+rY4zEXtZb+1Ndu/ODTjhEz9TlsD8uHyW2NTmd0nnkJRzAsxqx/r1Z9mR+/1v1EivhZHJRp5vVGXx1yYYLGzup1BsraURmHYd6SSFegTcmhB3c8Qs9nkPEUZEMoUdeliBHA0i6nDpcakrWKANo/9aeWlyzzIMB8yHvC2aQJgFwvQ88JPmqj0P0svzPPDpLExh3K352hcr4RiWuUrD/anDi++XpAWQs1ap3rGHUWZ0/Yt9P8vxqQQLqnCLBhOQxEm5fbd/l6L+bxhFADf8/NfdTTZ2XrxTW1DBeMg6qQNc/kIjVEmiraD0cAnkYY+nPUbVFiVBfkmHrXCXlVLXyqe1nlqLAsp3ayT0tyxAaPPRVs

My favorite are the lemmas about dependent decidable equality. Mostly
because of how hard many are to prove when the dependent parts of types
get very messy (which are my favorite types).

In https://github.com/jonleivent/deptacs, I was playing with an Ltac
mechanism to automatically prove lemmas of dependent decidable
equality that were too hard for Coq's built-in "decide equality" to
solve (at least that was the case 4 years ago). It worked pretty well,
but there were still some very hard nuts it couldn't crack on its own.

On Sun, 24 May 2020 20:30:05 -0700
Talia Ringer <tringer AT cs.washington.edu> wrote:

> 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

[Coq-Club] Reasoning about equalities of equalities, Talia Ringer, 05/25/2020
- Re: [Coq-Club] Reasoning about equalities of equalities, Jason Gross, 05/25/2020
- Re: [Coq-Club] Reasoning about equalities of equalities, jonikelee AT gmail.com, 05/25/2020