Skip to content

Instantly share code, notes, and snippets.

@damhiya

damhiya/IndexedContainer.v

Last active August 1, 2025 05:14
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save damhiya/72588897a5100c09b1b9cfb2bee069a1 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save damhiya/72588897a5100c09b1b9cfb2bee069a1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
IndexedContainer.v
Set Primitive Projections.
Module Container.
Record t (I : Type) (O : Type) : Type :=
{
Command : forall (o : O), Type; (* shape *)
Response : forall (o : O) (c : Command o), Type; (* position or degree *)
next : forall (o : O) (c : Command o) (r : Response o c), I;
} as C.
Arguments Command {I O} C o.
Arguments Response {I O} C o c.
Arguments next {I O} C o c r.
Record ext {I O} (C : t I O) (X : I -> Type) (o : O) : Type :=
{ command : C.(Command) o;
subtree : forall (r : C.(Response) o command), X (C.(next) o command r);
} as t.
Arguments command {I O C X o} t.
Arguments subtree {I O C X o} t r.
Definition map {I} {C : t I I} {X Y} (f : forall [i], X i -> Y i) [i] (x : ext C X i) : ext C Y i :=
{|
command := x.(command);
subtree := fun r => f (x.(subtree) r);
|}.
End Container.
Module ContainerNotations.
Notation "⟦ C ⟧" := (Container.ext C).
End ContainerNotations.
Import ContainerNotations.
Module Mu.
Inductive t {I} (C : Container.t I I) (X : I -> Type) (i : I) : Type :=
| sup (ts : ⟦ C ⟧ (t C X) i) : t C X i
.
Arguments sup {I C X} [i] ts.
End Mu.
Module Free.
Inductive t {I} (C : Container.t I I) (X : I -> Type) (i : I) : Type :=
| ret (x : X i) : t C X i
| cons (ts : ⟦ C ⟧ (t C X) i) : t C X i
.
Arguments ret {I C X} [i] x.
Arguments cons {I C X} [i] ts.
Fixpoint map {I} {C : Container.t I I} {X Y} (f : forall [i], X i -> Y i) [i] (x : t C X i) : t C Y i :=
match x with
| ret x => ret (f x)
| cons ts => cons (Container.map (map f) ts)
end.
Fixpoint join {I} {C : Container.t I I} {X} [i] (x : t C (t C X) i) : t C X i :=
match x with
| ret x => x
| cons ts => cons (Container.map join ts)
end.
End Free.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment