Crash with induction_on'

Stream: general

[Stuart Presnell]

The following #mwe immediately crashes for me with Server has stopped due to signal SIGSEGV. If I comment out the induction line then it compiles ok.

import data.multiset.basic

variables (α β : Type*)

lemma multiset.map_insert (S : multiset α) (a : α) (g : α → β) :
  multiset.map g (insert a S) = insert (g a) (multiset.map g S) :=
begin
  induction S using multiset.induction_on',
  sorry,
end

[Patrick Johnson]

Unable to reproduce.
Windows 10, Lean: v3.38.0, Mathlib: 7ee41aab
I see error:

induction tactic failed, failed to create new goal

[Stuart Presnell]

And then, for no reason I can diagnose, it will sometimes stop causing a crash and will instead simply raise the error induction tactic failed, failed to create new goal.

[Julian Berman]

Segfaults here too, even with just lean foo.lean.

[Stuart Presnell]

And then closing and re-starting VS Code reproduces the crashing behaviour.

[Kyle Miller]

A workaround is to use the refine tactic. I've run into induction bugs before (not crashes, but incorrect types), and that's generally been the advice.

[Eric Rodriguez]

segfaults on my M1 mac, doesn't segfault on my Windows machine

[Julian Berman]

Thread 2 Crashed:
0   lean                                   0x104905ce0 lean::rb_map<lean::name, lean::metavar_decl, lean::name_quick_cmp>::find(lean::name const&) const + 52
1   lean                                   0x104905cd0 lean::rb_map<lean::name, lean::metavar_decl, lean::name_quick_cmp>::find(lean::name const&) const + 36
2   lean                                   0x104905b9c lean::metavar_context::find_metavar_decl(lean::expr const&) const + 28
3   lean                                   0x1049c4248 lean::intron_core(lean::environment const&, lean::options const&, lean::metavar_context&, lean::expr const&, unsigned int, lean::buffer<lean::name, 16u>&, std::__1::function<lean::name (lean::local_context const&, lean::name const&)> const&) + 100
4   lean                                   0x1049f4040 lean::set_intron(lean::expr&, lean::type_context_old&, lean::options const&, lean::expr const&, unsigned int, lean::optional<lean::name> const&, lean::list<lean::name>&, lean::buffer<lean::name, 16u>&, bool) + 272
5   lean                                   0x1049f125c lean::induction(lean::environment const&, lean::options const&, lean::transparency_mode const&, lean::metavar_context&, lean::expr const&, lean::expr const&, lean::name const&, lean::list<lean::name>&, lean::list<lean::list<lean::expr> >*, lean::list<lean::rb_map<lean::name, lean::expr, lean::name_quick_cmp> >*, lean::buffer<lean::name, 16u>&) + 4684
6   lean                                   0x1049f4490 lean::induction_tactic_core(lean::transparency_mode const&, lean::expr const&, lean::name const&, lean::list<lean::name> const&, lean::tactic_state const&) + 284
7   lean                                   0x1049f5188 lean::tactic_induction(lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&) + 216
8   lean                                   0x104be691c lean::vm_state::invoke_fn(void*, unsigned int) + 2488
9   lean                                   0x104be9334 lean::vm_state::invoke_cfun(lean::vm_decl const&) + 96
10  lean                                   0x104be7f20 lean::vm_state::run() + 1968
11  lean                                   0x104be750c lean::vm_state::invoke_closure(lean::vm_obj const&, unsigned int) + 328
12  lean                                   0x104be9da0 lean::vm_state::invoke(lean::vm_obj const&, lean::vm_obj const&) + 600
13  lean                                   0x1049b3be0 lean::tactic_with_ast(lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&) + 148
14  lean                                   0x104be658c lean::vm_state::invoke_fn(void*, unsigned int) + 1576
15  lean                                   0x104be9334 lean::vm_state::invoke_cfun(lean::vm_decl const&) + 96
16  lean                                   0x104be7f20 lean::vm_state::run() + 1968
17  lean                                   0x104be750c lean::vm_state::invoke_closure(lean::vm_obj const&, unsigned int) + 328
18  lean                                   0x104be9da0 lean::vm_state::invoke(lean::vm_obj const&, lean::vm_obj const&) + 600
19  lean                                   0x104c27a20 lean::scope_trace(lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&, lean::vm_obj const&) + 308
20  lean                                   0x104be658c lean::vm_state::invoke_fn(void*, unsigned int) + 1576
21  lean                                   0x104be9334 lean::vm_state::invoke_cfun(lean::vm_decl const&) + 96
22  lean                                   0x104be7f20 lean::vm_state::run() + 1968
23  lean                                   0x104be750c lean::vm_state::invoke_closure(lean::vm_obj const&, unsigned int) + 328
24  lean                                   0x104be9da0 lean::vm_state::invoke(lean::vm_obj const&, lean::vm_obj const&) + 600
25  lean                                   0x1049a3d04 lean::interaction_monad<lean::tactic_state>::evaluator::operator()(lean::expr const&, lean::buffer<lean::vm_obj, 16u> const&, lean::tactic_state const&) + 372
26  lean                                   0x104a708d4 lean::tactic_evaluator::operator()(lean::expr const&, lean::buffer<lean::vm_obj, 16u> const&, lean::tactic_state const&) + 28
27  lean                                   0x1049a4254 lean::interaction_monad<lean::tactic_state>::evaluator::operator()(lean::expr const&, lean::tactic_state const&) + 80
28  lean                                   0x104dd11a8 lean::elaborator::invoke_tactic(lean::expr const&, lean::expr const&) + 472
29  lean                                   0x104dd1c58 lean::elaborator::synthesize_using_tactics() + 156
30  lean                                   0x104db8334 lean::elaborator::synthesize() + 88
31  lean                                   0x104dd3330 lean::elaborator::elaborate_with_type(lean::expr const&, lean::expr const&) + 528
32  lean                                   0x104e0c540 lean::task_builder<lean::expr>::base_task_imp<lean::single_definition_cmd_core(lean::parser_info&, lean::decl_cmd_kind, lean::ast_data*, lean::cmd_meta)::$_0::operator()(lean::expr) const::'lambda'()>::execute(void*) + 704
33  lean                                   0x10496e6c8 lean::library_scopes_imp::execute(void*) + 100
34  lean                                   0x1047a1ac0 lean::cancellable_task_imp::execute(void*) + 60
35  lean                                   0x1047e2eb8 lean::task_cell<lean::expr>::execute() + 144
36  lean                                   0x1047a14c4 lean::task_queue::execute(std::__1::shared_ptr<lean::gtask_cell> const&) + 396
37  lean                                   0x10496c5dc std::__1::__function::__func<lean::mt_task_queue::spawn_worker()::$_2, std::__1::allocator<lean::mt_task_queue::spawn_worker()::$_2>, void ()>::operator()() + 668
38  lean                                   0x10479e098 lean::lthread::imp::_main(void*) + 44
39  libsystem_pthread.dylib                0x190ca5240 _pthread_start + 148
40  libsystem_pthread.dylib                0x190ca0024 thread_start + 8

