Making change to type judgement according to assumptions

Stream: Type theory

[Yiming Xu]

Hi, all.

I am interested in the problem of how does theorem provers based on DTT, such as Lean, make change to type judgment according to assumptions, such as in the example below, or if it is possible at all.

If the goal looks like
a: A->B
p: A = B

---

phi

I want the goal to become:

a:B->B
(p:B= B here, or whatever, I only care about a:A->B is substituted into a:B->B according to the assumption B=B,)

---

phi

My main quest is that I want the a : B->B, to be literally the same as the ones in the original goal, that is, I do not want an argument such like: the path p:A=B induces a function (A ->B) -> (B ->B), so we can feed a as an argument to this function, and get a term a':B->B, and we can rename a' into a.

Instead, I want just to substitute all the occurrences of A in the assumptions directly into B, and if the goal looks like:

a:A->B
a': \sum_{x:A} P(x)
a'':\prod_{x:A} P(x)
A = B

---

phi

I want the goal to become

a:B->B
a': \sum_{x:B} P(x)
a'':\prod_{x:B} P(x)
B = B

---

phi

according to the assumption B = B, where a, a', a'' are all literally the same as the original goal, we just make changes to the type annotation of them.

According to my experience in a non-dependent typed theorem prover, a "direct substitution" will appeal to equalities such as "a:A->B = a:B->B", and I am confused because such equality is in principle not well-formed at all because the LHS and RHS are not obviously of the same type.

Is making such direct substitution on type-judgment possible in Lean (or in some other DTT theorem provers) whose type information can depend on assumption? If it does, which rule enables us to do this?

[Horatiu Cheval]

I'll try to give my understanding here, but I am far from being an expert, so take it with a grain of salt. I'll use the simpler example of a : A instead of a : A -> B because I think the idea is the same if I understand your question correctly.

If a : A then that's it, it can't be of any other type, even with A = B, unless the A and B are definitionally equal, in which case they are really the same thing, as far as Lean is concerned. So in Lean any term has precisely one type (up to definitional equality). So no, I don't think you can just do such substitutions.

Such substitutions are performed through "functions generated paths arguments" as you called them and that you wanted to avoid. Particularly, in Lean it's all based on eq.rec, the recursor on equalities, which allows you do this kind of things, and whose type also kind of looks like a substitution rule for equality. But still, such substituted terms will ultimately still be eq.rec of something, or other type cast variations based on it.

example (a : A) (h : A = B) : B := eq.rec a h

According to my experience in a non-dependent typed theorem prover, a "direct substitution" will appeal to equalities such as "a:A->B = a:B->B", and I am confused because such equality is in principle not well-formed at all because the LHS and RHS are not obviously of the same type.

I don't think I understand what you mean here by a direct substitition appealing to equalites. But indeed, that equality won't typecheck. And even before that you can't have (a : A -> B) and (a : B -> B), one of them will have to be a cast.

On the other hand, when writing in tactic mode, some tactics do appear to transform the proof state as you describe.

def f1 (a : A) (h : A = B) : B :=
begin
  /-
  A B : Type,
  a : A,
  h : A = B
  ⊢ B
  -/
  subst h,
  /-
  A : Type,
  a : A
  ⊢ A
  -/
  exact a,
end

or

def f2 (a : A) (h : A = B) : B :=
begin
/-
A B : Type,
a : A,
h : A = B
⊢ B
-/
  rw h at a,
  /-
  A B : Type,
  h : A = B,
  a : B
  ⊢ B
  -/
  exact a,
end

I don't really know how these tactis work internally, but the term they generate in the end will still involve some kind of type casting through eq, and things you saw happening to the goal are not really what happens internally, but rather some goal-view tricks meant to hide all this from you.

#print f1
def f1 : Π {A B : Type}, A → A = B → B :=
λ {A B : Type} (a : A) (h : A = B), eq.rec a h

