## Stream: general

### Topic: cases

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

#### Mario Carneiro (May 02 2018 at 12:47):

and what is the hypothesis?

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

I'll try

#### Jakob von Raumer (May 02 2018 at 12:53):

Oh, so tactic.cases lacks the generalizing part?

I guess so

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

#### Kevin Buzzard (May 02 2018 at 12:58):

(but in a different namespace :-) )

#### Jakob von Raumer (May 02 2018 at 12:59):

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

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

#### Mario Carneiro (May 02 2018 at 13:02):

there is no elaborate namespace resolution like normal

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

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


#### Jakob von Raumer (May 02 2018 at 13:06):

And the failing tactic is

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


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

#### Mario Carneiro (May 02 2018 at 13:09):

seems like you want a structure to hold all that

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

#### Mario Carneiro (May 02 2018 at 13:10):

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

#### Mario Carneiro (May 02 2018 at 13:11):

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

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

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

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

#### Jakob von Raumer (May 02 2018 at 16:08):

Any more clues? :(

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

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

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

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

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

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

#### Jakob von Raumer (May 02 2018 at 18:34):

That would be a shame :disappointed:

#### 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
have x : foo, exact bar,
cases x,
end


#### Jakob von Raumer (May 03 2018 at 16:44):

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

yes

#### Jakob von Raumer (May 03 2018 at 16:57):

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

#### Sebastian Ullrich (May 03 2018 at 16:58):

You can use induction :)

#### Jakob von Raumer (May 03 2018 at 17:03):

induction doesn't do the generalizing itself, right?

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

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

#### Jakob von Raumer (May 04 2018 at 09:53):

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

#### Jakob von Raumer (May 04 2018 at 10:44):

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

#### Sebastian Ullrich (May 04 2018 at 10:50):

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

#### Jakob von Raumer (May 04 2018 at 12:00):

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

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

#### Sebastian Ullrich (May 04 2018 at 12:45):

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

#### Jakob von Raumer (May 04 2018 at 13:04):

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

#### Jakob von Raumer (May 04 2018 at 13:05):

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

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

#### Sebastian Ullrich (May 04 2018 at 14:04):

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

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

#### Jakob von Raumer (May 04 2018 at 14:20):

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

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


#### Jakob von Raumer (May 08 2018 at 09:19):

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

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

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


o_O

#### Kevin Buzzard (May 08 2018 at 10:58):

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

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


#### Kevin Buzzard (May 08 2018 at 11:00):

With set_option trace.check true we see

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


#### Kevin Buzzard (May 08 2018 at 11:01):

(this is with the 20/4 nightly)

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

#### Jakob von Raumer (May 09 2018 at 14:21):

Do you think this will change in Lean 4?

#### Sebastian Ullrich (May 09 2018 at 14:26):

Lean 4 will probably not have any ginductives

#### Jakob von Raumer (May 09 2018 at 16:16):

Care to elaborate?

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

#### Jakob von Raumer (May 09 2018 at 16:57):

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

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

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

#### Jakob von Raumer (May 10 2018 at 14:49):

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

#### Jakob von Raumer (May 10 2018 at 15:17):

Is it still Daniel who maintains the ginductive compiler?

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