Why are tactics like `simpl` valid?

Using Rocq
1

Absolute beginner to Coq and proof assistants here, and this silly question has been bothering me for some time now.

I was wondering why the simpl tactic, for example (reduction-based tactics, in general), is “valid” - in the same sense in which induction is valid because of the structural induction that holds on inductively defined types.

So, why exactly is it okay to replace a term in a goal with another term that it is convertible to? I understand that such terms are called definitionally equal to one another, but why does this imply that they can be interchanged in any scenario?

For example, 2 + 2 and 4 are convertible terms, and I understand why using a reduction tactic on 2 + 2 for a goal that involves equality is valid – because if we can prove that an expression with 4 is equal to another expression, then so is the initial expression with 2 + 2 instead of 4 - because of the convertibility of these expressions.

But, what justifies replacing 2 + 2 by 4 in a goal, in general (not just involving equality)? One sense in which 2 + 2 is not “equivalent” to 4 is that one is a function application expression and another is simply a value of type nat, but I don’t think such syntactic differences are expressible in Coq. Nonetheless, how do I convince myself that they are indeed equivalent in all scenarios?


My apologies if I haven’t framed the question well enough. My thoughts are all over the place. Any help would be appreciated, thank you!

PS: I posted this question on Proof Assistants StackExchange too, but I don’t understand the responses that I’ve received there so far.

2

It depends what you mean by “why”. I will let others try to give you some kind of philosophical intuition. But I can give you a pragmatical reason.

A formal system is described by a set of inference rules. As long as this set is consistent (that is, one cannot infer a contradiction), then everything is okay. Whether the rules make sense or not is of little importance. As long as you do not break the consistency of the system, you can add whichever inference rule you want. (Obviously, if the rules somehow make sense to the human mind, it might be easier to ensure their consistency, but that is not a strong prerequisite.)

In the case of Coq (which is believed to be consistent), one of the rules says that, if a term is of a given type A, it is also of any type B convertible to A (under a few wellformedness assumptions). Since P (2 + 2) and P 4 are convertible types for some specific definitions of +, 2, and 4 (whatever the definition of P), this validates the behavior of simpl.

1 Like
3

[This is only a first approximation, and I hope I won’t make any major mistakes.]

Look for Voevodsky’s lectures on YouTube about formalization of mathematics up to the reasons for Univalence: not per chance equality/equivalence plays a central role in that discourse. But there is also another side to it, which is recognizing the various components that make up a “formalized theory”, of mathematics or otherwise.

Roughly speaking, and only to the extent that I have understood and remember it (and please feel free to nitpick):

There are 3 components: 1) the mathematics, i.e. what we talk about, or would write “on paper”, and (here) the actual target of investigation; 2) its formalization (aka the encoding, aka the implementation): a piece of “functional” code that, under compilation/evaluation, expresses, by its recognizable behaviour, the mathematical notions we have in mind/on paper; 3) a (formal) semantics attached to the formal objects that… allows us to reason about the formal objects regardless of the mathematics (up to “model theory”, I suppose).

That said, when you are asking why/how a tactic is “valid”, you are in fact (in hindsight) not asking a sensible question at at least two levels: immediately because in Rocq tactics are not first-class, and whatever term the tactics produce, it’s still actually a Gallina term: it’s Qed/Defined where the term gets type-checked; but also keep in mind that the program you are actually writing in Gallina (the dependently-typed functional core language of Rocq), is “only” the implementation component of a formalization effort: as in e.g. with lambda calculus “computation” is a “side-effect” of beta-reduction.

I was wondering why the simpl tactic, for example (reduction-based tactics, in general), is “valid” - in the same sense in which induction is valid because of the structural induction that holds on inductively defined types.

So, taking induction as an example: we read it “induction” because we are thinking mathematically, but behind the scenes those are simply eliminators for “inductive” types…

4

So essentially terms that are convertible are defined to be equal, as per the inference rules? And do properties of equality such as symmetry, transitivity and reflexivity follow from this?

Can terms that are not convertible to one another be equal?

5

I found a few videos of Voevodsky but most of that is too high-level for me – I just got done with 2^{\mathrm{nd}} year of a bachelor’s degree. Are there any specific lectures that you recommend watching?


By valid, I mean to say something like

A tactic is valid if it takes a goal state S_1 to a goal state S_2 where proving S_1 is, “equivalent” to proving S_2, vaguely speaking.

For example, a tactic that would transform a goal


============================
2 = 3

into


============================
3 = 3

would be invalid, in this sense.

So, from what I understand now, what simpl and other reduction-based tactics do is “allowed” because the inference rules of CIC. Is that correct?

6

No. The inference rules do not know about equality. In Coq, equality is not a builtin symbol but a user definition (which is provided by the standard library):

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : eq A x x.

So, assuming a type A, you get a relation eq : A -> A -> Prop, whose only generator is the constructor eq_refl x (for any x) which has type eq x x.

