coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] how to stop Coq from unfolding defined constants

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] how to stop Coq from unfolding defined constants
Date: Thu, 9 Jul 2020 23:46:07 +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=5AXsMBFtumNaESrWfNqdLM7bjDBlt3Gc0VybqzmN8wI=; b=DOAVQm7/g76fIuz/fDZKt2nTK74TjQnHI/cFuTq0uDg8ZG+iDfqdhNeBOr7lcO3cjcBHblz9s5lbpb0wFRW/fPtNnIZhSkzCF/Cw4F00Rp2/lLBAushV8Wz/eS4/H3CcxbGqJ1dt8s7H7ecb9RnO/p8BDjVpJpjA8E9AoWCfhAHkzv5/XqhZZEuF/ArwGNJ4qQj+iVgoazJ3gIfwJYIwM86imOa27XSrEDD0skA6SdQY9qQcep9e3CrNaoAKMqblpm8R9ZjvQDYfrzWFX6BrhvU0S6d1ZxjIBM6g1njNEOKYekbj2t4EVI0TawVAVcDKo35C9CQeHdtb9cYEo9rxdQ==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=HITX6Rj7ugWDwm6s9rdjJco65d9Ab/Y2j0cjLs3ldxFIg+5r/7jCxc9SEw/O3D30kaiey8f2t0ebhsEYQgPn5Je8LNYXsldGi8TRogqTEyYQZ01G1M68kUE70/QPC7bpJfrktSo309IyDk+F9bdPRrw92jfsYepvIeJUsWLPZB2bZ2UxMKMSAfSVVUyiGjdg9wLbgHviUHgzZtlOitH0XjLCni3YJ0MFvQ3AHSIQewPyu9z5FSPo3i5Yl0hR8VzUBD/YWs99n1baFILEtK8KRtsqqEdKyi+bssgE/J5tNyOS2ED0P3FUpuHNxbXXWxKAvSh7UA4/hQQyvTc5VlbJpA==
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-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:70WRdRRFfatabQ98voNy3Jrbdtpsv+yvbD5Q0YIujvd0So/mwa6zYBGN2/xhgRfzUJnB7Loc0qyK6v6mAD1LvM3J8ChbNsAVClld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6c8xgHUrnZMdOhbxW1lLk+Xkxrg+8u85pFu/zlQtv4768JMTaD2dLkkQLJFCzgrL3o779DxuxnZSguP6HocUmEInRdNHgPI8hL0UIrvvyXjruZy1zWUMsPwTbAvRDSt9LxrRwPyiCcGLDE27mfagdFtga1BoRKhoxt/w5PIYIyQKfFzcL/Rcc8cSGFcWMtaSi5PDZ6mb4YXD+QPI/tWoYrzqVQAsRSwCgajBOL0xz9UhHL7x7E23/gvHAzE2gErAtIAsG7TrNXwLKocVf66zLPWwjXGb/JdxDnz55LGcxA6pvGMW697fM3Vx0YxDQPKkFCQqIz/Mz2bzOsMvXOb7+1mVe+0kWEnrRxxriKxycgxl4nFnJgayk3d+Ch/3Y06KsG2RlRhbt64DJtfqTuaN41uT80tTG9ltzo2x7IatZO/cyUEx5oqyh3RZvCaboSF7BLtWeWfLDplmH5oZbayihKu/UWixODxSNe53UtEoCZYjtTBsG0G2R/L6sWfRfZx4l2t1SuT2w3R8O1IPE45mKjBJ5Ml3LI8jpUevEDZEiPrmkj7iLWaelsm9+Sy9ujrf7brq5mBPIFukA7+KL4hmsmnDOQ4LAcOW2+b9Pyg2bLt4EP1XKhGguQrnKbbvp3WPMMbqbWnDANP1YYj9gq/ACyh0NQFm3kIMUhJeAqdj4juJ1HBPuz3Deu+g1Srljdn3ffGPqD9ApXJKXjDl7Thcaxh5E5bzQo/1dFf55RKBbEdOP/+VVP9uMbFAhMlMQG42fvrBdt/248EXW+DHLeVMKbIvl+J4uIvLfOMZIgQuDvlL/Yq+eTugmE8mV4dZ6Wn04EYaX6jHvRhJUWUemDjgtEcEWsQoAUxUfHqhEeYXj5Of3qyRb4z5iknCIK6CofOXpyigLuY3CuiApJWYn1GBUuXHHfzd4SEXu8MZziILs9glDwET7mhRJU72RGgrg+pg4Zge6Df/TRdvpb+3vB04ffSnFc873Y8W8+ayiSGS3x+tmIOXT4/mq5l9x9T0FCGhIp1mfFdBJR/7uxSVQFyYbzR1eF/GpbeUx3aedGhQVC7BNiqHHc4U4RikJc1f09hFoD63Vj41C2wDupNzu3ZNNkP6qvZmkPJCYN4wnfC2rMmigB8EMJJKCurirM5/hWBXteUwXXcrL6jcOEn5ACI9GqHyjbR7mhla1YpFJ70BjUYbEaQqsnl7ETfSbPoEa4gLgZK1c+FLO1Nd8HtilJFAvzkPYaHOj7jqyKLHR+Ng4i0Qs/yYWxEhnfUDlVCngwOu3+bZ1Az

Hi,

I have a goal

swapped ((single a ++ qs) ++ vs) ((qs ++ vs) ++ single a)

where single is defined by

Definition single X (a : X) := [a].

When I try

rewrite - !app_comm_cons.

it unfolds one of the occurrences of single x

(which stops my carefully written Ltac function from working and took ages to pinpoint what was happening).

How do I stop this from happening?

Thanks

Jeremy

[Coq-Club] how to stop Coq from unfolding defined constants, Jeremy Dawson, 07/09/2020