lthms' avatar, a hand drawing looking person, wearing a headset, close to a window on a raining night
Thomas Letan
lthms · he/him

Did you come across something which caught your attention? Don’t hesitate to shoot me an email in my public inbox.

A Series on Ltac

Ltac is the “tactic language” of Coq. It is commonly advertised as the common approach to write proofs, which tends to bias how it is introduced to new Coq usersI know I was introduced to Coq in a similar way in my Master courses. . In this series, we present Ltac as the metaprogramming tool it is, since fundamentally it is an imperative language which allows for constructing Coq terms interactively and incrementally.

Ltac is an Imperative Metaprogramming Language

Ltac generates terms, therefore it is a metaprogramming language. It does it incrementally, by using primitives to modifying an implicit state, therefore it is an imperative language. Henceforth, it is an imperative metaprogramming language.

Pattern Matching on Types and Contexts

Ltac allows for pattern matching on types and contexts. In this article, we give a short introduction on this feature of key importance. Ltac programs (“proof scripts”) generate terms, and the shape of said terms can be very different regarding the initial context. For instance, induction x will refine the current goal using an inductive principle dedicated to the type of x.

Mixing Ltac and Gallina for Fun and Profit

One of the most misleading introduction to Coq is to say that “Gallina is for programs, while tactics are for proofs.” Gallina is the preferred way to construct programs, and tactics are the preferred way to construct proofs. The key word here is “preferred.” Coq actually allows for mixing Ltac and Gallina together.