coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to write variadic tactics

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] How to write variadic tactics
Date: Wed, 19 Aug 2020 11:13:18 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f178.google.com
Ironport-phdr: 9a23:NvNzbRa6PLMZPl6YvHyXr+7/LSx+4OfEezUN459isYplN5qZrsq6bnLW6fgltlLVR4KTs6sC17OI9fm4CSdeuN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLRi6txjdutUVjIdtK6s91wbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDMi7mrZltJ/g75aoBK5phxw3YjUYJ2ONPFjeq/RZM4WSXZdUspUUSFKH4GyYJYVD+cZM+hWr5fzqUYNoxS8CwmiA+zgxSNHiHLtwa030f4sHR3c0QA8Ad4DtmnfotXvNKcVVOC41KfEzTfEb/NQ2Df965bHchQ/rv6SRr9wfs/RxlMuFwPBlFmftYvlPzab2u8QtGWb7e1gVeSui24ktQ5xpiagydk3h4nGg4Ia0FHE9SFjzIkpIt24TVd2bNi5G5Rfqy+ULZF5Qt8+Q252oiY6zKULtYK0cSQX1Zgq2R7SZv+EfoWH/B/tWumcLzl2iX9rZr6yiRa//FW9x+P8WMS4zUhHoCRbn9TPuH4A0xzd5MiER/Z740yv2i6P2hjN5u1YJU04j6nWJp47zrItl5cfrV7PEjL0lUj1lKOaaEQp9vS15+nif7nrooOTOop7hwz/LqgihsmyDfkmPggAWmWb9/iz2KPt/UD8XLpHgfM2kqfcvZDUO8sXu7K2DgpP3Ysj9hqyDDGr28kCk3YdNlJKYheHgpDpO17QJPD4Cu+yg1G2nzdqw/DKJ6ThAonQInTanrftYLRw5k1GxAo8ytBf4J1UCrUfL/7pRkDxs9nYAgc4Mwyy3ennFM1w2p0CVW+LGKOUM6PfvUWV6u8uP+WAfpIZtTT+JvQ94v7hl345mVsTfamz2psXbWi1HvZhI0WfYHrsgckOEWMUsQUgV+Hqh1iCXiRSZ3a2Ra4z+jY7CIe+AYfZWo+tmKCB3Du8HpBOem9GDUmMHW70eIWARvcDczmfItRhkzwBTbiuUZUt1RCotA/gyrpoNPDY+iMCtcGr6N8gxeTIkhd62iZzFN/Vh2OEVGZykXkPXCRn9K96qE15jFyE1P4rreZfEIkZ5fRPUwQ3MZPR5+N/AtH2HAnGe53BHFShRNSlDDU8Q/o+xtYPZwB2HND03UOL5DajH7JAz+/DP5cz6K+JmiGpf58smUaD77EoihwdeuUKMGSngqBl8A2KXtzGlkyYk+ChcqFOhXeRplfG9nKHuQRjaCA1Sb/MBClNaU7frNC/7UTHHef3VOYXdzBZwMvHEZNkL93kiVIcGqXmMdXaJnutwiK+XEnYgLyLa4XudiMW2yCPUEU=

On Wed, 19 Aug 2020 00:05:56 -0400
Jason Gross <jasongross9 AT gmail.com> wrote:

> There are two ways to do this:
> 1. Write a "dependently typed" tactic that takes a `nat` encoding how
> many arguments it expects, e.g.,
> Ltac myintros_then n k :=
> lazymatch n with
> | O => k ()
> | S ?n
> => fun H
> => myintros_then n ltac:(fun _ => k (); intro H)
> end.
> Ltac myintros n := myintros_then n ltac:(fun _ => idtac).
> Goal True -> True -> True -> True.
> myintros 3 A B C.

A perverse version of the above uses failure and backtracking to
accumulate the arguments instead of an explicit n:

Ltac myintros_then k :=
multimatch goal with
| _ => k ()
| _ => fun H => myintros_then ltac:(fun _ => k (); intro H)
end.
Ltac myintros := myintros_then ltac:(fun _ => idtac).
Goal True -> True -> True -> True.
myintros A B C.

[Coq-Club] How to write variadic tactics, Christopher Ernest Sally, 08/19/2020
- Re: [Coq-Club] How to write variadic tactics, Jason Gross, 08/19/2020
  - Re: [Coq-Club] How to write variadic tactics, jonikelee AT gmail.com, 08/19/2020
    - Re: [Coq-Club] How to write variadic tactics, jonikelee AT gmail.com, 08/19/2020