Modify a hypothesis referenced by `classical.some`

Stream: new members

[Patrick Johnson]

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]

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]

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]

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

[Kyle Miller]

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]

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]

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]

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]

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]

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

[Johan Commelin]

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]

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]

@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]

@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]

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]

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]

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

[Kyle Miller]

Why the "but"?

[Kyle Miller]

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]

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]

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]

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]

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]

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