# Why does the conversion rule for CIC apply only to types instead of all terms?

**URL:** <https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790>\
**Category:** Miscellaneous\
**Created:** [August 7, 2025, 3:06am UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790 "2025-08-07T03:06:59Z")\
**Posts on this page:** 12\
**Page:** 1

<div class="post-metadata">

**Author:** ![sskeirik](https://avatars.discourse-cdn.com/v4/letter/s/e56c9b/32.png) [@sskeirik](https://discourse.rocq-prover.org/u/sskeirik)\
**Post date:** [August 7, 2025, 3:06am UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/1 "2025-08-07T03:06:59Z")

</div>

I’m currently learning Rocq and working my way through the typing rules.

One thing that stuck out to me while I was reading the rules is:

- the convertibility rules are defined for terms in general;
- however, the conversion typing ( **Conv** ) rule only allows types (but not terms in general) to be transformed.

Is the decision to restrict conversion to types instead of terms:

- documented in any papers/resources on the history of Rocq?
- due to any consistency issues in logic?
- merely a stylistic choice that aids some way in the development of Rocq itself, in Rocq usage, or Rocq education?
- due to some other reason?

Context: while I’ve had formal training in logic/theorem proving, it was in a non-type-theoretic setting, so it seems there is some bits of intuition/understanding/folk-lore which I haven’t picked up yet — this feels like one of those pieces.

---

<div class="post-metadata">

**Author:** ![thomas-lamiaux](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/thomas-lamiaux/32/982_2.png) [@thomas-lamiaux](https://discourse.rocq-prover.org/u/thomas-lamiaux)\
**Post date:** [August 7, 2025, 4:14am UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/2 "2025-08-07T04:14:49Z")

</div>

Conversion applies to terms too, but what would you reduce term in type checking ?  
Reduction of terms is for computation

PS: don’t hesitate to check the zulip  
PS2: a reference [https://dl.acm.org/doi/10.1145/3706056](https://dl.acm.org/doi/10.1145/3706056)

---

<div class="post-metadata">

**Author:** ![jp-diegidio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jp-diegidio/32/819_2.png) [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Post date:** [August 7, 2025, 7:08am UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/3 "2025-08-07T07:08:39Z")

</div>

(In Rocq,) all types are terms, but not all terms are types.

In particular, the conversion rules for terms in general are a thing, that `Conv` rule instead is about changing (“converting”) the type of a term given subtyping of the type: that’s no restriction, it’s just a piece of the puzzle that relates terms to types…

---

<div class="post-metadata">

**Author:** ![sskeirik](https://avatars.discourse-cdn.com/v4/letter/s/e56c9b/32.png) [@sskeirik](https://discourse.rocq-prover.org/u/sskeirik)\
**Post date:** [August 7, 2025, 7:40pm UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/4 "2025-08-07T19:40:42Z")

</div>

## Addressing Feedback

Thanks for the replies all! Let me address them first.

> Reduction of terms is for computation

This is a good intuition! Thanks for that. At the same time, that doesn’t necessarily imply (at least to me) that general term reduction would be _unhelpful_ during type checking.

> PS: don’t hesitate to check the zulip

I wasn’t aware of the Rocq Zulip — is that a better place to ask questions than here?

> PS2: a reference [https://dl.acm.org/doi/10.1145/3706056](https://dl.acm.org/doi/10.1145/3706056)

Thanks for this reference — it doesn’t seem to directly answer this question, but it delves alot into the meta-theory of Rocq which helps alot with understanding!

> \> (In Rocq,) all types are terms, but not all terms are types.

Yep, this is important context needed to understand the overall question. Thanks for clarifying that.

> that `Conv` rule instead is about changing (“converting”) the type of a term given subtyping of the type: that’s no restriction, it’s just a piece of the puzzle that relates terms to types…

It’s not obvious to me why your statement above is true — to my untrained eyes, the way ( **Conv** ) is written _seems_ restricting somehow, but that could be due to my own ignorance.

## Follow-up Thoughts

After thinking about my question, I realized there are some good reasons why term reduction would be unhelpful for Rocq, a type-checking based theorem prover:

1. Incorporating general term reduction into the type-checking process requires type-checking to preserve decidability

2. Arbitrary term reduction would break any syntax directedness for the rules of the proof system

At this point, I feel pretty convinced from the the two points I mentioned above that general term reduction in a dependently typed setting would be a bad idea.

So, two last questions:

1. Do you guys agree with my points above? If not, I’d love to know why!
2. Are there any other points aside from the above two that would demonstrate that general term reduction would be unhelpful for a type-checking-based theorem prover like Rocq?

---

<div class="post-metadata">

**Author:** ![jp-diegidio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jp-diegidio/32/819_2.png) [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Post date:** [August 7, 2025, 9:25pm UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/5 "2025-08-07T21:25:47Z")

</div>

> Do you guys agree with my points above? If not, I’d love to know why!

No, Rocq is not a “type-checking-based theorem prover”, it is more generally a full-fledged dependently-typed _functional language_. And few of those [term conversion rules](https://rocq-prover.org/doc/V9.0.0/refman/language/core/conversion.html), i.e. alpha-conversion and beta-reduction, you can indeed already find in plain lambda-calculus.

The _typing_, and especially the _dependent typing_, rather adds expressivity and complexity, up to proving theorems: but then again, that does not reduce to any system of “just logic”.

> to my untrained eyes, the way ( **Conv** ) is written seems restricting somehow

As for the typing rules, [the `Conv` rule](https://rocq-prover.org/doc/V9.0.0/refman/language/cic.html#subtyping-rules) says, in short, that if `t : T`, then also `t : U` for any supertype `U` of `T`. It’s an enlargement/lifting (maybe more precisely a kind of _cumulativity_, but I am not 100% sure that label is appropriate there), anyway the very opposite of a “restriction”.

> So, firstly, recall that β-reduction on untyped terms is non-terminating, e.g., consider self-applying the un-typable ω combinator `λx.xx`.

Except that indeed you cannot do that in (plain) Rocq/CIC…

The devil is in the detail. ; )

---

<div class="post-metadata">

**Author:** ![sskeirik](https://avatars.discourse-cdn.com/v4/letter/s/e56c9b/32.png) [@sskeirik](https://discourse.rocq-prover.org/u/sskeirik)\
**Post date:** [August 7, 2025, 11:44pm UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/6 "2025-08-07T23:44:55Z")

</div>

> No, Rocq is not a “type-checking-based theorem prover”, it is more generally a full-fledged dependently-typed _functional language_. And few of those [term conversion rules](https://rocq-prover.org/doc/V9.0.0/refman/language/core/conversion.html), i.e. alpha-conversion and beta-reduction, you can indeed already find in plain lambda-calculus.
> 
> The _typing_, and especially the _dependent typing_, rather adds expressivity and complexity, up to proving theorems: but then again, that does not reduce to any system of “just logic”.

Thanks for that clarification. I agree!

> As for the typing rules, [the `Conv` rule](https://rocq-prover.org/doc/V9.0.0/refman/language/cic.html#subtyping-rules) says, in short, that if `t : T`, then also `t : U` for any supertype `U` of `T`. It’s an enlargement/lifting (maybe more precisely a kind of _cumulativity_, but I am not 100% sure that label is appropriate there), anyway the very opposite of a “restriction”.

Hmm… perhaps I did not express myself clearly enough. My original point was that the **Conv** rule with premises:

`E;Γ |- U : s E;Γ |- t : T E;Γ |- T <= U`

And conclusion:

`E;Γ |- t : U`

Restricts the application of any reduction/convertibility rules including:

- β
- δ
- ζ
- and so on…

embedded in the `_ <= _` relation to _types_, when these embedded rules also apply to terms. So we could imagine an alternate form of the conversion rule **Conv2** that has the premises:

`E;Γ |- U : s E;Γ |- t : T E;Γ |- t |> t' E;Γ |- T <= U`

And the conclusion:

`E;Γ |- t' : U`

where `t |> t’` is the transitive closure of the union of all of the reduction/convertibility relations (β, δ, ζ, …).

The restriction to which I was referring was the fact that the reduction/convertibility relation is not applied freely in **Conv** but limited to be used on types.

> Except that indeed you cannot do that in (plain) Rocq/CIC…

I agree!

My point in that paragraph was that the **untyped** lambda calculus is non-terminating — I was not talking about CIC or any other **typed** lambda calculus-based system.

I made that point to discuss the need for well-typedness in order to preserve termination, decidability of term normalization, and decidability of type checking (in a dependently typed system).

Hopefully that’s more clear. Thanks.

---

<div class="post-metadata">

**Author:** ![jp-diegidio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jp-diegidio/32/819_2.png) [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Post date:** [August 8, 2025, 9:03am UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/7 "2025-08-08T09:03:58Z")

</div>

> My original point was that the **Conv** rule [… r]estricts the application of any reduction/convertibility rules

I don’t see it: that `Conv` is a bit a misnomer, but the two things, term conversion rules and the typing rules, are rather _orthogonal_.

> `t |> t’` is the transitive closure of the union of all of the reduction/convertibility relations

That I find literally meaningless (as part of a typing rule), anyway I think I get the intent: let `t'` be any term that `t` converts/reduces to, then `t'` (too!) has type `T'` for any supertype `T'` of `T`: but, you can get the same by 1) reducing the term, which won’t change its type, then 2) lifting the type; or vice versa, i.e. lifting the type then reducing the term. IOW, as said, it seems to me you are rather mixing orthogonal concepts there.

---

<div class="post-metadata">

**Author:** ![thomas-lamiaux](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/thomas-lamiaux/32/982_2.png) [@thomas-lamiaux](https://discourse.rocq-prover.org/u/thomas-lamiaux)\
**Post date:** [August 12, 2025, 1:58pm UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/8 "2025-08-12T13:58:46Z")

</div>

I understand my first answer was unprecise. You do not have a rule `a : A` and `a conv v` =\> `v : A` because this is a property of typing: subject reduction. You do have computation of term in types, for instance `vec A (1 + 3) conv vec A 4`. This is vital as soon as you start having real type dependency.

> The restriction to which I was referring was the fact that the reduction/convertibility relation is not applied freely in **Conv** but limited to be used on types.

This is wrong. Reduction is applied generically in typing. In Rocq conversion is untyped, so it is the same algorithm for types and terms. If it is only applied to types, it is because they are no reason to apply it to anything else in the definition of typing. This will still reduce any term in types, using whatever rules it needs, like in the vec example above.

> term conversion rules and the typing rules, are rather _orthogonal_.

This is rather false. Decidability of conversion is fundamental for decidability of type checking, and to verify most properties we care about typing like subject reduction. Moreover, if you start having a typed conversion, then typing and conversion become mutually inductive which makes the whole thing complicated, and having typed conversion to get eta-conversion is a subject of research.

However, @sskeirik you are right to think that applying conversion to well-formed types is important.  
From what I rememeber, it is cruciall to prove properties like validity, i.e. `t : T => exists s, T : Sort s`. I think this can be seen in how conversion is split and dispatch in the bidirectional algorithm that is used in practice to type check terms.

---

<div class="post-metadata">

**Author:** ![jp-diegidio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jp-diegidio/32/819_2.png) [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Post date:** [August 12, 2025, 4:08pm UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/9 "2025-08-12T16:08:06Z")

</div>

> [@thomas-lamiaux](#):
>
> > term conversion rules and the typing rules, are rather _orthogonal_.
> 
> This is rather false. Decidability of conversion is fundamental for decidability of type checking, and to verify most properties we care about typing like subject reduction. Moreover, if you start having a typed conversion, then typing and conversion become mutually inductive which makes the whole thing complicated, and having typed conversion to get eta-conversion is a subject of research.

But “orthogonal” entails “independent”, which is the opposite of how you are reading it. OTOH, your reference to “type checking” is rather all encompassing and just beside the point in the context of the original question and the explanations I have been giving.

(P.S: I didn’t know flagging your post would hide it and I cannot undo it: I am only complaining about a behaviour that is as unreasonable and destructive as it’s becoming a habit. As a minimum, you should take a little bit more time reading things before you jump your guns: and do stick to Zulip please, if that’s all eventually you have to say.)

---

<div class="post-metadata">

**Author:** ![sskeirik](https://avatars.discourse-cdn.com/v4/letter/s/e56c9b/32.png) [@sskeirik](https://discourse.rocq-prover.org/u/sskeirik)\
**Post date:** [August 14, 2025, 3:34am UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/10 "2025-08-14T03:34:41Z")

</div>

Thanks for the pointers @jp-diegidio @thomas-lamiaux.

After the last round of posts, something finally clicked for me.

I realized that my mental model of Rocq was inaccurate and that led me to misunderstand the Conv rule.

Essentially, Rocq can be understood through two lenses:

1. As a dependently typed functional language with a type-checker and evaluator for the language;
2. As a theorem prover for a logic embedded in the language via the Curry-Howard correspondence, i.e. propositions-as-types and proofs-as-terms.

Previously, I have been primarily viewing Rocq through lens (2). From this lens, I was viewing the typing rules of Rocq like proof rules for a higher-order logic proof system (of course, this is not really precise).

But from the point of view of a logical proof system, I was thinking that it would be good to normalize terms aggressively (and perhaps have an invariant that terms are stored in normalized form). I have encountered proof systems that do this very thing. If used correctly, normalization can make a proof much smaller/more efficient.

On the other hand, from lens (1), i.e., a functional programming and programming language theory lens, it feels so _obvious_ why terms are not reduced during the type checking algorithm — because that’s how _type checking_ itself is defined! And I believe this is the point that @thomas-lamiaux was trying to make in his original response.

Indeed, we want to type check the input term as written by the programmer and _not_ some term that the input term reduces to ! Going further, it may even be the case that an ill-typed term reduces to a well-typed term, so attempting this may actually _break_ type checking instead of optimizing it.

Anyway, that summarizes my thoughts up to this point. As always, I welcome your feedback. Thanks much!

---

<div class="post-metadata">

**Author:** ![jp-diegidio](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jp-diegidio/32/819_2.png) [@jp-diegidio](https://discourse.rocq-prover.org/u/jp-diegidio)\
**Post date:** [August 14, 2025, 9:15am UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/11 "2025-08-14T09:15:49Z")

</div>

> Essentially, Rocq can be understood through two lenses […]  
> (of course, this is not really precise).

And isn’t a more precise understanding exactly what you are looking for? E.g. if you get deeper, even Curry-Howard needs some caution:  
[https://ncatlab.org/nlab/show/propositions+as+types](https://ncatlab.org/nlab/show/propositions+as+types)  
[https://ncatlab.org/nlab/show/propositions+as+some+types](https://ncatlab.org/nlab/show/propositions+as+some+types)

And a plain “proposition as types” I find not even particularly illuminating, all the more so if we look at the concrete details of Rocq: indeed, Prop (and even SProp, in principle) are just sorts with some peculiar rules, and they only approximately represent any propositional or otherwise _logic_.

> it feels so _obvious_ why terms are not reduced  
> during the type checking algorithm

And I did say orthogonal. And then again, the devil is in the detail: e.g. can you tell in [the Core chapter](https://rocq-prover.org/doc/V9.0.0/refman/language/core/index.html) of the manual, where exactly “type checking” (without further qualifications) starts and where it ends? We could rather get even deeper there, and my point just was: 1) we shouldn’t be blurring the very distinctions we were trying to make; and, indeed, 2) as I am sure you’d agree, past an initial introductory level, reading (and linking from) the manual is in fact crucial…

---

<div class="post-metadata">

**Author:** ![thomas-lamiaux](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/thomas-lamiaux/32/982_2.png) [@thomas-lamiaux](https://discourse.rocq-prover.org/u/thomas-lamiaux)\
**Post date:** [August 16, 2025, 10:21pm UTC](https://discourse.rocq-prover.org/t/why-does-the-conversion-rule-for-cic-apply-only-to-types-instead-of-all-terms/2790/12 "2025-08-16T22:21:20Z")

</div>

I do not understand what you mean by

> But “orthogonal” entails “independent”, which is the opposite of how you are reading it.

FYI: I have no animosity towards you. I don’t know you 😃. You are simply saying sth that looks scientifically false, so I answered using my experience and knowledge of Type Theory and MetaRocq. That is it. If you think my answer is false for a good reason, or misunderstood you which can obviously happen when people do not speak in their native language, you are free to answer to clarify your thoughts or point out an error I would have made.

> and do stick to Zulip please

Let us make one thing clear. You got ban from zulip for repeated infringement to the code of conduct. Not me. I am free to answer here, and because it is not part of your sanction, so are you provided you respect the code of conduct. If you feel my behaviour is not appropriate and breaks the code of conduct, you are free to signal it to the moderators, and they will look at it. However, you are not a moderator and telling people there are not allowed to discuss here is not acceptable.

This being said, I really have nothing against you and I wish you to have a good summer.

Best,  
Thomas Lamiaux