what does motive is not type correct mean

Stream: new members

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

thanks in advance lol

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Kevin Buzzard]

What am I missing?

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

yep, that's simp

[Kevin Buzzard]

I see!

[Mario Carneiro]

The drawback is that some subterms are not accessible to simp

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

Oh so it is true??

[Mario Carneiro]

Equality is an isomorphism of groups

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

extensional type theory

[Mario Carneiro]

like I said, make defeq just plain equality

[Mario Carneiro]

aka "set theory with types"

[Kevin Buzzard]

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]

then we have h' : A = B

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

please feel free to try

[Kevin Buzzard]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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