Zulip Chat Archive

Stream: general

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


Kenny Lau (Mar 06 2018 at 01:21):

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 (Mar 06 2018 at 01:21):

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

Kenny Lau (Mar 06 2018 at 01:21):

the bug is that it creates another v

Reid Barton (Mar 06 2018 at 01:46):

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 (Mar 06 2018 at 01:50):

dsimp works

Mario Carneiro (Mar 06 2018 at 02:54):

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

Mario Carneiro (Mar 06 2018 at 02:55):

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 (Mar 06 2018 at 05:25):

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 (Mar 06 2018 at 05:26):

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

Mario Carneiro (Mar 06 2018 at 05:29):

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

Mario Carneiro (Mar 06 2018 at 06:19):

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 (Mar 06 2018 at 06:33):

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.


Last updated: Dec 20 2023 at 11:08 UTC