Zulip Chat Archive

Stream: general

Topic: cases


view this post on Zulip Jakob von Raumer (May 02 2018 at 12:46):

I know this is fuzzy as hell, but I've run into the problem that when writing an automated tactic, cases fails for a goal in which it succeeds when I run cases manually. It fails with cases tactic failed, it is not applicable to the given hypothesis.

view this post on Zulip Mario Carneiro (May 02 2018 at 12:47):

and what is the hypothesis?

view this post on Zulip Mario Carneiro (May 02 2018 at 12:47):

Keep in mind that tactic.cases and tactic.interactive.cases are not the same. Does calling the other one result in the same thing?

view this post on Zulip Jakob von Raumer (May 02 2018 at 12:52):

I'll try

view this post on Zulip Jakob von Raumer (May 02 2018 at 12:53):

Oh, so tactic.cases lacks the generalizing part?

view this post on Zulip Mario Carneiro (May 02 2018 at 12:54):

I guess so

view this post on Zulip Kevin Buzzard (May 02 2018 at 12:58):

The distinction between tactic and tactic.interactive is I think never mentioned in Programming In Lean, and caused me some grief when I discovered it the hard way (attempting to write basic tactics which ran tactics which were already there).

view this post on Zulip Kevin Buzzard (May 02 2018 at 12:58):

(but in a different namespace :-) )

view this post on Zulip Jakob von Raumer (May 02 2018 at 12:59):

So does begin ... end open tactic.interactive?

view this post on Zulip Mario Carneiro (May 02 2018 at 13:02):

Not exactly. More accurate is that if the first token in an interactive script line is token, then that is interpreted as a call to the tactic tactic.interactive.token

view this post on Zulip Mario Carneiro (May 02 2018 at 13:02):

there is no elaborate namespace resolution like normal

view this post on Zulip Jakob von Raumer (May 02 2018 at 13:05):

Hmm okay... looking at the definition of tactic.interactive.cases it doesn't look like this is the problem here...

view this post on Zulip Jakob von Raumer (May 02 2018 at 13:06):

So the goal looks like this:

