coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with constructive rewriting

From: Jason Gross <jasongross9 AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Problem with constructive rewriting
Date: Fri, 12 May 2017 20:55:09 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f171.google.com
Ironport-phdr: 9a23:vLAxShMfAF+CPNfX8/8l6mtUPXoX/o7sNwtQ0KIMzox0Ivz6rarrMEGX3/hxlliBBdydsKMYzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFHiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZUclRWS5ODIOyYYUMEuQPI/pXopLnqFcStxazHxWgCP/txzJOm3T43bc60+MkEQze2AIvBckOsHPSrN7oNakSS+e1zLLTzT7eaP5W2y3y6JPPchAnrvGMR7VwcdHKyUQrDA7FgVCQppbkPzORzOgCr2+b7+95WO+plmUppQZxoj21ycctjInEnoQVxU7K9Cpj2oY1Ody4SFVhbt6iC5tcrT2VN4xzQs4kXmpmuz46x6UYtZKneCUG0pcqyh7FZ/CZbYSE/gjvWPuTLDtlgn9uZaixiAyo8Ue6z+3xTsm030hOripCitTMs2oC1x3X6sSeU/t9/Vut1S+B1wzO6OxIPFo4laXcK54mzb4wkoQcvV7fES/xnUX6lK6WdkM69ei08+nrfKnqq5uGO4J3igzyKLoiltKjDegiLwQDXXWX9fy51LL5/E35RLtKjucxkqncqJ3aJ94UprW+Aw9T3YYj8RG/Dyy90NkchnQHI1dFdwiGj4jtIV3BPPf4DfKnj1S2jDhr3+zGPqHmApjVMnfDl67hca9h5E5Y1Qo81stS54lUC7EEOPL8QFX9tN3eDh8jMgy72fzrCNtn1tBWZWXaKaiAeIjWrFXAsukoOqyHYJIfkDf7MfksofD02ywXg1gYKIugxpwRIF+iGe99axGbaGHrhNgbFnwR7yIxSeXrjBuJVjsFNCX6ZL41+jxuUNHuNozEXI34xeXZhCo=

Can you make a small example and report it on the bug tracker? It seems like something in setoid_rewrite might be dropping universes or something, since there's no explicit "universe inconsistency" message.

On Fri, May 12, 2017 at 4:35 PM John Wiegley <johnw AT newartisans.com> wrote:

>>>>> "JG" == Jason Gross <jasongross9 AT gmail.com> writes:

JG> What happens if you Set Printing Universes? It sounds like this might be a
JG> bug...

The output then is:

Error: Illegal application:
The term "@flip@{Top.8173 Top.8174 Top.8175}" of type
"∀ (A : Type@{Top.8173}) (B : Type@{Top.8174}) (C : Type@{Top.8175}),
(A → B → C) → B → A → C"
cannot be applied to the terms
"Type@{max(Coq.Classes.CEquivalence.6, Top.4)}"
: "Type@{max(Coq.Classes.CEquivalence.6+1, Top.4+1)}"
"Type@{max(Coq.Classes.CEquivalence.6, Top.4)}"
: "Type@{max(Coq.Classes.CEquivalence.6+1, Top.4+1)}"
"Type@{Top.8172}" : "Type@{Top.8172+1}"
"arrow@{Top.8170 Top.8171}"
: "Type@{Top.8170} → Type@{Top.8171} → Type@{max(Top.8170, Top.8171)}"
The 4th term has type
"Type@{Top.8170} → Type@{Top.8171} → Type@{max(Top.8170, Top.8171)}"
which should be coercible to
"Type@{max(Coq.Classes.CEquivalence.6, Top.4)}
→ Type@{max(Coq.Classes.CEquivalence.6, Top.4)} → Type@{Top.8172}".

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Problem with constructive rewriting, John Wiegley, 05/12/2017
- <Possible follow-up(s)>
- [Coq-Club] Problem with constructive rewriting, John Wiegley, 05/12/2017
  - Re: [Coq-Club] Problem with constructive rewriting, Jason Gross, 05/12/2017
    - Re: [Coq-Club] Problem with constructive rewriting, John Wiegley, 05/12/2017
      - Re: [Coq-Club] Problem with constructive rewriting, Jason Gross, 05/12/2017
        
        Re: [Coq-Club] Problem with constructive rewriting, John Wiegley, 05/13/2017