Theoretical symmetry between specialize and generalize dependent

Miscellaneous
1

Hi all,

I am currently following “Software Foundations” to learn Rocq, and I came across “specialize” and “generalize dependent.” One seems to remove a quantifier and the other seems to add one. I found this interesting because they act like inverses of each other, and I wonder if there is a deeper meaning behind these tactics.

2

These tactics both correspond to the same rule of “forall instantiation”: if we know forall x, P x then can deduce P t, for whatever concrete term t.

  • specialize uses that rule on a hypothesis: you have a hypothesis H : forall x, P x, then specialize (H t) gives you H : P t
  • generalize dependent uses that rule on the goal: you start with the goal P t, then generalize dependent t reasons backwards to generalize it to forall x, P x.

Although they correspond to the same logical rule, they differ in whether they act on the hypotheses or the goal, and that determines whether the tactic “removes” or “inserts” a quantifier.

This is but one example of duality: two worlds that are kind of the same but also kind of the opposite. It is a deep topic that appears in many places in mathematics.

1 Like
3

Probably worth to mention that this duality is exactly the insight behind Gentzen’s Natural Deduction, which is a calculus so commonly used in today’s logic.

2 Likes