## Stream: new members

### Topic: Modify a hypothesis referenced by classical.some

#### Patrick Johnson (Dec 07 2021 at 07:53):

MWE:

import tactic
open classical

example (h :  (x : ), (x = 0) = true) : some h = 0 := begin
simp_rw eq_true at h,
sorry,
end

The simp_rw tactic creates a new premise instead of updating the existing premise h. I guess that's because the goal references h. Working backwards is possible:

example (h :  (x : ), (x = 0) = true) : some h = 0 := begin
rw ←@eq_true (some h = 0),
apply some_spec h,
end

But if the goal is more complicated, it is intractable. How to deal with this situation?

#### Kyle Miller (Dec 07 2021 at 08:02):

revert and generalize can be useful:

example (h :  (x : ), (x = 0) = true) : some h = 0 := begin
have := some_spec h,
revert this,
generalize : some h = n,
simp,
end

#### Kyle Miller (Dec 07 2021 at 08:05):

The idea is to put everything into the goal that has some kind of dependence on some value (via revert), and then you can generalize that value out of everything simultaneously.

#### Marcus Rossel (Dec 07 2021 at 08:06):

I recall the generalize_proofs tactic also being useful for these kinds of problems.

#### Kyle Miller (Dec 07 2021 at 08:14):

It's helpful to know roughly how rewriting actually works in Lean. It needs to create the motive for eq.rec, which is sort of an expression with holes, and then given this motive and a proof that a = b, what eq.rec gives you is that plugging in a into all the holes is equal to plugging in b into all the holes.

When you rw h where h : a = b, then the tactic creates a motive from the goal by looking for all the a's and turning them into holes. When you rw h at h', then it basically has to revert h', do the rewrite (but restricting its search for a's inside the h' part of the goal), and then intro h'. If h depends on h', then the revert would fail, and instead h' is duplicated first. At least, this is my understanding.

#### Kyle Miller (Dec 07 2021 at 08:19):

So, said another way, the idea with using revert and generalize is to more carefully control how rw h at h' operates -- you can rewrite the goal and multiple hypotheses simultaneously this way.

#### Patrick Johnson (Dec 07 2021 at 08:24):

Thanks. But it doesn't work if the goal also contains some_spec:

example
(h :  (x : ), (x = 0) = true) :
some h = 0  some_spec h = some_spec h :=
begin
have h₁ := some_spec h,
revert h₁,
generalize : some h = n,
simp,
end

Produces error:

generalize tactic failed, result is not type correct
nested exception message:
check failed, application type mismatch
[check] application type mismatch at
eq _
argument type
(λ (x : ), x = 0 = true) (some h)
expected type
n = 0 = true

Of course in this lemma we can use split, but I am talking in general.

#### Kyle Miller (Dec 07 2021 at 08:26):

example
(h :  (x : ), (x = 0) = true) :
some h = 0  some_spec h = some_spec h :=
begin
generalize_proofs h',
have h₁ := some_spec h,
revert h₁,
simp,
end

#### Kyle Miller (Dec 07 2021 at 08:35):

The problem is that some_spec h contains some h in its type, and it's not possible to create a motive in this situation. It's possible if you first remove some_spec h from the expression, since then it can no longer require some h literally being there.

#### Eric Rodriguez (Dec 07 2021 at 08:42):

"motive" = "expression with metavariables", right? how do the dreaded "motive is not type-correct" errors fit into this?

#### Johan Commelin (Dec 07 2021 at 08:57):

I have no idea what a motive is precisely. My mental model is that it's the combination (term_expr, type_expr). When that error shows up, something doesn't typecheck or is not a well-formed formula in some sense.

#### Kyle Miller (Dec 07 2021 at 08:59):

I still find "motive not type correct" to be somewhat mysterious, but I think many cases are related to my last comment. It can happen when the holes punched out are actually implied by other parts of the expression.

rw some_spec h in this example gets "motive is not type correct", but I don't understand the motive it comes up with (I assume that's what it prints) or what's type incorrect about it:

