## Stream: new members

### Topic: what does motive is not type correct mean

#### Huỳnh Trần Khanh (Apr 02 2021 at 02:48):

i encounter that error quite often and yeah i know there are like 998244353 ways to get around the error but I don't know what the error REALLY means

#### Bryan Gin-ge Chen (Apr 02 2021 at 02:51):

I remember liking this discussion of the error and how to work around it in this older thread.

#### Kevin Buzzard (Apr 02 2021 at 09:36):

My impression is that the error is just because the rewrite tactic is not powerful enough rather than there being any profound reason for its failure. Prove me wrong!

#### Mario Carneiro (Apr 02 2021 at 09:38):

I would say it fails for a fundamental reason, but there are more clever ways to do different things that may not encounter this issue and instead suffer from different problems

#### Kevin Buzzard (Apr 02 2021 at 10:01):

We have congr_arg (is it that one? The one that says if a=b then f(a)=f(b) ) so I don't see why this can't just be recursively applied everywhere until the motive is type correct. What am I missing?

#### Mario Carneiro (Apr 02 2021 at 10:03):

The issue is when f has a dependent type like \all a : X, P a -> B and you want to rewrite f a x = f b y using a = b

#### Mario Carneiro (Apr 02 2021 at 10:03):

you can't use x = y as a hypothesis because it is not type correct

#### Mario Carneiro (Apr 02 2021 at 10:04):

You can use x == y and this is what the congr tactic does in practice, but == lacks a lot of properties of = that you would like here and in particular you can't rewrite with it or use congr on it to traverse further into subterms

#### Kevin Buzzard (Apr 02 2021 at 10:10):

x : P a and a=b so P a = P b by congr_arg so x : P b. What is the problem here? I don't get it. I say again that a more powerful rewrite tactic could do this and that this whole motive not type correct thing is just a myth

#### Mario Carneiro (Apr 02 2021 at 10:12):

so x : P b

This is the problem. x : P a and P a = P b does not imply x : P b in intensional type theories

#### Kevin Buzzard (Apr 02 2021 at 10:12):

You can just rewrite the proof of P a = P b at x

#### Kevin Buzzard (Apr 02 2021 at 10:13):

What am I missing?

#### Mario Carneiro (Apr 02 2021 at 10:13):

That won't prove x : P b, it will construct a new value of type P b which is not x but rather eq.rec h x

#### Mario Carneiro (Apr 02 2021 at 10:13):

The tactic state does some smoke and mirrors so that you don't notice this

#### Mario Carneiro (Apr 02 2021 at 10:14):

but this trick doesn't work when you are rewriting inside a term

#### Mario Carneiro (Apr 02 2021 at 10:15):

Mario Carneiro said:

so x : P b

This is the problem. x : P a and P a = P b does not imply x : P b in intensional type theories

This is not an issue that set theory, or extensional type theory, have

#### Mario Carneiro (Apr 02 2021 at 10:16):

extensional type theory is where you add a rule that says that from x = y conclude that x is defeq to y

#### Kevin Buzzard (Apr 02 2021 at 10:17):

I see. But then we could still have a tactic which does the rewrite rather than bailing out. We'd get f b (h.rec x) = f b y

#### Mario Carneiro (Apr 02 2021 at 10:17):

yep, that's simp

I see!

#### Mario Carneiro (Apr 02 2021 at 10:18):

The drawback is that some subterms are not accessible to simp

#### Kevin Buzzard (Apr 02 2021 at 10:18):

I don't get this bit. You've still not given an example where the rewrite can't happen

#### Kevin Buzzard (Apr 02 2021 at 10:19):

Or are you just saying that we could have a better tactic?

#### Mario Carneiro (Apr 02 2021 at 10:19):

congr doesn't actually rewrite in all subterms, it will hold some things fixed when it thinks that it would be a bad idea to rewrite them because the recs upon recs get out of hand

#### Mario Carneiro (Apr 02 2021 at 10:20):

for example, when rewriting add A x y, it will not rewrite at A

#### Mario Carneiro (Apr 02 2021 at 10:21):

because you would end up with add B (h.rec x) (h.rec y), and now rewriting at x will only make things worse

