What is the tactic to generate`drec`, `cases_on`, etc?

Stream: general

[Cyril Cohen]

In interactive mode, drec, cases_on,... are generated at inductive declaration

inductive myeq1 {α : Sort u} : α → α → Prop | refl (a : α) : myeq1 a a
#print myeq1.drec
#print myeq.cases_on

However in tactic mode, they are not!

import tactic
open expr native tactic

run_cmd (do
  l ← mk_fresh_name, let u := level.param l,
  add_inductive "myeq" [l] 1
    (pi "α" binder_info.implicit (sort u)
    $ pi "a" binder_info.default (var 0)
    $ pi "a" binder_info.default (var 1) $ sort level.zero)
   [(("myeq" : name) ++ "refl",
    pi "α" binder_info.implicit (sort u)
    $ pi "a" binder_info.default (var 0)
    $ mk_app (const "myeq" [u]) [var 1, var 0, var 0])
   ])

#print myeq
#print myeq.drec /- not found -/
#print myeq.cases_on /- not found -/

How to generate them or call a tactic that does?

[Mario Carneiro]

There is a community lean tactic for this

[Mario Carneiro]

https://github.com/leanprover-community/lean/blob/master/library/init/meta/environment.lean#L91-L107

[Cyril Cohen]

There is a community lean tactic for this

should I install lean_community/lean master to access it?

[Mario Carneiro]

I think there are nightlies

[Mario Carneiro]

https://github.com/leanprover-community/lean-nightly/releases/tag/nightly-2019-07-15

[Mario Carneiro]

The alternative for stock lean is to produce the necessary inductive command as a text expression and call a parser command to splice it into the file

[Cyril Cohen]

Thanks

[Cyril Cohen]

Is mathlib supposed to be built on top of lean 3.4.2 or lean-community/lean master?

[Mario Carneiro]

both

[Mario Carneiro]

we haven't made any backwards incompatible changes yet

[Cyril Cohen]

both

so noone used add_ginductive so far?

[Mario Carneiro]

not in any mathlib tactics

[Cyril Cohen]

ok...

[Mario Carneiro]

Right now most people still use 3.4.2. We want to make it worth switching

[Cyril Cohen]

OK... now this makes my community lean master crash...

import tactic
open expr native tactic

run_cmd (do
  l ← mk_fresh_name,
  let u := level.param l,
  let params := [(sort u : expr)],
  let ty : expr := pi "a" binder_info.default (var 0)
    $ pi "a" binder_info.default (var 1) $ sort level.zero,
  let ctorty : expr := pi "a" binder_info.default (var 0)
    $ mk_app (const `myeq [u]) [var 1, var 0, var 0],
  let inds := [((`myeq, ty),
    [{environment.intro_rule . constr := `refl, type := ctorty}])],
  updateex_env $ λe, e.add_ginductive options.mk [l] params inds ff)

[Bryan Gin-ge Chen]

My debug build says that this assert is failing before it crashes.

[Cyril Cohen]

I reduced the crash to this,

import tactic
open expr native tactic

run_cmd do
  let ty : expr := sort level.zero,
  updateex_env $ λe,
    e.add_ginductive options.mk [] [ty] [(("test", ty), [])] ff

This goes through

import tactic
open expr native tactic

run_cmd do
  let ty : expr := sort level.zero,
  updateex_env $ λe,
    e.add_ginductive options.mk [] [] [(("test", ty), [])] ff /- removed parameter ty -/

but I have this strange debug/warning/error looping in the output buffer:

cannot parse: foo bar
cannot parse: bar foo bar

[Mario Carneiro]

lol did someone leave some debug code in the build?

[Bryan Gin-ge Chen]

Looks like the foo bar stuff is coming from here.

[Mario Carneiro]

oh dear it was me

[Mario Carneiro]

there is a new nightly out at https://github.com/leanprover-community/lean-nightly/releases/tag/nightly-2019-07-26 without the foo bar

[Wojciech Nawrocki]

Spider-Man-meme.jpeg