coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to combine tactics

From: David Holland <dholland-coq AT netbsd.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to combine tactics
Date: Thu, 15 Aug 2019 17:52:16 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=dholland-coq AT netbsd.org; spf=Pass smtp.mailfrom=dholland AT netbsd.org; spf=None smtp.helo=postmaster AT mail.netbsd.org
Ironport-phdr: 9a23:qH8yZhac9RSOSm6Uw8i8xsX/LSx+4OfEezUN459isYplN5qZoM2+bnLW6fgltlLVR4KTs6sC17OM9fm7ACdZuMvJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MQu6oR/MusQYnIduJbs9xgbJr3BVZ+lY2GRkKE6JkR3h/Mmw5plj8ypRu/Il6cFNVLjxcro7Q7JFEjkoKng568L3uxbNSwuP/WYcXX4NkhVUGQjF7Qr1UYn3vyDnq+dywiiaPcnxTbApRTSv6rpgRRH0hCsbMTMy7WfagdFygq1GuhKsvxJxzY7Kbo+IN/R+cKzScs8HSmVDUMlcTDBBDp+mYocTE+YMJ/hUoo/grFUOtxu+AgysCfvhxDBSmH/23LA12PkjHwHB2AwgG8gBsHLJo97oM6odTOC1zK7MzTXHdfxW3yry5JHUfRAmuPGBRrRwftTNyUY0DAPKk0+cqYv/PzOaz+kAtXWQ4el4Ve+3lmIqrwV8riKxysoihITFnJwZxk3G+Clj3oo5OcG0RUhmatC+CpRQrTuVN45uT8MiXW5ovCE6x6UDuZGhfSgKzI4rxxjBZPybaIeI+Q/sWPyWITdii3JpYLO/hxCs/ki80uDwS8253VJQoiZbnNTBuGoB2wLO5sWFUPdx4Fut1SqX2wDW8O5EIEQ0laTBK54mx749joccsUTEHi/ynEX5lqmWeVg/9+iu9evnfq7ppoSBOINujQH+KKsultSlAeskKggOQ3Sb+eOk2bL/+k35WaxGgeEykqnEq5/XPt8bp668Aw9NyIkv8Re/DzG80NQZh3YLNlxFeAjUx7TublrJObXzCeq1q1WqijZigf7cbZP7BZCYAnHdkbupXbF570daxEJnwdBY45ZdDL1EK/Xqckn8qNbDAlk+KQPikLWvM8l0yo5LATHHOaSeKq6H6QbUtNJqGPGFYcougBi4M+IsvqS8i3Ilk0QRO66z0slPMS3qLrFdO0ycJEHUrJIBHGMN51VsSeXrjBuEXCJZfHr0WLgztGliWdCWSLzbT4Xou4SvmSKyH5lYfGdDUwreF3r0fZ6IHfAWZ3DLLw==

On Mon, Aug 05, 2019 at 01:44:31PM +0000, Jeremy Dawson wrote:
> Further to my previous messages I have experimented some more, and find
> that
>
> induction H ; (eapply derI ; [ NLrule_I | idtac]).
>
> does work. Ie the parentheses are needed, and make a difference, in
> this case.

I have also found that you can work around these problems by inserting
a dummy match, along these lines:

induction H;
match goal with
| [ |- _ ] => eapply derI; [ apply NLrule_I | ]
end.

After reading the rest of this thread I'm now not sure if this is a
consequence of the same syntactic factors or whether the matching
does actually changes the way the goals are processed like I
originally thought it did. :-/

--
David A. Holland
dholland AT netbsd.org

[Coq-Club] how to combine tactics, Jeremy Dawson, 08/04/2019
- Re: [Coq-Club] how to combine tactics, Laurent Thery, 08/04/2019
  - Re: [Coq-Club] how to combine tactics, Jason -Zhong Sheng- Hu, 08/04/2019
    - Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/05/2019
- Message not available
  - Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/05/2019
    - Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/05/2019
      - Re: [Coq-Club] how to combine tactics, Jason -Zhong Sheng- Hu, 08/05/2019
        
        Re: [Coq-Club] how to combine tactics, Fabian Kunze, 08/05/2019
        
        Re: [Coq-Club] how to combine tactics, Li-yao Xia, 08/05/2019
        
        Re: [Coq-Club] how to combine tactics, Jeremy Dawson, 08/06/2019
      - Re: [Coq-Club] how to combine tactics, David Holland, 08/15/2019
        
        Re: [Coq-Club] how to combine tactics, Pierre Courtieu, 08/20/2019