#print f2
def f2 : Π {A B : Type}, A → A = B → B :=
λ {A B : Type} (a : A) (h : A = B), eq.mp _ a

[Horatiu Cheval]

That's all Lean specific of course, but I believe most of it applies to other DTT proof assistants based on CIC (like Coq) or to HoTT.
Maybe in extensional type theory you can have such direct substitutions, but I know virtually nothing about that

[Chris B]

Yiming Xu said:

I only care about a:A->B is substituted into a:B->B according to the assumption B=B,)

If you're saying the assumption has changed from A=B to B=B, it sounds like you might be talking about bound variable substitution for a polymorphic definition?

def myDef {A B : Sort*} (h1 : A = B) (phi : Prop) := (A -> B) -> phi
variables (B : Sort*) (phi : Prop)
example : myDef (rfl : B = B) phi :=
begin
  unfold myDef,
  intros,
end

goal state:
B: Sort u_1
phi: Prop
a: B → B
⊢ phi

[Kevin Buzzard]

My main quest is that I want the a : B->B, to be literally the same as the ones in the original goal

But p : A = B does not mean "A is literally the same as B", it means nothing more than "p is a term of the inductive type eq A B". Would you say that x + y is literally the same as y + x, if x and y are natural numbers?

[Yiming Xu]

Kevin Buzzard said:

My main quest is that I want the a : B->B, to be literally the same as the ones in the original goal

But p : A = B does not mean "A is literally the same as B", it means nothing more than "p is a term of the inductive type eq A B". Would you say that x + y is literally the same as y + x, if x and y are natural numbers?

Yes, p : A = B means p is a term of the inductive type eq A B, this is specific for DTT. I had trouble in a somehow weird workspace, and I am trying to grab idea from DTT for solving this, in my setting, I just have equality, so I do not have things like p: A = B, but just A = B, so I am trying to ignore the (which I agree that is helpful...) viewpoint that "p is a term of eq A B".

To be specific, I am mainly interested in the cases which causes the A and B are literally the same. The two cases I can think of which I care about is:

1.Abbrevation: That is, A is a type with complicated construction, say, it is a huge combination of Pi and Sum, and we want to give it an abbreviation, so we do not need to write it out everywhere. In HOL4, it is a tactic called abbrev_tac, such that you can write abbrev_tac A = B, and it substitute the A into B everywhere in the goal. In this case, A and B are literally the same.

2.inputs equal results in that the output of function is equal: say, I have two arrows f,g:A->B. after proving f = g, I want all occurrences of the "equalizer of f and g" to become "equalizer of f and f", they should be literally the same as well.

[Yiming Xu]

Horatiu Cheval said:

I'll try to give my understanding here, but I am far from being an expert, so take it with a grain of salt. I'll use the simpler example of a : A instead of a : A -> B because I think the idea is the same if I understand your question correctly.

If a : A then that's it, it can't be of any other type, even with A = B, unless the A and B are definitionally equal, in which case they are really the same thing, as far as Lean is concerned. So in Lean any term has precisely one type (up to definitional equality). So no, I don't think you can just do such substitutions.

Such substitutions are performed through "functions generated paths arguments" as you called them and that you wanted to avoid. Particularly, in Lean it's all based on eq.rec, the recursor on equalities, which allows you do this kind of things, and whose type also kind of looks like a substitution rule for equality. But still, such substituted terms will ultimately still be eq.rec of something, or other type cast variations based on it.

example (a : A) (h : A = B) : B := eq.rec a h

According to my experience in a non-dependent typed theorem prover, a "direct substitution" will appeal to equalities such as "a:A->B = a:B->B", and I am confused because such equality is in principle not well-formed at all because the LHS and RHS are not obviously of the same type.

I don't think I understand what you mean here by a direct substitition appealing to equalites. But indeed, that equality won't typecheck. And even before that you can't have (a : A -> B) and (a : B -> B), one of them will have to be a cast.

On the other hand, when writing in tactic mode, some tactics do appear to transform the proof state as you describe.

