From ebef033daf64edf70b1063d511d9a59bb1d55641 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Wed, 29 Apr 2026 02:08:00 +0200 Subject: [PATCH 01/17] write intro tuto ltac2forltac1 --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 706 ++++++++++++++++++ 1 file changed, 706 insertions(+) create mode 100644 src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v new file mode 100644 index 0000000..3f35bbe --- /dev/null +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -0,0 +1,706 @@ +(** * Tutorial Ltac2 : Ltac2 for Ltac1 Users + + *** Main contributors + - Thomas Lamiaux + + *** Summary + + Ltac2 is the successor of Ltac1, and is designed to replace Ltac1 as the + standard tactic language for the Rocq proof assistant. + + This tutorial is meant to introduce Ltac2 for users that already are + familiar with Ltac1. We mainly focus on the differences with Ltac1, and how + to translate your existing Ltac1 knowledge into Ltac2 idioms. + + *** Table of content + + - 1. Introduction + - 1.1 A Brief History of Ltac1 + - 1.2 Design Flaws of Ltac1 + - 1.3 Ltac2 + - 1.4 Status of Ltac2 + - 2. Using Ltac2 to Write Proofs + - 2.1 Basic Syntax Changes + - 2.2 Interoperability Between Ltac1 and Ltac2 + - 2.3 Some Notations Are Missing + - 3. Ltac2 is a Proper Functional Programming Language + - 3.1 Types and Type Inference + - 3.2 Call-by-Value Semantics and Thunking + - 3.3 Effects: Printf and References + - 4. Ltac2 as a Meta-Programming Language for Rocq + - 4.1 Foreign Function Interface + - 4.2 Quoting and Unquoting + - 4.3 Matching Terms and Goals + - 4.4 Backtracking + - 4.5 Notations + + *** Prerequisites + + Needed: + - Familiarity with Ltac1 and basic Rocq proof writing. + + Installation: + - Ltac2 and its core library are available by default with Rocq. + +*) + +From Ltac2 Require Import Ltac2. +From Ltac2 Require Import Printf. + + +(** ** 1. Introduction + + *** 1.1 A Brief History of Ltac1 + + Ltac1 was introduce in 2000 (Coq 7.0) to enable users to write their own + tactics by combining existing primitive tactics using an expressive set of + combinators. + + For instance, users have been using Ltac1 to write variants of existing + tactics domain specific automation tactic. + + Ltac1 was key in the success of Rocq, and of many formalization efforts as + it enabled us to write proofs in a more incremental, efficient and more + robust way than the state of the art of that time. + + + *** 1.2 Design Flaws of Ltac1 + + Yet, Ltac1 was not planned for so advanced uses and suffer designed flaws. + + 1. At the time, there were no idea of what a good tactic language ought to be + and Ltac1 was not designed following current PL conventions + + 2. The development of Ltac1 was not carefully planned, and features have + added piecewise over times by different contributors. + Consequently, the language is far from well-designed, uniform, or well + implemented, making improvements and every day use complicated. + + 3. Ltac1 tried to accomodate two contradictory feature: for tactics + to be both automagical and predictible. + To do so, Ltac1 implements many dynamic decision procedures to facilitates + writing tactics that works well for small example but do not scale well. + + With experirence, there are several well-known design flaws with Ltac1: + + - **No type system.** Ltac1 is completely untyped. Any value can be passed to + any function, and type errors are only caught at runtime, often with cryptic + error messages. This makes writing large library and tactics and debugging + very tedious. + + - **No data structures.** Ltac1 has no lists, no records, and no algebraic + types. All state must be threaded through the goal or through side channels. + + - **Unclear Semantic** It is hard to predict when a tactic will be + evaluated, or whether a name refers to a Rocq term or an Ltac1 variable. + This leads to subtle and hard-to-diagnose bugs. + + - **Limited effects.** Ltac1 lacks support for many basic effects that + are useful in a programming language like printing, or mutable references. + + - **Implicit quoting.** The boundary between Gallina (Rocq terms) and Ltac1 + meta-programs is not syntactically marked. Ltac1 uses dynamic scoping rules + to resolve names, which are hard to understand and debug. + + - **Poor FFI.** Functions from the Rocq kernel are imported all at once, + without types and without any control over what is in scope. + + + *** 1.3 Ltac2 + + Ltac2 is designed to be the replacement of Ltac1, and offer both a + reliable and scalable tactic language for Rocq, while being as backward + compatible as possible. + + Its core improvements over Ltac1 are: + + - It is a proper typed functional programming language of the Hindley–Milner + family, similarly to OCaml, with type inference, algebraic data types, + and a clear call-by-value semantic. + + - It has an explicit typed Foreign Function Interface. + This makes it easy to extend Ltac2 to expose and access primitive like unification, + that were not accessible before, while providing better documentation for it. + As a consequence, it is possible to do more stuff in Ltac2 than in Ltac1. + For instance, it is now possible to manipulate to goal state, and modify + the set of goals under focus etc. + + - Quoting and unquoting between Rocq terms (Gallina) and Ltac2 values is now + explicit and syntactically marked. It no longer relies on a hard to predict + dynamic decision procedure. + + - Backtracking is modelled as streams of possibilities, with fine-grained + primitives to manipulate it. + + *** 1.4 Status of Ltac2 + + Ltac2 is actively developed and included in every Rocq distribution. + No extra package is needed. Ltac2 may still contain bugs or limitations, + but it is already more reliable and expressive than Ltac1. + + Therefore, while Ltac1 is not going away anytime soon, we would like to + strongly encourage users to use Ltac2 (or other alternatives) instead of Ltac1 + for new projects and new automation code in existing projects. + + It comes with a CoreLibrary that is meant to contain basic building blocks + for creating complex tactics. It keeps evolving and may contain more + exposed primitives in more recent versions of Rocq. + See https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 for + the master branch of Rocq. + +*) + + +(** ** 2. Using Ltac2 to Write Proofs *) + +(** *** 2.1 Basic Syntax Changes + + The first thing you will notice when moving from Ltac1 to Ltac2 is that the + declaration syntax has changed. + + In Ltac1, a tactic is defined as: +<< + Ltac my_tac := tac1; tac2. +>> + In Ltac2, the syntax becomes: +<< + Ltac2 my_tac () := tac1; tac2. +>> + The extra [()] parameter, of type [unit], is required because Ltac2 is a + strict call-by-value language (see Section 3.2 for the details). + Without it, the body would be evaluated immediately at definition time rather + than when the tactic is called. + + Semicolon chaining [;] works exactly as in Ltac1: [tac1; tac2] applies [tac2] + to all goals generated by [tac1]. + Standard tactics ([intros], [destruct], [rewrite], [apply], [exact], etc.) + are available with the same names. + + Here is the same simple tactic written in both languages: +*) + +(* Ltac1: + Ltac my_split_exact := split; exact I. *) + +Ltac2 my_split_exact0 () := split; exact I. + +Goal True /\ True. + my_split_exact0 (). +Qed. + +(** Writing [()] at every call site is noisy. + The standard idiom is to declare a [Ltac2 Notation] — here a simple + abbreviation — that inserts the [()] application automatically. +*) + +Ltac2 Notation my_split_exact := my_split_exact0 (). + +Goal True /\ True. + my_split_exact. +Qed. + + +(** *** 2.2 Interoperability Between Ltac1 and Ltac2 + + You do not have to rewrite everything at once. + Ltac1 and Ltac2 can freely call each other, which makes incremental migration + practical. + + **** 2.2.1 Calling Ltac2 from Ltac1 + + To embed a Ltac2 tactic inside an Ltac1 proof script, use [ltac2:(...)]. + The Ltac2 expression inside must have type [unit]. + This is the most common migration pattern: keep existing proof scripts in + Ltac1 while writing new automation in Ltac2. + + For instance, the following Ltac1 tactic delegates entirely to a Ltac2 + definition. It can be called in any Ltac1 proof script: +<< + Ltac use_ltac2_in_ltac1 := ltac2:(greet_and_close ()). + Goal True. use_ltac2_in_ltac1. Qed. +>> +*) + +Ltac2 greet_and_close () := + printf "closing goal with exact I"; + exact I. + +(** We can verify the Ltac2 function itself works in a Ltac2 proof: *) + +Goal True. + greet_and_close (). +Qed. + +(** **** 2.2.2 Calling Ltac1 from Ltac2 + + Symmetrically, a Ltac2 definition can invoke Ltac1 code using [ltac1:(...)]. + This is useful to reuse existing Ltac1 automation that you have not yet ported. +*) + +Ltac2 use_auto () := ltac1:(auto). + +Goal 0 = 0. + use_auto (). +Qed. + +(** **** 2.2.3 The "Classical" Migration Pattern + + A natural approach when migrating a large development is: + 1. Write new automation helpers in Ltac2. + 2. Bridge them into Ltac1 via [ltac2:(...)]. + 3. Use them in existing proof scripts without further changes. + + This lets you enjoy Ltac2's type safety and expressiveness in new code while + leaving all existing proofs untouched. + For example, suppose you want to port an Ltac1 assumption-solver to Ltac2. + You can define it in Ltac2 and expose it as an Ltac1 tactic via [ltac2:(...)]: +*) + +Ltac2 my_exact_assumption0 () := + match! goal with + | [h : ?t |- ?g] => + if Constr.equal t g + then let term := Control.hyp h in exact $term + else Control.zero (Tactic_failure None) + end. + +(** The bridge for existing Ltac1 proof scripts looks like: +<< + Ltac my_exact_assumption := ltac2:(my_exact_assumption0 ()). + Goal nat -> nat. intros n. my_exact_assumption. Qed. +>> + + In the rest of this tutorial we work directly in Ltac2, so we define a + notation instead: +*) + + +(** *** 2.3 Some Notations Are Missing + + Not all Ltac1 shorthand is available in Ltac2 by default. + In particular, several tactics that accept inline introduction patterns + — such as [intros [H1 H2]] or [induction n as [|n' IH]] — require the + extra [Ltac2.Notations] module in Ltac2. + + Importing [Ltac2.Notations] recovers most of them: +*) + +From Ltac2 Require Import Notations. + +Goal forall n : nat, n + 0 = n. + intro n. induction n as [|n' IH]. + - reflexivity. + - simpl. rewrite IH. reflexivity. +Qed. + + +(** ** 3. Ltac2 is a Proper Functional Programming Language *) + +(** *** 3.1 Types and Type Inference + + The most fundamental difference between Ltac1 and Ltac2 is that Ltac2 is a + statically typed language with Hindley–Milner type inference, very similar + to OCaml. + + In Ltac1 there is no type system: values are opaque and type errors are only + caught at runtime with cryptic messages. + In Ltac2, every expression has a type, and ill-typed programs are rejected + before they are run. + Type annotations are optional — the type checker infers them — but can be + written for documentation or disambiguation. + + As in OCaml, constructor names must start with an **uppercase** letter + ([Some], [None], [S], [O], …), while variable and function names must start + with a **lowercase** letter. + + Here is a simple typed function: +*) + +Ltac2 add (x : int) (y : int) : int := Int.add x y. +Ltac2 Eval add 2 3. + +(** Ltac2 supports Hindley–Milner polymorphism. + The following identity function works at any type: +*) + +Ltac2 my_id (x : 'a) : 'a := x. +Ltac2 Eval my_id 42. +Ltac2 Eval my_id true. + +(** Ltac2 provides standard data structures: lists, options, pairs, etc. + These are available from the Ltac2 standard library after the base import. + For example, here are a list computation and a polymorphic function over + options: +*) + +Ltac2 Eval List.map (fun x => Int.add x 1) [1; 2; 3]. + +Ltac2 safe_head (l : 'a list) : 'a option := + match l with + | [] => None + | h :: _ => Some h + end. + +Ltac2 Eval safe_head [1; 2; 3]. +Ltac2 Eval safe_head ([] : int list). + + +(** *** 3.2 Call-by-Value Semantics and Thunking + + Ltac1 has an unclear, hard-to-predict evaluation order. + Ltac2 is strictly **call-by-value**: function arguments are fully evaluated + before the function body is entered. + This makes behavior predictable and intuitive, but it has one important + consequence for passing tactics as arguments. + + If you pass a tactic [t] as an argument to a function, [t] is evaluated + — i.e. executed — immediately, before the body of the function has a chance + to decide whether to use it. + To illustrate, consider a function that ignores its argument and does nothing: +*) + +Ltac2 bad_ignore (_ : unit) : unit := (). + +(** Passing [fail] to [bad_ignore] causes the whole call to fail, because + [fail] is evaluated before [bad_ignore] is entered: +*) + +Goal True. + Fail bad_ignore fail. +Abort. + +(** The fix is to **thunk** the argument: wrap the tactic in [fun () => ...]. + A thunk is only evaluated when applied to [()], so the callee can decide + when (or whether) to run it. +*) + +Ltac2 good_ignore0 (_ : unit -> unit) : unit := (). + +Goal True. + good_ignore0 (fun () => fail). + exact I. +Qed. + +(** Writing [fun () => ...] at every call site is noisy. + A [Ltac2 Notation] with the [thunk(tactic)] parser inserts thunks automatically, + hiding this detail from callers. + + For simple abbreviations (no extra parsing), it suffices to declare a notation + that applies the thunked function: +*) + +Ltac2 Notation good_ignore := good_ignore0. + +Goal True. + good_ignore fail. + exact I. +Qed. + +(** For more details on thunking and the type of tactics, see + [tutorial_types_and_thunking.v] in this folder. +*) + + +(** *** 3.3 Effects: Printf and References + + In Ltac1, [idtac] is the only way to print, and there is no mutable state. + Ltac2 has a proper typed [printf] and ML-style mutable references. + + **** 3.3.1 Printf + + [printf] takes a format string with typed specifiers: + - [%t] formats a [constr] (a Rocq term) + - [%I] formats an [ident] (a hypothesis or variable name) + - [%s] formats a [string] + + This makes it much easier to inspect the proof state or debug automation + than the [idtac] approach: +*) + +Goal nat -> bool -> True. + intros n b. + printf "n has type %t" (Constr.type (Control.hyp @n)); + printf "b has type %t" (Constr.type (Control.hyp @b)). + exact I. +Qed. + +(** **** 3.3.2 Mutable References + + Ltac2 provides ML-style mutable references of type ['a ref], with a + mutable [contents] field. + They can be used to accumulate state across multiple tactic calls — something + that is impossible in Ltac1. + + A reference is created as a record literal [{ contents := initial_value }], + its current value is read with [r.(contents)], and it is mutated with + the setter [Ref.set r new_value]. + See the Ltac2 core library for the full [Ref] module API: + https://github.com/rocq-prover/rocq/blob/master/theories/Ltac2/Ref.v +*) + + +(** ** 4. Ltac2 as a Meta-Programming Language for Rocq *) + +(** *** 4.1 Foreign Function Interface + + In Ltac1, all interaction with the Rocq kernel happens through built-in + tactics imported as a single opaque block — no types, no control over what + is in scope. + + Ltac2 has an explicit, typed Foreign Function Interface (FFI). + Kernel functions are exposed in a hierarchy of typed modules: + - [Constr]: inspect, build, and compare Rocq terms + - [Std]: reduce terms, call unification, access the environment + - [Unsafe]: access the raw kernel representation of terms + - [Ind]: inspect inductive types and their constructors + - [Control]: interact with the proof state and backtracking + + The full core library is at: + https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 + + For example, [Constr.type] retrieves the type of a term and [Std.eval_hnf] + reduces it to head-normal form: +*) + +Ltac2 print_type (t : constr) : unit := + printf "%t : %t" t (Constr.type t). + +Ltac2 print_hnf_type (t : constr) : unit := + print_type (Std.eval_hnf t). + +Goal True. + print_hnf_type '(1 + 1). + exact I. +Qed. + + +(** *** 4.2 Quoting and Unquoting + + One of the main sources of confusion in Ltac1 is the implicit boundary + between Gallina (the language of Rocq terms) and Ltac1 meta-programs. + Ltac1 uses dynamic scoping rules to resolve names, leading to subtle bugs + when a name is mistaken for a Rocq term instead of an Ltac1 variable, or + vice versa. + + Ltac2 makes this boundary **explicit** through quoting and unquoting operators. + + **** 4.2.1 Quoting Rocq Terms + + To embed a Rocq term into Ltac2 as a value of type [constr], use ['] (apostrophe). + In Ltac1, terms in patterns were implicitly quoted; there was no explicit notation: +*) + +(* Ltac1: + Ltac use_T := + match goal with + | _ : T |- _ => assumption (* T is implicitly a Rocq term *) + end. *) + +Ltac2 Eval 'nat. +Ltac2 Eval '(0 = 0). +Ltac2 Eval '(forall n : nat, n + 0 = n). + +(** **** 4.2.2 Unquoting + + To use a Ltac2 [constr] value back in a tactic position, unquote it with + [$] (dollar sign): +*) + +Goal True /\ True. + let t := 'I in + split; exact $t; exact $t. +Qed. + +(** **** 4.2.3 Identifiers and References + + To create an [ident] value (the name of a hypothesis or variable), use + [@name] syntax. + To recover the corresponding term from a hypothesis name, use [Control.hyp]: +*) + +Goal nat -> 0 = 0. + intros H. + printf "H : %t" (Constr.type (Control.hyp @H)). + reflexivity. +Qed. + +(** [reference:(name)] creates a [Std.reference] pointing to a global constant. + Pass it to [Env.instantiate] to recover the corresponding Rocq term: +*) + +Ltac2 Eval Env.instantiate reference:(nat). + +(** For a complete treatment of quoting, see [tutorial_quoting.v] in this folder. *) + + +(** *** 4.3 Matching Terms and Goals + + Ltac1 provides [match goal] and [lazymatch goal] for pattern-matching the + proof state. + Ltac2 provides three matching combinators: + + - [lazy_match! goal] — like Ltac1 [lazymatch goal]: tries patterns in order, + does **not** backtrack into a branch once a pattern has matched. + - [match! goal] — like Ltac1 [match goal]: tries patterns in order, and + **does** backtrack into a branch if it raises an exception. + - [multi_match! goal] — backtracks both into branches and into patterns. + + The key syntactic differences from Ltac1: + - Write [lazy_match! goal with] instead of [lazymatch goal with] + - Hypothesis bindings [h : ?t] produce [h : ident] (the name) and + [t : constr] (the type). To recover the corresponding term, use + [Control.hyp h]. + + Here is a direct comparison. + + In Ltac1: +<< + Ltac show_hyp_type := + lazymatch goal with + | H : ?T |- _ => idtac T + end. +>> + In Ltac2: +*) + +Ltac2 show_hyp_type0 () := + lazy_match! goal with + | [_h : ?t |- _] => printf "a hypothesis has type %t" t + end. + +Ltac2 Notation show_hyp_type := show_hyp_type0 (). + +Goal nat -> True. + intros H. + show_hyp_type. + exact I. +Qed. + +(** With [match!], the match backtracks into the branch if it fails, which allows + trying every matching hypothesis in turn. + For example, here is a reimplementation of [assumption] that iterates over + all hypotheses, trying [exact] on each one, until one succeeds: +*) + +Ltac2 my_assumption0 () := + match! goal with + | [h : _ |- _] => let term := Control.hyp h in exact $term + end. + +Ltac2 Notation my_assumption := my_assumption0 (). + +Goal nat -> nat. + intros n. my_assumption. +Qed. + +(** If the goal type does not match any hypothesis, [exact $term] fails for + every candidate, and the whole [match!] ultimately raises an exception: +*) + +Goal nat -> bool -> nat. + intros n b. my_assumption. +Qed. + +(** For a deeper treatment of matching, see [tutorial_matching_terms_and_goals.v]. *) + + +(** *** 4.4 Backtracking + + Ltac1 controls backtracking through: + - [match goal] (backtracks into branches on failure), + - [fail n] (propagates failure [n] levels up through [match] branches), + - [first [tac1 | tac2 | ...]] (tries alternatives in order). + + Ltac2 models backtracking as **streams of possibilities** and exposes three + explicit low-level primitives: + + - [Control.zero : exn -> 'a] — raises an exception and triggers backtracking. + This is the primitive underlying Ltac2 [fail]. + - [Control.plus : (unit -> 'a) -> (exn -> 'a) -> 'a] — stacks a backtracking + choice: try the first thunk; on exception, try the handler. + This is the primitive underlying [tac1 + tac2]. + - [Control.case : (unit -> 'a) -> ('a * (exn -> 'a)) result] — inspects + whether a tactic has at least one success without consuming it. + + Note that in Ltac2, [fail] is defined as + [Control.enter (fun () => Control.zero (Tactic_failure None))], + making its meaning precise. + + Regarding [fail n]: Ltac1's [fail n] propagates failure through [n] levels of + [match] branches. This is not needed in Ltac2 because backtracking always + propagates unless explicitly stopped via [Control.throw] (a non-backtrackable + exception). + + Here is a reimplementation of [first] using [Control.plus]: +*) + +Ltac2 rec my_first (tacs : (unit -> unit) list) : unit := + match tacs with + | [] => + Control.zero (Tactic_failure (Some (fprintf "my_first: all tactics failed"))) + | t :: rest => + Control.plus t (fun _ => my_first rest) + end. + +Ltac2 always_fail () : unit := + Control.zero (Tactic_failure (Some (fprintf "always_fail"))). + +Goal 0 = 0. + my_first [always_fail; always_fail; fun () => reflexivity]. +Qed. + +Goal 0 = 0. + Fail my_first [always_fail; always_fail]. +Abort. + +(** For a detailed treatment of backtracking and its primitives, see + [tutorial_backtracking.v] in this folder. +*) + + +(** *** 4.5 Notations + + Ltac1 defines tactic notations using [Tactic Notation]: +<< + Tactic Notation "my_or" tactic(t1) "or" tactic(t2) := + first [t1 | t2]. +>> + Ltac2 has [Ltac2 Notation] with explicit argument parsers. + The crucial difference is that tactic arguments should be declared with + [thunk(tactic)] to avoid premature evaluation (see Section 3.2). + + The available argument parsers include: + - [tactic] — parse a tactic (evaluated eagerly; use [thunk] for tactics) + - [thunk(tactic)] — parse a tactic, wrap it in [fun () => ...] + - [ident] — parse an identifier + - [constr] — parse a Rocq term + + For infix notations, the separator keyword must not be a Rocq built-in, and + arguments must be delimited to avoid ambiguous greedy parsing. + A safe pattern is to use brackets, following the convention of the built-in + [first [tac1 | tac2]] notation: +*) + +Ltac2 my_or0 (t1 : unit -> unit) (t2 : unit -> unit) : unit := + Control.plus t1 (fun _ => t2 ()). + +Ltac2 Notation "my_or" "[" t1(thunk(tactic)) "|" t2(thunk(tactic)) "]" := + my_or0 t1 t2. + +Goal True. + my_or [ exact I | fail ]. +Qed. + +Goal True. + my_or [ fail | exact I ]. +Qed. + +(** For simple aliases with no extra parsing, use an abbreviation notation that + just expands to a Ltac2 expression: +*) + +Ltac2 Notation my_exact_assumption := my_exact_assumption0 (). + +Goal nat -> nat. + intros n. my_exact_assumption. +Qed. From c93ffda59cf0dd51473a69715a1bb5c9005f4db9 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Wed, 29 Apr 2026 18:25:55 +0200 Subject: [PATCH 02/17] write sec 2 about proof mode --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 328 ++++++++++++------ 1 file changed, 223 insertions(+), 105 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 3f35bbe..1c34ea8 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -20,9 +20,8 @@ - 1.3 Ltac2 - 1.4 Status of Ltac2 - 2. Using Ltac2 to Write Proofs - - 2.1 Basic Syntax Changes - - 2.2 Interoperability Between Ltac1 and Ltac2 - - 2.3 Some Notations Are Missing + - 2.1 Using Ltac2 in the Ltac1 Proof Mode + - 2.2 Using the Ltac2 Proof Mode - 3. Ltac2 is a Proper Functional Programming Language - 3.1 Types and Type Inference - 3.2 Call-by-Value Semantics and Thunking @@ -44,9 +43,6 @@ *) -From Ltac2 Require Import Ltac2. -From Ltac2 Require Import Printf. - (** ** 1. Introduction @@ -137,162 +133,284 @@ From Ltac2 Require Import Printf. Ltac2 is actively developed and included in every Rocq distribution. No extra package is needed. Ltac2 may still contain bugs or limitations, but it is already more reliable and expressive than Ltac1. - Therefore, while Ltac1 is not going away anytime soon, we would like to strongly encourage users to use Ltac2 (or other alternatives) instead of Ltac1 for new projects and new automation code in existing projects. - It comes with a CoreLibrary that is meant to contain basic building blocks - for creating complex tactics. It keeps evolving and may contain more - exposed primitives in more recent versions of Rocq. + It comes with a Core Library that is meant to contain basic building blocks + for creating complex tactics. The Core Library keeps evolving and may contain + more exposed primitives in more recent versions of Rocq. See https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 for the master branch of Rocq. + Most noticeably, Ltac2 still lacks notations for some for the basic tactics. + For the moment, Ltac2 is not loaded by default with the Prelude. + It needs to be imported with [From Ltac2 Require Import Ltac2]. + Additional modules can be required or imported if needed. *) +From Ltac2 Require Import Ltac2 Printf Option. -(** ** 2. Using Ltac2 to Write Proofs *) +(** ** 2. Using Ltac2 to Write Proofs -(** *** 2.1 Basic Syntax Changes + Before discussing the Ltac2 language itself let us consider how to + the differences between Ltac1 and Ltac2 proof mode, and how to use on + in the other. - The first thing you will notice when moving from Ltac1 to Ltac2 is that the - declaration syntax has changed. + *** 2.1 Using Ltac2 in the Ltac1 Proof Mode - In Ltac1, a tactic is defined as: -<< - Ltac my_tac := tac1; tac2. ->> - In Ltac2, the syntax becomes: -<< - Ltac2 my_tac () := tac1; tac2. ->> - The extra [()] parameter, of type [unit], is required because Ltac2 is a - strict call-by-value language (see Section 3.2 for the details). - Without it, the body would be evaluated immediately at definition time rather - than when the tactic is called. + The main use for Ltac2 is to write predictable tactics. + Yet, you do not need to port your whole development to Ltac2 to benefit from Ltac2. + You can write new script in Ltac2 but call it in the usual Ltac1 proof mode. + This lets you enjoy Ltac2's type safety and expressiveness while + leaving all existing proofs untouched, and avoid dealing with differences + between Ltac1 and Ltac2's proof mode. + + Consequently, a natural approach when migrating a large development is: + 1. Write new Ltac1 scipt or port them existing one in Ltac2. + 2. Import them into Ltac1 via [ltac2:(...)]. + 3. Use them in existing proof scripts without further changes. - Semicolon chaining [;] works exactly as in Ltac1: [tac1; tac2] applies [tac2] - to all goals generated by [tac1]. - Standard tactics ([intros], [destruct], [rewrite], [apply], [exact], etc.) - are available with the same names. + Importing Ltac2 automatically set the proof mode to Ltac2. + You can decide to keep using Ltac1 proof mode by using [Set Proof Mode "Classic"]. + Conversly [Set Proof Mode "Ltac2"] to use the Ltac2 proof mode. + You can then write script in Ltac2, and call them in a Ltac1 proof using + [ltac2:()] wrapper. - Here is the same simple tactic written in both languages: + As an example, let us leverage the [printf] function for Ltac2. *) -(* Ltac1: - Ltac my_split_exact := split; exact I. *) +Ltac2 greet_and_close () := + printf "closing goal with exact true"; + exact true. -Ltac2 my_split_exact0 () := split; exact I. +(** We can verify the Ltac2 function itself works in a Ltac2 proof: *) -Goal True /\ True. - my_split_exact0 (). +Goal bool. +Proof. + greet_and_close (). Qed. -(** Writing [()] at every call site is noisy. - The standard idiom is to declare a [Ltac2 Notation] — here a simple - abbreviation — that inserts the [()] application automatically. -*) +(** To call it from a Ltac1 proof script, wrap it with [ltac2:(...)]. + The Ltac2 expression inside must have type [unit]: *) -Ltac2 Notation my_split_exact := my_split_exact0 (). +(* set the default mode to Ltac1 *) +Set Default Proof Mode "Classic". -Goal True /\ True. - my_split_exact. +Ltac use_ltac2_in_ltac1 := + ltac2:(greet_and_close ()). + +Goal bool. +Proof. + use_ltac2_in_ltac1. Qed. +(** Importantly, [ltac2:(...)] creates a scope boundary: the code inside is pure + Ltac2, and Ltac1 variables are not in scope there. -(** *** 2.2 Interoperability Between Ltac1 and Ltac2 + For instance, in a function [my_intro (id : ident) := ltac2:(intro id)], the + [id] inside [ltac2:(...)] would be treated as the Ltac2 literal name [id], + not as the Ltac1 variable — so the tactic would always introduce a + hypothesis named [id] regardless of what was passed. - You do not have to rewrite everything at once. - Ltac1 and Ltac2 can freely call each other, which makes incremental migration - practical. + To pass Ltac1 values across this boundary, one uses the binder syntax + [ltac2:(x1 .. xn |- expr)], which explicitly receives Ltac1 values as Ltac2 + arguments and binds them under the names [x1 .. xn] in the Ltac2 scope. + Inside the expression, [x1 .. xn] have type [Ltac1.t] and are converted to + typed Ltac2 values using helpers such as [Ltac1.to_constr] and [Ltac1.to_ident]. + The ltac2 wrapper must then be defined as a letin and applied due to Ltac1 inner working. +*) - **** 2.2.1 Calling Ltac2 from Ltac1 +Set Default Proof Mode "Classic". - To embed a Ltac2 tactic inside an Ltac1 proof script, use [ltac2:(...)]. - The Ltac2 expression inside must have type [unit]. - This is the most common migration pattern: keep existing proof scripts in - Ltac1 while writing new automation in Ltac2. +Ltac my_exact t := + let f := + ltac2:(t |- + let t := Option.get (Ltac1.to_constr t) in + exact $t) + in f t. - For instance, the following Ltac1 tactic delegates entirely to a Ltac2 - definition. It can be called in any Ltac1 proof script: -<< - Ltac use_ltac2_in_ltac1 := ltac2:(greet_and_close ()). - Goal True. use_ltac2_in_ltac1. Qed. ->> +Goal bool. +Proof. + my_exact true. +Qed. + +(** *** 2.2 Using the Ltac2 Proof Mode + + The first possibility is to use Ltac2 proof mode directly. + It is very similar to Ltac1 outside of a few syntax change. + + Most noticeably dispatching tactics has changed syntax, and parsing + In Ltac1, when a tactic create more than one new goal, you can specify which + tactic to apply with the syntax [tac2; [tac31 | tac32]]. + Moreover, [tac1; tac2; [tac31 | tac32]] is parsed as + [(tac1; tac2); [tac31 | tac32]]. *) -Ltac2 greet_and_close () := - printf "closing goal with exact I"; - exact I. +Set Default Proof Mode "Classic". -(** We can verify the Ltac2 function itself works in a Ltac2 proof: *) +Goal forall P Q R S : Prop, P -> Q -> R -> S -> (P /\ Q) /\ (R /\ S). +Proof. + intros P Q R S HP HQ HR HS. + split; split; [exact HP | exact HQ | exact HR | exact HS]. +Qed. -Goal True. - greet_and_close (). +(** In Ltac2, this now written with the syntax [tac1; [tac21 | tac22 ]] in order + to avoid syntax conflict with ???. Moreover, [tac1; tac2; [tac31 | tac32]] + is now parsed as [tac1; (tac2; [tac31 | tac32])] as Ltac2 no longer + automatically delay tactic execution. + + Consequently, if [tac1] generates multiple goals, the dispatcher will + attempt to apply the list [tac31|tac32] to the subgoals generated by [tac2] + independently for each goal produced by [tac1]. + This typically results in an "Incorrect number of goals" error. To achieve + standard Ltac1 factoring, you must use parentheses to explicitly group the + sequence: (tac1; tac2) > [foo|bar]. +*) + +Set Default Proof Mode "Ltac2". + +Goal forall P Q R S : Prop, P -> Q -> R -> S -> (P /\ Q) /\ (R /\ S). +Proof. + intros P Q R S HP HQ HR HS. + Fail split; split > [exact HP | exact HQ | exact HR | exact HS]. + (split; split) > [exact HP | exact HQ | exact HR | exact HS]. Qed. -(** **** 2.2.2 Calling Ltac1 from Ltac2 - Symmetrically, a Ltac2 definition can invoke Ltac1 code using [ltac1:(...)]. - This is useful to reuse existing Ltac1 automation that you have not yet ported. +(** Similarly, some tactic combinators now parse as if they were normal functions. + Parentheses are now required around complex arguments, such as abstractions. + The tacticals affected are: [try], [repeat], [do], [once], [progress], [time], [abstract]. + + For instance, [try exact HP] is now parsed as [(try exact) HP]: [try] receives + [exact] as its sole argument, and [HP] is left dangling, causing an error. + It is hence required to write [try (exact HP)]. Respectively for the others. *) -Ltac2 use_auto () := ltac1:(auto). +Set Default Proof Mode "Classic". -Goal 0 = 0. - use_auto (). +Goal forall P : Prop, P -> P. +Proof. + intros P HP. try exact HP. Qed. -(** **** 2.2.3 The "Classical" Migration Pattern +Set Default Proof Mode "Ltac2". - A natural approach when migrating a large development is: - 1. Write new automation helpers in Ltac2. - 2. Bridge them into Ltac1 via [ltac2:(...)]. - 3. Use them in existing proof scripts without further changes. +Goal forall P : Prop, P -> P. +Proof. + intros P HP. + Fail try exact HP. + try (exact HP). +Qed. - This lets you enjoy Ltac2's type safety and expressiveness in new code while - leaving all existing proofs untouched. - For example, suppose you want to port an Ltac1 assumption-solver to Ltac2. - You can define it in Ltac2 and expose it as an Ltac1 tactic via [ltac2:(...)]: -*) +Goal forall P : Prop, P -> P. +Proof. + intros P HP. + Fail do 1 exact HP. + do 1 (exact HP). +Qed. -Ltac2 my_exact_assumption0 () := - match! goal with - | [h : ?t |- ?g] => - if Constr.equal t g - then let term := Control.hyp h in exact $term - else Control.zero (Tactic_failure None) - end. +(** However, a real issue with the Ltac2 proof mode is that some tactics + are imported but are currently missing notations for them in the Corelib. + For instance, in Rocq 9.0, a notation is missing for the tactic [clearbody]. + This problem will be solved over time with contributions to the Corelib. -(** The bridge for existing Ltac1 proof scripts looks like: -<< - Ltac my_exact_assumption := ltac2:(my_exact_assumption0 ()). - Goal nat -> nat. intros n. my_exact_assumption. Qed. ->> + In the meantime, there are two workarounds. - In the rest of this tutorial we work directly in Ltac2, so we define a - notation instead: + The first option is to define the missing notation locally. + In this case, one should also consider contributing it upstream to the Corelib. + The underlying primitive lives in [Std] and expects an [ident list], so a + notation using the [list1(ident)] parser — which parses one or more + space-separated identifiers — is sufficient: *) +Goal forall A, A -> A * A. +Proof. + intros. pose (x := 2). Fail clearbody x. +Abort. -(** *** 2.3 Some Notations Are Missing +Ltac2 Notation "clearbody" ids(list1(ident)) := Std.clearbody ids. - Not all Ltac1 shorthand is available in Ltac2 by default. - In particular, several tactics that accept inline introduction patterns - — such as [intros [H1 H2]] or [induction n as [|n' IH]] — require the - extra [Ltac2.Notations] module in Ltac2. +Goal forall A, A -> A * A. +Proof. + intros. pose (x := 2). clearbody x. +Abort. - Importing [Ltac2.Notations] recovers most of them: +(** The second option is to call the tactic through the Ltac1 compatibility + bridge using [ltac1:(...)]. + This is the simplest workaround when you only need the tactic occasionally + and do not want to introduce a local notation, but it comes with the usual + caveats of mixing Ltac1 and Ltac2 (no type checking, limited interoperability + with Ltac2 values). *) -From Ltac2 Require Import Notations. +Goal forall A, A -> A * A. +Proof. + intros. pose (x := 2). ltac1:(clearbody x). +Abort. + +(** More generally, any Ltac1 tactic can be embedded into Ltac2 using [ltac1:(...)]. + The resulting Ltac2 expression has type [unit] and runs the Ltac1 tactic on + the current goal. + + However, [ltac1:(...)] creates a scope boundary: the code inside is pure + Ltac1, and Ltac2 variables are not in scope there. For instance, in a + function [my_intro (id : ident) := ltac1:(intro id)], the [id] inside + [ltac1:(...)] would be treated as the Ltac1 literal name [id], not as the + Ltac2 variable — so the tactic would always introduce a hypothesis named + [id] regardless of what was passed. + + To pass Ltac2 values across this boundary, one uses the binder syntax + [ltac1:(x1 .. xn |- tac)], which explicitly receives Ltac2 values as Ltac1 + arguments and binds them under the names [x1 .. xn] in the Ltac1 scope. + The resulting expression has type [Ltac1.t -> .. -> Ltac1.t -> unit] and + must be applied to the Ltac2 values, converted to [Ltac1.t] using helpers + such as [Ltac1.of_constr] and [Ltac1.of_ident]. +*) -Goal forall n : nat, n + 0 = n. - intro n. induction n as [|n' IH]. - - reflexivity. - - simpl. rewrite IH. reflexivity. +Ltac2 my_exact (t : constr) := + ltac1:(t |- exact t) (Ltac1.of_constr t). + +Goal 1 + 1 = 2. +Proof. + my_exact '(eq_refl). Qed. +Ltac2 my_intro (id : ident) := + ltac1:(id |- intro id) (Ltac1.of_ident id). + +Goal forall n : nat, n = n. +Proof. + my_intro @n. reflexivity. +Qed. + + + + + + + + + + + + + + + +(* -------------------------------------------------------------------------- *) + +(* THE FOLOWING CODE IS GENERATED USING DIRECTED IA. + IT STILL NEEDS TO BE REWRITTEN AND COMPLETED. *) + +(* -------------------------------------------------------------------------- *) + + + + + + + (** ** 3. Ltac2 is a Proper Functional Programming Language *) From 49693b9cff0754e6204ed8208a397299be7d9d07 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Thu, 30 Apr 2026 15:15:42 +0200 Subject: [PATCH 03/17] write sec3 Ltac2 as a Functional PL --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 249 +++++++++++------- 1 file changed, 155 insertions(+), 94 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 1c34ea8..0ca0c80 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -210,7 +210,7 @@ Qed. For instance, in a function [my_intro (id : ident) := ltac2:(intro id)], the [id] inside [ltac2:(...)] would be treated as the Ltac2 literal name [id], - not as the Ltac1 variable — so the tactic would always introduce a + not as the Ltac1 variable -- so the tactic would always introduce a hypothesis named [id] regardless of what was passed. To pass Ltac1 values across this boundary, one uses the binder syntax @@ -320,8 +320,8 @@ Qed. The first option is to define the missing notation locally. In this case, one should also consider contributing it upstream to the Corelib. The underlying primitive lives in [Std] and expects an [ident list], so a - notation using the [list1(ident)] parser — which parses one or more - space-separated identifiers — is sufficient: + notation using the [list1(ident)] parser -- which parses one or more + space-separated identifiers -- is sufficient: *) Goal forall A, A -> A * A. @@ -357,7 +357,7 @@ Abort. Ltac1, and Ltac2 variables are not in scope there. For instance, in a function [my_intro (id : ident) := ltac1:(intro id)], the [id] inside [ltac1:(...)] would be treated as the Ltac1 literal name [id], not as the - Ltac2 variable — so the tactic would always introduce a hypothesis named + Ltac2 variable -- so the tactic would always introduce a hypothesis named [id] regardless of what was passed. To pass Ltac2 values across this boundary, one uses the binder syntax @@ -386,76 +386,100 @@ Qed. +(** ** 3. Ltac2 is a Proper Functional Programming Language *) +(** Ltac1 is a non standard tactic language with no type system, opaque + dynamically-typed values, and a non-standard evaluation strategy, making + tactics fragile and hard to predict and debug. - - - - - - - - - - -(* -------------------------------------------------------------------------- *) - -(* THE FOLOWING CODE IS GENERATED USING DIRECTED IA. - IT STILL NEEDS TO BE REWRITTEN AND COMPLETED. *) - -(* -------------------------------------------------------------------------- *) - - - - - - - - -(** ** 3. Ltac2 is a Proper Functional Programming Language *) + In constrast, Ltac2 is a proper programming language that belongs to the + well-known class of ML languages: it is a call-by-value functional language + with a Hindley–Milner type system. + Expressions have static types that can be inferred, hence ill-typed programs + are rejected at compile time rather than runtime, and are easy to write. + Moreover, evaluation is fully predictable thanks to call by-value semantic. + This makes Ltac2 tactics reliable and composable by design, opposed to Ltac1. +*) (** *** 3.1 Types and Type Inference The most fundamental difference between Ltac1 and Ltac2 is that Ltac2 is a - statically typed language with Hindley–Milner type inference, very similar - to OCaml. + statically typed language with Hindley–Milner type system, similarly to OCaml. In Ltac1 there is no type system: values are opaque and type errors are only - caught at runtime with cryptic messages. - In Ltac2, every expression has a type, and ill-typed programs are rejected - before they are run. - Type annotations are optional — the type checker infers them — but can be - written for documentation or disambiguation. + caught at runtime with cryptic messages. In Ltac2, every expression has a + type, and ill-typed programs are rejected before they are run. Type + annotations are optional -- the type checker infers them -- but can be written + for documentation or disambiguation. - As in OCaml, constructor names must start with an **uppercase** letter - ([Some], [None], [S], [O], …), while variable and function names must start - with a **lowercase** letter. - - Here is a simple typed function: + For instance, if we define an alias for addition of integer, Ltac2 will + automatically figure out the type is `int -> int -> int`: *) Ltac2 add (x : int) (y : int) : int := Int.add x y. Ltac2 Eval add 2 3. +Fail Ltac2 Eval add 2 true. (** Ltac2 supports Hindley–Milner polymorphism. - The following identity function works at any type: + The following identity function works at any type as its type is [`a -> `a]. *) Ltac2 my_id (x : 'a) : 'a := x. Ltac2 Eval my_id 42. Ltac2 Eval my_id true. -(** Ltac2 provides standard data structures: lists, options, pairs, etc. - These are available from the Ltac2 standard library after the base import. - For example, here are a list computation and a polymorphic function over - options: +(** Ltac2 provides primitive types both for p: + - [unit]: the unit type, with its single value [()]. + - [bool]: Booleans, with values [true] and [false]. + - [int]: machine integers (63-bit on a 64-bit platform). + - [string]: character strings. + - [ident]: Rocq identifiers (names of hypotheses, variables, …). + - [constr]: type of Rocq terms in Ltac2 + + Beyond the built-in types, you can define your own algebraic data + types with [Ltac2 Type]. As in OCaml, constructor names must start with an + **uppercase** letter ([Some], [None], [S], [O], …), while variable and + function names **must** start with a **lowercase** letter. + For instance, a type for arithmetic expressions can be defined by: +*) + +Ltac2 Type rec expr := + [ Num(int) + | Add(expr, expr) + | Mul(expr, expr) + ]. + +Fail Ltac2 foo X := X. + +(** Functions can then be defined with the [rec] keyword for recursivity, + and [match] for pattern-matching similarly to OCaml. + Constructors are then refered without parentheses, like [Add a b]. *) +Ltac2 rec eval_expr (e : expr) : int := + match e with + | Num n => n + | Add a b => Int.add (eval_expr a) (eval_expr b) + | Mul a b => Int.mul (eval_expr a) (eval_expr b) + end. + +(* 1 + 2×3 = 7 *) +Ltac2 Eval eval_expr (Add (Num 1) (Mul (Num 2) (Num 3))). + +(** The CoreLib provides some of the usual polymorphic types like [list] and + [option], and a few basic functions for it. +*) + +Ltac2 Eval [1; 2; 3]. Ltac2 Eval List.map (fun x => Int.add x 1) [1; 2; 3]. +(** [option] represents a possibly-absent value: [Some x] for presence and + [None] for absence. Here is a function returning the head of a list as an + option, with pattern matching on the constructors of the [list] type: *) + Ltac2 safe_head (l : 'a list) : 'a option := match l with - | [] => None + | [] => None | h :: _ => Some h end. @@ -465,16 +489,15 @@ Ltac2 Eval safe_head ([] : int list). (** *** 3.2 Call-by-Value Semantics and Thunking - Ltac1 has an unclear, hard-to-predict evaluation order. - Ltac2 is strictly **call-by-value**: function arguments are fully evaluated - before the function body is entered. - This makes behavior predictable and intuitive, but it has one important - consequence for passing tactics as arguments. + Ltac1 has an unclear, hard-to-predict evaluation order. Ltac2 is strictly + **call-by-value**: function arguments are fully evaluated before the + function body is entered. - If you pass a tactic [t] as an argument to a function, [t] is evaluated - — i.e. executed — immediately, before the body of the function has a chance - to decide whether to use it. - To illustrate, consider a function that ignores its argument and does nothing: + This makes behavior predictable and intuitive, but it has one important + consequence for passing tactics as arguments. If you pass a tactic [t] as an + argument to a function, [t] is evaluated -- i.e. executed -- immediately, + before the body of the function has a chance to decide whether to use it. To + illustrate this, consider a function that ignores its argument and does nothing: *) Ltac2 bad_ignore (_ : unit) : unit := (). @@ -514,55 +537,93 @@ Goal True. exact I. Qed. -(** For more details on thunking and the type of tactics, see - [tutorial_types_and_thunking.v] in this folder. -*) - - (** *** 3.3 Effects: Printf and References - In Ltac1, [idtac] is the only way to print, and there is no mutable state. - Ltac2 has a proper typed [printf] and ML-style mutable references. + Compared to Ltac1, Ltac2 has proper effects, noticeably printing and references. - **** 3.3.1 Printf + **** 3.3.1 Printf - [printf] takes a format string with typed specifiers: - - [%t] formats a [constr] (a Rocq term) - - [%I] formats an [ident] (a hypothesis or variable name) - - [%s] formats a [string] + In Ltac1, [idtac] is the only way to print, and there is no mutable state. + Ltac2 has a proper typed [printf]. + + [printf] takes a format string with typed specifiers: + - << i >>: prints an [int] + - << I >>: prints an [ident] + - << s >>: prints a [string] + - << m >>: prints a [message] + - << t >>: prints a [constr] (a Rocq term) + - << a >>: prints a value of any type using a custom formatter [fun () x => ...] + - << A >>: same as << a >> but the formatter takes no [unit] argument + - << % >>: outputs a literal [%] This makes it much easier to inspect the proof state or debug automation - than the [idtac] approach: + than the [idtac] approach. For instance, here is a small tactic to + print the type of an hypothesis. We will explain the exact syntax + in the next section. *) +Ltac2 print_type0 (h : ident) := + printf "the type of the hypothesis %I is %t" h (Constr.type (Control.hyp h)). + +Ltac2 Notation "print_type" h(ident) := print_type0 h. + Goal nat -> bool -> True. - intros n b. - printf "n has type %t" (Constr.type (Control.hyp @n)); - printf "b has type %t" (Constr.type (Control.hyp @b)). - exact I. -Qed. + intros a b. + print_type a. + print_type b. +Abort. (** **** 3.3.2 Mutable References - Ltac2 provides ML-style mutable references of type ['a ref], with a - mutable [contents] field. - They can be used to accumulate state across multiple tactic calls — something - that is impossible in Ltac1. + Ltac2 provides ML-style mutable reference cells of type ['a ref]. + A reference is a box holding a single mutable value of type ['a]. + References make it possible to accumulate state across tactic calls — + something that pure functional code cannot express. + + The [Ref] module provides the following primitives: + - [Ref.ref v]: creates a fresh reference initialised to [v]. + - [Ref.get r]: returns the current value of [r]. + - [Ref.set r v]: replaces the value stored in [r] with [v]. + - [Ref.update r f]: applies [f] to the current value and stores the result. + + For [int ref] specifically, [Ref.incr r] and [Ref.decr r] add or subtract 1. - A reference is created as a record literal [{ contents := initial_value }], - its current value is read with [r.(contents)], and it is mutated with - the setter [Ref.set r new_value]. - See the Ltac2 core library for the full [Ref] module API: - https://github.com/rocq-prover/rocq/blob/master/theories/Ltac2/Ref.v + For example, here is a tactic that tracks how many hypotheses it clears: *) +Goal forall (n m : nat), True. + intros n m. + let count := Ref.ref 0 in + clear n; Ref.incr count; + clear m; Ref.incr count; + printf "cleared %i hypotheses" (Ref.get count); + exact I. +Qed. + +(** Note that mutations to a reference are **not rolled back on backtracking**. + If a branch modifies a reference and then fails, the modification persists. + Keep this in mind when combining references with backtracking tactics. +*) + + + + + + + + +(* THE FOLOWING CODE IS GENERATED USING DIRECTED IA. + IT STILL NEEDS TO BE REWRITTEN AND COMPLETED. *) + +(* -------------------------------------------------------------------------- *) + (** ** 4. Ltac2 as a Meta-Programming Language for Rocq *) (** *** 4.1 Foreign Function Interface In Ltac1, all interaction with the Rocq kernel happens through built-in - tactics imported as a single opaque block — no types, no control over what + tactics imported as a single opaque block -- no types, no control over what is in scope. Ltac2 has an explicit, typed Foreign Function Interface (FFI). @@ -657,11 +718,11 @@ Ltac2 Eval Env.instantiate reference:(nat). proof state. Ltac2 provides three matching combinators: - - [lazy_match! goal] — like Ltac1 [lazymatch goal]: tries patterns in order, + - [lazy_match! goal] -- like Ltac1 [lazymatch goal]: tries patterns in order, does **not** backtrack into a branch once a pattern has matched. - - [match! goal] — like Ltac1 [match goal]: tries patterns in order, and + - [match! goal] -- like Ltac1 [match goal]: tries patterns in order, and **does** backtrack into a branch if it raises an exception. - - [multi_match! goal] — backtracks both into branches and into patterns. + - [multi_match! goal] -- backtracks both into branches and into patterns. The key syntactic differences from Ltac1: - Write [lazy_match! goal with] instead of [lazymatch goal with] @@ -732,12 +793,12 @@ Qed. Ltac2 models backtracking as **streams of possibilities** and exposes three explicit low-level primitives: - - [Control.zero : exn -> 'a] — raises an exception and triggers backtracking. + - [Control.zero : exn -> 'a] -- raises an exception and triggers backtracking. This is the primitive underlying Ltac2 [fail]. - - [Control.plus : (unit -> 'a) -> (exn -> 'a) -> 'a] — stacks a backtracking + - [Control.plus : (unit -> 'a) -> (exn -> 'a) -> 'a] -- stacks a backtracking choice: try the first thunk; on exception, try the handler. This is the primitive underlying [tac1 + tac2]. - - [Control.case : (unit -> 'a) -> ('a * (exn -> 'a)) result] — inspects + - [Control.case : (unit -> 'a) -> ('a * (exn -> 'a)) result] -- inspects whether a tactic has at least one success without consuming it. Note that in Ltac2, [fail] is defined as @@ -788,10 +849,10 @@ Abort. [thunk(tactic)] to avoid premature evaluation (see Section 3.2). The available argument parsers include: - - [tactic] — parse a tactic (evaluated eagerly; use [thunk] for tactics) - - [thunk(tactic)] — parse a tactic, wrap it in [fun () => ...] - - [ident] — parse an identifier - - [constr] — parse a Rocq term + - [tactic] -- parse a tactic (evaluated eagerly; use [thunk] for tactics) + - [thunk(tactic)] -- parse a tactic, wrap it in [fun () => ...] + - [ident] -- parse an identifier + - [constr] -- parse a Rocq term For infix notations, the separator keyword must not be a Rocq built-in, and arguments must be delimited to avoid ambiguous greedy parsing. From e31882b2dad255df44b3481cf06bbc86e4206300 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Thu, 30 Apr 2026 17:35:07 +0200 Subject: [PATCH 04/17] swrite sec 4.1, 4.3 and 5 --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 188 +++++++++++------- .../ltac2/tutorial_matching_terms_and_goals.v | 1 - 2 files changed, 119 insertions(+), 70 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 0ca0c80..2b809b5 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -32,6 +32,7 @@ - 4.3 Matching Terms and Goals - 4.4 Backtracking - 4.5 Notations + - 5. Small Case Study *** Prerequisites @@ -622,17 +623,25 @@ Qed. (** *** 4.1 Foreign Function Interface - In Ltac1, all interaction with the Rocq kernel happens through built-in + In Ltac1, all interaction with the Rocq codebase happens through built-in tactics imported as a single opaque block -- no types, no control over what is in scope. Ltac2 has an explicit, typed Foreign Function Interface (FFI). - Kernel functions are exposed in a hierarchy of typed modules: + Rocq API -- kernel or higher levels fuynctions -- can be easily. + This enables easy access to API that were not accessible in Ltac1, + making Ltac2 much more expressive. + + Many API are exposed in different modules in the core library available at: + https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 + + Most noticeable examples:: + - [Control]: interact with the proof state (goal) and backtracking - [Constr]: inspect, build, and compare Rocq terms - [Std]: reduce terms, call unification, access the environment - - [Unsafe]: access the raw kernel representation of terms - - [Ind]: inspect inductive types and their constructors - - [Control]: interact with the proof state and backtracking + - [Fresh]: to create fresh [ident] + - [Unification]: to call unification in a controled way + - [Constr.Unsafe]: to access the raw kernel representation of terms The full core library is at: https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 @@ -641,17 +650,17 @@ Qed. reduces it to head-normal form: *) -Ltac2 print_type (t : constr) : unit := - printf "%t : %t" t (Constr.type t). +Ltac2 print_hnf_type0 (h : ident) : unit := + let th := Control.hyp h in + let ty_h := Constr.type th in + let hnf_ty_h := Std.eval_hnf ty_h in + printf "the hnf of the type of %I is %t" h hnf_ty_h. -Ltac2 print_hnf_type (t : constr) : unit := - print_type (Std.eval_hnf t). - -Goal True. - print_hnf_type '(1 + 1). - exact I. -Qed. +Ltac2 Notation "print_hnf_type" h(ident) := print_hnf_type0 h. +Goal (let x := 1 in x = 1) -> False. + intros x. print_hnf_type x. +Abort. (** *** 4.2 Quoting and Unquoting @@ -661,7 +670,8 @@ Qed. when a name is mistaken for a Rocq term instead of an Ltac1 variable, or vice versa. - Ltac2 makes this boundary **explicit** through quoting and unquoting operators. + The goal was to ease user life but in practice this does not scale well. + To fix this, Ltac2 makes this boundary **explicit** through quoting and unquoting operators. **** 4.2.1 Quoting Rocq Terms @@ -709,13 +719,14 @@ Qed. Ltac2 Eval Env.instantiate reference:(nat). -(** For a complete treatment of quoting, see [tutorial_quoting.v] in this folder. *) - (** *** 4.3 Matching Terms and Goals - Ltac1 provides [match goal] and [lazymatch goal] for pattern-matching the - proof state. + Ltac1 provides [lazymatch], [match] and [multimatch] for matching + patterns and goal. This still exists in Ltac2 but has changed syntax to + avoid confusion with the [match] for matching algebraic types. + + The new syntax is [lazy_match!], [match!], and [multi_match!]. Ltac2 provides three matching combinators: - [lazy_match! goal] -- like Ltac1 [lazymatch goal]: tries patterns in order, @@ -723,64 +734,34 @@ Ltac2 Eval Env.instantiate reference:(nat). - [match! goal] -- like Ltac1 [match goal]: tries patterns in order, and **does** backtrack into a branch if it raises an exception. - [multi_match! goal] -- backtracks both into branches and into patterns. - - The key syntactic differences from Ltac1: - - Write [lazy_match! goal with] instead of [lazymatch goal with] - - Hypothesis bindings [h : ?t] produce [h : ident] (the name) and - [t : constr] (the type). To recover the corresponding term, use - [Control.hyp h]. - - Here is a direct comparison. - - In Ltac1: -<< - Ltac show_hyp_type := - lazymatch goal with - | H : ?T |- _ => idtac T - end. ->> - In Ltac2: *) -Ltac2 show_hyp_type0 () := - lazy_match! goal with - | [_h : ?t |- _] => printf "a hypothesis has type %t" t +Ltac2 print_all_hyp () := + match! goal with + | [h : ?t |- _] => printf "the hypothesis %I has type %t" h t; fail + | [ |- _] => () end. -Ltac2 Notation show_hyp_type := show_hyp_type0 (). - -Goal nat -> True. - intros H. - show_hyp_type. - exact I. -Qed. +Goal nat -> bool -> 0 = 1 -> False. + intros. print_all_hyp (). +Abort. -(** With [match!], the match backtracks into the branch if it fails, which allows - trying every matching hypothesis in turn. - For example, here is a reimplementation of [assumption] that iterates over - all hypotheses, trying [exact] on each one, until one succeeds: +(** Another difference with Ltac1 is that a pattern containing variable binding + must now be explicitly, whereas it used to be optional and dynamically + figured out if not specified. For instance, to match [let var := ?expr in + ?body], one must one write [let var := ?expr in @?body var]. *) -Ltac2 my_assumption0 () := - match! goal with - | [h : _ |- _] => let term := Control.hyp h in exact $term +Ltac2 print_body_hyp_letin () : unit := + lazy_match! goal with + | [_ : let var := _ in @?body var |- _] => + printf "the body is expanded as a function :%t" body end. -Ltac2 Notation my_assumption := my_assumption0 (). - -Goal nat -> nat. - intros n. my_assumption. -Qed. - -(** If the goal type does not match any hypothesis, [exact $term] fails for - every candidate, and the whole [match!] ultimately raises an exception: -*) - -Goal nat -> bool -> nat. - intros n b. my_assumption. -Qed. +Goal forall x y : nat, (let a := x + 2 in let b := y + 1 in a = b) -> True. + intros. print_body_hyp_letin (). +Abort. -(** For a deeper treatment of matching, see [tutorial_matching_terms_and_goals.v]. *) (** *** 4.4 Backtracking @@ -878,8 +859,77 @@ Qed. just expands to a Ltac2 expression: *) -Ltac2 Notation my_exact_assumption := my_exact_assumption0 (). +(* Ltac2 Notation my_exact_assumption := my_exact_assumption0 (). Goal nat -> nat. intros n. my_exact_assumption. -Qed. +Qed. *) + +(** ** 5. Small Case Study + + Let us now, consider a small study and write a tactic that [simplify_let] + that takes a hypothesis [h] whose type is a let-in [let var := expr in + body[var]], and turns it into [body[x']], where [x' := expr] is a new shared + definition introduced in the whole context and goal. + + In Ltac1, it would have be written has: +*) + +Ltac simplify_let H := + let H := lazymatch goal with [ H : let var := ?t in _ |- _ ] => H end in + let type_h := type of H in + lazymatch type_h with + | let var := ?expr in ?body => + idtac body; + let x := fresh "x" in + set (x := expr) in *; + change (body x) in H; + lazy head beta in H + end. + +(** In Ltac2, we need to: + - use small cap for variables + - now have [Control.hyp] to recover the body of h + - [Constr.type] is now a proper function rather than a ad-hoc construction + - use the [Fresh] module to create a fresh variables + - use [$] to unquote variables back to Rocq's world + + In the end, this gives us a script that is similar but, but with a few + decoration, and a clearer semantic which can be written with or without + importing the modules. + +*) + +Import Control Constr. + +Ltac2 simplify_let (h : ident) : unit := + let type_h := type (hyp h) in + lazy_match! type_h with + | let var := ?expr in @?body var => + printf "the body is :%t" body; + let x := Fresh.in_goal @x in + set ($x := $expr) in *; + let x := hyp x in + change ($body $x) in h; + lazy head beta in h + end. + +(** The advantage of Ltac2 is that the FFI interface enables us to write script + we could not have in Ltac1. For instance, we can now use the [Constr.Unsafe] + API to write the [simplify_let] tactic by directly accessing the structure + of the term, and performing the substitution by hand rather than relying on + high-level tactics like [lazy head beta]. +*) +Import Unsafe. + +Ltac2 simplify_let_bis (h : ident) : unit := + let type_h := type (hyp h) in + match kind type_h with + | LetIn _ expr body => + let x := Fresh.in_goal @x in + set ($x := $expr) in *; + let x := hyp x in + let new_body := substnl [x] 0 body in + change ($new_body) in h + | _ => fail + end. diff --git a/src/metaprogramming/ltac2/tutorial_matching_terms_and_goals.v b/src/metaprogramming/ltac2/tutorial_matching_terms_and_goals.v index 66cd11b..ec5f9b8 100644 --- a/src/metaprogramming/ltac2/tutorial_matching_terms_and_goals.v +++ b/src/metaprogramming/ltac2/tutorial_matching_terms_and_goals.v @@ -354,7 +354,6 @@ Ltac2 simplify_let_bis0 (h : ident) : unit := let new_body := substnl [x] 0 body in change ($new_body) in h | _ => Control.zero (Tactic_failure (Some (fprintf "the type %t of %I is not a letin" type_h h))) - end. Ltac2 Notation "simplify_let_bis" h(ident) := simplify_let_bis0 h. From 2366ad4fabc7a52229962d940afa8c7d67d04163 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Thu, 30 Apr 2026 23:11:47 +0200 Subject: [PATCH 05/17] write 4.4 --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 59 ++++++------------- 1 file changed, 17 insertions(+), 42 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 2b809b5..e79ecfd 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -767,58 +767,33 @@ Abort. (** *** 4.4 Backtracking Ltac1 controls backtracking through: - - [match goal] (backtracks into branches on failure), - - [fail n] (propagates failure [n] levels up through [match] branches), - - [first [tac1 | tac2 | ...]] (tries alternatives in order). + - [match goal] (backtracks into branches on failure, and co), + - Combinators like [first [tac1 | tac2 | ...]] + - [fail n] (propagates failure [n] levels up through [match] branches) - Ltac2 models backtracking as **streams of possibilities** and exposes three - explicit low-level primitives: + Ltac2 has more fine grained controls on backtracking. + Matching and combinators are still available, though [fail n] is not currently. + In additionn, Ltac2 has low-level primitives to manipulate values + as stream of possibilities, and backtracking. + Combinators like [first] can then be reimplemented using theses primitives. + + Most users do not have the needs for these primitives, and the existing + combinators are enough. We mention them briefly, and refer to the + documentation for more details. The three primitives are: - [Control.zero : exn -> 'a] -- raises an exception and triggers backtracking. This is the primitive underlying Ltac2 [fail]. + - [Control.plus : (unit -> 'a) -> (exn -> 'a) -> 'a] -- stacks a backtracking choice: try the first thunk; on exception, try the handler. - This is the primitive underlying [tac1 + tac2]. + This is the primitive underlying [tac1 + tac2], but it is finer + since different decision can be performed depending on the exception raised. + - [Control.case : (unit -> 'a) -> ('a * (exn -> 'a)) result] -- inspects whether a tactic has at least one success without consuming it. - Note that in Ltac2, [fail] is defined as - [Control.enter (fun () => Control.zero (Tactic_failure None))], - making its meaning precise. - - Regarding [fail n]: Ltac1's [fail n] propagates failure through [n] levels of - [match] branches. This is not needed in Ltac2 because backtracking always - propagates unless explicitly stopped via [Control.throw] (a non-backtrackable - exception). - - Here is a reimplementation of [first] using [Control.plus]: -*) - -Ltac2 rec my_first (tacs : (unit -> unit) list) : unit := - match tacs with - | [] => - Control.zero (Tactic_failure (Some (fprintf "my_first: all tactics failed"))) - | t :: rest => - Control.plus t (fun _ => my_first rest) - end. - -Ltac2 always_fail () : unit := - Control.zero (Tactic_failure (Some (fprintf "always_fail"))). - -Goal 0 = 0. - my_first [always_fail; always_fail; fun () => reflexivity]. -Qed. - -Goal 0 = 0. - Fail my_first [always_fail; always_fail]. -Abort. - -(** For a detailed treatment of backtracking and its primitives, see - [tutorial_backtracking.v] in this folder. -*) - -(** *** 4.5 Notations + *** 4.5 Notations Ltac1 defines tactic notations using [Tactic Notation]: << From 67a231aa7a27aa8f5df12421ad15c7ad7aa043cb Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Fri, 1 May 2026 00:27:15 +0200 Subject: [PATCH 06/17] write sec 4.5 --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 112 ++++++++++++------ 1 file changed, 77 insertions(+), 35 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index e79ecfd..786c8f1 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -763,7 +763,6 @@ Goal forall x y : nat, (let a := x + 2 in let b := y + 1 in a = b) -> True. Abort. - (** *** 4.4 Backtracking Ltac1 controls backtracking through: @@ -772,8 +771,10 @@ Abort. - [fail n] (propagates failure [n] levels up through [match] branches) Ltac2 has more fine grained controls on backtracking. - Matching and combinators are still available, though [fail n] is not currently. - In additionn, Ltac2 has low-level primitives to manipulate values + Matching and combinators are still available. + However, [fail n] is no longer supported, it was a hack to deal with a lack + of good primitives to deal with backtracking. + Instead, Ltac2 has fine grained primitives to manipulate values as stream of possibilities, and backtracking. Combinators like [first] can then be reimplemented using theses primitives. @@ -795,50 +796,91 @@ Abort. *** 4.5 Notations - Ltac1 defines tactic notations using [Tactic Notation]: -<< - Tactic Notation "my_or" tactic(t1) "or" tactic(t2) := - first [t1 | t2]. ->> - Ltac2 has [Ltac2 Notation] with explicit argument parsers. - The crucial difference is that tactic arguments should be declared with - [thunk(tactic)] to avoid premature evaluation (see Section 3.2). + Ltac2 supports two kinds of custom syntax via [Ltac2 Notation]. + + An **abbreviation** is a [Ltac2 Notation] with no argument clause; it + simply expands to a fixed Ltac2 expression. + It does not add a new rule to the Ltac2 grammar nor new keywords: + the name is resolved as a plain identifier at parse time, so it cannot + cause parsing conflicts., e.g. with variable names. + It should be used when you want short name to a combinator or a + fixed tactic sequence. +*) + +Ltac2 Notation "obvious" := first [assumption | reflexivity]. + +Goal 1 = 1 /\ True. + split; obvious. +Qed. + +(** A full [Ltac2 Notation] declares new parsing rule and keyworks which are + specified with ["tac_name"]. Arguments are then given with the syntax + [name_arg(X)] and [X] specifies that type of [name_arg]. The available argument parsers include: - - [tactic] -- parse a tactic (evaluated eagerly; use [thunk] for tactics) - - [thunk(tactic)] -- parse a tactic, wrap it in [fun () => ...] - - [ident] -- parse an identifier - - [constr] -- parse a Rocq term - For infix notations, the separator keyword must not be a Rocq built-in, and - arguments must be delimited to avoid ambiguous greedy parsing. - A safe pattern is to use brackets, following the convention of the built-in - [first [tac1 | tac2]] notation: + There are first basic atoms: + - [tactic] / [tactic(n)] -- parse a tactic at precedence level [n] + (default 5); evaluated eagerly, so use [thunk] when the argument is a + tactic branch that must be delayed. + - [thunk(e)] -- parse [e], then wrap the result in [fun () => ...]. + The most common form is [thunk(tactic)], which turns each tactic + argument into a [unit -> unit] thunk to prevent premature evaluation. + - [ident] -- parse a plain identifier (type [ident]). + - [constr] -- parse a Rocq term (type [constr]). + - [string] -- parse a string literal (type [string]). + - [int] -- parse an integer literal (type [int]). + + There also are combinators for optional arguments and list of arguments: + - [list0(e)] -- parse a whitespace-separated, possibly empty, list of [e] + - [list0(e, "sep")] -- same, but with a literal keyword separator [sep]. + - [list1(e)] / [list1(e, "sep")] -- like [list0] but require at least one + element. The notation [my_first [...]] above uses + [list1(thunk(tactic(6)), "|")] to parse one or more [|]-separated + tactic branches. + - [opt(e)] -- parse an optional argument [e] of type [option e] + - [seq(e1, e2, ...)] -- parse a fixed sequence of entries and bind them as a tuple. + + As an example consider reimplementing [first] using the backtracking operators + as implemented in the CoreLib. *) -Ltac2 my_or0 (t1 : unit -> unit) (t2 : unit -> unit) : unit := - Control.plus t1 (fun _ => t2 ()). +Ltac2 rec my_first0 tacs := +match tacs with +| [] => Control.zero (Tactic_failure None) +| tac :: tacs => Control.enter (fun _ => orelse tac (fun _ => my_first0 tacs)) +end. -Ltac2 Notation "my_or" "[" t1(thunk(tactic)) "|" t2(thunk(tactic)) "]" := - my_or0 t1 t2. +(** To write a notation for it, we write: -Goal True. - my_or [ exact I | fail ]. -Qed. + - ["my_first"] and ["["] / ["]"] ase literal keywords that the parser matches + verbatim; so that [my_first [...]] is unambiguous -Goal True. - my_or [ fail | exact I ]. -Qed. + - [tacs] is the name bound in the body to the parsed argument + + - [list1(..., "|")] parses a non-empty list of elements separated by [|]. + + - [tactic(6)] parses one tactic branch at precedence level 6. + Level 6 is high enough to accept most compound tactics, yet low enough + that the parser stops at [|] and ["]"] instead of consuming them. -(** For simple aliases with no extra parsing, use an abbreviation notation that - just expands to a Ltac2 expression: + - [thunk(...)] wraps the parsed branch in [fun () => ...], so each branch + is turned into a thunk [unit -> unit]. Without [thunk], every branch + would be executed eagerly -- before [my_first0] even runs -- which would + defeat the whole purpose of trying alternatives one by one. + + The result is that [my_first [t1 | t2 | t3]] is elaborated to + [my_first0 [(fun () => t1); (fun () => t2); (fun () => t3)]]. + All together, it gives us the notation: *) -(* Ltac2 Notation my_exact_assumption := my_exact_assumption0 (). +Ltac2 Notation "my_first" "[" tacs(list0(thunk(tactic(6)), "|")) "]" := my_first0 tacs. + +Goal True. + my_first [ (printf "tactic 1"; fail) | (printf "tactic 2"; fail) | exact I ]. +Qed. + -Goal nat -> nat. - intros n. my_exact_assumption. -Qed. *) (** ** 5. Small Case Study From 76ce8ac003f2f20cdfbd2ddb7efe4abdbd78247b Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Fri, 1 May 2026 01:35:39 +0200 Subject: [PATCH 07/17] write sec 4.3 --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 160 ++++++++++-------- 1 file changed, 89 insertions(+), 71 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 786c8f1..7c61cf0 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -28,8 +28,8 @@ - 3.3 Effects: Printf and References - 4. Ltac2 as a Meta-Programming Language for Rocq - 4.1 Foreign Function Interface - - 4.2 Quoting and Unquoting - - 4.3 Matching Terms and Goals + - 4.2 Matching Terms and Goals + - 4.3 Quoting and Unquoting - 4.4 Backtracking - 4.5 Notations - 5. Small Case Study @@ -608,17 +608,6 @@ Qed. - - - - - -(* THE FOLOWING CODE IS GENERATED USING DIRECTED IA. - IT STILL NEEDS TO BE REWRITTEN AND COMPLETED. *) - -(* -------------------------------------------------------------------------- *) - - (** ** 4. Ltac2 as a Meta-Programming Language for Rocq *) (** *** 4.1 Foreign Function Interface @@ -662,65 +651,8 @@ Goal (let x := 1 in x = 1) -> False. intros x. print_hnf_type x. Abort. -(** *** 4.2 Quoting and Unquoting - - One of the main sources of confusion in Ltac1 is the implicit boundary - between Gallina (the language of Rocq terms) and Ltac1 meta-programs. - Ltac1 uses dynamic scoping rules to resolve names, leading to subtle bugs - when a name is mistaken for a Rocq term instead of an Ltac1 variable, or - vice versa. - - The goal was to ease user life but in practice this does not scale well. - To fix this, Ltac2 makes this boundary **explicit** through quoting and unquoting operators. - - **** 4.2.1 Quoting Rocq Terms - To embed a Rocq term into Ltac2 as a value of type [constr], use ['] (apostrophe). - In Ltac1, terms in patterns were implicitly quoted; there was no explicit notation: -*) - -(* Ltac1: - Ltac use_T := - match goal with - | _ : T |- _ => assumption (* T is implicitly a Rocq term *) - end. *) - -Ltac2 Eval 'nat. -Ltac2 Eval '(0 = 0). -Ltac2 Eval '(forall n : nat, n + 0 = n). - -(** **** 4.2.2 Unquoting - - To use a Ltac2 [constr] value back in a tactic position, unquote it with - [$] (dollar sign): -*) - -Goal True /\ True. - let t := 'I in - split; exact $t; exact $t. -Qed. - -(** **** 4.2.3 Identifiers and References - - To create an [ident] value (the name of a hypothesis or variable), use - [@name] syntax. - To recover the corresponding term from a hypothesis name, use [Control.hyp]: -*) - -Goal nat -> 0 = 0. - intros H. - printf "H : %t" (Constr.type (Control.hyp @H)). - reflexivity. -Qed. - -(** [reference:(name)] creates a [Std.reference] pointing to a global constant. - Pass it to [Env.instantiate] to recover the corresponding Rocq term: -*) - -Ltac2 Eval Env.instantiate reference:(nat). - - -(** *** 4.3 Matching Terms and Goals +(** *** 4.2 Matching Terms and Goals Ltac1 provides [lazymatch], [match] and [multimatch] for matching patterns and goal. This still exists in Ltac2 but has changed syntax to @@ -763,6 +695,92 @@ Goal forall x y : nat, (let a := x + 2 in let b := y + 1 in a = b) -> True. Abort. +(** *** 4.3 Quoting and Unquoting + + One of the main sources of confusion in Ltac1 is the implicit boundary + between Gallina (the language of Rocq terms) and Ltac1 meta-programs. + Ltac1 uses dynamic scoping rules to resolve names, leading to subtle bugs + when a name is mistaken for a Rocq term instead of an Ltac1 variable, or + vice versa. + + The goal was to ease user life but in practice this does not scale well. + To fix this, Ltac2 makes this boundary **explicit** through quoting and unquoting operators. + + For example, a tactic that splits a conjunction and closes both goals with [I]: +*) + +Ltac ltac1_close_conj t := split; exact t. + +Set Default Proof Mode "Classic". + +Goal True /\ True. +Proof. + ltac1_close_conj I. +Qed. + +(** In Ltac2, every Rocq term must be explicitly **quoted** with ['] which + produces a Ltac2 term of type [constr], and **unquoted** to recover a Rocq term. + + If we wanted to rewrite [ltac1_close_conj] in Ltac2, we would take variable + [t : constr] as argument, as [constr] is the only type we can manipulate. + Yet, to apply it to [exact] which expects a Rocq term, we need to unquote it. + This gives us: + +*) + +Ltac2 ltac2_close_conj0 (t : constr) := split; exact $t. + +Set Default Proof Mode "Ltac2". + +(** To be able to use it with a Rocq value, one then need to quote it to a [constr]. + For instance, like the following. +*) + +Goal True /\ True. +Proof. + ltac2_close_conj0 'I. +Qed. + +(** The quoting can be done automatically using a notation, we refer to the + following section for further explanations. +*) + +Ltac2 Notation "ltac2_close_conj" t(constr) := ltac2_close_conj0 t. + +(** The same apply to Rocq identifier which can be created using [@]. + In Ltac1, you could just write: +*) + +Set Default Proof Mode "Classic". + +Ltac ltac1_print_hyp_type h := + let T := type of h in idtac "type:" T. + +Goal nat -> False. +Proof. + intros H. + ltac1_print_hyp_type H. +Abort. + +(** In Ltac2, hypothesis names have the dedicated type [ident]. + Write [@name] to create an [ident] literal, then use [Control.hyp] to + recover the corresponding [constr]: +*) + +Set Default Proof Mode "Ltac2". + +Ltac2 ltac2_print_hyp_type (h : ident) := + printf "type: %t" (Constr.type (Control.hyp h)). + +Goal nat -> False. +Proof. + intros H. + Fail ltac2_print_hyp_type H. + ltac2_print_hyp_type @H. +Abort. + + + (** *** 4.4 Backtracking Ltac1 controls backtracking through: From be29183b462e2b4fc139e727e38e12a15a7ddee4 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Fri, 1 May 2026 01:45:02 +0200 Subject: [PATCH 08/17] fix typos --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 134 +++++++++--------- 1 file changed, 67 insertions(+), 67 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 7c61cf0..1648d91 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -22,7 +22,7 @@ - 2. Using Ltac2 to Write Proofs - 2.1 Using Ltac2 in the Ltac1 Proof Mode - 2.2 Using the Ltac2 Proof Mode - - 3. Ltac2 is a Proper Functional Programming Language + - 3. Ltac2 Is a Proper Functional Programming Language - 3.1 Types and Type Inference - 3.2 Call-by-Value Semantics and Thunking - 3.3 Effects: Printf and References @@ -49,12 +49,12 @@ *** 1.1 A Brief History of Ltac1 - Ltac1 was introduce in 2000 (Coq 7.0) to enable users to write their own + Ltac1 was introduced in 2000 (Coq 7.0) to enable users to write their own tactics by combining existing primitive tactics using an expressive set of combinators. For instance, users have been using Ltac1 to write variants of existing - tactics domain specific automation tactic. + tactics or domain-specific automation tactics. Ltac1 was key in the success of Rocq, and of many formalization efforts as it enabled us to write proofs in a more incremental, efficient and more @@ -63,22 +63,22 @@ *** 1.2 Design Flaws of Ltac1 - Yet, Ltac1 was not planned for so advanced uses and suffer designed flaws. + Yet, Ltac1 was not planned for such advanced uses and suffered from design flaws. - 1. At the time, there were no idea of what a good tactic language ought to be + 1. At the time, there was no idea of what a good tactic language ought to be and Ltac1 was not designed following current PL conventions - 2. The development of Ltac1 was not carefully planned, and features have - added piecewise over times by different contributors. + 2. The development of Ltac1 was not carefully planned, and features have been + added piecemeal over time by different contributors. Consequently, the language is far from well-designed, uniform, or well implemented, making improvements and every day use complicated. - 3. Ltac1 tried to accomodate two contradictory feature: for tactics - to be both automagical and predictible. - To do so, Ltac1 implements many dynamic decision procedures to facilitates - writing tactics that works well for small example but do not scale well. + 3. Ltac1 tried to accommodate two contradictory features: for tactics + to be both automagical and predictable. + To do so, Ltac1 implements many dynamic decision procedures to facilitate + writing tactics that work well for small examples but do not scale well. - With experirence, there are several well-known design flaws with Ltac1: + With experience, there are several well-known design flaws with Ltac1: - **No type system.** Ltac1 is completely untyped. Any value can be passed to any function, and type errors are only caught at runtime, often with cryptic @@ -88,7 +88,7 @@ - **No data structures.** Ltac1 has no lists, no records, and no algebraic types. All state must be threaded through the goal or through side channels. - - **Unclear Semantic** It is hard to predict when a tactic will be + - **Unclear Semantics.** It is hard to predict when a tactic will be evaluated, or whether a name refers to a Rocq term or an Ltac1 variable. This leads to subtle and hard-to-diagnose bugs. @@ -105,7 +105,7 @@ *** 1.3 Ltac2 - Ltac2 is designed to be the replacement of Ltac1, and offer both a + Ltac2 is designed to be the replacement of Ltac1, and offers both a reliable and scalable tactic language for Rocq, while being as backward compatible as possible. @@ -116,10 +116,10 @@ and a clear call-by-value semantic. - It has an explicit typed Foreign Function Interface. - This makes it easy to extend Ltac2 to expose and access primitive like unification, + This makes it easy to extend Ltac2 to expose and access primitives like unification, that were not accessible before, while providing better documentation for it. - As a consequence, it is possible to do more stuff in Ltac2 than in Ltac1. - For instance, it is now possible to manipulate to goal state, and modify + As a consequence, it is possible to do more in Ltac2 than in Ltac1. + For instance, it is now possible to manipulate the goal state, and modify the set of goals under focus etc. - Quoting and unquoting between Rocq terms (Gallina) and Ltac2 values is now @@ -143,7 +143,7 @@ more exposed primitives in more recent versions of Rocq. See https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 for the master branch of Rocq. - Most noticeably, Ltac2 still lacks notations for some for the basic tactics. + Most noticeably, Ltac2 still lacks notations for some of the basic tactics. For the moment, Ltac2 is not loaded by default with the Prelude. It needs to be imported with [From Ltac2 Require Import Ltac2]. @@ -154,28 +154,28 @@ From Ltac2 Require Import Ltac2 Printf Option. (** ** 2. Using Ltac2 to Write Proofs - Before discussing the Ltac2 language itself let us consider how to - the differences between Ltac1 and Ltac2 proof mode, and how to use on + Before discussing the Ltac2 language itself, let us consider + the differences between Ltac1 and Ltac2 proof modes, and how to use one in the other. *** 2.1 Using Ltac2 in the Ltac1 Proof Mode The main use for Ltac2 is to write predictable tactics. Yet, you do not need to port your whole development to Ltac2 to benefit from Ltac2. - You can write new script in Ltac2 but call it in the usual Ltac1 proof mode. + You can write new scripts in Ltac2 but call them in the usual Ltac1 proof mode. This lets you enjoy Ltac2's type safety and expressiveness while leaving all existing proofs untouched, and avoid dealing with differences between Ltac1 and Ltac2's proof mode. Consequently, a natural approach when migrating a large development is: - 1. Write new Ltac1 scipt or port them existing one in Ltac2. + 1. Write new Ltac1 scripts or port existing ones in Ltac2. 2. Import them into Ltac1 via [ltac2:(...)]. 3. Use them in existing proof scripts without further changes. - Importing Ltac2 automatically set the proof mode to Ltac2. + Importing Ltac2 automatically sets the proof mode to Ltac2. You can decide to keep using Ltac1 proof mode by using [Set Proof Mode "Classic"]. - Conversly [Set Proof Mode "Ltac2"] to use the Ltac2 proof mode. - You can then write script in Ltac2, and call them in a Ltac1 proof using + Conversely, [Set Proof Mode "Ltac2"] to use the Ltac2 proof mode. + You can then write scripts in Ltac2, and call them in a Ltac1 proof using [ltac2:()] wrapper. As an example, let us leverage the [printf] function for Ltac2. @@ -219,7 +219,7 @@ Qed. arguments and binds them under the names [x1 .. xn] in the Ltac2 scope. Inside the expression, [x1 .. xn] have type [Ltac1.t] and are converted to typed Ltac2 values using helpers such as [Ltac1.to_constr] and [Ltac1.to_ident]. - The ltac2 wrapper must then be defined as a letin and applied due to Ltac1 inner working. + The Ltac2 wrapper must then be defined as a let-in and applied, due to Ltac1's inner workings. *) Set Default Proof Mode "Classic". @@ -239,11 +239,11 @@ Qed. (** *** 2.2 Using the Ltac2 Proof Mode The first possibility is to use Ltac2 proof mode directly. - It is very similar to Ltac1 outside of a few syntax change. + It is very similar to Ltac1 outside of a few syntax changes. - Most noticeably dispatching tactics has changed syntax, and parsing - In Ltac1, when a tactic create more than one new goal, you can specify which - tactic to apply with the syntax [tac2; [tac31 | tac32]]. + Most noticeably, the dispatching syntax has changed. + In Ltac1, when a tactic creates more than one new goal, you can specify which + tactic to apply with the syntax [tac1; [tac21 | tac22]]. Moreover, [tac1; tac2; [tac31 | tac32]] is parsed as [(tac1; tac2); [tac31 | tac32]]. *) @@ -256,10 +256,10 @@ Proof. split; split; [exact HP | exact HQ | exact HR | exact HS]. Qed. -(** In Ltac2, this now written with the syntax [tac1; [tac21 | tac22 ]] in order +(** In Ltac2, this is now written with the syntax [tac1 > [tac21 | tac22]] in order to avoid syntax conflict with ???. Moreover, [tac1; tac2; [tac31 | tac32]] - is now parsed as [tac1; (tac2; [tac31 | tac32])] as Ltac2 no longer - automatically delay tactic execution. + is now parsed as [tac1; (tac2; [tac31 | tac32])] as Ltac2 no longer + automatically delays tactic execution. Consequently, if [tac1] generates multiple goals, the dispatcher will attempt to apply the list [tac31|tac32] to the subgoals generated by [tac2] @@ -387,19 +387,19 @@ Qed. -(** ** 3. Ltac2 is a Proper Functional Programming Language *) +(** ** 3. Ltac2 Is a Proper Functional Programming Language *) (** Ltac1 is a non standard tactic language with no type system, opaque dynamically-typed values, and a non-standard evaluation strategy, making tactics fragile and hard to predict and debug. - In constrast, Ltac2 is a proper programming language that belongs to the + In contrast, Ltac2 is a proper programming language that belongs to the well-known class of ML languages: it is a call-by-value functional language with a Hindley–Milner type system. Expressions have static types that can be inferred, hence ill-typed programs are rejected at compile time rather than runtime, and are easy to write. - Moreover, evaluation is fully predictable thanks to call by-value semantic. - This makes Ltac2 tactics reliable and composable by design, opposed to Ltac1. + Moreover, evaluation is fully predictable thanks to call-by-value semantics. + This makes Ltac2 tactics reliable and composable by design, as opposed to Ltac1. *) (** *** 3.1 Types and Type Inference @@ -429,7 +429,7 @@ Ltac2 my_id (x : 'a) : 'a := x. Ltac2 Eval my_id 42. Ltac2 Eval my_id true. -(** Ltac2 provides primitive types both for p: +(** Ltac2 provides the following primitive types: - [unit]: the unit type, with its single value [()]. - [bool]: Booleans, with values [true] and [false]. - [int]: machine integers (63-bit on a 64-bit platform). @@ -454,7 +454,7 @@ Fail Ltac2 foo X := X. (** Functions can then be defined with the [rec] keyword for recursivity, and [match] for pattern-matching similarly to OCaml. - Constructors are then refered without parentheses, like [Add a b]. + Constructors are then referred to without parentheses, like [Add a b]. *) Ltac2 rec eval_expr (e : expr) : int := @@ -468,7 +468,7 @@ Ltac2 rec eval_expr (e : expr) : int := Ltac2 Eval eval_expr (Add (Num 1) (Mul (Num 2) (Num 3))). (** The CoreLib provides some of the usual polymorphic types like [list] and - [option], and a few basic functions for it. + [option], and a few basic functions for them. *) Ltac2 Eval [1; 2; 3]. @@ -617,19 +617,19 @@ Qed. is in scope. Ltac2 has an explicit, typed Foreign Function Interface (FFI). - Rocq API -- kernel or higher levels fuynctions -- can be easily. - This enables easy access to API that were not accessible in Ltac1, + Rocq API -- kernel or higher-level functions -- can be easily exposed. + This enables easy access to APIs that were not accessible in Ltac1, making Ltac2 much more expressive. - Many API are exposed in different modules in the core library available at: + Many APIs are exposed in different modules in the core library available at: https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 - Most noticeable examples:: + Most notable examples: - [Control]: interact with the proof state (goal) and backtracking - [Constr]: inspect, build, and compare Rocq terms - [Std]: reduce terms, call unification, access the environment - [Fresh]: to create fresh [ident] - - [Unification]: to call unification in a controled way + - [Unification]: to call unification in a controlled way - [Constr.Unsafe]: to access the raw kernel representation of terms The full core library is at: @@ -655,7 +655,7 @@ Abort. (** *** 4.2 Matching Terms and Goals Ltac1 provides [lazymatch], [match] and [multimatch] for matching - patterns and goal. This still exists in Ltac2 but has changed syntax to + patterns and goals. This still exists in Ltac2 but has changed syntax to avoid confusion with the [match] for matching algebraic types. The new syntax is [lazy_match!], [match!], and [multi_match!]. @@ -678,10 +678,10 @@ Goal nat -> bool -> 0 = 1 -> False. intros. print_all_hyp (). Abort. -(** Another difference with Ltac1 is that a pattern containing variable binding - must now be explicitly, whereas it used to be optional and dynamically +(** Another difference with Ltac1 is that a pattern containing variable bindings + must now be explicit, whereas it used to be optional and dynamically figured out if not specified. For instance, to match [let var := ?expr in - ?body], one must one write [let var := ?expr in @?body var]. + ?body], one must write [let var := ?expr in @?body var]. *) Ltac2 print_body_hyp_letin () : unit := @@ -703,7 +703,7 @@ Abort. when a name is mistaken for a Rocq term instead of an Ltac1 variable, or vice versa. - The goal was to ease user life but in practice this does not scale well. + The goal was to ease users' lives, but in practice this does not scale well. To fix this, Ltac2 makes this boundary **explicit** through quoting and unquoting operators. For example, a tactic that splits a conjunction and closes both goals with [I]: @@ -747,7 +747,7 @@ Qed. Ltac2 Notation "ltac2_close_conj" t(constr) := ltac2_close_conj0 t. -(** The same apply to Rocq identifier which can be created using [@]. +(** The same applies to Rocq identifiers, which can be created using [@]. In Ltac1, you could just write: *) @@ -784,7 +784,7 @@ Abort. (** *** 4.4 Backtracking Ltac1 controls backtracking through: - - [match goal] (backtracks into branches on failure, and co), + - [match goal] (backtracks into branches on failure, etc.), - Combinators like [first [tac1 | tac2 | ...]] - [fail n] (propagates failure [n] levels up through [match] branches) @@ -794,7 +794,7 @@ Abort. of good primitives to deal with backtracking. Instead, Ltac2 has fine grained primitives to manipulate values as stream of possibilities, and backtracking. - Combinators like [first] can then be reimplemented using theses primitives. + Combinators like [first] can then be reimplemented using these primitives. Most users do not have the needs for these primitives, and the existing combinators are enough. We mention them briefly, and refer to the @@ -806,7 +806,7 @@ Abort. - [Control.plus : (unit -> 'a) -> (exn -> 'a) -> 'a] -- stacks a backtracking choice: try the first thunk; on exception, try the handler. This is the primitive underlying [tac1 + tac2], but it is finer - since different decision can be performed depending on the exception raised. + since different decisions can be performed depending on the exception raised. - [Control.case : (unit -> 'a) -> ('a * (exn -> 'a)) result] -- inspects whether a tactic has at least one success without consuming it. @@ -820,8 +820,8 @@ Abort. simply expands to a fixed Ltac2 expression. It does not add a new rule to the Ltac2 grammar nor new keywords: the name is resolved as a plain identifier at parse time, so it cannot - cause parsing conflicts., e.g. with variable names. - It should be used when you want short name to a combinator or a + cause parsing conflicts, e.g. with variable names. + It should be used when you want a short name for a combinator or a fixed tactic sequence. *) @@ -831,7 +831,7 @@ Goal 1 = 1 /\ True. split; obvious. Qed. -(** A full [Ltac2 Notation] declares new parsing rule and keyworks which are +(** A full [Ltac2 Notation] declares new parsing rules and keywords which are specified with ["tac_name"]. Arguments are then given with the syntax [name_arg(X)] and [X] specifies that type of [name_arg]. @@ -871,7 +871,7 @@ end. (** To write a notation for it, we write: - - ["my_first"] and ["["] / ["]"] ase literal keywords that the parser matches + - ["my_first"] and ["["] / ["]"] are literal keywords that the parser matches verbatim; so that [my_first [...]] is unambiguous - [tacs] is the name bound in the body to the parsed argument @@ -902,12 +902,12 @@ Qed. (** ** 5. Small Case Study - Let us now, consider a small study and write a tactic that [simplify_let] + Let us now consider a small case study and write a tactic [simplify_let] that takes a hypothesis [h] whose type is a let-in [let var := expr in body[var]], and turns it into [body[x']], where [x' := expr] is a new shared definition introduced in the whole context and goal. - In Ltac1, it would have be written has: + In Ltac1, it would have been written as: *) Ltac simplify_let H := @@ -923,14 +923,14 @@ Ltac simplify_let H := end. (** In Ltac2, we need to: - - use small cap for variables - - now have [Control.hyp] to recover the body of h - - [Constr.type] is now a proper function rather than a ad-hoc construction - - use the [Fresh] module to create a fresh variables + - use lowercase for variables + - use [Control.hyp] to recover the body of h + - [Constr.type] is now a proper function rather than an ad-hoc construction + - use the [Fresh] module to create fresh variables - use [$] to unquote variables back to Rocq's world - In the end, this gives us a script that is similar but, but with a few - decoration, and a clearer semantic which can be written with or without + In the end, this gives us a script that is similar but with a few + decorations and clearer semantics, which can be written with or without importing the modules. *) @@ -949,7 +949,7 @@ Ltac2 simplify_let (h : ident) : unit := lazy head beta in h end. -(** The advantage of Ltac2 is that the FFI interface enables us to write script +(** The advantage of Ltac2 is that the FFI interface enables us to write scripts we could not have in Ltac1. For instance, we can now use the [Constr.Unsafe] API to write the [simplify_let] tactic by directly accessing the structure of the term, and performing the substitution by hand rather than relying on From 8abc39ab25fa50c558aedeceb30d283f2709f235 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sat, 2 May 2026 15:42:17 +0200 Subject: [PATCH 09/17] fix most of Will Thomas's comments --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 45 +++++++++++++------ 1 file changed, 31 insertions(+), 14 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 1648d91..3e1db79 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -315,21 +315,23 @@ Qed. are imported but are currently missing notations for them in the Corelib. For instance, in Rocq 9.0, a notation is missing for the tactic [clearbody]. This problem will be solved over time with contributions to the Corelib. +*) + +Goal forall A, A -> A * A. +Proof. + intros. pose (x := 2). Fail clearbody x. +Abort. - In the meantime, there are two workarounds. +(** In the meantime, there are two workarounds. The first option is to define the missing notation locally. In this case, one should also consider contributing it upstream to the Corelib. The underlying primitive lives in [Std] and expects an [ident list], so a notation using the [list1(ident)] parser -- which parses one or more - space-separated identifiers -- is sufficient: + space-separated identifiers -- is sufficient. + See the corresponding section for more information. *) -Goal forall A, A -> A * A. -Proof. - intros. pose (x := 2). Fail clearbody x. -Abort. - Ltac2 Notation "clearbody" ids(list1(ident)) := Std.clearbody ids. Goal forall A, A -> A * A. @@ -377,12 +379,14 @@ Proof. my_exact '(eq_refl). Qed. -Ltac2 my_intro (id : ident) := +Ltac2 my_intro0 (id : ident) := ltac1:(id |- intro id) (Ltac1.of_ident id). +Ltac2 Notation "my_intro" id(ident) := my_intro0 id. + Goal forall n : nat, n = n. Proof. - my_intro @n. reflexivity. + my_intro n. reflexivity. Qed. @@ -421,8 +425,16 @@ Ltac2 add (x : int) (y : int) : int := Int.add x y. Ltac2 Eval add 2 3. Fail Ltac2 Eval add 2 true. -(** Ltac2 supports Hindley–Milner polymorphism. - The following identity function works at any type as its type is [`a -> `a]. +(** Ltac2 supports Hindley–Milner polymorphism, also called prenex polymorphism. + In prenex polymorphism, type-variable quantifiers must appear at the + outermost level of the type, never nested inside it. + + For instance, [∀ 'a, 'a -> 'a] is a valid polymorphic type: the quantifier + is at the front, and the function works at any type ['a]. It is the type of + a function that takes an input of a type ['a] and return a value fo the same type. + + However, [∀ 'a, (∀ 'b, 'b -> 'b) -> 'a] is not valid because ['b] is + quantified inside the type. Note, it is not the same as [∀ 'a 'b, ('b -> 'b) -> 'a]. *) Ltac2 my_id (x : 'a) : 'a := x. @@ -666,6 +678,9 @@ Abort. - [match! goal] -- like Ltac1 [match goal]: tries patterns in order, and **does** backtrack into a branch if it raises an exception. - [multi_match! goal] -- backtracks both into branches and into patterns. + + Though, it is common in Ltac1 to use cap variables for hypotheses, like [H], + in Ltac2, you need to use **lowercase** ones. *) Ltac2 print_all_hyp () := @@ -823,9 +838,11 @@ Abort. cause parsing conflicts, e.g. with variable names. It should be used when you want a short name for a combinator or a fixed tactic sequence. + + In Rocq 9.2 or above, use [Ltac2 Abbreviation]. *) -Ltac2 Notation "obvious" := first [assumption | reflexivity]. +Ltac2 Notation obvious := first [assumption | reflexivity]. Goal 1 = 1 /\ True. split; obvious. @@ -853,7 +870,7 @@ Qed. - [list0(e)] -- parse a whitespace-separated, possibly empty, list of [e] - [list0(e, "sep")] -- same, but with a literal keyword separator [sep]. - [list1(e)] / [list1(e, "sep")] -- like [list0] but require at least one - element. The notation [my_first [...]] above uses + element. The notation [my_first [...]] below uses [list1(thunk(tactic(6)), "|")] to parse one or more [|]-separated tactic branches. - [opt(e)] -- parse an optional argument [e] of type [option e] @@ -923,7 +940,7 @@ Ltac simplify_let H := end. (** In Ltac2, we need to: - - use lowercase for variables + - **use lowercase for variables** - use [Control.hyp] to recover the body of h - [Constr.type] is now a proper function rather than an ad-hoc construction - use the [Fresh] module to create fresh variables From 0e50deb2e1d24753b887b4e3fedd913a4d65d1b7 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sat, 2 May 2026 16:02:22 +0200 Subject: [PATCH 10/17] add sec on exceptions --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 3e1db79..9c69e99 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -26,6 +26,7 @@ - 3.1 Types and Type Inference - 3.2 Call-by-Value Semantics and Thunking - 3.3 Effects: Printf and References + - 3.4 Exceptions - 4. Ltac2 as a Meta-Programming Language for Rocq - 4.1 Foreign Function Interface - 4.2 Matching Terms and Goals @@ -619,6 +620,51 @@ Qed. *) +(** *** 3.4 Exceptions + + Ltac2 has a built-in type [exn] for exceptions. + Several exceptions are predefined in the standard library: + - [Tactic_failure (msg : message option)] -- the standard tactic failure, + raised by most combinators and by [fail]. + - [Out_of_bounds (msg : message option)] -- index out of range (e.g. list access). + - [Division_by_zero] -- integer division by zero. + - [Invalid_argument (msg : message option)] -- a function received an argument + it cannot handle. + - [Match_failure] -- an inexhaustive pattern match was not satisfied. + + The [exn] type is open: you can add your own variants with the + syntax [Ltac2 Type exn ::= [myEx (type)]]. +*) + +Ltac2 Type exn ::= [ OutOfFuel (message option) ]. + +(** To easiest method to build an object of type [message] is to use [fprintf] + that works exactly as [printf] except it returns an object of type + [message] instead of printing it + + There are two primitives to raise an exception, with different semantics: + + 1. [Control.throw : exn -> 'a] -- raises a **non-backtrackable** exception. + It cannot be caught by the backtracking combinators [Control.plus] or + [try]. It is meant for programming errors or hard failures where retrying + makes no sense (analogous to a panic). +*) + +Goal False. + Fail try (Control.throw (OutOfFuel (Some (fprintf "should fail")))). +Abort. + +(** 2. [Control.zero : exn -> 'a] -- raises a **backtrackable** exception. + It signals that the current branch has no solution, which triggers + backtracking: [Control.plus] will try the alternative branch, and [try] + will silently recover. Checkout the corresponding section for more information. +*) + +Goal False. + try (Control.zero (OutOfFuel (Some (fprintf "should succed and print nothing")))). +Abort. + + (** ** 4. Ltac2 as a Meta-Programming Language for Rocq *) From 8fc9d23aad75fd64d2ebc45c12e0476187f50121 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sat, 2 May 2026 16:23:02 +0200 Subject: [PATCH 11/17] typos --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 64 +++++++++---------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 9c69e99..798e2f7 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -12,7 +12,7 @@ familiar with Ltac1. We mainly focus on the differences with Ltac1, and how to translate your existing Ltac1 knowledge into Ltac2 idioms. - *** Table of content + *** Table of contents - 1. Introduction - 1.1 A Brief History of Ltac1 @@ -67,7 +67,7 @@ Yet, Ltac1 was not planned for such advanced uses and suffered from design flaws. 1. At the time, there was no idea of what a good tactic language ought to be - and Ltac1 was not designed following current PL conventions + and Ltac1 was not designed following current PL conventions. 2. The development of Ltac1 was not carefully planned, and features have been added piecemeal over time by different contributors. @@ -83,7 +83,7 @@ - **No type system.** Ltac1 is completely untyped. Any value can be passed to any function, and type errors are only caught at runtime, often with cryptic - error messages. This makes writing large library and tactics and debugging + error messages. This makes writing large libraries and tactics and debugging very tedious. - **No data structures.** Ltac1 has no lists, no records, and no algebraic @@ -114,9 +114,9 @@ - It is a proper typed functional programming language of the Hindley–Milner family, similarly to OCaml, with type inference, algebraic data types, - and a clear call-by-value semantic. + and a clear call-by-value semantics. - - It has an explicit typed Foreign Function Interface. + - It has an explicitly typed Foreign Function Interface. This makes it easy to extend Ltac2 to expose and access primitives like unification, that were not accessible before, while providing better documentation for it. As a consequence, it is possible to do more in Ltac2 than in Ltac1. @@ -124,7 +124,7 @@ the set of goals under focus etc. - Quoting and unquoting between Rocq terms (Gallina) and Ltac2 values is now - explicit and syntactically marked. It no longer relies on a hard to predict + explicit and syntactically marked. It no longer relies on a hard-to-predict dynamic decision procedure. - Backtracking is modelled as streams of possibilities, with fine-grained @@ -144,7 +144,7 @@ more exposed primitives in more recent versions of Rocq. See https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 for the master branch of Rocq. - Most noticeably, Ltac2 still lacks notations for some of the basic tactics. + Most notably, Ltac2 still lacks notations for some of the basic tactics. For the moment, Ltac2 is not loaded by default with the Prelude. It needs to be imported with [From Ltac2 Require Import Ltac2]. @@ -169,7 +169,7 @@ From Ltac2 Require Import Ltac2 Printf Option. between Ltac1 and Ltac2's proof mode. Consequently, a natural approach when migrating a large development is: - 1. Write new Ltac1 scripts or port existing ones in Ltac2. + 1. Write new scripts in Ltac2 or port existing Ltac1 ones to Ltac2. 2. Import them into Ltac1 via [ltac2:(...)]. 3. Use them in existing proof scripts without further changes. @@ -401,8 +401,8 @@ Qed. In contrast, Ltac2 is a proper programming language that belongs to the well-known class of ML languages: it is a call-by-value functional language with a Hindley–Milner type system. - Expressions have static types that can be inferred, hence ill-typed programs - are rejected at compile time rather than runtime, and are easy to write. + Expressions have static types that can be inferred, so ill-typed programs + are rejected at compile time rather than at runtime. Moreover, evaluation is fully predictable thanks to call-by-value semantics. This makes Ltac2 tactics reliable and composable by design, as opposed to Ltac1. *) @@ -418,7 +418,7 @@ Qed. annotations are optional -- the type checker infers them -- but can be written for documentation or disambiguation. - For instance, if we define an alias for addition of integer, Ltac2 will + For instance, if we define an alias for integer addition, Ltac2 will automatically figure out the type is `int -> int -> int`: *) @@ -432,10 +432,10 @@ Fail Ltac2 Eval add 2 true. For instance, [∀ 'a, 'a -> 'a] is a valid polymorphic type: the quantifier is at the front, and the function works at any type ['a]. It is the type of - a function that takes an input of a type ['a] and return a value fo the same type. + a function that takes an input of type ['a] and returns a value of the same type. However, [∀ 'a, (∀ 'b, 'b -> 'b) -> 'a] is not valid because ['b] is - quantified inside the type. Note, it is not the same as [∀ 'a 'b, ('b -> 'b) -> 'a]. + quantified inside the type. Note that it is not the same as [∀ 'a 'b, ('b -> 'b) -> 'a]. *) Ltac2 my_id (x : 'a) : 'a := x. @@ -448,7 +448,7 @@ Ltac2 Eval my_id true. - [int]: machine integers (63-bit on a 64-bit platform). - [string]: character strings. - [ident]: Rocq identifiers (names of hypotheses, variables, …). - - [constr]: type of Rocq terms in Ltac2 + - [constr]: type of Rocq terms in Ltac2. Beyond the built-in types, you can define your own algebraic data types with [Ltac2 Type]. As in OCaml, constructor names must start with an @@ -465,7 +465,7 @@ Ltac2 Type rec expr := Fail Ltac2 foo X := X. -(** Functions can then be defined with the [rec] keyword for recursivity, +(** Functions can then be defined with the [rec] keyword for recursion, and [match] for pattern-matching similarly to OCaml. Constructors are then referred to without parentheses, like [Add a b]. *) @@ -553,7 +553,7 @@ Qed. (** *** 3.3 Effects: Printf and References - Compared to Ltac1, Ltac2 has proper effects, noticeably printing and references. + Compared to Ltac1, Ltac2 has proper effects, notably printing and references. **** 3.3.1 Printf @@ -572,7 +572,7 @@ Qed. This makes it much easier to inspect the proof state or debug automation than the [idtac] approach. For instance, here is a small tactic to - print the type of an hypothesis. We will explain the exact syntax + print the type of a hypothesis. We will explain the exact syntax in the next section. *) @@ -638,9 +638,9 @@ Qed. Ltac2 Type exn ::= [ OutOfFuel (message option) ]. -(** To easiest method to build an object of type [message] is to use [fprintf] - that works exactly as [printf] except it returns an object of type - [message] instead of printing it +(** The easiest method to build a value of type [message] is to use [fprintf], + which works exactly like [printf] except it returns a [message] value + instead of printing it. There are two primitives to raise an exception, with different semantics: @@ -657,11 +657,11 @@ Abort. (** 2. [Control.zero : exn -> 'a] -- raises a **backtrackable** exception. It signals that the current branch has no solution, which triggers backtracking: [Control.plus] will try the alternative branch, and [try] - will silently recover. Checkout the corresponding section for more information. + will silently recover. See the corresponding section for more information. *) Goal False. - try (Control.zero (OutOfFuel (Some (fprintf "should succed and print nothing")))). + try (Control.zero (OutOfFuel (Some (fprintf "should succeed and print nothing")))). Abort. @@ -725,8 +725,8 @@ Abort. **does** backtrack into a branch if it raises an exception. - [multi_match! goal] -- backtracks both into branches and into patterns. - Though, it is common in Ltac1 to use cap variables for hypotheses, like [H], - in Ltac2, you need to use **lowercase** ones. + Although it is common in Ltac1 to use uppercase variables for hypotheses, like [H], + in Ltac2 you need to use **lowercase** ones. *) Ltac2 print_all_hyp () := @@ -748,7 +748,7 @@ Abort. Ltac2 print_body_hyp_letin () : unit := lazy_match! goal with | [_ : let var := _ in @?body var |- _] => - printf "the body is expanded as a function :%t" body + printf "the body is expanded as a function: %t" body end. Goal forall x y : nat, (let a := x + 2 in let b := y + 1 in a = b) -> True. @@ -849,15 +849,15 @@ Abort. - Combinators like [first [tac1 | tac2 | ...]] - [fail n] (propagates failure [n] levels up through [match] branches) - Ltac2 has more fine grained controls on backtracking. + Ltac2 has more fine-grained controls on backtracking. Matching and combinators are still available. - However, [fail n] is no longer supported, it was a hack to deal with a lack - of good primitives to deal with backtracking. - Instead, Ltac2 has fine grained primitives to manipulate values - as stream of possibilities, and backtracking. + However, [fail n] is no longer supported; it was a hack to deal with the lack + of good primitives for backtracking. + Instead, Ltac2 has fine-grained primitives to manipulate values + as streams of possibilities and backtracking. Combinators like [first] can then be reimplemented using these primitives. - Most users do not have the needs for these primitives, and the existing + Most users do not need these primitives, and the existing combinators are enough. We mention them briefly, and refer to the documentation for more details. The three primitives are: @@ -900,7 +900,7 @@ Qed. The available argument parsers include: - There are first basic atoms: + The basic atoms are: - [tactic] / [tactic(n)] -- parse a tactic at precedence level [n] (default 5); evaluated eagerly, so use [thunk] when the argument is a tactic branch that must be delayed. From 590c7016b22b4e52775c892138d4fa886e56bd66 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sun, 3 May 2026 02:15:06 +0200 Subject: [PATCH 12/17] use stdlib instead of corelib --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 798e2f7..90985a5 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -313,9 +313,9 @@ Proof. Qed. (** However, a real issue with the Ltac2 proof mode is that some tactics - are imported but are currently missing notations for them in the Corelib. + are imported but are currently missing notations for them in Ltac2 standard library. For instance, in Rocq 9.0, a notation is missing for the tactic [clearbody]. - This problem will be solved over time with contributions to the Corelib. + This problem will be solved over time with contributions to the standard library. *) Goal forall A, A -> A * A. @@ -326,7 +326,7 @@ Abort. (** In the meantime, there are two workarounds. The first option is to define the missing notation locally. - In this case, one should also consider contributing it upstream to the Corelib. + In this case, one should also consider contributing it upstream to the standard library. The underlying primitive lives in [Std] and expects an [ident list], so a notation using the [list1(ident)] parser -- which parses one or more space-separated identifiers -- is sufficient. @@ -480,8 +480,8 @@ Ltac2 rec eval_expr (e : expr) : int := (* 1 + 2×3 = 7 *) Ltac2 Eval eval_expr (Add (Num 1) (Mul (Num 2) (Num 3))). -(** The CoreLib provides some of the usual polymorphic types like [list] and - [option], and a few basic functions for them. +(** The standard library provides some of the usual polymorphic types like + [list] and [option], and a few basic functions for them. *) Ltac2 Eval [1; 2; 3]. @@ -923,7 +923,7 @@ Qed. - [seq(e1, e2, ...)] -- parse a fixed sequence of entries and bind them as a tuple. As an example consider reimplementing [first] using the backtracking operators - as implemented in the CoreLib. + as implemented in the Ltac2 standard library. *) Ltac2 rec my_first0 tacs := From 2e68ee64f4fcc1c292e32b1d89f2121a1248bfec Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sun, 3 May 2026 15:23:13 +0200 Subject: [PATCH 13/17] solve one comment by Gaetan --- src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 90985a5..5092b15 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -100,8 +100,8 @@ meta-programs is not syntactically marked. Ltac1 uses dynamic scoping rules to resolve names, which are hard to understand and debug. - - **Poor FFI.** Functions from the Rocq kernel are imported all at once, - without types and without any control over what is in scope. + - **Poor FFI.** Functions from the Rocq codebase are imported all at once, + as tactics without types and without any control over what is in scope. *** 1.3 Ltac2 From b519c859c117ccee439cd0c8c2219f791ab78b53 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sun, 3 May 2026 17:19:06 +0200 Subject: [PATCH 14/17] fix comments Antoine Gontard --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 102 ++++++++++++------ 1 file changed, 67 insertions(+), 35 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 5092b15..dcec9cb 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -41,7 +41,7 @@ - Familiarity with Ltac1 and basic Rocq proof writing. Installation: - - Ltac2 and its core library are available by default with Rocq. + - Ltac2 and its standard library are available by default with Rocq. *) @@ -139,8 +139,8 @@ strongly encourage users to use Ltac2 (or other alternatives) instead of Ltac1 for new projects and new automation code in existing projects. - It comes with a Core Library that is meant to contain basic building blocks - for creating complex tactics. The Core Library keeps evolving and may contain + It comes with a standard Library that is meant to contain basic building blocks + for creating complex tactics. The standard Library keeps evolving and may contain more exposed primitives in more recent versions of Rocq. See https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 for the master branch of Rocq. @@ -210,9 +210,9 @@ Qed. (** Importantly, [ltac2:(...)] creates a scope boundary: the code inside is pure Ltac2, and Ltac1 variables are not in scope there. - For instance, in a function [my_intro (id : ident) := ltac2:(intro id)], the - [id] inside [ltac2:(...)] would be treated as the Ltac2 literal name [id], - not as the Ltac1 variable -- so the tactic would always introduce a + For instance, in a Ltac1 function [my_intro (id : ident) := ltac2:(intro id)], + the [id] inside [ltac2:(...)] would be treated as the Ltac2 literal name [id], + not as the Ltac1 variable. The resulting tactic would always introduce a hypothesis named [id] regardless of what was passed. To pass Ltac1 values across this boundary, one uses the binder syntax @@ -249,8 +249,6 @@ Qed. [(tac1; tac2); [tac31 | tac32]]. *) -Set Default Proof Mode "Classic". - Goal forall P Q R S : Prop, P -> Q -> R -> S -> (P /\ Q) /\ (R /\ S). Proof. intros P Q R S HP HQ HR HS. @@ -422,7 +420,8 @@ Qed. automatically figure out the type is `int -> int -> int`: *) -Ltac2 add (x : int) (y : int) : int := Int.add x y. +Ltac2 add x y : int := Int.add x y. +Ltac2 Check add. Ltac2 Eval add 2 3. Fail Ltac2 Eval add 2 true. @@ -438,7 +437,8 @@ Fail Ltac2 Eval add 2 true. quantified inside the type. Note that it is not the same as [∀ 'a 'b, ('b -> 'b) -> 'a]. *) -Ltac2 my_id (x : 'a) : 'a := x. +Ltac2 my_id x := x. +Ltac2 Check my_id. Ltac2 Eval my_id 42. Ltac2 Eval my_id true. @@ -521,6 +521,7 @@ Ltac2 bad_ignore (_ : unit) : unit := (). *) Goal True. +Proof. Fail bad_ignore fail. Abort. @@ -547,6 +548,7 @@ Qed. Ltac2 Notation good_ignore := good_ignore0. Goal True. +Proof. good_ignore fail. exact I. Qed. @@ -582,6 +584,7 @@ Ltac2 print_type0 (h : ident) := Ltac2 Notation "print_type" h(ident) := print_type0 h. Goal nat -> bool -> True. +Proof. intros a b. print_type a. print_type b. @@ -606,6 +609,7 @@ Abort. *) Goal forall (n m : nat), True. +Proof. intros n m. let count := Ref.ref 0 in clear n; Ref.incr count; @@ -651,6 +655,7 @@ Ltac2 Type exn ::= [ OutOfFuel (message option) ]. *) Goal False. +Proof. Fail try (Control.throw (OutOfFuel (Some (fprintf "should fail")))). Abort. @@ -661,6 +666,7 @@ Abort. *) Goal False. +Proof. try (Control.zero (OutOfFuel (Some (fprintf "should succeed and print nothing")))). Abort. @@ -679,7 +685,7 @@ Abort. This enables easy access to APIs that were not accessible in Ltac1, making Ltac2 much more expressive. - Many APIs are exposed in different modules in the core library available at: + Many APIs are exposed in different modules in the standard library available at: https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 Most notable examples: @@ -690,7 +696,7 @@ Abort. - [Unification]: to call unification in a controlled way - [Constr.Unsafe]: to access the raw kernel representation of terms - The full core library is at: + The full standard library is at: https://github.com/rocq-prover/rocq/tree/master/theories/Ltac2 For example, [Constr.type] retrieves the type of a term and [Std.eval_hnf] @@ -706,6 +712,7 @@ Ltac2 print_hnf_type0 (h : ident) : unit := Ltac2 Notation "print_hnf_type" h(ident) := print_hnf_type0 h. Goal (let x := 1 in x = 1) -> False. +Proof. intros x. print_hnf_type x. Abort. @@ -715,18 +722,11 @@ Abort. Ltac1 provides [lazymatch], [match] and [multimatch] for matching patterns and goals. This still exists in Ltac2 but has changed syntax to avoid confusion with the [match] for matching algebraic types. - The new syntax is [lazy_match!], [match!], and [multi_match!]. - Ltac2 provides three matching combinators: + Otherwise, they work as in Ltac1. - - [lazy_match! goal] -- like Ltac1 [lazymatch goal]: tries patterns in order, - does **not** backtrack into a branch once a pattern has matched. - - [match! goal] -- like Ltac1 [match goal]: tries patterns in order, and - **does** backtrack into a branch if it raises an exception. - - [multi_match! goal] -- backtracks both into branches and into patterns. - - Although it is common in Ltac1 to use uppercase variables for hypotheses, like [H], - in Ltac2 you need to use **lowercase** ones. + Although it is common in Ltac1 to use uppercase variables for hypotheses, + like [H], keep in mind in Ltac2 you need to use **lowercase** ones. *) Ltac2 print_all_hyp () := @@ -736,6 +736,7 @@ Ltac2 print_all_hyp () := end. Goal nat -> bool -> 0 = 1 -> False. +Proof. intros. print_all_hyp (). Abort. @@ -752,6 +753,7 @@ Ltac2 print_body_hyp_letin () : unit := end. Goal forall x y : nat, (let a := x + 2 in let b := y + 1 in a = b) -> True. +Proof. intros. print_body_hyp_letin (). Abort. @@ -780,12 +782,13 @@ Proof. Qed. (** In Ltac2, every Rocq term must be explicitly **quoted** with ['] which - produces a Ltac2 term of type [constr], and **unquoted** to recover a Rocq term. + produces a Ltac2 term of type [constr], and **unquoted** to recover a Rocq + term using [$]. Note, for complex implementation reason [$] can only be + applied to variables. If we wanted to rewrite [ltac1_close_conj] in Ltac2, we would take variable [t : constr] as argument, as [constr] is the only type we can manipulate. - Yet, to apply it to [exact] which expects a Rocq term, we need to unquote it. - This gives us: + Yet, to apply it to [exact] which expects an unquoted term, which gives us: *) @@ -891,6 +894,7 @@ Abort. Ltac2 Notation obvious := first [assumption | reflexivity]. Goal 1 = 1 /\ True. +Proof. split; obvious. Qed. @@ -927,10 +931,10 @@ Qed. *) Ltac2 rec my_first0 tacs := -match tacs with -| [] => Control.zero (Tactic_failure None) -| tac :: tacs => Control.enter (fun _ => orelse tac (fun _ => my_first0 tacs)) -end. + match tacs with + | [] => Control.zero (Tactic_failure None) + | tac :: tacs => Control.enter (fun _ => orelse tac (fun _ => my_first0 tacs)) + end. (** To write a notation for it, we write: @@ -958,6 +962,7 @@ end. Ltac2 Notation "my_first" "[" tacs(list0(thunk(tactic(6)), "|")) "]" := my_first0 tacs. Goal True. +Proof. my_first [ (printf "tactic 1"; fail) | (printf "tactic 2"; fail) | exact I ]. Qed. @@ -974,17 +979,24 @@ Qed. *) Ltac simplify_let H := - let H := lazymatch goal with [ H : let var := ?t in _ |- _ ] => H end in let type_h := type of H in lazymatch type_h with | let var := ?expr in ?body => idtac body; let x := fresh "x" in set (x := expr) in *; - change (body x) in H; + change ((fun var => body) x) in H; lazy head beta in H end. +Set Default Proof Mode "Classic". + +Goal forall x y : nat, (let a := x + 2 in let b := y + 1 in a = b) -> True. + intros x y h. + Fail simplify_let x. + simplify_let h. +Abort. + (** In Ltac2, we need to: - **use lowercase for variables** - use [Control.hyp] to recover the body of h @@ -998,13 +1010,15 @@ Ltac simplify_let H := *) +Set Default Proof Mode "Ltac2". + Import Control Constr. -Ltac2 simplify_let (h : ident) : unit := +Ltac2 simplify_let0 (h : ident) : unit := let type_h := type (hyp h) in lazy_match! type_h with | let var := ?expr in @?body var => - printf "the body is :%t" body; + printf "the body is: %t" body; let x := Fresh.in_goal @x in set ($x := $expr) in *; let x := hyp x in @@ -1012,18 +1026,28 @@ Ltac2 simplify_let (h : ident) : unit := lazy head beta in h end. +Ltac2 Notation "simplify_let" h(ident) := simplify_let0 h. + +Goal forall x y : nat, (let a := x + 2 in let b := y + 1 in a = b) -> True. + intros x y h. + Fail simplify_let x. + simplify_let h. +Abort. + (** The advantage of Ltac2 is that the FFI interface enables us to write scripts we could not have in Ltac1. For instance, we can now use the [Constr.Unsafe] API to write the [simplify_let] tactic by directly accessing the structure of the term, and performing the substitution by hand rather than relying on - high-level tactics like [lazy head beta]. + high-level tactics like [lazy head beta]. This can be seend by + printing the resulting body. *) Import Unsafe. -Ltac2 simplify_let_bis (h : ident) : unit := +Ltac2 simplify_let_bis0 (h : ident) : unit := let type_h := type (hyp h) in match kind type_h with | LetIn _ expr body => + printf "the body is: %t" body; let x := Fresh.in_goal @x in set ($x := $expr) in *; let x := hyp x in @@ -1031,3 +1055,11 @@ Ltac2 simplify_let_bis (h : ident) : unit := change ($new_body) in h | _ => fail end. + +Ltac2 Notation "simplify_let_bis" h(ident) := simplify_let_bis0 h. + +Goal forall x y : nat, (let a := x + 2 in let b := y + 1 in a = b) -> True. + intros x y h. + Fail simplify_let_bis x. + simplify_let_bis h. +Abort. From 3b7dbab2fe1407dc27a5557f5e52a1fc7a132595 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Sun, 3 May 2026 17:23:08 +0200 Subject: [PATCH 15/17] fix notation discussion --- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index dcec9cb..6bc1ee0 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -310,9 +310,14 @@ Proof. do 1 (exact HP). Qed. -(** However, a real issue with the Ltac2 proof mode is that some tactics +(** However, a real issue with the Ltac2 proof mode is that some functions are imported but are currently missing notations for them in Ltac2 standard library. - For instance, in Rocq 9.0, a notation is missing for the tactic [clearbody]. + For instance, in Rocq 9.0, tactic [clearbody] is exposed as the Ltac2 function + + [[Ltac2 @ external clearbody : ident list -> unit := "rocq-runtime.plugins.ltac2" "tac_clearbody"]] + + but is lacking a notation enabling us to directly write [clearbody x y] to + clear the body of the local definitions [x] and [y]. This problem will be solved over time with contributions to the standard library. *) From 11f5dee771ef8b875c25b8ecc353cd7dde53a876 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux Date: Mon, 4 May 2026 22:59:41 +0200 Subject: [PATCH 16/17] fixs --- .../ltac2/tutorial_backtracking.v | 2 +- .../ltac2/tutorial_ltac2_for_ltac1_users.v | 17 ++++++++++------- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/metaprogramming/ltac2/tutorial_backtracking.v b/src/metaprogramming/ltac2/tutorial_backtracking.v index 3c9bcc1..135b232 100644 --- a/src/metaprogramming/ltac2/tutorial_backtracking.v +++ b/src/metaprogramming/ltac2/tutorial_backtracking.v @@ -380,7 +380,7 @@ Abort. which given a thunk [h] returns either: 1. an error [Err e] where [e] is an exception 2. or a pair [Res (x,k)] where [x : 'a] is the first succes of [h], and - [k : exn -> 'a] is the backtracking continuation to try in case of subsequent failure. + [k : exn -> 'a] is the backtracking continuation to try in case of subsequent failure. In the stream model, this basically consists in matching the stream checking if it is empty, and if not return the head with the rest of the stream. diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index 6bc1ee0..c10708f 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -311,14 +311,16 @@ Proof. Qed. (** However, a real issue with the Ltac2 proof mode is that some functions - are imported but are currently missing notations for them in Ltac2 standard library. - For instance, in Rocq 9.0, tactic [clearbody] is exposed as the Ltac2 function + are imported but are currently missing notations to handle the quoting + from Rocq to Ltac2. + For instance, in Rocq 9.0, the function [clearbody] is exposed in + the standard library as: [[Ltac2 @ external clearbody : ident list -> unit := "rocq-runtime.plugins.ltac2" "tac_clearbody"]] - but is lacking a notation enabling us to directly write [clearbody x y] to - clear the body of the local definitions [x] and [y]. - This problem will be solved over time with contributions to the standard library. + However, is lacking a notation enabling us to directly write [clearbody x y] + to clear the body of the local definitions [x] and [y]. + You would have to write the quoting yourself [clearbody [@x; @y]]. *) Goal forall A, A -> A * A. @@ -326,7 +328,7 @@ Proof. intros. pose (x := 2). Fail clearbody x. Abort. -(** In the meantime, there are two workarounds. +(** In the meantime, there are two main workarounds not to write the quoting yourself. The first option is to define the missing notation locally. In this case, one should also consider contributing it upstream to the standard library. @@ -878,7 +880,7 @@ Abort. since different decisions can be performed depending on the exception raised. - [Control.case : (unit -> 'a) -> ('a * (exn -> 'a)) result] -- inspects - whether a tactic has at least one success without consuming it. + whether a tactic has at least one success. *** 4.5 Notations @@ -1008,6 +1010,7 @@ Abort. - [Constr.type] is now a proper function rather than an ad-hoc construction - use the [Fresh] module to create fresh variables - use [$] to unquote variables back to Rocq's world + - use [@] to create Rocq identifier In the end, this gives us a script that is similar but with a few decorations and clearer semantics, which can be written with or without From fcf19630fa97fac31bb34169fe430aac7b8c5c80 Mon Sep 17 00:00:00 2001 From: Thomas Lamiaux <85848641+thomas-lamiaux@users.noreply.github.com> Date: Sun, 17 May 2026 16:38:36 +0200 Subject: [PATCH 17/17] Update src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v --- src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v index c10708f..a6393d9 100644 --- a/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v +++ b/src/metaprogramming/ltac2/tutorial_ltac2_for_ltac1_users.v @@ -256,7 +256,9 @@ Proof. Qed. (** In Ltac2, this is now written with the syntax [tac1 > [tac21 | tac22]] in order - to avoid syntax conflict with ???. Moreover, [tac1; tac2; [tac31 | tac32]] + to avoid confusion between chaining tactics and dispatching. + The latter is asymetric and does not compose opposite to [;]. + Moreover, [tac1; tac2; [tac31 | tac32]] is now parsed as [tac1; (tac2; [tac31 | tac32])] as Ltac2 no longer automatically delays tactic execution.