coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Avoiding the use of JMeq_eq

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Avoiding the use of JMeq_eq
Date: Fri, 26 May 2017 20:06:18 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Neutral smtp.mailfrom=e AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-b.ensmp.fr
Ironport-phdr: 9a23:XT5/QBwSi+Vwx5vXCy+O+j09IxM/srCxBDY+r6Qd1OIWIJqq85mqBkHD//Il1AaPBtSFra8bw6qO6ua7CDNGuc7A+Fk5M7VyFDY9yv8q1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twvcu80XjId4Kqs8yAbCrn9Ud+hL329lK1aekhTm6sus4JJv9jlbtu48+cJHTaj1cKM0QKBCAjghL247+tDguwPZTQuI6HscU2EWnQRNDgPY8hz0XYr/vzXjuOZl1yaUIcP5TbYvWTS/9KhrUwPniD0GNzEi7m7ajNF7gb9BrxKgoxx/xJPUYJ2QOfFjcK7RYc8WSGxcVctXSidPAJ6zb5EXAuQBI+hWso79p1UAoxS8BgejCuzgxSNHiHLtwa06yv4sHR3a0AE6Hd8DtmnfotXvNKcVVOC41LfHwC7Mbv5VxTvx8o/IcgouofqRWb5+fs/RyUgrFwPEiVWbtIjrMC2O1vwXqGiQ8utuWviri24jtQ5xrT+vzdowh4nTh4Ia0EvE+SB/zY0oJtO4UFZ2bcOgHZZfrS2WKZZ6T8w4T211uCs3yacKtYO1cSUL0JgqxB/SZ+aGfoWK+B7uUPydLSl2iX57fr+0mgy8/lK6yuLmU8m5yFZKoTRBktnLrn0CywDc5tGbSvtg5keuwzCP2xnJ6uFDO080kKvbK5guwrIpjZUfq1rMHintmEXzlK+abEsk+vKw5+TmZLXpuIOcOpdphgz6PakigNKzDfk3PwQUQmSW+eex2Kf+8UD3QbhGlvg2nbPYsJDeK8QbvKm5AwpN34k98Bu+ADSr3MgCkXkANlJFdwqLj5L1NFHWPPD4EfC/jkywnzds3vDKJ6HuApHQLnfYi7rhZrZ860tEyAUp19xf5pRUCqsAIP3pQEPxusbYXVcFNFm/xP+iA9Fg3KsfX3iOC+mXKvD8q1iNs+8HM7nUIogPt369Bv0k4//pxV00gs0GNYag2Z8aZ3fwN+5nKl7YMimkucsIDWpf5ll2d+ftklDXCTM=
Organization: X80 Heavy Industries

e AT x80.org
(Emilio Jesús Gallego Arias) writes:

> You could try using `eq_dep`, with can be usually made axiom-free as
> long as you can prove you indexes are decidable. In this case you need
> to elaborate a bit more:

Also as Dominique points out, you could try define inversion lemmas, I
prefer to have them with some computational content (small inversion??)
so that using them as views is easier, but YMMV, they may become
cumbersome.

Example:

Lemma RoofHom_inv o1 o2 (f : RoofHom o1 o2) :
match o1, o2 with
| RNeg, RNeg => consequence_1
...

E.

[Coq-Club] Avoiding the use of JMeq_eq, John Wiegley, 05/26/2017
- Re: [Coq-Club] Avoiding the use of JMeq_eq, Dominique Larchey-Wendling, 05/26/2017
  - Re: [Coq-Club] Avoiding the use of JMeq_eq, Dominique Larchey-Wendling, 05/27/2017
    - Re: [Coq-Club] Avoiding the use of JMeq_eq, John Wiegley, 05/28/2017
- Re: [Coq-Club] Avoiding the use of JMeq_eq, Emilio Jesús Gallego Arias, 05/26/2017
  - Re: [Coq-Club] Avoiding the use of JMeq_eq, Emilio Jesús Gallego Arias, 05/26/2017