# Theoretical symmetry between specialize and generalize dependent

**URL:** <https://discourse.rocq-prover.org/t/theoretical-symmetry-between-specialize-and-generalize-dependent/3006>\
**Category:** Miscellaneous\
**Created:** [March 31, 2026, 2:26pm UTC](https://discourse.rocq-prover.org/t/theoretical-symmetry-between-specialize-and-generalize-dependent/3006 "2026-03-31T14:26:43Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![qvd808](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/qvd808/32/1250_2.png) [@qvd808](https://discourse.rocq-prover.org/u/qvd808)\
**Post date:** [March 31, 2026, 2:26pm UTC](https://discourse.rocq-prover.org/t/theoretical-symmetry-between-specialize-and-generalize-dependent/3006/1 "2026-03-31T14:26:43Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [April 1, 2026, 1:07pm UTC](https://discourse.rocq-prover.org/t/theoretical-symmetry-between-specialize-and-generalize-dependent/3006/2 "2026-04-01T13:07:05Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![pedroabreu](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/pedroabreu/32/203_2.png) [@pedroabreu](https://discourse.rocq-prover.org/u/pedroabreu)\
**Post date:** [April 1, 2026, 6:09pm UTC](https://discourse.rocq-prover.org/t/theoretical-symmetry-between-specialize-and-generalize-dependent/3006/3 "2026-04-01T18:09:31Z")

</div>

> [@Lyxia](#):
>
> 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.

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.