coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to rewrite, needed to match goal

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to rewrite, needed to match goal
Date: Wed, 30 Dec 2020 15:55:01 +1100
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=Qu/jr+YNV0aehw3OQriI6wfZyByPgtWZxLqNrccj7jc=; b=YLyUnl6DCBsZJQkbSc5WPUbz6Fs/ycqF11Q/qrOt2BOfEIwr88k2jXKwGdeFj56BH6k7vpTmJdni280BSzzsQKdXC3Q9wlfpsk4E9yWFGRSgRGAJWAs3dM21J2UpsRqm05MZUrD4+eBHWMMh+WfbvTAq5wZ2bqnydoZ4xS0z+07SUmwwEFljoyT1027Q4kOF9dZ5RF1+gOJKaO45vsmHAl9ilGD1Q8373DJ6VaqTpNtGu3qD2CeIbqve3pRl9tn++N8ONDIK/A6DFmC/3Dw3g3dBtkDvaGIhLCq51G7kepN1q8ri819h14b7A63sw2HWDx2ogsnTPwbdBGzqACmrTg==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=nA5j2OEYY1hhXvcoKSgHC3Q4KNBU91qvTUeUc89e2DUiKcIxKs08qM2WMtvpud7lc2Pzn0w0BQoSYo3I3i4XiwN/elvP7RFajdfFirjFUBLUspMkA1IYtqglbdjwt9Keja6qVpW5SSIGAAqNUkQ7qSWNRj1wQ2e6TbyoGLRISZZeN4GuqBhkvlznfG4kvg7YZPmX6h5BI20QLTo6JGrPNlLCZ/edIXQuK+jFCEZC0qqh+Ge3kFVx+yYmPlN0QDiCg0j60ntqIzFU/knTAbYtDI7/2NHAyfOBxasyN4/RF0EoSUMjanfoFwtsehUBNtH+7jXysxNe71Sr+VJg4p3s7Q==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY4-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:If/8jh8GuWccEf9uRHKM819IXTAuvvDOBiVQ1KB32uocTK2v8tzYMVDF4r011RmVBNqdsagewLWL+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhKiTanf79+Mgu6oQrTu8QWnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahNFugqJVoByvpBJxzIDWb46JO/R+f6zScMgGRWdCRMtdSzBND42+YoYJEuEPPfxYr474p1YWqRWxGxOsC/3qyj5Im3T407c10uo6EQHB2gwrAtUDvnDKo9XvKqgSVOC0wLPGwzrZYfJWwjD96I7Tfx87p/GMQKh8ftTMxkkyDQ/KlEiQpJXjMjiI2esDr3KV4PB8VeKzlWEnsQdxryChyMswloXHiZ4Yx1PY+ChlwIg5OMO0RFBlbdK5DZZeuT+XOYt1T848Xm1ltyk0x7IJtJO0fSUG1psqyhzRZfGHdYWD/xHtVP6JLDp3mH5pYq+ziwqw/ES61+HwSsu53ExOoydGitXBuXQA2wbO5sWFTvZx5Fut1SyS2w3Q7OxPPFo6mrDBK5E7x749jpoTvlrHHi/xgEj7kKGZeFg49uS18ujpf7fpq5CFO49zkQ7xLL4imsuiAeQkKQcOWHWb+eKh27H55U35WrJKjuEonabFrJDaJMMbpqijDw9Sz4Yj9xK/DzCh0NQbh3UIMFVFeBefg4joPVHBPuz4AO+wjliwijtn2uzKM7/7DpnQMnTOkq3tcLJ+5kJEzQo819Ff55ZaCrEbJ/LzX1f8utjGAR8jLQO0xubmBM9z2IwEV2OPGaiZMKXJvFCS4OIvPvOAa5EItzbgMfQq/ePugWcjmVABZampwYcXaHegE/t6JEWZeGPgjcsFEWcXpQUzV/fqiV2HUT5LfXm+RaM85jchCIKnF4jPXI6tgKbSlBu8S5ZRfyVNDk2GOXbubYSNHfkWOwyIJco0sDEeWL2wA6Moygqpskeu6bd9I+/FvAERqonk0vB84fCVmB0vszVpWZfOm1qRRn15yztbDwQ927py9BQkmwWzlJNgivkdLuR9ovZAUwM0L5nZlrYoAtbvHA/NY5GAVQT/G4j0MXQKVts0huQ2TQN9FtGl0k+R9heRW+ZQrI3XQZs+/+TbwmT7INt7xzDezq49glI6Q8xJc2q7mqp48AuVDInMwRzAy/SaMJ8E1SuIz1+tiHKUtRgCAgd2TOPIUW1Zb1aE9dk=

Hi Clement,

Thanks - but this doesn't help.

Ie
Set Printing All.
Show.
then Check (cut and paste from the goal, with lots of @ everywhere)
still gives the error,

The term "d1" has type
"@dersrec (prod (list (PropF V)) (PropF V)) (@LJArules V)
(@emptyT (prod (list (PropF V)) (PropF V))) lpst"
while it is expected to have type
"@dersrec (prod (list (PropF V)) (PropF V)) (@LJArules V)
(@emptyT (srseq (PropF V)))
(@cons (prod (list (PropF V)) (PropF V))
(etc)

Thanks also for your other reply

Cheers,

Jeremy

On 30/12/20 2:50 pm, Clément Pit-Claudel wrote:

On 12/29/20 8:36 PM, Jeremy Dawson wrote:

I don't understand how this can be possible. Wouldn't you expect Coq to
refuse to have a goal containing a type error? What would be happening here?

It's a type inference issue. If you use `Set Printing All` before `Show` it
will give you all implicit arguments, and then Check should work.

[Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
- Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
  - Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/17/2020
    - Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/17/2020
    - Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/28/2020
      - Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
        
        Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
        
        Re: [Coq-Club] how to rewrite, needed to match goal, Jeremy Dawson, 12/30/2020
        
        Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020
      - Re: [Coq-Club] how to rewrite, needed to match goal, Clément Pit-Claudel, 12/30/2020