Zulip Chat Archive

Stream: new members

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


view this post on Zulip Marko Grdinić (Oct 27 2019 at 16:19):

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?

view this post on Zulip Mario Carneiro (Oct 27 2019 at 16:24):

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

view this post on Zulip Marko Grdinić (Oct 27 2019 at 16:26):

@Mario Carneiro

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

view this post on Zulip Mario Carneiro (Oct 27 2019 at 16:27):

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

view this post on Zulip Marko Grdinić (Oct 27 2019 at 16:31):

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

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

view this post on Zulip Mario Carneiro (Oct 27 2019 at 16:31):

Recursive arguments are not allowed to be dependent

view this post on Zulip Mario Carneiro (Oct 27 2019 at 16:33):

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

view this post on Zulip Marko Grdinić (Oct 27 2019 at 16:38):

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?

view this post on Zulip Mario Carneiro (Oct 27 2019 at 16:47):

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

view this post on Zulip Marko Grdinić (Oct 27 2019 at 17:02):

I see. Thank you for the help.

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

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.

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

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.

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

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.

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

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.

view this post on Zulip Marko Grdinić (Oct 31 2019 at 08:45):

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.

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:51):

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

view this post on Zulip Mario Carneiro (Oct 31 2019 at 08:52):

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


Last updated: May 10 2021 at 19:16 UTC