def f1 (a : A) (h : A = B) : B :=
begin
  /-
  A B : Type,
  a : A,
  h : A = B
  ⊢ B
  -/
  subst h,
  /-
  A : Type,
  a : A
  ⊢ A
  -/
  exact a,
end

or

def f2 (a : A) (h : A = B) : B :=
begin
/-
A B : Type,
a : A,
h : A = B
⊢ B
-/
  rw h at a,
  /-
  A B : Type,
  h : A = B,
  a : B
  ⊢ B
  -/
  exact a,
end

I don't really know how these tactis work internally, but the term they generate in the end will still involve some kind of type casting through eq, and things you saw happening to the goal are not really what happens internally, but rather some goal-view tricks meant to hide all this from you.

#print f1
def f1 : Π {A B : Type}, A → A = B → B :=
λ {A B : Type} (a : A) (h : A = B), eq.rec a h

#print f2
def f2 : Π {A B : Type}, A → A = B → B :=
λ {A B : Type} (a : A) (h : A = B), eq.mp _ a

Thank you! In your example where you used exact a where Lean asks for a term B, to me it really looks like Lean allows you to use a as of type B, the eq.rec stuff looks relevant! I would search for how rw uses it.

[Chris B]

The first case you can do in Lean by declaring a definition. The corresponding rule in the theory is called delta reduction. In that case, the long version and the short version are definitionally equal, which is like a "literally the same as" relation which is respected by the kernel.

In the second case, if f and g aren't definitionally equal, then you can't substitute them without the stuff you said you wanted to avoid (the eq.rec stuff).

[Chris B]

There are also let short := long expressions, which also get unfolded. The rule for those is called zeta reduction.

[Yiming Xu]

Chris B said:

The first case you can do in Lean by declaring a definition. The corresponding rule in the theory is called delta reduction. In that case, the long version and the short version are definitionally equal, which is like a "literally the same as" relation which is respected by the kernel.

In the second case, if f and g aren't definitionally equal, then you can't substitute them without the stuff you said you wanted to avoid (the eq.rec stuff).

Thanks for the quick reply! I will check for the rules and think about them. It is a bit sad that the second case must involve eq.rec stuff though. I have not done enough reading on stuff on delta reduction/zeta reduction yet (I will have a look at them), but at first glance it sounds to me that they are the thing that happens in the meta-level, and is not a part of Lean core logic, but the thing which is done by the language which Lean is written in.

[Yiming Xu]

Horatiu Cheval said:

I'll try to give my understanding here, but I am far from being an expert, so take it with a grain of salt. I'll use the simpler example of a : A instead of a : A -> B because I think the idea is the same if I understand your question correctly.

If a : A then that's it, it can't be of any other type, even with A = B, unless the A and B are definitionally equal, in which case they are really the same thing, as far as Lean is concerned. So in Lean any term has precisely one type (up to definitional equality). So no, I don't think you can just do such substitutions.

Such substitutions are performed through "functions generated paths arguments" as you called them and that you wanted to avoid. Particularly, in Lean it's all based on eq.rec, the recursor on equalities, which allows you do this kind of things, and whose type also kind of looks like a substitution rule for equality. But still, such substituted terms will ultimately still be eq.rec of something, or other type cast variations based on it.

example (a : A) (h : A = B) : B := eq.rec a h

According to my experience in a non-dependent typed theorem prover, a "direct substitution" will appeal to equalities such as "a:A->B = a:B->B", and I am confused because such equality is in principle not well-formed at all because the LHS and RHS are not obviously of the same type.

I don't think I understand what you mean here by a direct substitition appealing to equalites. But indeed, that equality won't typecheck. And even before that you can't have (a : A -> B) and (a : B -> B), one of them will have to be a cast.

On the other hand, when writing in tactic mode, some tactics do appear to transform the proof state as you describe.

