52d0f715c3
Consider
```
import Std.Tactic.ShowTerm
opaque a : Nat
opaque b : Nat
axiom a_eq_b : a = b
opaque P : Nat → Prop
set_option pp.explicit true
-- Using rw
example (h : P b) : P a := by show_term rw [a_eq_b]; assumption
```
Before, a typical proof term for `rewrite` looked like this:
```
-- Using the proof term that rw produces
example (h : P b) : P a :=
@Eq.mpr (P a) (P b)
(@id (@Eq Prop (P a) (P b))
(@Eq.ndrec Nat a (fun _a => @Eq Prop (P a) (P _a))
(@Eq.refl Prop (P a)) b a_eq_b))
h
```
which is rather round-about, applying `ndrec` to `refl`. It would be
more direct to write
```
example (h : P b) : P a :=
@Eq.mpr (P a) (P b)
(@id (@Eq Prop (P a) (P b))
(@congrArg Nat Prop a b (fun _a => (P _a)) a_eq_b))
h
```
which this change does.
This makes proof terms smaller, causing mild general speed up throughout
the code; if the brenchmarks don’t lie the highlights are
* olean size -2.034 %
* lint wall-clock -3.401 %
* buildtactic execution s -10.462 %
H'T to @digama0 for advice and help.
NB: One might even expect the even simpler
```
-- Using the proof term that I would have expected
example (h : P b) : P a :=
@Eq.ndrec Nat b (fun _a => P _a) h a a_eq_b.symm
```
but that would require non-local changes to the source code, so one step
at a time.
|
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||