proof without rsimp

Stream: general

[Sean Leather]

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]

what is rsimp?

[Mario Carneiro]

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

[Sean Leather]

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

It doesn't.

[Mario Carneiro]

What are the types of things?

[Sean Leather]

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]

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

[Patrick Massot]

something he can copy-paste

[Mario Carneiro]

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

[Sean Leather]

Right, I see. I can try.

[Sean Leather]

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]

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

[Mario Carneiro]

You don't need it

[Mario Carneiro]

@[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]

[Sean Leather]

Very nice.

[Mario Carneiro]

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

[Sean Leather]

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]

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

human speed :-)

[Sean Leather]

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.

[Kenny Lau]

2018-07-17.png

[Kenny Lau]

irreproducible

[Kevin Buzzard]

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
 4694ms    87.9%   interaction_monad_orelse
 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
  219ms     4.1%   _private.3989697749.add_lemma._lambda_1
  214ms     4.0%   _private.410121379.to_hinst_lemmas._main._lambda_3
  214ms     4.0%   hinst_lemma.mk_from_decl_core
  214ms     4.0%   interaction_monad.monad._lambda_9
   38ms     0.7%   _private.410121379.to_hinst_lemmas._main._lambda_2
    5ms     0.1%   hinst_lemmas.add
    2ms     0.0%   name_set.contains
    1ms     0.0%   attribute.get_instances

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

2018-07-17-1.png

[Kenny Lau]

reproduced

[Sean Leather]

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