coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] why does simpl fail?

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] why does simpl fail?
Date: Sat, 25 Apr 2020 20:51:25 +1000
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=hHkPRtpNjlUX/sSW6VpO/EgS/fUWEMMQ/7SVLAzvbK4=; b=KNy806IywEl7U6CSuPgBjIGYrc10GWcaYQCUye2nWrLah5FZDgUa2ZSuxFsE5IFf7wVNn/NVGlUJm5/i19NJI+A+uNaX7QUGdJ/wIeC7+asHIcQMz4G+CUEQXsxhnPN5lLTxKsdBOjqv+HOsezs0/SKpX6X0JZ/hwbV6EBhoRoTGZ6wsZr0uZIvDC3EmDPvNTKOGmIHr8F4sPZ6hyJ+Yjc82mIZVEXL9/YzqdYdKFmL7tWBLFamgxdJgnDBvvsXkuuFa39nQdGRAnB+3R3RTw42E4Doo0zWHl7h2RhWmL9vmGLW01gSTMzGGugvIP2BsXXJsoOmL2ttzbiozAR4Awg==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=mgi4Z5cC7huMrjsYlqAl+G3y8Jj+bBIF8lGCzfIRqU7v2zH4cgDkZ84AtGg8fngq7o47rtcV2vjR0XGsnVZ4LQWG154j5WRsNfoj7bSSNsReiixaoUbm458om+zydsinaB04ylDHH+kKJ8+5LFn4WF7lN7/TtBgx66lQXxbmr8AlGXKzoAozvPEolO4Z4GYkupbA7V3jWo0YA3Cpx9ruGiUF3/k2OPiBeqXzNUwFSG4r3yTCInuEbIq5B+iMt3JZ63GZUUG1BNTIoY0qTyJKujLVo3lPp7MIvEpBilA4RDS9SolTb/NCxO/L3SxzjltDBS3O6LqRwvy+IJlK2YOobQ==
Authentication-results: mail3-smtp-sop.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-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:cScJtBNOCNUyJFDJKYEl6mtUPXoX/o7sNwtQ0KIMzox0Iv7+rarrMEGX3/hxlliBBdydt6sZzbeK+Pi/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe9bL9oLBi7ogrdutUUjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaktJ+gqJGrhyiqRJwzZLbbo6aO/p/Za7dYdEXSHBdUspNWSFMAIWxZJYPAeobOuZYqpHwqV8QohukGwasAePuwSJGiHDs06w6yOMhEQfb1wEnG9wBrm7Uo8vwNKYSS+y7wrPHzDvYb/NR3zfw85LHchY8of2WQ71/bNfRxVM1GAPYl1idr5HuMTCN1ukVvGWX8/BsWf+zh2MlsQ19vzaiy8U2hoXUiI8YxEjI+Cp9zYovONG1S1J3bcSmHZZerS2WKpV6Tt8kTmp1oig10KcGtoS+fCUSyJQo2Rrfa/uffoWU7B3tSfqdLSphiHx4er2yiQ++8U+7xeLiTMW010tKrjZendnLq3AN0QHc5tKfSvtn+UehxSiA2BzP6uFFJkA0k7DXK5k8wr4skpoTtkPDHizslErqi6+Wc10o+umu6+v5frXrvpCRO5Nuhg3jLqgjmNazDfk2PwUMRWSX5Oqx2bP78U38WrpKj/k2kqfDsJDdIMQWvqq3DBFP0ok97ha+Dy2q3toCkngJN1JFfxSHgpPzNFHIPfD0F+mwjEmxkDtx3f/GI6XtAo/RIXjbjLfhYbF95lZAxwo01NBT/o5bCrUcIP3oQULxr9zZDhohMwOu2ernCdN91pkfWW2VGKOZPrnS4he04bdlKO6VIYQRpTzVKv4/5veog2Vz0QsWerDs1p8KYli5GO5nKgOXeyy/rM0GFDIosxAzSf2ipFSdSjlVLyKQUrgx4yB9JIu5FoDFbomrnfqM0Dr9F4AANTMOMUyFDXq9L9bMYPwLci/HepYwwAxBbqCoTsoa7T/rsQb7z7R9Ke+NoH8Rs4+l2dRooeTOx0hrqG5ESv+F2mTIdFla22MFQzhqg/JWnHclkxK44PM9hPZVU9tO+/lOTwE2c4bGyPB3AMzzXQSHecqVTFGhQZOtBjRjF4ttke9LWF50HpCZtj6GxzCjWuVHnrqWQpE47+TVwiqpKg==

Hi,

I have a definition

Fixpoint dersrec_hd X rules prems c cs
(ders : @dersrec X rules prems (c :: cs)) :=
match ders with
| dlCons d ds => d
end.

but when I try do prove the following, I would expect the simpl step to simplify it to d = d

Lemma dersrec_hd_eq X rs ps c cs
(d : @derrec X rs ps c) (ds : @dersrec X rs ps cs) :
dersrec_hd (dlCons d ds) = d.
Proof. simpl. (* does nothing *)

What could be the reason for failure here?

Thanks

Jeremy Dawson

[Coq-Club] why does simpl fail?, Jeremy Dawson, 04/25/2020
- Re: [Coq-Club] why does simpl fail?, BEGAY Pierre-leo, 04/25/2020
  - Re: [Coq-Club] why does simpl fail?, Théo Winterhalter, 04/25/2020
    - Re: [Coq-Club] why does simpl fail?, Jeremy Dawson, 04/25/2020