coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why must || make progress?

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Why must || make progress?
Date: Tue, 17 Apr 2018 03:22:42 +0000
Accept-language: en-CA, en-US
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 NAM04-BN3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:BMb6bhcai/Ia8TAUnyXkFVDxlGMj4u6mDksu8pMizoh2WeGdxcS8Yh7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyuuxNwzpXOb42JKPZzZL/Rcc8HSWdHQ81fVzZBAoS5b4YXC+QOJ/1Yr477p1ATtBexBgmsBOTpyj9Hm3T4wK063PonEQHJxQArAtAAsGnJp9jyOqcdTOC1zajTzTndc/9axCvx5ZPIchAmvfGMWKh/ccvVyUU1CwzFiVCQpJXjMjiI2OoNtG2b4PBhVeKpk2MnqgdxoiKuxsg2kIXJiJgVx1bZ/it62IY4PdK1RFJhbdOgDpdcrSWXO5F2T84hW21otjg1x74atZO+eSUKxogryhzcZvGCd4WF4RLuWeeULDhlhn9ldrGyihOs/US91OHzTc+520tQoCVfiNnDrHUN2gTT6seZTvt9+V+s1y6T2g7U9u1JLlk4mLfDJZMv27IwkYEcvlrZEi/xhUX2kLSZdkI5+uiu9uvreK3mpoWbN49olA7xLrgums24AeQ+KAQOWHWb+fi41L3k+k35Q69GgeExkqncqJzaJMIbqbClAwJN3Ysv9wyzAjO43NgCmXQLNlJIdRGfg4jsIV7OIfT4Dfmlg1SrlTdm3/7GMaDhApTMNXjPjqvtcath50NHyAozysxf55dOBbEAJPL/QFP+tNvdDhMhKQy73/7nCMlh1oMZQW+AHqiZMLrLvVCU4uIvPvKDaZQOuDf9Lvgl/+ThgWU4mV8bZ6mp3IEYZGq2HvR8cA2lZi+midAYVGwOowAWTerwiVTEXyQZLyK5WLt57TUmAqqnC53CT8ajmurS8j28G8h0b3tBDBjJI3fvcYrMYPcBbi3Xau982mgKWbizUNV5jEmGtAjmzrNmKqzf/ShO5sGr78R8++CGzUJ6zjdzFcnIizjcHVExpXsBQnoN5I46pEV8zlmZ1q0h2K5YEsBW7vJNFAw9MMyFlrAoO5XJQgvEO+yxZhO+WNz/WmMxSc40yt4KJU16Hof6102R72+RG7YQ0oezKtk0/6bbgyejAe9YkyqD/o96yl4sT41IKHGsgbN5+07LHYnVnk6FlqGsM6MBwCrK82TFxm2L7hhV

Hi all,

From the documentation https://coq.inria.fr/refman/ltac.html#hevea_tactic222, it says that

> expr1 || expr2 is equivalent to first [ progress expr1 | expr2 ]

While the documentation of Ltac + says following

expr₁ + expr₂

expr₁ and expr₂ are evaluated to v₁ and v₂ which must be tactic values. The tactic value v₁ is applied to each focused goal independently and if it fails or a later tactic fails, then the proof backtracks to the current goal and v₂ is applied.

which says expr1 does not have to make progress. Following program illustrates the difference:

Goal True.
idtac || idtac "here".
(* here *)
(idtac "here" + idtac "not here").
(* here *)
Abort.

I used to consider || to be a "more controlled" version of +, and therefore expect their behavior should be the same, modulo the backtracking part. So why || would need to have an extra requirement for making progress? If somehow it must, then why doesn't expr2 have to make progress as well? Also why doesn't expr1 of [tryif] have to make progress? Sorry but this is a quite puzzling point.

Sincerely Yours,

Jason Hu

[Coq-Club] Why must || make progress?, Jason -Zhong Sheng- Hu, 04/17/2018