# Zulip Chat Archive

## Stream: general

### Topic: simplify_proof

#### Scott Morrison (Jun 06 2018 at 09:04):

At some point Mario told me how to write a "simplify_proof" tactic, but in my fiddling with it I seem to have lost the essential magic step where the new, simplified proof is actually installed in place of the original proof:

open tactic meta def simplify_proof {α} (tac : tactic α) : tactic α := λ s, let tac1 : tactic (α × expr) := do a ← tac, r ← result, lems ← simp_lemmas.mk_default, dr ← (lems.dsimplify [] r <|> pure r), pure (a, dr) in match tac1 s with | result.success (a, r) s' := (result >>= unify r >> pure a) s' | result.exception msg e s' := result.exception msg e s' end

#### Scott Morrison (Jun 06 2018 at 09:04):

Or am I misunderstanding what this should do?

#### Scott Morrison (Jun 06 2018 at 09:11):

Ah, got it! Somewhere along the way I put a spurious ' at the end of the `result.success`

line, preventing the tactic from doing its time travel trick.

#### Kevin Buzzard (Jun 06 2018 at 09:19):

I sometimes wonder what `simp`

is doing, and I know that I can look, but I can never be bothered. I vaguely suspect there might be times where replacing a call to `simp`

with a call to what it actually does might be better -- am I just living in a dream world do you think? (in the sense that it's unlikely to make any noticeable difference other than obfusctating my code?)

Last updated: Aug 03 2023 at 10:10 UTC