How to insert a proposition as a field of an inductive type?

Stream: new members

[Marko Grdinić]

import data.rat
import data.list data.vector

inductive InfosetedGame (players : list string) (infoset_count : nat) (infoset_sizes : vector nat infoset_count)
| Terminal (player : {i // i ∈ players}) (reward : rat) : InfosetedGame
| Response
    (player : {i // i ∈ players})
    (subnodes : list InfosetedGame)
    (infoset_id : fin infoset_count)
    (wf : infoset_sizes.nth infoset_id = subnodes.length)
    : InfosetedGame
| Chance (player : {i // i ∈ players}) (subnodes : list InfosetedGame) : InfosetedGame

nested occurrence 'eq.{1} nat (vector.nth.{0} nat infoset_count infoset_sizes infoset_id) (list.length.{0} InfosetedGame subnodes)' lives in universe '0' but must live in resultant universe '1'

The problem here is (wf : infoset_sizes.nth infoset_id = subnodes.length). This kind of code would work in Coq and Agda, though I do remember running into issues with propositions and types being two different things in Coq as well. In addition to the above problem, I've run into problems with not being able to return equalities in tuples and such. I find that quite annoying.

What should I do here?

[Mario Carneiro]

The easiest thing to do would be to use a function fin n -> A in place of {l : list A // length l = n}

[Marko Grdinić]

@Mario Carneiro

I do not follow. What do you mean by that?

[Mario Carneiro]

import data.rat

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

[Marko Grdinić]

This is an interesting way of doing this. It is quite nice.

Still, why is putting that equality into a field a problem?

[Mario Carneiro]

Recursive arguments are not allowed to be dependent

[Mario Carneiro]

Plus, you used list T -> T so it's actually a nested inductive, and these are not built in, lean simulates them, and not that well

[Marko Grdinić]

What do you mean by dependent? What do you mean by not simulating lists inside other types well? Would it be possible to do it by wrapping the proposition in a type?

(wf : {i : unit // infoset_sizes.nth infoset_id = subnodes.length})

nested inductive type compiled to invalid inductive type
nested exception message:
inductive type being declared can only be nested inside the parameters of other inductive types

It seems not. This does seem like a limitation Lean has that I haven't seen in other provers. Is this restriction going to be removed in Lean 4 maybe?

[Mario Carneiro]

You can't make reference to the name subnodes at all in the type of another argument

[Marko Grdinić]

I see. Thank you for the help.

[Marko Grdinić]

I was curious so I decided to check. As it turns out, I was wrong Coq allowing that kind of definition.

Require Import Vector.

Inductive InfosetedGame (infoset_count : nat) (infoset_sizes : t nat infoset_count): Type :=
| Response :
  forall (subnodes : list (InfosetedGame infoset_count infoset_sizes))
  (infoset_id : Fin.t infoset_count)
  (wf : nth infoset_sizes infoset_id = length subnodes),
  InfosetedGame infoset_count infoset_sizes.

Non strictly positive occurrence of "InfosetedGame" in
 "forall (subnodes : list (InfosetedGame infoset_count infoset_sizes))
    (infoset_id : Fin.t infoset_count),
  nth infoset_sizes infoset_id = length subnodes ->
  InfosetedGame infoset_count infoset_sizes".

I was right about Agda though.

open import Data.List
open import Data.Vec
open import Data.Nat
open import Data.Fin
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

data InfosetedGame (infoset-count : ℕ) (infoset-sizes : Vec ℕ infoset-count) : Set where
  Response :
    (subnodes : List (InfosetedGame infoset-count infoset-sizes))
    → (infoset-id : Fin infoset-count)
    → (wf : Data.Vec.lookup infoset-sizes infoset-id ≡ length subnodes)
    → InfosetedGame infoset-count infoset-sizes

I am not sure if this particular issue is related to Prop vs Type split that Lean inherited from Coq, or whether it is purely a matter of termination checking which Agda seems to excel at.

[Mario Carneiro]

I think it has more to do with accepting exotic inductive types. Lean has a well defined schema for inductive types, based on a paper by Dybjer. Coq and Agda have extended the kernel many times to support any inductive construction which isn't obviously inconsistent. AFAIK no one has proved that what is available is actually consistent though.

[Mario Carneiro]

Coq and Agda also both have "termination checkers", where lean does not - it uses only recursors and the equation compiler is a compiler that turns equations into definitions using the recursor.

[Mario Carneiro]

I think this was a good move on Lean's part; the "termination checker" approach makes the slope a bit more slippery when it comes to adding features that are inconsistent for non-obvious reasons.

[Marko Grdinić]

inductive Vec (α : Type) : ℕ → Type
| nil : ∀ {n : ℕ}, Vec n
| cons : ∀ {n : ℕ}, α → Vec n → Vec (n + 1)

inductive GameTree' (infoset_sizes : Infoset → Size)
| Terminal (reward : ℚ) : GameTree'
| Response (id : Infoset) (subnodes : Vec GameTree' (infoset_sizes id)) : GameTree'

As it turns out it is possible to make this work in Lean. It seems it is just the Props that cause trouble in inductive types. The above does not work with the standard library's vector though.

[Mario Carneiro]

Yes, you can also write the mutual inductive yourself:

mutual inductive GameTree'', GameTree_vec (infoset_sizes : Infoset → Size)
with GameTree'' : Type
| Terminal (reward : ℚ) : GameTree''
| Response (id : Infoset) : GameTree_vec (infoset_sizes id) → GameTree''
with GameTree_vec : ℕ → Type
| nil : GameTree_vec 0
| cons {n} : GameTree'' → GameTree_vec n → GameTree_vec (n+1)

or even the resulting plain inductive:

inductive GameTree_mut (infoset_sizes : Infoset → Size) : option ℕ → Type
| Terminal (reward : ℚ) : GameTree_mut none
| Response (id : Infoset) : GameTree_mut (some (infoset_sizes id)) → GameTree_mut none
| nil : GameTree_mut (some 0)
| cons {n} : GameTree_mut none → GameTree_mut (some n) → GameTree_mut (some (n+1))

[Mario Carneiro]

It is important to recognize that whenever you use a nested or mutual inductive, what lean actually builds is the latter plain inductive, plus an interpretation layer. This matters because defeq sometimes matters, as I indicated in the other thread