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 12:04:00 -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-qk1-f169.google.com
Ironport-phdr: 9a23:UjiTYxyVIxfMBuzXCy+O+j09IxM/srCxBDY+r6Qd2uwWIJqq85mqBkHD//Il1AaPAdyFrasc26GI7ejJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhTexe65+IAm1oAnet8QbgJZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLzliwJKyA2/33WisxojaJUvhShpwBkw4XJZI2ZLedycr/Bcd8fQ2dKQ8RfWDFbAo6kYYUBD/QPM/tboYb/qVsAqhSxChWjCu701j9FhGX70bEg3ug9Dw3L2hErEdIUsHTTqdX4LKkeUeKyzKnOzDXDbO1Z2TPj54fWaR0hrvSMUqhxccrV00UgCwTFjlCepYf4OD6V1OMNs26a7+pjS+2vj3AopB9qrzigw8cjkIjJhoYPxl/Y8iV5xZ84KNulQ0F0fdCqCoFftz2GN4RoWMMiRXlltDo1x7EbpJK2YigHxZckyhPQdfGJfYeF7BztWeufPzt1inJoda+iihiy/0Ws1/PxWMeq3VtJoCRIltnCuHAO2hHV98OJSeN981+/1TqT0w3f8OJJLEAumabFNZIt3KQ8mocSvEnHBiP6hkT7gLOLekgh5+Sl7/job7Dpq5KdK4N4lgTzPrkwlsyxBOk4PBQBU3aV+em5yLLu8kP5QLtPg/04jKbVrYzVKMEBqaO5HgNY0YAu4AulATi8ytQXh3wHIUpFeB2Zi4jpPEnDIPXiAve+h1SgiS5rx/PbMrH4DJXBM3nOnbP7cbZy7E5czwUzzdRB6J5OFr4BJ/fzVlfwtNzeEBA5LxS5z/j7BNh5zI8TWmKCDrWHPK/Mr1OE/P8jLuiIaYMNvTbyMfkl5/rgjX8jnl8deLGk3ZkQaHC+H/RmIFuWYX7yjdgfCmoKsQ8+Q/briF2GSzJce3GyX6ck6jEhFI2mFZvDRpyqgLGZwCi7GYRWanlaBVCIDHfnbJ6JW+wMaSKXOs9uiCYIVbmnS4871BGhrhX2y7R9LrmcxipNl5v40949yPfUjgp6oT59FMOb3HuKVHoltmwNTj4ymqt4pBou5E2E1P0ygfteFN9e4/5Eegg/PJ/Yied9Dpq6DgDGeNaKRVKrT/2pBDgwSpQ6xNpYMBU1IMmrkh2Wh3niOLQSjbHeQcVsqvuNjUi0HN50zjP97IdkilAnRsVVMmj/3/xw8gHSA8jClEDLzv/3J5RZ5zbE8SK49UTLvExcV1QuA6DMXHRaf0iP6NqguBKEQLipBrAqdABGzJzac/cYWpjSlVxDAczbFpHGeWvowjW/AB+JwvWHa4+4I2g=

On Wed, 19 Aug 2020 11:13:18 -0400
"jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:

> 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.

Actually, it's best to flip the order of those two branches so
that k runs just once when there are no further arguments left to
accumulate:

Ltac myintros_then k :=
multimatch goal with
| _ => fun H => myintros_then ltac:(fun _ => k (); intro H)
| _ => k ()
end.
Ltac myintros := myintros_then ltac:(fun _ => idtac "just once").
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