λ (_a : Prop), (some h = 0  some_spec h = some_spec h) = (_a  some_spec h = some_spec h)

#### Kyle Miller (Dec 07 2021 at 09:09):

@Johan Commelin My understanding is that the definition of a motive is this argument of the recursor:

example {a b c : } (h : a = b + c) : a * a + a = (b + c) * a + (b + c) :=
@eq.rec _ _ (λ (m : ), a * a + a = m * a + m) rfl _ h
-- ^ motive

#### Kyle Miller (Dec 07 2021 at 09:13):

@Eric Rodriguez In this example, m is like a metavariable for the expression a * a + a = m * a + m. (Conceptually it's an expression with a metavariable, but it's also just a lambda expression.)

#### Kyle Miller (Dec 07 2021 at 09:19):

Here's a "motive not type correct" I've run into frequently:

example (α β : Type) [fintype α] [fintype β] (h : α = β) :
fintype.card α = fintype.card β :=
begin
rw h, -- rewrite tactic failed, motive is not type correct
end

Having it print implicit arguments, this is the motive it comes up with:

λ (x : Type),
(@fintype.card α _inst_1 = @fintype.card β _inst_2)
= (@fintype.card x _inst_1 = @fintype.card β _inst_2)

That @fintype.card x _inst_1 is the issue. The _inst_1 argument is fintype α, not fintype x, so there's a type error.

(Side note: it seems that rw rewrites by taking the current goal g (even if it's an equality) and creating motives for g = g, putting holes in the second g.)

#### Kyle Miller (Dec 07 2021 at 09:36):

simp [h] works here, but then you have to convert rfl

example (α β : Type) [fintype α] [fintype β] (h : α = β) :
fintype.card α = fintype.card β :=
begin
simp_rw [h],
convert rfl,
end

#### Eric Rodriguez (Dec 07 2021 at 09:55):

But I think that's to do with the instances being wrong completely; does rw at * work? Subst should, too

Why the "but"?

#### Kyle Miller (Dec 07 2021 at 10:01):

I doubt rw at * would work because I'm pretty sure it does rw one at a time. subst is more likely to work since it's basically reverting everything before creating its motive for the rewrite (at least, according to how I think it works)

#### Kyle Miller (Dec 07 2021 at 10:02):

rw does work if you revert the instances:

example (α β : Type) [fintype α] [fintype β] (h : α = β) :
fintype.card α = fintype.card β :=
begin
tactic.unfreeze_local_instances,
revert _inst_1 _inst_2,
-- ∀ [_inst_1 : fintype α] [_inst_2 : fintype β], @fintype.card α _inst_1 = @fintype.card β _inst_2
rw h,
-- ∀ [_inst_1 : fintype β] [_inst_2 : fintype β], @fintype.card β _inst_1 = @fintype.card β _inst_2
intros, congr,
end

#### Eric Rodriguez (Dec 07 2021 at 10:13):

rw at * creates a goal that the instances are equal, which seems sensible to me. The reason I said but is because it seems like a pretty transparent case, imo; if you just do a "dumb" rw then the goal becomes @fintype.card ‹fintype α› β = @fintype.card ‹fintype β› β, which is clear nonsense. simp_rw is a bit cleverer and turns the lhs into @fintype.card (h.rec ‹fintype α›) β.

#### Eric Rodriguez (Dec 07 2021 at 10:13):

Also, interestingly rw at * didn't need to unfreeze instances; I worry this is a bug, as whenever I've rewritten instances without unfreezing I've gotten the weirdest behaviour possible...

#### Kyle Miller (Dec 07 2021 at 10:17):

Eric Rodriguez said:

if you just do a "dumb" rw then the goal becomes @fintype.card ‹fintype α› β = @fintype.card ‹fintype β› β, which is clear nonsense.

Exactly, I was giving you simple example of "motive not type correct" where it's clear why the motive is not type correct.

#### Eric Rodriguez (Dec 07 2021 at 10:18):

also, never mind about rw at * working, I was seeing ghosts

Last updated: Dec 20 2023 at 11:08 UTC