Ltac: arguments optionnels tactique

Question

Je veux faire une tactique Ltac en coq qui prendrait 1 ou 3 arguments. Je l'ai lu sur ltac_No_arg dans le module LibTactics mais si je l'ai compris, j'invoquer bien avoir ma tactique avec:

Coq < mytactic arg_1 ltac_no_arg ltac_no_arg. 

qui est pas très pratique.

Est-il possible d'obtenir un résultat comme celui-ci? :

Coq < mytactic arg_1. 

Coq < mytactic arg_1 arg_2 arg_3. 

Answer 1

Nous pouvons utiliser le mécanisme Tactic Notation pour tenter de résoudre votre problème, car il peut traiter les arguments variadique.

Nous allons réutiliser ltac_No_arg et définir une tactique factice mytactic aux fins de démonstration

Inductive ltac_No_arg : Set := 
    | ltac_no_arg : ltac_No_arg. 

Ltac mytactic x y z := 
    match type of y with 
    | ltac_No_arg => idtac "x =" x (* a bunch of cases omitted *) 
    | _ => idtac "x =" x "; y =" y "; z =" z 
    end. 

Maintenant, nous allons définir les notations tactique ci-dessus:

Tactic Notation "mytactic_notation" constr(x) := 
    mytactic x ltac_no_arg ltac_no_arg. 
Tactic Notation "mytactic_notation" constr(x) constr(y) constr(z) := 
    mytactic x y z. 

Tests:

Goal True. 
    mytactic_notation 1. 
    mytactic_notation 1 2 3. 
Abort.