def f1 (a : A) (h : A = B) : B :=
begin
  /-
  A B : Type,
  a : A,
  h : A = B
  ⊢ B
  -/
  subst h,
  /-
  A : Type,
  a : A
  ⊢ A
  -/
  exact a,
end

or

def f2 (a : A) (h : A = B) : B :=
begin
/-
A B : Type,
a : A,
h : A = B
⊢ B
-/
  rw h at a,
  /-
  A B : Type,
  h : A = B,
  a : B
  ⊢ B
  -/
  exact a,
end

I don't really know how these tactis work internally, but the term they generate in the end will still involve some kind of type casting through eq, and things you saw happening to the goal are not really what happens internally, but rather some goal-view tricks meant to hide all this from you.

#print f1
def f1 : Π {A B : Type}, A → A = B → B :=
λ {A B : Type} (a : A) (h : A = B), eq.rec a h

#print f2
def f2 : Π {A B : Type}, A → A = B → B :=
λ {A B : Type} (a : A) (h : A = B), eq.mp _ a

Maybe my parse of "direct substitution" is confusing, and maybe it is a wrong phrase. I was thinking of how a usual rewrite tactic work: It is provided an equality, and it looks for the LHS of equality in a goal, and substitute it into the RHS of such equality.

[Chris B]

I mean you can do these with the rw tactic, but they do make use of the recursor for eq.

example {A B : Sort*} (f : A -> B) (h : A = B) : (A -> B) = (B -> B) :=
begin
  rw h,
end

example {A B : Sort*} (f : A -> B) (h : A = B) : B -> B :=
begin
  rw h at f,
  exact f,
end

[Yiming Xu]

Chris B said:

I mean you can do these with the rw tactic, but they do make use of the recursor for eq.

example {A B : Sort*} (f : A -> B) (h : A = B) : (A -> B) = (B -> B) :=
begin
  rw h,
end

example {A B : Sort*} (f : A -> B) (h : A = B) : B -> B :=
begin
  rw h at f,
  exact f,
end

Yes, I understand that rw can do this. It is reasonable that Leans's rw has access to eq recursor. I should say is that the thing in my mind is a non-DTT rw, I would try have a look how Lean's rw use the eq.

[Horatiu Cheval]

Just out of curiosity, in what non-DTT setting are you more specifically working?

[Jannis Limperg]

Perhaps it'll be helpful to talk a bit about why intensional dependent type theory (ITT) doesn't let you do something like this. Basically, many design choices of ITT are made to ensure that type checking is decidable (and fast). If you go from x : A to eq.rec eq x, where eq : A = B, this is easy to typecheck. If you go from x : A to x : B by appealing to some ambient equation, without recording this equation in the term, that is much harder to check: the compiler must go through any equations currently in scope and try to construct some proof eq : A = B. This is undecidable in general since eq may involve an arbitrary number of transitivity steps.

Nevertheless, there are also extensional type theories, where "extensional" means that exactly the thing you're asking for is possible. An example would be F*. I don't know how they get around the undecidability in practice, but whatever they do seems to be working, so it's certainly not impossible. And of course there are systems which do not have proof terms anyway (Isabelle etc?), so they don't have to concern themselves with this.

[Kevin Buzzard]

Just to comment that if you name declarations then you can inspect them with #print:

def foo {A B : Sort*} (f : A -> B) (h : A = B) : (A -> B) = (B -> B) :=
begin
  rw h,
end

#print foo -- see explicit proof term involving eq.rec

[Yiming Xu]

Horatiu Cheval said:

Just out of curiosity, in what non-DTT setting are you more specifically working?