cases tactic failed, it is not applicable to the given hypothesis
state:
5 goals
DC.M.A' : Type,
DC.M.lt' : DC.M.A' → DC.M.A' → Type,
DC.M.iota_A : A → DC.M.A',
DC.M.mid : Π (DC.M.x DC.M.y : DC.M.A'), DC.M.lt' DC.M.x DC.M.y → DC.M.A',
DC.M.iota_lt : Π (a b : A), lt a b → DC.M.lt' (DC.M.iota_A a) (DC.M.iota_A b),
DC.M.mid_l :
  Π (DC.M.x DC.M.y : DC.M.A') (DC.M.p : DC.M.lt' DC.M.x DC.M.y), DC.M.lt' DC.M.x (DC.M.mid DC.M.x DC.M.y DC.M.p),
DC.M.mid_r :
  Π (DC.M.x DC.M.y : DC.M.A') (DC.M.p : DC.M.lt' DC.M.x DC.M.y), DC.M.lt' (DC.M.mid DC.M.x DC.M.y DC.M.p) DC.M.y,
b : DC.SI,
x : A,
a a' : DC.Rarg DC.SI.A',
ar : DC.rel DC.SI.A' (DC.S'.iota_A x) a,
ar' : DC.rel DC.SI.A' (DC.S'.iota_A x) a'
⊢ a = a'

view this post on Zulip Jakob von Raumer (May 02 2018 at 13:06):

And the failing tactic is

b ←  i_to_expr ```(ar'),
cases_core b [],

view this post on Zulip Mario Carneiro (May 02 2018 at 13:07):

your local variables have namespaces?

view this post on Zulip Jakob von Raumer (May 02 2018 at 13:08):

They're just composite names, because.... because I didn't know what else to do with them. Actually I'd want to put all of that DC.M into parameters of some section...

view this post on Zulip Mario Carneiro (May 02 2018 at 13:09):

seems like you want a structure to hold all that

view this post on Zulip Jakob von Raumer (May 02 2018 at 13:10):

Structures aren't exposed to the meta languages, so I thought I'd spare me the work.

view this post on Zulip Mario Carneiro (May 02 2018 at 13:10):

in any case I don't recommend variable names with dots in them

view this post on Zulip Mario Carneiro (May 02 2018 at 13:11):

not sure if it's causing the problem, but it might be related

view this post on Zulip Jakob von Raumer (May 02 2018 at 13:11):

If you want, you can have a look at the mess that is my attempt to implement inductive-inductive types at https://bitbucket.org/javra/indind/src/master/

view this post on Zulip Jakob von Raumer (May 02 2018 at 13:11):

Okay, thanks for the advice

view this post on Zulip Mario Carneiro (May 02 2018 at 13:13):

Structures aren't exposed to the meta languages, so I thought I'd spare me the work.

What do you mean by this?

view this post on Zulip Jakob von Raumer (May 02 2018 at 13:16):

Since I want to create all that stuff automatically, I need to rely on what's available to the meta language which afaik is just add_inductive. I'd have to define all the projections of the structure myself, no?

view this post on Zulip Jakob von Raumer (May 02 2018 at 16:08):

Any more clues? :(

view this post on Zulip Mario Carneiro (May 02 2018 at 16:20):

It's not quite clear to me what you are trying to do, exactly. If you are doing an automatic theorem, presumably all the assumptions are generated from the inputs somehow? What is induction-induction and how does it map to your representation?

view this post on Zulip Sebastian Ullrich (May 02 2018 at 16:25):

@Jakob von Raumer It's so hacky I haven't even thought about it until now, but since you're inside a user-defined command, I guess you could define structures by assembling them as strings and passing them to the parser, like Gabriel did in hott3 https://github.com/gebner/hott3/blob/ec79a762a478f775ca03de45361e215a5ad4c129/src/hott/init/meta/support.lean#L97-L98

view this post on Zulip Sebastian Ullrich (May 02 2018 at 16:27):

This is quite fragile of course since the pretty printer doesn't always roundtrip, even with pp.all

view this post on Zulip Jakob von Raumer (May 02 2018 at 17:40):

@Mario Carneiro I can tell you all of that but it's pretty irrelevant to my problem :D In short the thing I'm trying to write gets some expressions as input and adds some stuff to the environment. So yes, the type of the theorem I'm proving is generated with some steps from these inputs. DC.SI, DC.Rarg and DC.rel are all inductive types that I add via add_inductive before I get to prove the theorem with the goal which I stated above. (Said theorem I'm adding via add_theorem_by, so I assemble the type directly but prove the theorem itself by a tactic which I'm just about to write.

The question is just why I'm getting this error message instead of cases being sucessful in destructing ar'.

view this post on Zulip Jakob von Raumer (May 02 2018 at 17:41):

@Sebastian Ullrich Oh wow, that's evil. Thanks for the pointer. But I guess I'd rather stay away from that :D

view this post on Zulip Jakob von Raumer (May 02 2018 at 18:33):

Ohhh could it be that cases just doesn't deal with inductive types that have been added using add_inductive when they lack rec_names, for example?

view this post on Zulip Jakob von Raumer (May 02 2018 at 18:34):

That would be a shame :disappointed:

view this post on Zulip Jakob von Raumer (May 03 2018 at 12:00):

I got a MNWE here:

meta def add_stuff : tactic unit :=
do tactic.add_inductive `foo [] 0 `(Type) $
   [(`bar, expr.const `foo [])]

example : unit :=
begin
  add_stuff,
  have x : foo, exact bar,
  cases x,
end

view this post on Zulip Jakob von Raumer (May 03 2018 at 16:44):

Does is_ginductive fail for the inductive types added by add_inductive? guess

view this post on Zulip Sebastian Ullrich (May 03 2018 at 16:44):

yes

view this post on Zulip Jakob von Raumer (May 03 2018 at 16:57):

So there's just no way to use cases then? :(

view this post on Zulip Sebastian Ullrich (May 03 2018 at 16:58):

You can use induction :)

view this post on Zulip Jakob von Raumer (May 03 2018 at 17:03):

induction doesn't do the generalizing itself, right?

view this post on Zulip Sebastian Ullrich (May 04 2018 at 09:09):

@Jakob von Raumer This one? https://github.com/leanprover/lean/blob/e181232c8ffd2bc2ba1b2f9799f8ac0ea0e4e505/library/init/meta/interactive.lean#L518

view this post on Zulip Jakob von Raumer (May 04 2018 at 09:40):

Ah, I only tried tactic.induction before... The problem is not generalizing the expression itself but errors like induction tactic failed, argument #8 of major premise type DC.rel DC.M.A' DC.M.lt' DC.M.iota_A DC.M.mid DC.M.iota_lt DC.M.mid_l DC.M.mid_r DC.SI.A' (DC.S'.iota_A x) a is not a variable...

view this post on Zulip Jakob von Raumer (May 04 2018 at 09:47):

Isn't it a bit strange that the parsing bits of the interactive versions of these tactics are combined with adding more features?

view this post on Zulip Jakob von Raumer (May 04 2018 at 09:53):

It seems pretty bad that I have to fiddle around with the parser monad :(

view this post on Zulip Jakob von Raumer (May 04 2018 at 10:44):

In that sense cases is stronger than tactic.interactive.inductive...

view this post on Zulip Sebastian Ullrich (May 04 2018 at 10:50):

Hm, I thought we generalized major premise in induction as well

view this post on Zulip Jakob von Raumer (May 04 2018 at 12:00):

At least not in the version I'm on right now (3.3)

view this post on Zulip Jakob von Raumer (May 04 2018 at 12:01):

The best solution for this mismatch would be to somehow expose add_ginductive to the meta language, I guess

view this post on Zulip Sebastian Ullrich (May 04 2018 at 12:45):

Well, why would you use such an ancient version :P

view this post on Zulip Jakob von Raumer (May 04 2018 at 13:04):

Well, in 3.4.1 it doesn't look any different ;)

view this post on Zulip Jakob von Raumer (May 04 2018 at 13:05):

I think it's about generalizing the _argument_ to the major premise, no?

view this post on Zulip Jakob von Raumer (May 04 2018 at 13:07):

What's your best guess for the amount of work it would be to add an interface add_ginductive?

view this post on Zulip Sebastian Ullrich (May 04 2018 at 14:04):

I think it's about generalizing the _argument_ to the major premise, no?

There is https://github.com/leanprover/lean/blob/master/library/init/meta/interactive.lean#L545

view this post on Zulip Sebastian Ullrich (May 04 2018 at 14:06):

What's your best guess for the amount of work it would be to add an interface add_ginductive?

Well, first you have to fork Lean... but the implementation itself shouldn't be hard

view this post on Zulip Jakob von Raumer (May 04 2018 at 14:20):

There is https://github.com/leanprover/lean/blob/master/library/init/meta/interactive.lean#L545

I saw that, yes, but that's still not as general as cases, otherwise the message argument #8 of major premise type [...] is not a variable wouldn't make sense. I'll try to come up with a small example...

view this post on Zulip Jakob von Raumer (May 04 2018 at 14:20):

The generalization has some issues anyway, see for example the error that

inductive foo : bool → Type
| mk : foo ff

inductive bar : Π b, foo b → Type
| mk : bar ff foo.mk

example (y: foo ff) (x : bar ff y) : unit :=
begin
  induction x,
end

gives...

view this post on Zulip Jakob von Raumer (May 04 2018 at 14:26):

Small example where cases works:

inductive foo : bool → Type
| mk : foo ff

inductive bar : Π b, foo b → Type

example (x : bar ff foo.mk): unit :=
begin
  induction x,
end

view this post on Zulip Jakob von Raumer (May 08 2018 at 09:19):

Recreating all the reverts and generalizes is really difficult :-/

view this post on Zulip Jakob von Raumer (May 08 2018 at 10:41):

Does anybody have a good explanation of what's the difference between cases and induction there?

view this post on Zulip Kevin Buzzard (May 08 2018 at 10:54):

--bar.cases_on : Π (C : Π (b : bool) (a : foo b), bar b a → Sort l) {b : bool} {a : foo b} (n : bar b a), C b a n
--bar.rec_on   : Π (C : Π (b : bool) (a : foo b), bar b a → Sort l) {b : bool} {a : foo b} (n : bar b a), C b a n

view this post on Zulip Kevin Buzzard (May 08 2018 at 10:54):

o_O

view this post on Zulip Kevin Buzzard (May 08 2018 at 10:58):

But in Jacob's code, cases works and induction produces the error

view this post on Zulip Kevin Buzzard (May 08 2018 at 10:58):

generalize tactic failed, result is not type correct
nested exception message:
check failed, application type mismatch (use 'set_option trace.check true' for additional details)
state:
⊢ bar ff foo.mk → unit

view this post on Zulip Kevin Buzzard (May 08 2018 at 11:00):

With set_option trace.check true we see

view this post on Zulip Kevin Buzzard (May 08 2018 at 11:00):

[check] application type mismatch at
  bar _x foo.mk
argument type
  foo ff
expected type
  foo _x

view this post on Zulip Kevin Buzzard (May 08 2018 at 11:01):

(this is with the 20/4 nightly)

view this post on Zulip Jakob von Raumer (May 08 2018 at 12:46):

cases does something to generalize the arguments in the correct way that induction doesn't, it's not really about the recursor it uses

view this post on Zulip Jakob von Raumer (May 09 2018 at 14:21):

Do you think this will change in Lean 4?

view this post on Zulip Sebastian Ullrich (May 09 2018 at 14:26):

Lean 4 will probably not have any ginductives

view this post on Zulip Jakob von Raumer (May 09 2018 at 16:16):

Care to elaborate?

view this post on Zulip Sebastian Ullrich (May 09 2018 at 16:45):

With nested and mutual inductives moving into the kernel, there shouldn't be any need for an abstraction layer. Well, it's still not clear how nested inductives would be represented.

view this post on Zulip Jakob von Raumer (May 09 2018 at 16:57):

Why are they moved into the kernel if they can be reduced outside the kernel?

view this post on Zulip Sebastian Ullrich (May 09 2018 at 17:00):

They can't :) . The reduction rules are too weak, that is. Also, it's the most horrible part of the code base.

view this post on Zulip Jakob von Raumer (May 10 2018 at 14:27):

So I'll wait for Lean 4 or try to emulate what cases does for generalizing

view this post on Zulip Jakob von Raumer (May 10 2018 at 14:49):

Apparently the part I'm missing is mostly some magical no_confusion applications

view this post on Zulip Jakob von Raumer (May 10 2018 at 15:17):

Is it still Daniel who maintains the ginductive compiler?

view this post on Zulip Sebastian Ullrich (May 14 2018 at 07:22):

I think it's just Leo, who says he doesn't even understand the code any more

view this post on Zulip Jakob von Raumer (May 14 2018 at 16:03):

That's bad news :(


Last updated: May 12 2021 at 22:15 UTC