#### Mario Carneiro (Apr 02 2021 at 10:22):

let's say x is a + b, now associativity doesn't fire because you have h.rec (a + b) + h.rec y instead of (a + b) + y

#### Kevin Buzzard (Apr 02 2021 at 10:22):

I would imagine that in the HoTT provers they are having to deal with recs upon recs all the time. We've been jumping through all sorts of hoops to define cohomology of a complex because of this. Should we just be much less scared of eq.rec and have an API for it making it something we can deal with more easily?

#### Mario Carneiro (Apr 02 2021 at 10:22):

plus, h has some occurrences of x too, so you want to rewrite that too

#### Mario Carneiro (Apr 02 2021 at 10:23):

yeah, this is a nightmare in HoTT, half the library has to be lemmas about how h.rec commutes with everything

#### Mario Carneiro (Apr 02 2021 at 10:24):

We have an API for eq.rec in category theory, that's eq_to_hom

#### Kevin Buzzard (Apr 02 2021 at 10:25):

For example I assume it's a theorem that h.rec (a+b) = h.rec a + h.rec b? Oh -- the point is that this isn't formal, right? If I have P : X -> Type and then an add_group structure on P x then in practice I will know that the equality P a = P b is an isomorphism of groups, but am I right in thinking that this is not forced upon us by the type theory?

#### Mario Carneiro (Apr 02 2021 at 10:25):

but it makes things only slightly less painful, by making it more explicit (instead of making it completely invisible like we would like)

#### Mario Carneiro (Apr 02 2021 at 10:26):

For example I assume it's a theorem that h.rec (a+b) = h.rec a + h.rec b?

This is true, but not automatic. This is essentially saying that + is parametric in a certain way (keep in mind that the implicit args there are different in the two occurrences)

#### Kevin Buzzard (Apr 02 2021 at 10:27):

Oh so it is true??

#### Mario Carneiro (Apr 02 2021 at 10:27):

Equality is an isomorphism of groups

#### Mario Carneiro (Apr 02 2021 at 10:31):

I think the issues come up when you can't just commute the h.rec because of the form of the function. For example if f : A -> T A, and you have h.rec (f a) where h : T A = T B, you can't commute that to f (h'.rec a) where h' : A = B because you need h' to come from somewhere, and it isn't necessarily the case that T is injective

#### Mario Carneiro (Apr 02 2021 at 10:32):

In ETT you wouldn't have any h.rec term so the commutation is trivial, f a = f a

#### Kevin Buzzard (Apr 02 2021 at 10:33):

Right now in the homology2 branch Scott is trying the n'th iteration of this crazy idea of Johan to define a complex (which in a mathematician's mind is a bunch of groups $A_i$ equipped with group homomorphisms $d:A_i\to A_{i+1}$ satisfying $d^2=0$) by letting there be maps from A i to A j for all i j : int just to get around this motive nonsense. In some sense this is mathematicians giving up because they're scared of eq_to_hom but what really seems to be going on is that the decision to allow junk d's has just been deemed by the community to be the lesser of two evils.

#### Kevin Buzzard (Apr 02 2021 at 10:34):

I daren't ask what ETT is, I'm assuming it's not Lean

#### Mario Carneiro (Apr 02 2021 at 10:34):

extensional type theory

#### Mario Carneiro (Apr 02 2021 at 10:35):

like I said, make defeq just plain equality

#### Mario Carneiro (Apr 02 2021 at 10:35):

aka "set theory with types"

#### Kevin Buzzard (Apr 02 2021 at 10:45):

Going back to this T example above, it looks spurious to me. If you have h : T A = T B and if T isn't injective, a mathematician wouldn't expect to be able to turn h.rec (f a) into f (h'.rec a) in general because maybe A doesn't equal B. However if A does equal B then we have h' : A = B and now one can prove that h = congr_arg T h' because they're terms of a proposition, and now h.rec (f a) = (h'.rec a) is I guess unproblematic.

#### Mario Carneiro (Apr 02 2021 at 10:55):

then we have h' : A = B

Who is "we" here? Somehow the tactic needs to know or discover this