The object-arrow two-sorted first-order logic(but no more than first-order logic except for the fact that it is two-sorted, it is just like Makkai's FOLDS https://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf, the case for category theory, but without the complicated setting of kinds/sorts, just look at his working examples (that is basically the part in the link which you can directly understand without reading through his paper, for example, page 3 to page 4)). So a variable with name "a" and of sort A->B depends on two terms,namely A and B, which are objects. I have a function symbol called "coeqo", which takes a pair of arrow term with the same sort, I have a variable (simplified version) like:

a:coeqo(f,g) ->X

(Note that FOLDS does not get into this situation, because it does not allow equality on objects at all, and it only has predicates, no functions.)
and then I proved that f = g, and want to substitute the g to be f, so I get a post inverse of a. And I am messed up by this for several days, because I do not have rules to make changes on the sort of variable, and the sort is same a type-judgment, which is unique for each term.

[Yiming Xu]

Jannis Limperg said:

Perhaps it'll be helpful to talk a bit about why intensional dependent type theory (ITT) doesn't let you do something like this. Basically, many design choices of ITT are made to ensure that type checking is decidable (and fast). If you go from x : A to eq.rec eq x, where eq : A = B, this is easy to typecheck. If you go from x : A to x : B by appealing to some ambient equation, without recording this equation in the term, that is much harder to check: the compiler must go through any equations currently in scope and try to construct some proof eq : A = B. This is undecidable in general since eq may involve an arbitrary number of transitivity steps.

Nevertheless, there are also extensional type theories, where "extensional" means that exactly the thing you're asking for is possible. An example would be F*. I don't know how they get around the undecidability in practice, but whatever they do seems to be working, so it's certainly not impossible. And of course there are systems which do not have proof terms anyway (Isabelle etc?), so they don't have to concern themselves with this.

That makes sense and is eye-opening. And yes, Isabelle is one example of no proof term, I am a rather long-term HOL4 user, which does not have proof term either, so have not encountered such problems at all before.

[Yiming Xu]

Thanks to all who have replied. I think I see hope of getting my problem to be solved using a similar idea of eq.rec. But there raises a new problem.

[Yiming Xu]

How can we show that the predicates which previously hold for a term also holds for the term produced by eq.rec on that term?

[Yiming Xu]

Is there any usage of other primitive rules here?

[Mario Carneiro]

Yes, although this gets into "coercion hell". The primitive rule is the same one: eq.rec can be used to prove that P a implies P (eq.rec h a) assuming P is suitably parametric in the types to make that typecheck

[Mario Carneiro]

There is a much simpler approach, which will be familiar to you if you have used HOL: Instead of using a dependent type to express the property of an element, have a simpler type and assert a proposition about the element. For example, instead of having a : term nat, use a : term and h : typed a nat

[Mario Carneiro]

If you never have any nontrivial equalities of types, this issue doesn't come up

[Yiming Xu]

Mario Carneiro said:

There is a much simpler approach, which will be familiar to you if you have used HOL: Instead of using a dependent type to express the property of an element, have a simpler type and assert a proposition about the element. For example, instead of having a : term nat, use a : term and h : typed a nat

I tried that, in HOL, exactly. It is horrible. If sort information is not an intrinsic property of a term, then even composition rules like (a o b) o c = a o b o c is not a simple equality anymore, but need to be conditional rw. if we have long-long arrow term, then it is time consuming to get out of nested composition.

[Yiming Xu]

Another way to get rid of non-trivial equality on types is to never have functions which produce the things which type-information can rely on, which basically demands us to have no functions at all. But that mean predicates everywhere. As in common sense I know, rw's likes equalities ,not predicates. Also, using predicates means that if def1 replies on def2, then we require all the inputs of the def2 to also be inputs in def1. Say, definition of exponential relies on the definition of product, the definition of exponential would be messy, since it involves the predicate of being a product.

[Yiming Xu]

People which do not like the idea of equality of objects in category theory claims that we can use predicates everywhere! But then give simple examples, and do not really go through all basic category theory using predicates and get rid of all functions. Yes, I am complaining about this :-( .

[Mario Carneiro]

Another way to get rid of non-trivial equality on types is to never have functions which produce the things which type-information can rely on, which basically demands us to have no functions at all.

I'm not sure how you got here. You can certainly have functions in simple type theory, they just don't have dependent types (i.e. the type of the result doesn't depend on the non-type arguments). But really, both positions are extremist, and the reality is somewhere in the middle. Use simple types when convenient, but reach for dependent types when you have a categorical style problem and you think you can maintain the discipline to keep your defeq problems sane.

[Mario Carneiro]

Working in a DTT theorem prover means you can bend the rules when simple types everywhere is too onerous

[Mario Carneiro]

If sort information is not an intrinsic property of a term, then even composition rules like (a o b) o c = a o b o c is not a simple equality anymore, but need to be conditional rw.

By the way, you can also use typeclasses for this sort of thing, although I don't think we've ever tried it for composition. Mathlib uses dependent types for category theory.

[Mario Carneiro]

Also, using predicates means that if def1 replies on def2, then we require all the inputs of the def2 to also be inputs in def1. Say, definition of exponential relies on the definition of product, the definition of exponential would be messy, since it involves the predicate of being a product.

I think I'm missing the context for this assertion. This isn't the case in lean, you can have the definition of a product packed up in a typeclass and the exponential function can have a simple type

[Yiming Xu]

Here is the context: we tried formalising some basic category theory in HOL4, and we use "type judgments as formulas", so we can prove things like h is an arrow from an object A to an object B, but then, it turns out that even simple facts such like:

∀A B X Y Z f1 f2 f3 f4.
f1∶ X → Y ∧ f2∶ Y → Z ∧ f3∶ Z → A ∧ f4∶ A → B ⇒
f4 o (f3 o f2) o f1 = f4 o f3 o f2 o f1

takes long(if you use metis, with minimal intermediate steps, than it takes ages)/or some human work (if you want the proof to run fast, figure out step-by-step how the LHS becomes RHS, and then tell HOL to do the detailed proof) to prove. But won't everyone agree that this is such a simple thing which should completely be automatic and should not take so long?!

and we are trying to design a new thing, which we want to be on a sweet spot when dealing with problems like in the situation in basic category theory, where sorts information of term is an intrinsic property, so it works nicely for such a simple proof. So I am not claiming "we cannot have functions in simple type theory". So I want to borrow things from Lean and HOL, if possible.

[Yiming Xu]

Mario Carneiro said:

Also, using predicates means that if def1 replies on def2, then we require all the inputs of the def2 to also be inputs in def1. Say, definition of exponential relies on the definition of product, the definition of exponential would be messy, since it involves the predicate of being a product.

I think I'm missing the context for this assertion. This isn't the case in lean, you can have the definition of a product packed up in a typeclass and the exponential function can have a simple type

If we have function symbols whose output is an object, say, we can produce the coequalizer object of f,g:A->B, using a function called coeqo, and we make the sort information of a term an intrinsic property, then we can have a goal asking us to prove:

P(a:coeqo(f,g) ->X)

where P is a predicate on a. Then if we have f = g by hand, and want the goal to become P(a:coeqo(f,f) ->X), it gets changing the type of a involves.

My claim is that if we do not have function symbols, at least the ones whose output is an object, then we do not get into a situation like this, because then we can avoid substitution on dom/cod of arrows. Because instead of having coeqo(f,g) as an object, we have a predicate iscoeqo(f,g,E), so if we want something we can prove from the fact that the domain of a is a coequalizer of f and f, then we just prove forall f g E. iscoeqo (f,g,E) ==> forall a:E ->X,P(a), then instead of substitution, we use the strategy of proving "the property holds for all the thing satisfies certain predicates" holds.

[Yiming Xu]

Mario Carneiro said:

Yes, although this gets into "coercion hell". The primitive rule is the same one: eq.rec can be used to prove that P a implies P (eq.rec h a) assuming P is suitably parametric in the types to make that typecheck

If it is not so hard to state, could you give a bit explaination, maybe an example, on what is "coercion hell"? I am interested in which trouble will it bring us in practice.