Why is there a hidden variable in this example?

Stream: new members

[Marko Grdinić]

import data.rat

inductive InfosetedGame (players : list string) {infoset_count : nat} (infoset_sizes : fin infoset_count → ℕ)
| Terminal (player : {i // i ∈ players}) (reward : rat) : InfosetedGame

def utility (infoset_count : nat) (infoset_sizes : fin infoset_count → nat) : InfosetedGame ["One", "Two"] infoset_sizes → rat
    | (InfosetedGame.Terminal a b c) := a

equation type mismatch, term
  infoset_sizes
has type
  fin infoset_count → ℕ
but is expected to have type
  ℚ

And furthermore if I replace a with by {}...

Tactic State
1 goal
infoset_count : ℕ,
infoset_sizes : fin infoset_count → ℕ,
utility : InfosetedGame ["One", "Two"] infoset_sizes → ℚ,
b : {i // i ∈ ["One", "Two"]},
c : ℚ
⊢ ℚ

For some reason a is not even there. This definitely seems like some kind of compiler bug to me.

[Kevin Buzzard]

I didn't look carefully at this question but yes, there is an a bug in 3.4.2. Try changing the name of your variable?

[Marko Grdinić]

It makes no difference, either in the error message for the first example or the goal state for the second.

[Chris Hughes]

In this code a has to be equal to infoset_sizes in order for Terminal a b c to have the right type. The equation compiler seems to have replaced a with infoset_sizes for this reason.

[Marko Grdinić]

@Chris Hughes
Yeah, but that is besides the point as that binding should not even be there in the first place. Terminal should only have two fields as far as I can see.

[Mario Carneiro]

It has three explicit args; the first is infoset_sizes

[Mario Carneiro]

parameters are arguments to the constructors too

[Mario Carneiro]

you should just leave the first argument as _ since it is forced

[Reid Barton]

I think the rule is that parameters which otherwise wouldn't be determined are explicit in the constructor, though in practice I never find it easy to predict what Lean will do

[Marko Grdinić]

@Mario Carneiro
Why is it forced?

[Mario Carneiro]

Because you are doing a recursive definition over InfosetedGame, so that argument is forced to the value it is given in the parameter in the def itself (the infoset_sizes argument to the function). Nevertheless, the constructor appears in the pattern with all its arguments, including the parameters; you are not allowed to put anything else in that field

[Mario Carneiro]

If you moved infoset_sizes right of the colon, you would have a little more flexibility, although you can't pattern match on it in any interesting way because it's a function type, not an inductive

[Marko Grdinić]

Because you are doing a recursive definition over InfosetedGame

I do not really understand this. The particular example I am showing here as (opposed to) is not recursive as far as I can see.

so that argument is forced to the value it is given in the parameter in the def itself (the infoset_sizes argument to the function).

Sorry, I can't follow this. What is what here exactly?

[Mario Carneiro]

I mean "recursive" only in the sense that you are using the recursor, i.e. cases on an inductive type

[Mario Carneiro]

The definition has to look like this:

def utility (infoset_count : nat) (infoset_sizes : fin infoset_count → nat) : InfosetedGame ["One", "Two"] infoset_sizes → rat
| (InfosetedGame.Terminal infoset_sizes b c) := _

[Mario Carneiro]

You can leave it implicit if you like (I usually always do this for forced arguments):

def utility (infoset_count : nat) (infoset_sizes : fin infoset_count → nat) : InfosetedGame ["One", "Two"] infoset_sizes → rat
| (InfosetedGame.Terminal _ b c) := _

[Mario Carneiro]

but anything like this is not valid:

def utility (infoset_count : nat) (infoset_sizes : fin infoset_count → nat) : InfosetedGame ["One", "Two"] infoset_sizes → rat
| (InfosetedGame.Terminal (\lam _, 2) b c) := _

[Mario Carneiro]

Technically this is an "inaccessible pattern". Back in the day you had to write these as ._ (or .(infoset_sizes)) to indicate that they aren't being matched by the equation compiler, but it later learned how to infer these annotations so they are basically never needed anymore

[Marko Grdinić]

Ok, thanks.