Now, since one of the inference rules says that two convertible types have the same inhabitants, it implies that, if u and v are convertible and if eq x u is provable, then so is eq x v. In particular, if x and y are convertible, then eq_refl x is a proof of eq x y.

The relation eq is indeed reflexive (by virtue of the type of its constructor eq_refl). As for symmetry and transitivity, this is also the case, but it needs to be proved (which the standard library has already done).

In the empty context (that is, no assumption of any kind), two equal terms are necessarily convertible. This is a nontrivial fact. Here is an intuition: In the empty context, the only inhabitant of eq x y is eq_refl x, which has type eq x x. So, the types eq x y and eq x x have to be convertible, which in turn means that x and y are convertible because eq is a free symbol.

1 Like
7

Maybe take it as a long term learning goal. Also, after re-watching some of those lectures, I have realized the picture I have painted above is not exactly the same as Voevodsky’s: but keep in mind mathematics (and mathematical logic) is a little bit of a special case, since “formal semantics” is itself a piece of mathematics. Anyway, never mind, let’s simplify slightly:

There are many ways to approach the distinction I am trying to point out. Maybe think about a formula (a piece of syntax and machinery) vs its interpretation (the associated meaning or semantics): when you code in Rocq you are manipulating syntax (formal objects); the interpretation (i.e. how we “read” those formal expressions), up to e.g. mathematical-logical notions such as “validity”, is only in the eye of the beholder, rather made manifest by the naming and organization of things. (We could formalize that interpretation into a formal meta-theory, but in turn the interpretation of the meta-theory, a meta-meta-theory, would still be informal: and so on, i.e. an informal ultimate element remains irreducible).

Or, think about the distinction between a numeral and a number. Or, more to the point, think about the fact that Rocq’s core language has “typing rules”, not “inference rules”…

I am sorry I cannot be more substantial than that, but it’s a very broad topic. Meanwhile, here are two lectures that I find relatively accessible:

Foundations of Mathematics and Homotopy Theory - Vladimir Voevodsky
https://youtu.be/84vW1hQLFu8?si=h-kkzr67OpMb89tQ

How I became seduced by univalent foundations - Emily Riehl
https://youtu.be/XIYoI5j5Flo?si=lDF__pybzYDIFuKP

The other way round: somebody wrote the tactic with some logical notion in mind, plus all the knowledge as to how that notion “maps” (read, Curry-Howard) into Rocq’s formal constructions and rules together with how it plays with the pre-existing formal definitions and theorems and even libraries, which already bear some relevant/intended interpretation. But, eventually, whether the tactic is or is not “valid” remains an informal issue: concretely, only the terms the tactic constructs, when and where those terms get constructed, get “validated”, and only in the concrete sense that they get type-checked.

1 Like
8

I’d like to leave a bit of a summary of what I’ve gathered from the discussion, and I hope you can correct me, if that’s alright.

So, Rocq doesn’t have a “built-in” notion of equality, and the = that we use in proofs is a user-defined inductive proposition eq, with the constructor eq_refl serving as proof for the same. And the way eq_refl is defined says something like “for any x, eq_refl x serves as proof for x = x”.

This, paired with the Conv rule, which says that a term of type P also has the type Q if P and Q are convertible, make eq hold for two definitionally equal terms.

And in an empty context, two terms being equal is equivalent to them being convertible to each other. What about in a non-empty context? Can terms that are not convertible to each other be equal? And if so, is it inaccurate to think of the eq equality in terms of definitional equality?

9

Sure. First of all, terms can be equal by assumption. For instance, if you are trying to prove the symmetry of the equality (i.e., forall u v, u = v -> v = u), you will sooner or later end up in a proof context where u is provably equal to v by hypothesis, but u and v are not convertible since they are fresh variables.

Even worse, suppose you are doing a proof by absurd. At some point, you might end up with the equality 0 = 1 in your proof context, yet 0 and 1 are certainly not convertible, and they do not even contain variables that you could substitute to make them convertible (contrarily to u and v above).

So, “definitionally equal” is a reasonable intuition for eq, but with two caveats: 1. in the empty context, and 2. modulo convertibility.

1 Like
10

I’ve heard this phrase “modulo convertibility” a few times now, but I’m not sure I understand what it’s supposed to mean. From what I understand (see here), modulo convertibility means something like “as far as convertibility goes”. But, definitional equality and convertibility are the same thing, no? I must be misunderstanding something because I don’t understand how modulo convertibility is a caveat in thinking of eq as definitional equality.

11

“Definitional equality” usually denotes that two terms are syntactically equal after unfolding all the definitions/abbreviations and renaming binders they contain. But then some people might consider that this equivalence relation also involves some additional properties:

  1. closing upon other equalities in the context,
  2. performing primitive recursion,
  3. performing full convertibility (which implies 2 in the case of Coq).

That is why I preferred to be explicit about which of these properties are involved, as the meaning of “definitional equality” depends on the community.

1 Like