cases

Stream: general

[Jakob von Raumer]

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.

[Mario Carneiro]

and what is the hypothesis?

[Mario Carneiro]

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

[Jakob von Raumer]

I'll try

[Jakob von Raumer]

Oh, so tactic.cases lacks the generalizing part?

[Mario Carneiro]

I guess so

[Kevin Buzzard]

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).

[Kevin Buzzard]

(but in a different namespace :-) )

[Jakob von Raumer]

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

[Mario Carneiro]

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

[Mario Carneiro]

there is no elaborate namespace resolution like normal

[Jakob von Raumer]

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

[Jakob von Raumer]

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'

[Jakob von Raumer]

And the failing tactic is

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

[Mario Carneiro]

your local variables have namespaces?

[Jakob von Raumer]

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

[Mario Carneiro]

seems like you want a structure to hold all that

[Jakob von Raumer]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jakob von Raumer]

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/

[Jakob von Raumer]

Okay, thanks for the advice

[Mario Carneiro]

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

What do you mean by this?

[Jakob von Raumer]

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?

[Jakob von Raumer]

Any more clues? :(

[Mario Carneiro]

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?

[Sebastian Ullrich]

@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

[Sebastian Ullrich]

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

[Jakob von Raumer]

@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'.

[Jakob von Raumer]

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

[Jakob von Raumer]

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?

[Jakob von Raumer]

That would be a shame :disappointed:

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Sebastian Ullrich]

yes

[Jakob von Raumer]

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

[Sebastian Ullrich]

You can use induction :)

[Jakob von Raumer]

induction doesn't do the generalizing itself, right?

[Sebastian Ullrich]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Sebastian Ullrich]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Sebastian Ullrich]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

o_O

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

With set_option trace.check true we see

[Kevin Buzzard]

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

[Kevin Buzzard]

(this is with the 20/4 nightly)

[Jakob von Raumer]

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

[Jakob von Raumer]

Do you think this will change in Lean 4?

[Sebastian Ullrich]

Lean 4 will probably not have any ginductives

[Jakob von Raumer]

Care to elaborate?

[Sebastian Ullrich]

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.

[Jakob von Raumer]

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

[Sebastian Ullrich]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

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

[Jakob von Raumer]

Is it still Daniel who maintains the ginductive compiler?

[Sebastian Ullrich]

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

[Jakob von Raumer]

That's bad news :(