rcases ignores my variable names

Stream: general

[Hunter Freyer]

I'm so confused by rcases and the fact that it seems to almost entirely ignore the variable names I suggest.

Here's my code (sorry for the huge types, but it's what I'm working with):

@[derive decidable_eq]
inductive val : Type
| nat
| nil
| cons : Π (car : val) (cdr: val), val

@[derive decidable_eq]
inductive fn : val -> val -> Type
| zero : fn val.nil val.nat
| succ : fn val.nat val.nat
| car  : Π {tcar tcdr: val}, fn (val.cons tcar tcdr) tcar
| cdr  : Π {tcar tcdr: val}, fn (val.cons tcar tcdr) tcdr
| nil  : Π {tin : val}, fn tin val.nil
| cons : Π {tin tcar tcdr: val} (car : fn tin tcar) (cdr: fn tin tcdr), fn tin (val.cons tcar tcdr)
| comp : Π {tin tint tout: val} (f : fn tint tout) (g: fn tin tint), fn tin tout
| prec : Π {trest tout: val} (z_case : fn trest tout) (s_case: fn (val.cons val.nat (val.cons tout trest)) tout),
    fn (val.cons val.nat trest) tout

example : Π (z:val), false := begin
    intro z,
    have x : (fn z val.nat), sorry,
    rcases x with ( _ | _ | foo | bar | baz | qux ),
    iterate {sorry},
end

[Hunter Freyer]

If you put it in the editor and look at the end of the line with rcases, what complete baffles me is that only "bar" gets used.

[Hunter Freyer]

the car constructor is nearly identical to cdr, so why should bar work, but not foo???

[Reid Barton]

normally for a case with 5 arguments to the constructor one would have something like ⟨x₁, x₂, x₃, x₄, x₅⟩

[Reid Barton]

rather than a single variable like bar--what is bar meant to represent?

[Hunter Freyer]

The fact that I don't know what I'm doing :P

[Reid Barton]

in this case it's more complicated because of the inductive family--also note that impossible cases should still have a corresponding _ alternative in rcases

[Hunter Freyer]

I think I kinda figured it out. The problem was I have so many implicit variables and apparently rcases binds names to those even though you don't see them.

[Hunter Freyer]

The other thing that confuses me is that \<a, b\> is used to bind variables within a constructor... but \<\> (open and close) matches an empty case split? Or something?

[Hunter Freyer]

I'm not sure why rintro \<\> works to eliminate an empty type.

[Reid Barton]

I think that is kind of a hack to account for the fact that you can't write _ | _ | ... | _ with 0 _s

[Reid Barton]

especially when nested inside another structure

[Hunter Freyer]

not with that attitude!

[Hunter Freyer]

yeah I'm not sure if my huge inductive type family is a good idea or not

[Hunter Freyer]

I'm trying to represent primitive recursive functions, which I want to basically always be well-typed so I figured I'd build the typing rules into the function type itself, but maybe that's bad style?

[Hunter Freyer]

is it better to have a separate has_type predicate?

[Mario Carneiro]

yes

[Mario Carneiro]

BTW mathlib already has primitive recursive functions, they are defined as an inductive predicate over either nat -> nat or vector nat n -> nat

[Mario Carneiro]

docs#nat.primrec

[Mario Carneiro]

but it should be possible to make your approach work, since the index type isn't very complicated

[Johan Commelin]

On the topic of primrec... the downside of one big inductive type like that, is that you can't reuse it for other complexity classes. It would be fun to have the https://en.wikipedia.org/wiki/Grzegorczyk_hierarchy in mathlib