if-then-else & simp

Stream: general

[Alexander Bentkamp]

Hello, I stumbled upon a curious behavior of simp with if-then-else:

Here, simp cannot resolve the if-then-else:

example {γ : Type*} [decidable_eq γ] (x : γ) (a b : ℝ) (as : γ → ℝ)
(h : as = λ(k : γ), ite (x = k) a b) : as x = a :=
begin
  simp [h],   -- ⊢ ite (x = x) a b = a
  sorry
end

Here, it can:

begin
  rw h,
  simp
end

But it looks like rw h does exactly the same as simp [h] above.

Does someone know what's going on here?

[Mario Carneiro]

I don't think they are actually different, seeing as this works too:

begin
  simp [h],   -- ⊢ ite (x = x) a b = a
  simp,
end

[Mario Carneiro]

I suspect that the beta redex is causing simp to not see the second simplification until after the first is complete

[Alexander Bentkamp]

Oh, that makes sense. Thank you.

[Kevin Buzzard]

It doesn't make sense to me. What is "beta redex"?

[Mario Carneiro]

(\lam x, A) B

[Kevin Buzzard]

oh -- it's the same as beta reduction?

[Mario Carneiro]

beta reduction is the simplification of beta redexes

[Mario Carneiro]

a beta redex is a thing that is subject to beta reduction

[Kevin Buzzard]

Aah I see. OK I've now googled. Thanks.