#### Mario Carneiro (Apr 02 2021 at 10:56):

You could have a lemma that says (congr_arg T h').rec (f a) = f (h'.rec a) but that won't fire as a simp lemma

#### Kevin Buzzard (Apr 02 2021 at 11:25):

Right -- I guess what I am trying to understand right now is what things would look like if we just defined complexes the way mathematicians would like to define them and then instead of just giving up with the first eq.rec we instead learn how to battle it.

#### Mario Carneiro (Apr 02 2021 at 11:29):

I don't think I can say anything in particular without a more concrete setting - there will be battles to be had, and they can be overcome by various application-specific techniques

#### Kevin Buzzard (Apr 02 2021 at 11:41):

Basically I think I am saying that now I actually understand what's going on a bit better I should try the cdga game again but in a different way -- battling the recs head on. Or maybe I'll just play the homology game. Maybe it will just be horrible!

#### Eric Wieser (Apr 02 2021 at 22:19):

I played around with some lemmas about eq.rec in #6837

#### Eric Wieser (Apr 02 2021 at 22:19):

The rest of the PR is junk, but those lemmas may be worth salvaging

#### Eric Wieser (Apr 02 2021 at 22:21):

Notably this one covered some versions of Kevin Buzzard's addition example:

lemma rec_apply₂ {ι : Sort*} {A B C: ι → Sort*} : ∀ {i j : ι} (h : i = j)
(f : Π i, A i → B i → C i) (x : A i) (y : B i),
h.rec (f i x y) = f j (h.rec x) (h.rec y)
| _ _ rfl f x y := rfl


#### Kevin Buzzard (Apr 02 2021 at 22:49):

I'm not sure whether in pushing for more eq.rec or less. I was talking to Amelia recently who has been avoiding == in her MSc thesis but then Chris Hughes told her that it wasn't that hard to work with really; on the other hand it gets a lot of bad press around here.

#### Mario Carneiro (Apr 02 2021 at 23:10):

If you are in DTT hell then heq is certainly going to be one of the tools in your tool belt. There are a couple different things like subst and eq.rec and == and pattern matching on rfl and congr_arg that get used in these kinds of proofs, and they are all problematic in entirely different ways. If you are lucky you can navigate between them and avoid the pitfalls

#### Mario Carneiro (Apr 02 2021 at 23:11):

For example, notice that theorems like rec_apply are always very easy to prove, they are always just "case on rfl, rfl"

#### Mario Carneiro (Apr 02 2021 at 23:11):

however, the stating the theorem is complex, and it's difficult to create these theorems on the fly in the middle of a proof, you have to generalize exactly the right things

#### Mario Carneiro (Apr 02 2021 at 23:14):

For example, take a look at this file from the lean 2 hott library: https://github.com/leanprover/lean2/blob/master/hott/init/path.hlean and notice how many theorems are proved by induction p; refl

#### Mario Carneiro (Apr 02 2021 at 23:18):

but it's also believed that the (first order) theory of equality is not "finitely axiomatizable" with a fixed number of theorems like the ones in that file, you get associators that commute with inverses, and these operators are themselves objects that cohere in some complicated way in the next level up, and all the proofs are by induction p; refl but the library is forever incomplete, so you can't just write rec_apply once and be done with it because you will need rec_apply3 or rec_rec_apply and so on

#### Mario Carneiro (Apr 02 2021 at 23:21):

By the way, == is basically equivalent to a theorem about eq.rec. For example that theorem above can also be stated as

lemma rec_apply₂ {ι : Sort*} {A B C: ι → Sort*} : ∀ {i j : ι} (h : i = j)
(f : Π i, A i → B i → C i) (x : A i) (y : B i),
f i x y == f j (h.rec x) (h.rec y)


The main difference is that == forgets the proof that i = j or C i = C j (it existentially quantifies over a proof of C i = C j), so you have to supply the proof when you want to get back to a regular equality

#### Kevin Buzzard (Apr 03 2021 at 08:55):

Thanks for this. I was trying to turn it all into a blog post yesterday but I'm now thinking of writing two -- one on induction and then one on this stuff

Last updated: May 07 2021 at 00:30 UTC