## Stream: general

### Topic: proof without rsimp

#### Sean Leather (Jul 16 2018 at 14:15):

Any suggestion on how to prove this? rsimp works, but I'm guessing there's a better way.

α : Type u_1,
n : ℕ,
i j : fin n,
a : fin n → α,
h : i = j
⊢ eq.rec (a j) ((eq.rec (iff.refl (i = j)) (eq.trans (congr (congr_arg eq h) (eq.refl j)) (propext (eq_self_iff_true j)))).mpr true.intro) = a j


#### Kenny Lau (Jul 16 2018 at 14:16):

what is rsimp?

#### Mario Carneiro (Jul 16 2018 at 14:18):

I can't test because that's not a MWE but I think rfl should work

#### Sean Leather (Jul 16 2018 at 14:18):

I can't test because that's not a MWE but I think rfl should work

It doesn't.

#### Mario Carneiro (Jul 16 2018 at 14:19):

What are the types of things?

#### Sean Leather (Jul 16 2018 at 14:19):

what is rsimp?

I'm not sure, but it's slow. I reworked a couple of proofs in mathlib to not use it because it slowed down the build. :simple_smile:

#### Sean Leather (Jul 16 2018 at 14:21):

@Mario Carneiro Why isn't it a MWE? That's the entire context. What else do you need?

#### Patrick Massot (Jul 16 2018 at 14:21):

something he can copy-paste

#### Mario Carneiro (Jul 16 2018 at 14:21):

DId you try making an example out of that? the motive of the eq.rec isn't inferrable

#### Sean Leather (Jul 16 2018 at 14:23):

Right, I see. I can try.

#### Sean Leather (Jul 16 2018 at 14:26):

This is my current hacky proof progress:

variables {α : Type*} {n : ℕ}

def modify (a : array n α) (i : fin n) (f : α → α) : array n α :=
a.write i $f$ a.read i

@[simp] theorem modify_id (a : array n α) (i : fin n) : a.modify i id = a :=
by simp [modify, read, write, d_array.write, d_array.read];
cases a with a;
congr;
funext j;
dsimp; dsimp at a;
by_cases h : i = j; simp [h]; dsimp


#### Sean Leather (Jul 16 2018 at 14:27):

Oh, I just realized I don't have decidable_eq α. Perhaps that's what's missing?

#### Mario Carneiro (Jul 16 2018 at 14:28):

You don't need it

#### Mario Carneiro (Jul 16 2018 at 14:33):

@[simp] theorem modify_id (a : array n α) (i : fin n) : a.modify i id = a :=
array.ext \$ λ j, by by_cases i = j; simp [h, modify]


Very nice.

#### Mario Carneiro (Jul 16 2018 at 14:34):

Don't gratuitously unfold things, it often makes your life harder

#### Sean Leather (Jul 16 2018 at 14:34):

Huh, looks like my hacks were doing something similar:

protected lemma ext {a b : d_array n α} (h : ∀ i, read a i = read b i) : a = b :=
by cases a; cases b; congr; exact funext h


#### Sean Leather (Jul 16 2018 at 14:35):

Don't gratuitously unfold things, it often makes your life harder

Indeed. I didn't think to look for an extensionality lemma.

#### Kevin Buzzard (Jul 16 2018 at 18:34):

what is rsimp?

I'm not sure, but it's slow. I reworked a couple of proofs in mathlib to not use it because it slowed down the build. :simple_smile:

set_option profiler true
example : true := by rsimp

elaboration: tactic execution took 2.91s
num. allocated objects:  6337
num. allocated closures: 4935


human speed :-)

#### Sean Leather (Jul 17 2018 at 06:23):

set_option profiler true
example : true := by rsimp

elaboration: tactic execution took 2.91s
num. allocated objects:  6337
num. allocated closures: 4935


The allocation results make sense. When I looked at the generated proof terms of some rsimp usages, they included tons of gratuitous reflexivity, commutativity, and transitivity terms. I bet that's the case here, too.

2018-07-17.png

irreproducible

#### Kevin Buzzard (Jul 17 2018 at 07:04):

tactic compilation != tactic execution

kb_value.lean:302:8: information
parsing took 0.0767ms
kb_value.lean:302:21: information
elaboration: tactic compilation took 2.74ms
kb_value.lean:302:21: information tactic profile data
elaboration: tactic execution took 5.34s
num. allocated objects:  7164
num. allocated closures: 5642
5343ms   100.0%   scope_trace
5343ms   100.0%   _interaction._lambda_2
5343ms   100.0%   tactic.istep
5343ms   100.0%   tactic.step
5343ms   100.0%   tactic.rsimp
5343ms   100.0%   tactic.focus1
5343ms   100.0%   tactic.istep._lambda_1
5343ms   100.0%   using_smt
4477ms    83.8%   rsimp.collect_implied_eqs._lambda_4
4475ms    83.8%   rsimp.collect_implied_eqs._lambda_1
4475ms    83.8%   smt_tactic.iterate_at_most._main._lambda_3
4475ms    83.8%   smt_tactic.ematch_core
866ms    16.2%   smt_state.mk
225ms     4.2%   rsimp_attr._lambda_1
224ms     4.2%   _private.410121379.to_hinst_lemmas._main._lambda_5
224ms     4.2%   to_hinst_lemmas
214ms     4.0%   _private.410121379.to_hinst_lemmas._main._lambda_3
214ms     4.0%   hinst_lemma.mk_from_decl_core
38ms     0.7%   _private.410121379.to_hinst_lemmas._main._lambda_2
2ms     0.0%   name_set.contains
1ms     0.0%   attribute.get_instances


#### Kevin Buzzard (Jul 17 2018 at 07:04):

Profiler seems to be giving out strictly less info in javascript version

#### Kevin Buzzard (Jul 17 2018 at 07:06):

@Kenny Lau try #check id (or indeed anything) after the rsimp in the online version

2018-07-17-1.png

reproduced

#### Sean Leather (Jul 17 2018 at 07:11):

Okay, so the allocations aren't what I thought they might be.

Last updated: Dec 20 2023 at 11:08 UTC