What is a motive?

Stream: new members

[Keeley Hoek]

In the course of leaning (some rw h at h1), I've gotten rewrite tactic failed, motive is not type correct. What's a motive?

[Keeley Hoek]

MWE:

inductive struct
| mk (α : Type) (a : α)

axioms (α β : Type) (a : α) (h : α = β)

example : false := begin
  have ss : struct.mk α a = struct.mk α a := rfl,
  rw h at ss,
end

[Mario Carneiro]

The goal of a cases_on or a rec_on is of the form \all a, C a. C is the motive

[Mario Carneiro]

In the case of rw (bla : a = b), it's constructing an eq.rec_on application, and so the motive is a lambda term C such that C b is the goal and C a is where rw wants to end up

[Keeley Hoek]

Aha, so does this mean that rw is not smart enough to (for example in my example above), after having rewritten the α into a β, use id to wrap a in a function application which views a as a term of type β?

[Mario Carneiro]

yes, that's exactly it. It rewrites α to let's say x (the lambda variable), but then a : α does not match the type x expected

[Mario Carneiro]

To resolve this, you can abstract a in some way. For example if the goal was struct.mk α a = struct.mk α a you could revert a to get \all a : α, struct.mk α a = struct.mk α a, and now uniformly rewriting α with x will not break typecorrectness

[Keeley Hoek]

Aha! great, thanks. On the other hand

example : false := begin
  have ss : struct.mk α a = struct.mk α a := rfl,
  simp only [h] at ss,
end

does work (ish, I guess simp automatically does something like cases when it sees an inductive constructor too, but modulo that). So is simp programmed to deal with situations like this? I always imagined it was doing something like a rw at every step...

[Mario Carneiro]

This, by the way, is why rw always rewrites a value everywhere; you are much more likely to get a type correct result than if you just rewrite half of the variables

[Keeley Hoek]

Yep, sure!

[Mario Carneiro]

Right, simp works here because it's using a completely different strategy for rewriting

[Mario Carneiro]

It uses congr lemmas

[Mario Carneiro]

Actually i'm not sure it does work in this example, I would expect it does nothing

[Keeley Hoek]

Well the result is

1 goal
ss : β = β ∧ a == a
⊢ false

[Keeley Hoek]

So I guess it worked?

[Mario Carneiro]

Here's a better example:

constant foo (α : Type) (a : α) : ℕ

axioms (α β : Type) (a b : α) (h : α = β)

example : false := begin
  have ss : foo α a = foo α b := sorry,
  simp [h] at ss,
end

[Mario Carneiro]

now simp's heuristic stuff doesn't apply, and so it does nothing

[Keeley Hoek]

Riiight, ok. So probably it was "working" before because of doing (something like) cases on the inductive constructor first, so the type-inter-dependencies weren't around anymore?

[Keeley Hoek]

Any completely unrelated I guess, why do I get a heq after the simp application in the previous example?

[Mario Carneiro]

because the lemma it applied is struct.mk A a = struct B b <-> (A = B /\ a == b)

[Keeley Hoek]

Thanks so much Mario, as always!

[Mario Carneiro]

Here's an example of simp rewriting under a dependency, where rw would fail:

constant α : Type
constant bar : α → Prop
constant foo (a : α) : bar a → ℕ

axioms (a b : α) (h : bar a) (e : a = b)

set_option pp.proofs true
example : foo a h = 0 := begin
  simp [e],
end

[Mario Carneiro]

This works because it generates a congr lemma for every constant and when one of the arguments is a subsingleton it is clever and avoids the subgoal. Notice the lack of a a_2 = a_3 assumption in the statement of the lemma:

#eval do c <- tactic.mk_congr_lemma `(foo), tactic.trace c.type
-- ∀ (a a_1 : α), a = a_1 → ∀ (a_2 : bar a) (a_3 : bar a_1), foo a a_2 = foo a_1 a_3

[Mario Carneiro]

If we look at the congr lemma for my first example, it determines that alpha has proper dependencies so it doesn't allow it to change at all:

constant foo (α : Type) (a : α) : ℕ

axioms (α β : Type) (a b : α) (h : α = β)

#eval do c <- tactic.mk_congr_lemma `(foo), tactic.trace c.type
-- ∀ (α : Type) (a a_1 : α), a = a_1 → foo α a = foo α a_1

So that means that simp will not "see" into the α argument of foo to apply any rewrites

[Johan Commelin]

Barry Mazur wrote a couple of pages in the Notices of the AMS under the exact same title: “What is a motive?” https://www.ams.org/notices/200410/what-is.pdf

[Scott Morrison]

Maybe Mario should write an update for them.

[Jesse Michael Han]

motives: mysterious to lean users and mathematicians alike

[Mario Carneiro]

why do we really do anything?

[Jesse Michael Han]

now that i think about it, "sorry, my motive isn't type correct" is an excellent way to politely decline a request...

[Kevin Buzzard]

I have always regarded this as a failure of rw rather than anything else. As well as simp there is erw which sometimes works when rw doesn't.

[Mario Carneiro]

I'm not exactly sure what erw does, but I think it's just the same as rw with some definitional unfolding

[Wojciech Nawrocki]

I'm not sure if this is the right thread, but I noticed that generally speaking rewriting seems to work better under binders like Mario mentioned here. For example:

example {α: ℕ → Type u} (x y: ℕ) (a: α (x+y)) (b: α (y+x)) (h: a == b): true := begin
  -- i want (h: a = b)
  -- rw [nat.add_comm] at a, -- h still depends on old (a: α (x+y)) :<
  -- have h: a = b := eq_of_heq h, -- fail
  revert a b,
  rw [nat.add_comm],
  intros a b h,
  have h: a = b := eq_of_heq h, -- good

  trivial,
end

Is there a tactic to do this?