Prompts for Dependent Types from Rocq to Lean 4

Initial request

For an upcoming article for our blog, let’s do a deep dive into dependent type systems, in particular calculus of constructions, as in Rocq, and the system behind Lean, its evolution, and Lean4. Inspired by this article https://www.lesswrong.com/posts/zHhGa3iQBQcdSifFL/a-critical-look-at-lean4-1 But the motivation is to refresh my forgotten understanding of Rocq (Coq at the time) and use it to teach me Lean. A fruitful triangulation for the level of writing is:

• People who used to be familiar with dependent types at a rather deep level but in their past life and need a refresher
• People who are unfamiliar with dependent types but are proficient mathematicians

Normalization and denotational semantics

Let’s go deeper into why proof irrelevance and impredicativity break normalization, with a worked example. I’d like to understand the mechanism, not just the distinction from inconsistency. On another tangent, how do these articles relate? https://arxiv.org/html/2603.12827 and https://arxiv.org/html/2507.04071. Would it be worth adding a denotational semantics section?

GADTs and dependent types

How much of the dependent types’ expressivity can be captured by GADTs?

Is Haskell or OCaml more expressive in this regard, or are they the same?

Let’s add a section on GADTs to the article, using the Haskell and OCaml examples to explain how far indexed families get us and what full dependent types add. Thanks!

Constructor declaration syntax

What does the second colon do in this part of the definition of Vec? cons {n : Nat} : α → Vec α n → Vec α (n + 1)

Why is it a colon rather than an arrow?

Ah so it’s just stylistic

Let’s add a brief explanation of this syntax to the article, showing the two equivalent forms of cons.

Naming the hypothetical constructor

“If we freely admitted a constructor (Bad → False) → Bad,” is the constructor named mk in the example that follows? I’d say “If we freely admitted a constructor mk : (Bad → False) → Bad,”

Positive and negative positions

It’s obvious to me what a positive and negative position is, but it might not be to all readers.

Understanding the diagonal counterexample

In the counterexample, is d (mk d) the only option, or can we pass some other arguments to d?

What would be the next smallest example of deriving False?

Is it possible to make the example not eventually close directly, but to alternate two reducts?

Do you think adding this example to the article would be a nice illustration or just a waste of readers’ time?

Yes, add this clarification and also add the open reduction sequence for d

Termination measures aside

Can we add an “off-topic details” box where we compare this to termination tracking type systems with a decreasing measure?

Reflexivity terms and tactics

What does this mean? example (n : Nat) : addLeft 0 n = n := rfl

I see; rfl is a tactic “reflexivity”? Let’s explain this.

Existential syntax and the type of a proof

I removed these sentences: ” This is a comparison of dependent programming techniques, not a total ranking of the languages.”, “This does not identify all propositions.” and changed “makes this a property of the type system itself” to “marks this as a property of the type system itself”. How does this parse in forgetWitness? “∃ x, P x”

So, the type of this type is Prop, and the values of this type are pairs?

What does this mean? “A proof of ∃ x, P x lives in Prop.”

Yes, let’s use that clearer wording in the article, and briefly explain how ∃ x, P x parses. (This is very clear to a mathematician, but an OCaml programmer will glitch for a while thinking it’s a pair.)

A visible benefit of proof irrelevance

What are the benefits of proof irrelevance?

So without proof irrelevance, we wouldn’t get get xs 0 = get xs 0 out of the box. Maybe that’s a good example to illustrate why we want this? For (1) we could imagine syntax sugar that does equivalencing; and (3) and (4) are not so visible to the users. All are benefits, but maybe (2) is most striking?

Choice and reasoning about programs

How can Classical.choose recover a witness if proof irrelevance identifies existential proofs that were constructed using different witnesses? Also, doesn’t function extensionality affect reasoning about programs?

Can we say that Classical.choice is a constant function?

The more interesting part is the effect of function extensionality on reasoning about programs. Can you comment on this in the article?

Is it a difference from Rocq?

My question was misleading then. It’s not the extensionality that limits reasoning about programs. It’s the framework of dependent types with equality that makes functions and programs different categories.

You can compress the four paragraphs that now discuss this program modeling limitation. The first paragraph, “For reasoning about programs, distinguish a function from an implementation”, is I think the best. Preserve from the others what’s striking / non-obvious.

Deriving function extensionality from quotients

What are the main ways that definitional identity is distinguishable from identity in general

Can we dig deeper into how function extensionality is derived using primitive quotients?

Let’s add it to the article. Would you put it as a subsection of “Extensional mathematics and primitive quotients”, or in an appendix section?

Separating typing from definitional equality

Let’s expand this into two lines to avoid confusing object and meta equality: z\,D\,i &: D=T\to T,

This is confusing: “If `a : A` and `b : B` prove two propositions, we can prove A ↔︎ B”

Propositions and formulas under assignments

So, Prop extensionally has two elements?

So what can we say without excluded middle?

Once it’s written down formally, it’s not that surprising because of the double-negated negation encoding of classical in intuitionistic logic. Maybe we can clarify something else. We can discuss how equivalence in Prop relates/is distinct from notions of equivalence and equisatisfiability with three variables.

I’d like to add this to the article, but I don’t know what we need to say to make it neither sound trivial nor sound like an unmotivated digression.

Weak and strong normalization

So d(w) has no terminating reduction because the only reduction sequence is the one we showed?

Let’s add a brief clarification of weak versus strong normalization to the article, and that this case is not weakly normalizing.

Removing empty cautions about nested inductives

This part is bad writing: “This complexity does not identify nesting with the mechanism in the normalization counterexample, and that counterexample does not establish that nested inductives are inconsistent. Keeping the mechanisms separate is essential to evaluating claims about either one.” First, we negate two obvious falsehoods (obvious when stated at this level of abstraction), and then we warn about keeping a mechanism we know about and a mechanism we don’t know about separate. What I would say is: “This is its own distinct can of worms.”

Still not quite right because partially redundant with “Nested inductive types are a further, distinct topic.” Maybe replace my lighthearted sentence with something like: “This gives rise to concerns even without invoking non-terminating reduction.” – if that’s true.

Universe levels in the set interpretation

“dependent products land at level \max(m+1,n)” – what is m here? Line 731

What con-leche assumes and constructs

Line 741: “the con-leche project states a consistency result for its external checker under a set-theoretic model assumption”. What’s their approach? Do they provide the semantics, or is it only a constraint of having a semantics?

Naming introduced variables and hypotheses

Can we also explain intro x y h in the proof near the end? Are these arbitrary identifiers, or are they constructed inside the initial proof state?

Universal quantifiers and dependent arrow syntax

Could ∀ ⦃x y : A⦄, f x = f y → x = y also be written (x y : A) → f x = f y → x = y?

Aha, so correcting for what I overlooked, the original and ⦃x y : A⦄ → f x = f y → x = y are the same. Could we make a side note about this in “Why implication and universal quantification are function types”?

Final editorial pass

Looks good! Do a final editorial pass. Thanks.

Index entry and commit

I also deleted: “Their types come from this goal; their names are our choice. They are not already available in the initial local context.” Let’s add an entry to index.html and commit, thanks!