## Stream: general

### Topic: rsimp

#### Jesse Michael Han (May 18 2019 at 21:36):

What is rsimp, how does it work, and why is it so slow?

#### Jesse Michael Han (May 18 2019 at 21:55):

prompted by the discussion about the simp lemma eq_self_iff_true, I was playing around with simp and its occasional inability to prove definitional equalities (depending on what is marked reducible, it seems)

i'm surprised that below {[smt] close} closes the goal, but cc doesnt (i thought they had the same strength)

import tactic.squeeze

def A : ℕ := 0

def B : ℕ := A

example : A = B :=
rfl -- works

example : A = B :=
by rsimp -- works

example : A = B :=
by {[smt] eblast} -- works

example : A = B :=
by {[smt] close} -- works

example : A = B :=
by cc -- fails

example : A = B :=
by simp -- fails


#### Mario Carneiro (May 19 2019 at 00:36):

I know the r stands for "robust", but I have not looked at the implementation. It's almost never used

#### Wojciech Nawrocki (Jun 21 2019 at 12:28):

why is it so slow

Is rsimp meant to be painfully slow? I just tried it on a single-hypothesis-with-the-goal-being-just-the-hypothesis example and it takes 10 seconds.

#### Wojciech Nawrocki (Jun 21 2019 at 12:30):

Regarding what rsimp actually is, it's described in chapter 2 here. It more or less tries to find the simplest form of every expression using congruence closure and rewrites it to that.

Last updated: Dec 20 2023 at 11:08 UTC