Indexed containers for game semantics

HTree.v

(** An (indexed) "container" encodes an indexed recursive type. *)
(** A container can also be seen as a game, with
    - [ix] as the type of positions,
    - [shape i] the Player moves at position [i],
    - [pos i s] the Opponent moves after Player plays move [s] on position [i],
    - [posix i s p] the new position after moves [s] and [p] from position [i].
  *)
Module Export Container.

Record container :=
  { ix : Type                             (* Indices *)
  ; shape : ix -> Type                    (* Constructors *)
  ; pos : forall i : ix, shape i -> Type  (* (Recursive) fields *)
  ; posix : forall (i : ix) (s : shape i), pos i s -> ix  (* Index for each field *)
  }.

End Container.

Definition _htree (c : container) (f : ix c -> Type) (i : ix c) (r : Type) : Type :=
  forall (s : shape c i), (forall p : pos c i s, f (posix c i s p)) -> r.

(** The fixed-point associated with container [c]. *)
Inductive htree (c : container) (i : ix c) : Type :=
| ToFix : _htree c (htree c) i (htree c i)
.

(** A trivial container. [htree c I] is isomorphic to [t]. *)
Definition const (t : Type) : container :=
  {| ix := True
  ; shape := fun _ => t
  ; pos := fun _ _ => False
  ; posix := fun _ _ v => match v : False with end
  |}.

(** "Tensor product" of containers/games: sum their constructors, which act
    independently on their indices. *)
Module Sum.
Section Sum.

Context (c1 c2 : container).

Definition ix : Type := ix c1 * ix c2.
Definition shape (i : ix) : Type := shape c1 (fst i) + shape c2 (snd i).

Definition pos (i : ix) (s : shape i) : Type :=
  match s with
  | inl s1 => pos c1 (fst i) s1
  | inr s2 => pos c2 (snd i) s2
  end.

Definition posix (i : ix) (s : shape i) : pos i s -> ix :=
  match s with
  | inl s1 => fun p => (posix c1 (fst i) s1 p, snd i)
  | inr s2 => fun p => (fst i, posix c2 (snd i) s2 p)
  end.

Definition sum : container :=
  {| Container.ix := ix
  ; Container.shape := shape
  ; Container.pos := pos
  ; Container.posix := posix
  |}.

End Sum.
End Sum.

(** Dual of a container. We take the initial Player move (who becomes the
    Opponent) as an external parameter.
    It is involutive modulo some isomorphism. *)
Module Dual.
Section Dual.

Context (c : container).

Definition ix : Type := { i : ix c & shape c i }.
Definition shape (i : ix) : Type := pos c _ (projT2 i).
Definition pos   (i : ix) (p : shape i) : Type := Container.shape c (Container.posix c _ _ p).
Definition posix (i : ix) (p : shape i) (s : pos i p) : ix := existT _ (Container.posix c _ _ p) s.

Definition i0 (i : Container.ix c) (s : Container.shape c i) : ix := existT _ i s.

Definition dual : container :=
  {| Container.ix := ix
  ; Container.shape := shape
  ; Container.pos := pos
  ; Container.posix := posix
  |}.

End Dual.
End Dual.

(** Containers form a category [ARR]:
    - objects are containers paired with initial indices/positions,
    - morphisms are htrees/strategies, parameterized by an initial opponent move.
  *)

(** "Arrow" constructor on containers/games. *)
Definition arr (c1 c2 : container) : container :=
  Sum.sum (Dual.dual c1) c2.

(** "Arrow" constructor on container-index pairs. *)
Definition ARR (c1 c2 : container) (i1 : ix c1) (i2 : ix c2) : Type :=
  forall (s : shape c1 i1), htree (arr c1 c2) (Dual.i0 c1 i1 s, i2).

(** Composition of morphisms. *)
Section Compose.

Context (c1 c2 c3 : container).

Fixpoint __compose (i1 : ix (Dual.dual c1)) (i2 : ix (Dual.dual c2)) (i3 : ix c3)
  (u : htree (arr c2 c3) (i2, i3))
  (k : forall (p : pos c2 _ (projT2 i2)) (i3 : ix c3)
              (u : forall s2 : shape c2 (posix c2 _ _ p), htree (arr c2 c3) (Dual.i0 c2 _ s2, i3)),
        htree (arr c1 c3) (i1, i3)) : htree (arr c1 c3) (i1, i3) :=
  match u with
  | ToFix _ _ s' k' =>
    match s' return (forall p : _ s', htree _ (posix (arr c2 c3) (i2, i3) s' p)) -> _ with
    | inl s2 => fun k' => k s2 _ (fun s => k' s)
    | inr s3 => fun k' => ToFix _ _
        (inr s3 : shape (arr c1 c3) (i1, i3))
        (fun p => __compose i1 i2 _ (k' p) k)
    end k'
  end.

Fixpoint _compose (i1 : ix (Dual.dual c1)) (i2 : ix c2) (i3 : ix c3)
  (t : htree (arr c1 c2) (i1, i2)) (u : forall s2 : shape c2 i2, htree (arr c2 c3) (Dual.i0 c2 i2 s2, i3))
  : htree (arr c1 c3) (i1, i3) :=
  match t with
  | ToFix _ _ s k =>
    match s return (forall p : _ s, htree _ (posix (arr c1 c2) (i1, i2) s p)) -> _ with
    | inl s1 => fun k => ToFix _ _
        (inl s1 : shape (arr c1 c3) (i1, i3))
        (fun p => _compose (Dual.posix _ _ s1 p) i2 i3 (k p) u)
    | inr s2 => fun k => __compose i1 _ i3 (u s2) (fun p i3 u => _compose i1 _ i3 (k p) u)
    end k
  end.

Definition compose (i1 : ix c1) (i2 : ix c2) (i3 : ix c3)
    (a12 : ARR c1 c2 i1 i2) (a23 : ARR c2 c3 i2 i3)
  : ARR c1 c3 i1 i3 :=
  fun s => _compose (existT _ i1 s) i2 i3 (a12 s) a23.

End Compose.