bug with simp (editor's note: not a bug)

Stream: general

[Kenny Lau]

import algebra.linear_algebra.basic

variables (α β : Type) [ring α] [module α β]

example (v : lc α β) (h : v 0 = 0) : sorry :=
begin
  simp [lc] at v,
end

[Kenny Lau]

α β : Type,
_inst_1 : ring α,
_inst_2 : module α β,
v : lc α β,
h : ⇑v 0 = 0,
v : β →₀ α
⊢ sorry

[Kenny Lau]

the bug is that it creates another v

[Reid Barton]

I think it has to do with the fact that the hypothesis h depends on v, but I'm not sure what you're supposed to do about that

[Reid Barton]

dsimp works

[Mario Carneiro]

Yeah, this is not a bug. The new v cannot necessarily take the place of the old v in h

[Mario Carneiro]

dsimp allows this because the rewrite is definitional, so the new v has the same type as the old one, but if it's merely a propositionally equal type, then you may have to replace v with cast v <ugly proof> in uses of v

[Scott Morrison]

It would be nice if there was either a mode for simp, or just a cousin, that was much more aggressive about replacing later appearances of the simplified hypothesis, even if it required casts. I run into this fairly often.

[Scott Morrison]

Very often a step or two later the cast itself becomes easy to simplify, and you're back on safe ground.

[Mario Carneiro]

I think you can achieve this effect by reverting the dependent hypotheses

[Mario Carneiro]

But in my experience casts are a pain to get rid of. What kind of proof strategy causes them to be "easy to simplify"?

[Scott Morrison]

At some point I'll try to come up with a full example. But I've certainly found situations where "almost trivial" lemmas such as

lemma {u₁ u₂} parallel_transport_for_trivial_bundles {α : Sort u₁} {a b : α} {β : Sort u₂} (p : a = b) (x : β) : @eq.rec α a (λ a, β) x b p = x :=
begin
induction p,
simp,
end

cause @eq.recs to vanish away again. Right now I have to deal with some jet lag.