As I understand, Gallina is the “programming language” embedded in Coq (that one can write proofs later which are checked using the formal system CIC Calculus of inductive constructions):
The first half of this chapter introduces the most essential elements of Coq’s native functional programming language, called Gallina . The second half introduces some basic tactics that can be used to prove properties of Gallina programs.
LTac seems to be a functional programming language for manipulating goals (what in my head I call coq terms) using tactics (or custom tactics).
My questions are (numbered to make it easier to address):
why do we need two different languages inside of Coq and not have everything be in a single unified language?
Is the main difference between Gallina vs LTac? Is the main difference that one is a language to express native programs in Coq while the second to create custom tactics?
is a proof script proving something about a coq term or a Gallina program in Gallina or LTac? (what is the language of proof scripts essentially)
Is this sort of a good approximation of Coq? Coq = Gallina (for programming) + Ltac (for tactics) + CIC (for formal system e.g. type system, judgments, etc)
Are Coq terms in Gallina or something else?
Context: I am transitioning from Isabelle to Coq and it seems everything in Isabelle is “one single language” (which makes sense if one reads its history coming from LCF Logic for Computable Functions - Wikipedia ) and I am trying to wrap my head around what exactly “is Coq”. Perhaps I shouldn’t be comparing it to what I am already used to but it seemed natural to try to compare them. In particular, perhaps this was true in Isabelle too, but I still can’t form a stable model in my head of what an evolving grammar that is not fixed means.
Gallina is an implementation of the (Predicative) Calculus of Cumulative Inductive Constructions, a much more expressive extension of CoC.
By the Curry-Howard correspondence, it can be seen at the same time as a pure functional programming language and a rich proof system.
Everything you can prove in Coq amounts under the hood to the construction of a Gallina term of the adequate type (the statement of your theorem). However writing out full terms can be long and repetitive: consider for instance the problem of writing decision procedures for equality on large inductives (such as the ones you get for the syntax of a real world language, e.g. javascript or C with sometimes hundreds of constructors). In order to simplify this task, one can use a meta-program that takes the description of the inductive as input and tries to generate a decision procedure for equality on this inductive (e.g. deriving in Haskell).
A proof script is actually the same: it is a meta-program generating a term of the adequate type when you run it. Ltac is one of the meta-programming language available in Coq to manipulate, generate Gallina terms and interact with the Coq system (unification engine, backtracking, …) but it is not the only one (you can use Ltac2, Mtac, Elpi, MetaCoq’s reflection system…).
So to answer more precisely your questions:
In theory it would be possible to have a single unified language, that’s what is done in Agda (though the meta-programming part is quite bare bone) or in Lean (at least at some point it was through a monad to access the goal, unification engine, and so on). It’s not how it was set up in Coq and there are some advantages to keep the meta-language distinct from the object language (Gallina here).
Yes, Gallina is the term language and Ltac the meta-programming language.
A proof script is mostly written in some meta-programming language such as Ltac and generates a Gallina term when run. Of course a proof script can also contain pieces of Gallina terms embedded (in exact or refine tactics for instance).
Some comment/questions (numbering to help referencing).
By the Curry-Howard correspondence, it can be seen at the same time as a pure functional programming language and a rich proof system.
Ah I think this makes sense. If we have a proof e.g. A->B then it makes sense that whenever we have a proof language we actually have a functional programming language under the hood (and visa versa).
To make it concrete I will ask with an example. When I define functions and types in Coq e.g.
Inductive nat : Set :=
| O
| S : nat -> nat.
Fixpoint add (a: nat) (b: nat) : nat :=
match a with
| O => b
| S x => S (add x b)
end.
is my custom type nat a Gallina term or is the actual value O of my type nat a Gallina code or is my code Inductive ... a Gallina term?
Is my addalso a Gallina term or is my code for it Fixpoint ... a Gallina term?
How are Gallina terms related to the hidden proof term sent to the kernel being built underneath this?
One more example - to help differentiate functional programming (in Gallina?) from proofs scripts in my head - is the following proof script (the actual text) in Gallina syntax or is this technically in Ltac?
Lemma zero_plus_n_equals_n:
forall n, (add O n) = n.
Proof.
intros.
simpl.
reflexivity.
Qed.
Here’s how I’ve usually heard these languages differentiated.
nat, O, add, match a with O => b | S x => S (add x b), and the definition/body of add fix add a b := match a with O => b | S x => S (add x b) end are all Gallina terms.
Inductive ..., Fixpoint ..., Check ..., About ..., Require Import ... are part of a language called the Vernacular (that’s where the .v extension for Coq files comes from). These are vernacular commands, or sentences (the things you end with a period).
intros, simpl, reflexivity, as well as more complicated composite tactics such as induction n; [ intros H; intros H1 H2 ]; try tauto. are all Ltac.
So looking at your example:
Lemma zero_plus_n_equals_n:
forall n, (add O n) = n.
Proof.
intros.
simpl.
reflexivity.
Qed.
I see a Lemma ... vernacular command that includes the Gallina type forall n, (add O n) = n and defines the identifier zero_plus_n_equals_n (which can now be used in Gallina terms).
Next, we have the vernacular command Proof., followed by three sentences of Ltac: intros. simpl. reflexivity.
Finally, we have the vernacular command Qed. which completes the proof/definition of zero_plus_n_equals_n.
If you then run the vernacular command Print zero_plus_n_equals_n. (or use an IDE to achieve the same thing), you get the output
zero_plus_n_equals_n =
fun n : nat => eq_refl
: forall n : nat, add 0 n = n
Here fun n : nat => eq_refl is the Gallina term constructed by the Ltac proof, and forall n : nat, add 0 n = n is its type (again in Gallina), just as it was specified in the Lemma command.
Gallina terms are very close to what gets sent to the kernel. Depending on your definitions there may be a bit of syntactic sugar separating Gallina terms from kernel terms, but they are mostly the same.
Ltac proofs work by constructing Gallina terms which are then sent to the kernel.
For what is worth, there has always been some debate and confusion on what “Vernacular” and “Gallina” exactly covered, even among developers. That’s why, lately, we have decided to remove the usage of the word “vernacular” from the user-facing documentation (preferring the word “command”): in the (recently updated for 8.13) reference manual (Introduction and Contents — Coq 8.13.0 documentation) you shouldn’t find this word anymore. “Gallina” isn’t used much either in this documentation, but you can indeed consider it as Coq’s implementation of the (much extended) Calculus of Inductive Constructions (CIC). Said otherwise, Gallina is the logical part and the internal programming language of Coq (as opposed to Ltac which, as was explained above, is a meta-programming language). One only proves Gallina programs correct, not Ltac programs, and only Gallina is extracted to OCaml, not anything else.
One thing that may be helpful to visualize how Ltac is building Gallina terms is to actually print a proof and see how that simply becomes a Gallina function under the hood.
Lemma n_plus_zero_equals_n:
forall (n : nat) , (n + 0) = n.
Proof.
intros.
destruct n; simpl; auto.
Defined. (* <--- Don't forget to make it Defined instead of Qed! Otherwise Coq won't print your program *)
Print n_plus_zero_equals_n.
Should print
n_plus_zero_equals_n =
fun n : nat =>
match n as n0 return (n0 + 0 = n0) with
| 0 => eq_refl
| S n0 =>
f_equal_nat nat S (n0 + 0) n0 (eq_sym (plus_n_O n0))
end
: forall n : nat, n + 0 = n
Arguments n_plus_zero_equals_n _%nat_scope