Zulip Chat Archive

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]

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

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

Kevin Buzzard (Jul 16 2018 at 18:35):

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.

Kenny Lau (Jul 17 2018 at 06:27):

2018-07-17.png

Kenny Lau (Jul 17 2018 at 06:27):

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
 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 (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

Kenny Lau (Jul 17 2018 at 07:10):

2018-07-17-1.png

Kenny Lau (Jul 17 2018 at 07:10):

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