Zulip Chat Archive

Stream: new members

Topic: Why is there a hidden variable in this example?


view this post on Zulip Marko Grdinić (Oct 28 2019 at 08:16):

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.

view this post on Zulip Kevin Buzzard (Oct 28 2019 at 10:35):

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?

view this post on Zulip Marko Grdinić (Oct 28 2019 at 12:11):

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

view this post on Zulip Chris Hughes (Oct 28 2019 at 12:26):

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.

view this post on Zulip Marko Grdinić (Oct 28 2019 at 12:48):

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

view this post on Zulip Mario Carneiro (Oct 28 2019 at 12:54):

It has three explicit args; the first is infoset_sizes

view this post on Zulip Mario Carneiro (Oct 28 2019 at 12:54):

parameters are arguments to the constructors too

view this post on Zulip Mario Carneiro (Oct 28 2019 at 12:56):

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

view this post on Zulip Reid Barton (Oct 28 2019 at 13:06):

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

view this post on Zulip Marko Grdinić (Oct 28 2019 at 13:08):

@Mario Carneiro
Why is it forced?

view this post on Zulip Mario Carneiro (Oct 28 2019 at 13:10):

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

view this post on Zulip Mario Carneiro (Oct 28 2019 at 13:11):

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

view this post on Zulip Marko Grdinić (Oct 28 2019 at 13:18):

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?

view this post on Zulip Mario Carneiro (Oct 28 2019 at 13:29):

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

view this post on Zulip Mario Carneiro (Oct 28 2019 at 13:31):

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) := _

view this post on Zulip Mario Carneiro (Oct 28 2019 at 13:31):

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) := _

view this post on Zulip Mario Carneiro (Oct 28 2019 at 13:32):

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) := _

view this post on Zulip Mario Carneiro (Oct 28 2019 at 13:33):

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

view this post on Zulip Marko Grdinić (Oct 28 2019 at 14:36):

Ok, thanks.


Last updated: May 14 2021 at 14:20 UTC