Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] match on multiple goals simultaneously

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] match on multiple goals simultaneously


Chronological Thread 
  • From: Jason Hu <fdhzs2010 AT hotmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] match on multiple goals simultaneously
  • Date: Thu, 28 Sep 2023 15:33:58 +0000
  • Accept-language: en-US, en-CA
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; 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-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=vDVFWBydtrO3mm7QXLNIFjbbOZ9ji8n7BgW9GWczvaQ=; b=IbEkgtzBQhFs1A27mSv+YQF2lyrcDmGvJJYkZgKYy3PpkodTjcqFtYk6Z6IyERwjqb/TgShz6/9FsHcx4h2hHZ3HsIZz35U2aPtR1JIgMB8tOSdjrwO1+9zVgFpoQcWKEyjOxBQvtTDccSk4XfvKKd4qznKYK7qzKWjPmmW5CCTysylCpYF/zTe/I0fzuPxve7dJR587WZs4cysmYeThMwU5iu9lfNEBbpro2JYe3eAPLAUC/Wid3SY0TiNrKKwzaFjbLUzFKd41XlGgVlil41MzJd7O9ilbMx3A6Yb0r0jNzG4qvg9t3iEivnjF+Kcs20KBZ9vz7JngH6tEaJKqNA==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=oURYQ9TgVTqLL5OaxqbwLKPoVWD5VUQYuBHgxz+K2JmKasNa4poFK/NRktL8+X+p95NdElPMGKmW8dL1YL2zUr03ulsXs5OGUsCQmfVwg7JJEgzjYLg80Zbl28Ve3Ps/WUiG1YIYUYwLlFNv7HK1/A1zrE2m12RM+/4FMkPLuN3ZdhrMzl2mTAHKljD0CqWvA6hUVs37CShzQkINijqG8dXHhnwNZ9sBey7WY1Pp3UCp5sVftp5CvKdT2+CQnZq4ynQjceBIy5/fTVH2uM6vJxAlcLIAHY9sD8neVWItBymGpfCs0Rg6xkx4taxW6qP9GHtXPP3Oq3JnML23245DAw==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM10-BN7-obe.outbound.protection.outlook.com
  • Ironport-data: A9a23:jhWeeamwuvV4vUDidL63Uq/o5gxPI0RdPkR7XQ2eYbSJt1+Wr1Gzt xIYCmHQaP7cNGf8Ktkjboiy9U1TuMXRmIJrSwpvqXo9FltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajl8B56r8ks156yj4mNA5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1zHhx1O9QWxt1GQmxt7 dk4Ex4AdS6c0rfeLLKTEoGAh+wFBeyyZMY1nC4lyjvUS/E7XZrEXqPGo8dC2ys9jdxPGvCYY NcFbT1ob1LLZBgn1lU/VMp4zb3u2iG5I2MwRFG9/cLb50DdwAxjy+K1aYL9etuWQMxUmgCTo WeuE2HRW0tKaIzBmWvamp6qrvDSv3nEfKk0KJaf9q9DhnKM4Gc0JxJDADNXptH80CZSQel3I EsNvyEqsKIa712uVtC7XhuioXfCsAR0ZjZLO+gz6QXIwKyL5Q+cXzADSj1HMoR26okxWCAg0 UKPk5XxHztzvbaJSHWbsLCJsTe1PitTJmgHDcMZcTY4DxDYiNlbpnryohxLS8ZZV/WkRW+i8 CPAtyUkmbQYgOgC0qjxrxiNgCuhqtKNBkQ57xneFDDtpA5oRp+XV6rx43ji7NFEMNm4SHuFt yM6gMSw1r0FIqyMsy2ve98zOo+VycyLCgCBvm43LaIdr2ys31WBYbFv5CpPIRY1E8QcJh7sT kzhmSJQw55xO3HxV7NGXIaqL8EM06LbNM/EU8rMZYFkealBdw6g/QBva3WP3mvrrlMerKEnN bqfcueuFXw/C5k76BaTWMEmzq4N1AIy4UjxVKLL5U2r/pTGbUHEVIpfFkWFa94IyZ+toSLX1 o16HNSLwRAOa9/OSHDb3qBLJG9bMEVhI479rvFWUeuxIgBGPmUFIN2JyJMDf71VpYhkpt3qz FqcBHABkEHegEfZIzqkcnpgMbPjfahupEIBYBADAwya5GgBU62OsoEvL4A6bJs2xtxFlPRUd cQIS++EI/ZISwnExQgjUInAnNRiWSmv1C2zPHuDQTkgfpRfaRTD1f36cyDOqiQfLCqFmvEvg r+n1wr0EMIJeCp6Bu2Lavj1l1KVlloekdJUQEHnDIRyekLt0Y4yMA33rKY9DP8tICX55Amx9 lipEzZBgsLSsaoZzcLsh6uVn7y2EuB7IFVWL1Pb4ZmyKyPe2Gipmq1Eb8qlYhHfU3HS6oy5R OAI0cz5DuILrGxKv6V4Dbxv66A0vPnrhr1CyzVbDGf5VEuqBpxgM0u585F27IMV/YBguCyyR k6r0ftZM+/QOMraTXggFDB8ZeGHjfwpij3e6MouG3rD5Qh1wuujcV5TNByymiBiPONLEIc68 9wA5u8SySKC0yQPDPjXrxpp51ytL2MBWZoJrps1IpHmoSt1x0BgYa7zMD7X4paOV9ZiFGwWC yOth/aZo4sNx3j5LmQ/JULM17FjmKYl5Q9ByQ5aFWuvwtP61+IT2UwI/RsnUA4P1Qh2ibNvG 2l0Nn9aIbeF0CdoifNiAUGtOVBlLz+I9nPhz2AmkDXicHCpcWjWPkgRBP2o/n1F1059JR9g4 6C/5EDpdR3IbfPB9HI+dmA9osOyUOEr0BPJnf6WOvisHr44RGHAqbCvb29ZkCnXK5o9q2Ofr NY74dsqT7PwMBMRhKgJC4O687A0YzLcLUxgRcBRxo84LVv+ShqThwfXc1uQf/lTLcPk6UW7U sxiBvxeXiSEiRqhkGopOr4uEZRVwtgZvdYMQ+a+bypO+b6StSFgv5/s5zDzzj1jCclnlcEmb JjdbXSeG2iXnmFZgHLJsNICAGejfN0Yf0fp6YhZKgnS+04r7ImAsH3e04dYe12zGS4+p1e+m lyGYKXbiet/1Y5rgo3gVL1ZABm5Is/yU+LO9x2vt9NJbpXENsKmW8Y9tAz8JwoPVVcOc40fq FhPmIefMID5UHIeU2fFnpCAE+9C4sDasC9/LJfsNHcD9cedcJaE3vbAklxU7bRJl89Y78ijA QC/baNcsDLTt8h1nBVoVsSVL/rR52kboEstSeNRYslg0iQg7DE=
  • Ironport-hdrordr: A9a23:+0lITKOC0PuFecBcTwr155DYdb4zR+YMi2TDiHoddfUFSKalfp 6V98jzjSWE8Ar5K0tQ4uxoWZPwN080kKQY3WB/B8bHYOCLggqVxcRZnPLfKl7bamTDH4xmpM BdmsFFYbWeY2SSz/yKhjVQeOxQo+VvhZrY4Ns2uE0dLz2CBZsB0y5JTiKgVmFmTghPApQ0UL CG4NBcmjamcXMLKuymG3gsRYH41pb2vaOjRSRDKw8s6QGIgz/twqX9CQKk0hAXVC4K6as+8F LCjxfy6syYwruGI17npiPuB9k/oqqt9jJwPr3DtiEnEESstu+cXvUvZ1Xb1ApF4N1Hpmxa0+ Uk6C1QRfibo0mhA11d5yGdkzUJ3FsVmgPfIHKj8AneSPbCNUcHItsEgZgcfgrS6kImst052K VX33iBv54SCR/bhizy69XBShkvzyOP0A0fuP9Wi2YaXZoVabdXo4Ba9ERJEI0YFCa/7Iw8Cu FhAMzV+f4Te1KHaHLSuHVp3bWXLwAO9jzveDl8hiW46UkkoJki9Tpo+CU2pAZxyHocI6M0md j5Dg==
  • Ironport-phdr: A9a23:ChUA4BIXtmgLePR1wdmcuIBuWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFtbM11BSUDc2bs6sC17CI9fi4GCQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgH c5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTajYr5+N gm6oRneusQWgoZpN6I9xgfUrndSdOla22JlKUiPkxrg48u74YJu/TlXt/897cBLTL/0f74/T bxWDTQmN3466cj2vhTdTgWB+2URXHwOnhVHHwbK4hf6XozssiThrepyxDOaPcztQr8qXzmp8 rpmRwXpiCcDMD457X3Xh8lth69VvB6tuxpyyJPTb4+IKfp+Zbvdcs0GSmpdUMhRUClBDZm9b 4sJEuENOelVoo34q1YIsBCwBxSjBPn3xzFImHH4wLE63eoiHwHI3gMvA90BvW/Oo9npKKsfS /y5wLXKwDjFcvhY2S396I/Nch05pf+DR6lwcc3XyUIyFQ3Fk0ibpIvrPzyI1uQMsnOb4/R8W e6yl2IqsAFxoj+zxscpkIbJh4YVxkrY+iV+xYY4PNu1Q1N0btC4CpVfrT2aN5doTcM4RWFlo Do2x7wGt5KlfCYH1psqyhDRZvCacIWF5g/uWumPLTp2hHxoe66yiwix/EWixODxS9W43VVLo ydFkdTBqnAD2hjV58OaRPV9+UKh1iyO1wDV8uxELkE0lbbbK5482bE8jJsTsUPbEiDqn0X2l qmWeVsg+uis8ejofKjppoKaOoRpiQ/+Krwjl8OjDegiNgUCQXKX9Oug2LH5/kD0Qa1GguM3n 6XFvp3XINkXqrKiDAJU14su6wuzAyuj3dgFknQIMFdIdReFgoXvJlrAOur3De2ljFSpiDprx +7JPrnmApjVNnbOjLDvcath50JF1Qc91dJS64tTCr4aPv3/QEjxtMHEDhAiNAy03uDnB8hn2 oMGQ2KPBbOZP73Ovl+U5+IvJO+MaJUSuDbgN/gl4/nujXg6mVMHYaap2p4XZGi5HvRgPUqZf WLhj9gdHWsQugcyUvbmhVKeXTJJZHu/Xrow5jQhB4KnCYfDSJqtgLuE3CqjEJ1Ze2BGC1GXE Xv2a4mIRusAZTmSIs9mjjwEUKKuS44l1R20qAD6zL9nIvLS+iIDrZ3jzsR65/XPlREu8jx5F 9mR33mXT25ohmMIWyM23KdnrENhzVeDyLF0jOBcFdxO/PxESRw6NJ7Zz+xiEd/+QAPBftGTS FanWNqqGz8xTshii+MJNk16ApCpig3Jl36hBKZQnLiWDrQ19Ljd1j7/PZAu5WzB0fwDhkIhR INvKCXyiKJ/5ROJX9eRu0Wei6OjdKBa1ynIojTQhVGStV1VBVYjGZ7OWmoSMxeHxTyYzkbLT rv0TK8iLhME08mJbK1Ddtzui1xCAvblItXXJWyryC+rHRjd4LSKYcLxfnkFmj3HAR0KnwAB5 izebFAWBiC9pmvfCHplEle8K1j0/7xGoWigBlQx0xnMakRg07Sv/RtAi/CcWehJhutckCcmt zB9HVL71NXTWJKbvwQ0RKxHepsm5Utfk2LUswsoJpu7M6VrnUITaSxRlma3j1BdLNoFlsIn6 nQ30AB1NKSUlktbcC+V1ozxPbuRLXTu+BeoaOjd3VS2PM++3KAJ5bx4rlziuFvsDU8+6zB91 NIT1XKA55LMBQ5UUJTrU09x+QIo77fdKjIw4Y/ZzxgOeeG9ryPC1tQ1BeAk1gfoftFRN7mBH RPzFMtSDtanKegjkVykJhweO+Ua+KkxNsKgP/yIvczjdOhsnCC91zweuKh91V6J/it4DOXP2 tdNwv2V2BeGSyaplE2o4Yj8nYFJYy1XH3LqlXCiVdQXOvU0LdhYbAXma9e6zdh/mZP3DntR9 Vr5QkgDxNfsYx2ZKVr0wQxX000T532hgyqxiTJuwFRL5uKS2jLDx+P6eV8JIGlOESNsgVf+O tLs1ogyXE+0agEokF2u4kOwlM057OxvanLeR0tFZX28IW1iQLDq7uPaS85I9JYhsCERW+O5K wP/KPa1s14R1CXtGHFbzTYwemSxu5n3qBd9jXqUMHd5qHexldhY/R7E/5ScQPdQ2mBDXyxkk XzNAVP6OdC1/NKSnpOFs+akVmvnWIcBOSXsyIqBsmO86wgISVWxk/ChgYe/SFAS0Sjn0tBrU WPDqxO0boTw1qu8OP5qZQE0XBmtsYwmQscuzMM5n9kI1GIfh4mJ8HZi8y+7Kthd1a/kLTIMS TMN39/J8V3g0UxnIGiOwtGxXXGcz819ItiiNz9OnHNnqZwSTvfKv9km1WNvr1G1rBzce614l zYZk7417WICxvsOs0wrxzmcBbYbGQ9ZOzbtnlKG9YPbzu0faWCxfLy3zEc7k8qmCeTIrA1cS m2jIs56NS938sB2MVaK23r2oNKBGpGYfZcIuxuYng2VxeZZKIAqzKJT3QJnPn74tHwhjeU8i FY9uPPy9JjCIGJr8qWjBxdePTCgfMIf9AbmiqNGl9qX1YSiTd1xXy8GV5zyQbe0ASof4L75Y h2WHmR2+RL5UfLPWBWS40B8ozfTHoC3YjuJcWIBw4wqRQHBdhEFxllMB3Ni2MZ+T1/ixdS9I hshoGFLoAa+8lwVlIcKf1H+SjuN/V/0LGtrDsLHakIRtFoK5l+JY5XGsqQvQGcBps3n9EvXc SSaf1gaVDlVHBDbQQ++eOHpv4WlkaDQB/LifaKWPfPS9qoDDLHVndX1jsNn52jebMzXZys7V qRp1BYbBSIrXJiJ/ldHAy0PyXCXZpbC9k7lo3958pjkoqasBFOn5JPRWeFbaYw9oknv06nfb 7XC1H4hcWQKkc5UoB2AgLkHggxIgnk3JWD0SOYO6XaWHqmIwvcFXVlGMmtyLJUatatkh1sUY JeJhI+tjex21qZtWQUCCAap38itYYZiz3iVDFrcHw7LMb2HIWeO2MTreeamTrYWiuxIthq2s DLdEkn5Pz3FmSO7HxyoNOhNimmcMnk88MmldQ1xDGH4UN/8QjuSFYYvyBcQnvgzjH6MMnMAO z9hdU8LtqeX8S5TnvR4HSpG82ZhKu6H3S2e6oy6Yt4avOBqDSJ9i+9BqChijeoPqn0cAqwr0 CLJ5sZjuVSnjvWCxnJ8XRxCpywKzIOHsEN+OLnIo5lNXXGXmXBFpW6UChkMu55kEoiz4+YBk J6TzOSjdmQnkZqc58YXCsnKJdjSNXMgNUCsAzvIFE4fSjXtM2jDhktbmfXU93uPr5F8pIK// fhGArJdSlExEesXT0p/G9lXapl7XiE/y+bC1OYI4ma7pRjVAs5du9qUM5DaSeWqMzufgbReM lEQxqjkKI0IKoDh82pLTwAi2a7sRA/XV90LpTB9ZAgppkkL6GJ5UmA4x0PibEWq/WMXEvm32 BUxj0EtBIZlvCep6FAxKF3QoSI2m0RkgtTpjweadzvpJbuxV4VbWGLk8lI8OZThT0NpfBW/y AZ6YSzcSesb3N4CPSh7zRXRspxVFbtAQL1YNVUOkOqPaaxg0EwA+Hn/gx4do7ODUdw7yUMra cL+8yoGglo8KoZzfeuJes8rhhBRnv7c43Xuj7hphldYfwFUrCuTYHJa4RRUcOV5YXLupqs1t kSDg2URImFUDqhz+6s4+B9lY7bSiH6wttwLYkGpab7FJvvA6TGZzJyGHgtrhBFPyxgN/KAog 50qKxPGDhl2nrXNT09bZZKacVMHKJcKkRqbNSeW77eXyMosbdzkT7LmEbfV5q1M2hr2TkF0R swN9ppTRJD0iROBdJ61IuJdkkcjvFyzdgfCUa4BPRuPlH1vSySXzJhr2IBcIncWBmAvaU1fB 57xjypz2L+peohzZX0XGIwZKngxRcu23TZDuGhNByW21eRfzxWe6zj7pWLbCzyuNrKLi9+UY g9pAdCyvz449vrv4WM=
  • Ironport-sdr: 65159cf1_z+1gTi2V1iao4x5HaKh0mluk+nf19sNwAj0uUhJKQoXGy7g kfzVtl6+lafLcaRPMdzgpbQ/yluX/CevLUIhzrA==
  • Msip_labels:

I am not aware of any mechanism like this. However, I think you can use solve​ and backtracking to force the completion of these two goals. This f​ should be implemented as a guided search and anticipate backtracking. This method, I expect, will be very slow, though.


From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Sent: Thursday, September 28, 2023 10:48 AM
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] match on multiple goals simultaneously
 
often, I have an evar shared between 2 goals and to correctly determine the right value of the 
evar, I need info from both goals.
is there some way to match on multiple goals like:
match goal1 with
  [H1: pat1 ?X |- C1] => 
        match goal2 with 
          [H2: pat2 ?Y |- C2] => unify shared_evar (f C1 C2 X Y)
         end
end




Archive powered by MHonArc 2.6.19+.

Top of Page