Zulip Chat Archive

Stream: general

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


view this post on Zulip Cyril Cohen (Jul 25 2019 at 11:24):

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?

view this post on Zulip Mario Carneiro (Jul 25 2019 at 12:07):

There is a community lean tactic for this

view this post on Zulip Mario Carneiro (Jul 25 2019 at 12:09):

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

view this post on Zulip Cyril Cohen (Jul 25 2019 at 12:38):

There is a community lean tactic for this

should I install lean_community/lean master to access it?

view this post on Zulip Mario Carneiro (Jul 25 2019 at 12:39):

I think there are nightlies

view this post on Zulip Mario Carneiro (Jul 25 2019 at 12:41):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 12:43):

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

view this post on Zulip Cyril Cohen (Jul 25 2019 at 12:51):

Thanks

view this post on Zulip Cyril Cohen (Jul 25 2019 at 12:55):

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

view this post on Zulip Mario Carneiro (Jul 25 2019 at 12:55):

both

view this post on Zulip Mario Carneiro (Jul 25 2019 at 12:56):

we haven't made any backwards incompatible changes yet

view this post on Zulip Cyril Cohen (Jul 25 2019 at 12:56):

both

so noone used add_ginductive so far?

view this post on Zulip Mario Carneiro (Jul 25 2019 at 12:57):

not in any mathlib tactics

view this post on Zulip Cyril Cohen (Jul 25 2019 at 12:57):

ok...

view this post on Zulip Mario Carneiro (Jul 25 2019 at 12:57):

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

view this post on Zulip Cyril Cohen (Jul 25 2019 at 14:55):

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)

view this post on Zulip Bryan Gin-ge Chen (Jul 25 2019 at 16:59):

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

view this post on Zulip Cyril Cohen (Jul 26 2019 at 08:53):

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

view this post on Zulip Mario Carneiro (Jul 26 2019 at 09:03):

lol did someone leave some debug code in the build?

view this post on Zulip Bryan Gin-ge Chen (Jul 26 2019 at 15:19):

Looks like the foo bar stuff is coming from here.

view this post on Zulip Mario Carneiro (Jul 26 2019 at 17:08):

oh dear it was me

view this post on Zulip Mario Carneiro (Jul 26 2019 at 20:16):

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

view this post on Zulip Wojciech Nawrocki (Jul 26 2019 at 20:19):

Spider-Man-meme.jpeg


Last updated: May 13 2021 at 05:21 UTC