[Eric Rodriguez]

it's also platform specific, yipee

[Stuart Presnell]

Just to confirm that it's not specific to multiset, the following also crashes when the induction line is uncommented:

import algebra.big_operators.basic

variables (α β : Type*) [comm_monoid β]

example {S : finset α} (g1 g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) :
  S.prod g1 ∣ S.prod g2 :=
begin
  -- induction S using finset.induction_on',
  sorry
end

[Stuart Presnell]

(In fact this finset example is where I first encountered this problem while editing #11521, but at the time I couldn't reproduce it.)

[Kyle Miller]

Here's the refine:

import data.multiset.basic

variables (α β : Type*)

lemma multiset.map_insert (S : multiset α) (a : α) (g : α → β) :
  multiset.map g (insert a S) = insert (g a) (multiset.map g S) :=
begin
  revert a,
  refine multiset.induction_on' S _ (λ b s hb hs ih, _),
  { sorry },
  { intro a,
    sorry },
end

[Kyle Miller]

@Stuart Presnell If you change that example to lemma foo does it still crash?

[Stuart Presnell]

It does

[Stuart Presnell]

Eric Rodriguez said:

segfaults on my M1 mac, doesn't segfault on my Windows machine

What editor are you using on the Windows machine? Does the example crash when the editor is closed and newly re-started?

[Eric Rodriguez]

Stuart Presnell said:

Eric Rodriguez said:

segfaults on my M1 mac, doesn't segfault on my Windows machine

What editor are you using on the Windows machine? Does the example crash when the editor is closed and newly re-started?

in VSCode 1.63.2, mathlib PR 946454a830, this does not crash on my windows machine. (Lean 3.38.0). On my m1 mac, it does; exact same Lean version (hand compiled because I don't want rosetta, but otherwise the same)

[Mario Carneiro]

Don't use induction using, it's flaky and more broken than I thought

[Julian Berman]

<deleted, I didn't realize there were more>

[Yakov Pechersky]

What happens if you say classical before induction using, that might help?

[Eric Wieser]

Is the lean4 version of induction using better?

[Stuart Presnell]

Yakov Pechersky said:

What happens if you say classical before induction using, that might help?

Thanks for the suggestion. I've just tried that and both of the above examples still crash with the addition of classical.