-
Notifications
You must be signed in to change notification settings - Fork 2
Expand file tree
/
Copy pathTypeTreeFintype.lean
More file actions
115 lines (88 loc) · 4.22 KB
/
Copy pathTypeTreeFintype.lean
File metadata and controls
115 lines (88 loc) · 4.22 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
/-
Copyright (c) 2026 PolyFun Contributors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Quang Dao
-/
module
public import Mathlib.Data.Fintype.Basic
public import PolyFun.Interaction.Basic.TypeTree
/-!
# Branching ornaments on interaction type trees
`Interaction.TypeTree.Fintype tree` and `Interaction.TypeTree.Nonempty tree`
are recursive typeclass-level ornaments asserting, respectively, that every
move space in `tree` is finite or nonempty.
Keeping the properties separate follows `PFunctor.Fintype` and
`OracleSpec.Fintype`: finiteness does not imply that a move is available.
`TypeTree` has many layers of positions, so each ornament recurses into every
subtree.
Together, `TypeTree.Fintype tree` and `TypeTree.Nonempty tree` provide the
assumptions needed by downstream uniform samplers. PolyFun itself remains
independent of any probability monad.
-/
public section
universe u
namespace Interaction
/-- Recursive finite-branching ornament on an interaction type tree.
The `.done` case holds vacuously. At a `.node X rest`, the ornament
stores a `Fintype X` witness together with a per-branch ornament on every
continuation `rest x`. Typeclass synthesis builds these structurally from
concrete trees via the companion instances below, the same way
`OracleSpec.Fintype` synthesizes from `PFunctor.Fintype`. -/
protected class inductive TypeTree.Fintype : TypeTree.{u} → Type (u + 1) where
| done : TypeTree.Fintype TypeTree.done
| node {X : Type u} (hFin : Fintype X)
{rest : X → TypeTree.{u}} (hRec : ∀ x, TypeTree.Fintype (rest x)) :
TypeTree.Fintype (TypeTree.node X rest)
namespace TypeTree.Fintype
/-- Canonical `TypeTree.Fintype` instance for the terminal tree. -/
instance instDone : TypeTree.Fintype TypeTree.done := .done
/-- Canonical `TypeTree.Fintype` instance for a node: synthesizes from
`Fintype X` and a per-branch ornament. -/
instance instNode {X : Type u} [hFin : Fintype X]
{rest : X → TypeTree.{u}} [hRec : ∀ x, TypeTree.Fintype (rest x)] :
TypeTree.Fintype (TypeTree.node X rest) :=
.node hFin hRec
/-- Extract the `Fintype` instance for the move space of the root node. -/
@[expose, reducible]
def rootFintype {X : Type u} {rest : X → TypeTree.{u}}
(h : TypeTree.Fintype (TypeTree.node X rest)) : Fintype X :=
match h with
| .node hFin _ => hFin
/-- Extract the ornament for every continuation of the root node. -/
@[expose, reducible]
def rest {X : Type u} {rest : X → TypeTree.{u}}
(h : TypeTree.Fintype (TypeTree.node X rest)) : ∀ x, TypeTree.Fintype (rest x) :=
match h with
| .node _ hRec => hRec
end TypeTree.Fintype
/-- Recursive nonempty-branching ornament on an interaction type tree.
The `.done` case holds vacuously. At a `.node X rest`, the ornament stores a
`Nonempty X` witness and recursively requires every continuation to be
nonempty-branching. This is separate from `TypeTree.Fintype`: a finite move
space may be empty. -/
protected class inductive TypeTree.Nonempty : TypeTree.{u} → Prop where
| done : TypeTree.Nonempty TypeTree.done
| node {X : Type u} (hNonempty : Nonempty X)
{rest : X → TypeTree.{u}} (hRec : ∀ x, TypeTree.Nonempty (rest x)) :
TypeTree.Nonempty (TypeTree.node X rest)
namespace TypeTree.Nonempty
/-- Canonical `TypeTree.Nonempty` instance for the terminal tree. -/
instance instDone : TypeTree.Nonempty TypeTree.done := .done
/-- Canonical `TypeTree.Nonempty` instance for a node: synthesizes from
`Nonempty X` and a per-branch ornament. -/
instance instNode {X : Type u} [hNonempty : Nonempty X]
{rest : X → TypeTree.{u}} [hRec : ∀ x, TypeTree.Nonempty (rest x)] :
TypeTree.Nonempty (TypeTree.node X rest) :=
.node hNonempty hRec
/-- Extract the `Nonempty` instance for the move space of the root node. -/
theorem rootNonempty {X : Type u} {rest : X → TypeTree.{u}}
(h : TypeTree.Nonempty (TypeTree.node X rest)) : Nonempty X :=
match h with
| .node hNonempty _ => hNonempty
/-- Extract the ornament for every continuation of the root node. -/
theorem rest {X : Type u} {rest : X → TypeTree.{u}}
(h : TypeTree.Nonempty (TypeTree.node X rest)) : ∀ x, TypeTree.Nonempty (rest x) :=
match h with
| .node _ hRec => hRec
end TypeTree.Nonempty
end Interaction