rsimp

Stream: general

[Jesse Michael Han]

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

[Jesse Michael Han]

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]

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

[Wojciech Nawrocki]

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]

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.