coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Why doesn't there exist a 'patterns' tactic?

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Why doesn't there exist a 'patterns' tactic?
Date: Wed, 10 Oct 2018 16:43:09 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f51.google.com
Ironport-phdr: 9a23:riUFHhBf+QVzwVp2djUCUyQJP3N1i/DPJgcQr6AfoPdwSPv7rsbcNUDSrc9gkEXOFd2Cra4c1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIOD43/m/UhMJtkqxUvAmsqAZjz4POeoyZKOZyc6HbcNgHRWRBRMFRVylZD46ib4sPFesBPf1FpIfzvVQOqAC+DhSrCezzyj9InH723bYg3+s8Cw7G2RcgE8gIsHTQt9j1O6ISXvq0zKnM1znMc/RW2TLk5YXObxsvoumMUKpufcbNzUQjDQDIg1WKpYD4IT+Y1f4BvmiG4+dmSOmhkXQoqxtrrTiq3sosipfGhoYSyl3c8CV22oc1JdmhRE91ZN6oDYJcty+aOodrWM8iTGZouCE1yr0Cp5G3ZjQFyJMixxLHavyHdZaH4g77WeqPPTt1gGhpdbG/ihqo7ESs1O7xWtO03VpXtiZFl8PDtnEJ1xzd8MiHTf5981+91jaPzQDT6/pELVopmqXBLp4h2aQ8lpwXsUnYES/2nV/5jK6Sdkk+5ueo7OHnbq38ppCAL490lh3+MqM2l8OjBuQ4KxECUHSf+eShz7Lu5lb5QbVPjv0uiKbVqpHaJcIBpq64GQBZyIgj6wzsRwuhhd8fhDwMKE9PMEaMiJGsMFXTKtj5C+2+ihKiimE46erBO+jKAo/MNTDvmbL6NeJ261Rd00w/xNVEoZRQIr4EKfP3HET2sYqLXVcCLwWozrO/W51G3YQEVDfXW/7LAObpqVaNo9kXDayJbY4Rtiz6LqF8tfHrhH4931QaePvwhMdFWDWDBv1jZn6hTz/0mN5YSDUFuwM/SKrhj1jQCWcONUb3ZLo143QAMKzjDYrHQdrw0rmI3SP+AZgPI24bUxaDFnDnc4jCUPAJOnqf

Dear all,

We all know the 'pattern' tactic but I was looking for something that takes multiple terms and does the same but came up empty. The idea is that we have, for instance the goal a + b = b + a and then can do 'patterns a b' to get the goal (fun a0 b0 : nat => a0 + b0 = b0 + a0) a b. Or have I missed something?

Have a nice day,

Chris

[Coq-Club] Why doesn't there exist a 'patterns' tactic?, Chris Dams, 10/10/2018
- Re: [Coq-Club] Why doesn't there exist a 'patterns' tactic?, Dominique Larchey-Wendling, 10/10/2018
  - Re: [Coq-Club] Why doesn't there exist a 'patterns' tactic?, Chris Dams, 10/10/2018
- Re: [Coq-Club] Why doesn't there exist a 'patterns' tactic?, Laurent Thery, 10/10/2018