intuition for "correct" formal definitions in λD

Stream: new members

[rzeta0]

I'm working though Type Theory & Formal Proof (Nederpelt) as it was recommended here as a good way to learn the basics of how a proof assistant like Lean works.

Chapter 8 introduces formal definitions, and Chapter 9 starts to extend λC to λD, by extending the derivation rules to incorporate formal definitions (link).

In the exercises to Chapter 9, the author introduces the concept of a definition $D$ being correct in environment $\Delta$ if

$$\Delta, D ; \emptyset \vdash *:\Box$$

Terminology: An environment is an ordered list of definitions, similar but separate to the usual context which can bind free variables. The $\emptyset$ above is this usual context, but empty. Also $*$ is the type of types, eg $\mathbb{N} : *$, including propositions and sets. The $\Box$ is the type of $*$, and needed to deal with eg $* \to * : \Box$.

Question: I don't understand intuitively the concept of correct. I'd welcome help.

---

My Thinking

Imagine I have a correct definition $D_1$ in the empty environment $\emptyset$. This means

$$\emptyset, D_1 ; \emptyset \vdash *:\Box$$

Now if I have another definition $D_2$, which we assume for the purpose of contradiction is not correct in the environment $D_1$.

Next we consider the environment and empty context $D_1, D_2 ; \emptyset$. I believe I can still derive $*:\Box$ simply by ignoring $D_2$, and using the correctness of $D_1$. This would mean $D_2$ is in fact correct in the environment $D_1$.

Clearly I'm confused about either the meaning of correct, or misguided on how to derive $*:\Box$ from a given environment and context.

This would mean $D_2$ is correct in environment $D_1$.

---

Note: I'm a self-teaching beginner so there may be many flaws in the above. I appreciate your patience!

[Aaron Liu]

this makes sense to me

[rzeta0]

It doesn't make sense to me sadly. Are you able to give me a notion of what "correct" is supposed to mean?

Perhaps an example of a non-correct definition could help me see how it contravenes the test $\Delta, D_{\text{bad}}; \emptyset \vdash *:\Box$ ?

[Aaron Liu]

well the (sort) formation rule only works in the empty environment

[Aaron Liu]

so at some point you have to add in the definition $D_{\text{bad}}$ using the (def) rule

[rzeta0]

So it seems I can add any definition to an environment, using the (def) rule, which only imposes the requirement that the types of the variables in the definition parameter list can themselves be derived.

But if I have a bad $D_{\text{bad}}$ where this requirement is not met, I can still have

$$\Delta, D_{\text{bad}}; \emptyset \vdash *:\Box$$

So even though I have constructed a definition which doesn't satisfy the premises of the (def) rule, the above suggests it is correct.

What am I missing? Sorry for being slow, this has bugged me for days and I re-reading Chapter 9 twice hasn't helped.

[Aaron Liu]

rzeta0 said:

So it seems I can add any definition to an environment, using the (def) rule, which only imposes the requirement that the types of the variables in the definition parameter list can themselves be derived.

You have to derive that the value has the correct type

[Aaron Liu]

rzeta0 said:

But if I have a bad $D_{\text{bad}}$ where this requirement is not met, I can still have

$$\Delta, D_{\text{bad}}; \emptyset \vdash *:\Box$$

wait I'm confused

[Aaron Liu]

why do you say you can have this

[rzeta0]

You have to derive that the value has the correct type

Which value do you mean? The only values I can think of are those that are substituted for the parameter variables at instantiation time - the (inst) rule, not during the (def) rule.

why do you say you can have this

Because I can derive $*:\Box$ using $\Delta$ and simply ignore $D_{\text{bad}}$.

This would be like saying $x=2, y=3$ allows me to derive $x+y=5$. And then adding a superfluous $z=10$ to give $x=2, y=3, z=10$ still allows me to derive $x+y=5$.

I hope this is exposing the root of my misunderstanding..

[Aaron Liu]

rzeta0 said:

Because I can derive $*:\Box$ using $\Delta$ and simply ignore $D_{\text{bad}}$.

Then you get $\Delta; \emptyset \vdash * : \Box$

[Aaron Liu]

which is clearly not the same thing

[Aaron Liu]

and there's no rule that lets you add $D_{\text{bad}}$ onto that without verifying it

[rzeta0]

So this leads me to understand correct as meaning verifying the types of the parameters of the definition can be derived in the given environment, as illustrated by the attached image.

D0 copy.png

Furthermore, correct does not imply any other kind of verification, only this.

Am I right?

[Aaron Liu]

hold on, I don't understand what the bars mean

[Aaron Liu]

is that like a list of parameters

[Aaron Liu]

so what this looks like to me is, "in environment $\Delta$ with context of free variables $\overline{x} : \overline{A}$, if you can derive $M : N$ then you can add $a$ as a new definition to the environment $\Delta$ so that $a(\overline{x})$ has type $N$ and value $M$"

[rzeta0]

yes, the bar is the book author's notation for abbreviating a list of things

[rzeta0]

and yes that is the interpretation of the (def) rule.

so I'm still not certain of what correctness is supposed to mean... I'll sleep now and look again tomorrow.

[Aaron Liu]

a correct definition is just one that typechecks basically

[Aaron Liu]

The part at the end with $\vdash * : \Box$ is just a dummy

[Aaron Liu]

it's like saying ∃ x, True, the True is just a dummy

[Aaron Liu]

the important part is not the True but the x