coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] anyone using SProp?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Dirk Pattinson <dirk.pattinson AT anu.edu.au>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] anyone using SProp?
Date: Thu, 23 Jan 2020 20:39:41 -0500
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-qk1-f177.google.com
Ironport-phdr: 9a23:Kb75qB+DKiRuZf9uRHKM819IXTAuvvDOBiVQ1KB31e4cTK2v8tzYMVDF4r011RmVBNmdsakP0ree8/i5HzBZutDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sArcutMIjYZsJao91xvEqWZMd+hK2G9kP12ekwvy68uq4JJv7yFcsO89+sBdVqn3Y742RqFCAjQ8NGA16szrtR3dQgaK+3ARTGYYnAdWDgbc9B31UYv/vSX8tupmxSmVJtb2QqwuWTSj9KhkVhnlgzoaOjEj8WHXjstwjL9HoB+kuhdyzZLYbJ2TOfFjZa7WY88USnRdUcZQTyxBA52zb40TD+oaIO1Uq5Dxq0YSoReiAAWhAv7kxD1ViX/sxaA03eQvHx/b0gIjHd0OvnPao9rpO6kdSu210LDIwC/fY/5MxTvw6o7FeQ0hr/GWWrJwdNLcxUctFwPCiFWQqI/lMC2R1usTrWeW9OVgVee1hG4mrwF9uCSgxsApioXHm4kYzVLE9SJ/wIY0Jt23Vkp7bsC6H5ZLuCGaMpF5QsImQ21ypCk6zbgGtIe9cSMXy5on3wbSZ+Kbf4WM+B7uV+acLS1miH57Zr6znQu+/Eqix+HkV8S50UxGoyRZntXWqHwBywLf5tKaRvZ9+kqs3yuE2RrJ5eFeO080kLLWK54/zb40kZoeqUHDETX3mEXylaOWb0Yk9vWx5+Tpf7nrpJ2RO5V7igH5NaQulci/DvoiPgcSWGib/Pyw1Lzl/ULnXLVHluM6nrXdvZzAJskWprS1DxFL3oo98RqzEjWr3dYAkXkCNl1FeRaHj4bzO1HJJfD1FfW/g1OqkDdqxPDJILnhDYvTIXXYn7fheKxy609YyAYp0d9f4JdUBqkbIP3vQk/xqMDYDhghPgOoxObnEcxx2Z8aWWKSGaCUK7jSsF+N5uI3OeaAfo4VuDDnK/gk/fHil3E5mUVONZWuiLcWcnPwJv16P0Sfen3qyoMNEH0J+BI3UPDrjkaFVxZaYWv0Uq4hoDgmXtGIF4DGE8qvh7qA3yq/E5B+aWVPC1TKGnDtPc3QWfAKaSGfJsJsujMBXLmlDYQm0Ef950fB17N7I7+MqWUjvpX52Y0wvrWLzE1gxXlPF82Yllq1YSRshGpRHm052al+pQp2zVLRifEp0cwdLsRa4rZyail/MJfdy+JgDNWrA1DOe96ITBCtRdD0WGhsHOJ0+McHZgNGI/vnjh3H2HD0UboclrjOHZ9tt6yFgCe3KMF6xHLLkqImigt+Tw==

On Fri, 24 Jan 2020 00:55:43 +0000
Dirk Pattinson
<dirk.pattinson AT anu.edu.au>
wrote:

> I was wondering about the same.
>
> For the example below, I gather that you are aware that Qed succeeds
> if you "Set Allow StrictProp” before the lemma.

I am using 8.11beta, and in that release, Set Allow StrictProp is not
required. In 8.10, my understanding is that Set Allow StrictProp
allows SProp to be recognized (which it is by default in 8.11beta), but
does not change the behavior of Qed. So Qed still fails.

If one does "Unset Elaboration StrictProp Cumulativity." before the
lemma, then the failure occurs immediately at the statement of the
lemma, I think because '=' is defined on Types only.

I guess the way forward is to define a library of theories using
SProp, and always use Unset Elaboration StrictProp Cumulativity. The
issue I was pointing out about the default behavior, which has
Elaboration StrictProp Cumulativity set, is that it breaks the
usability of many tactics.

-- Jonathan

[Coq-Club] anyone using SProp?, jonikelee AT gmail.com, 01/18/2020
- Re: [Coq-Club] anyone using SProp?, Dirk Pattinson, 01/24/2020
  - Re: [Coq-Club] anyone using SProp?, jonikelee AT gmail.com, 01/24/2020