Skip to content

Commit

Permalink
Update doc for Fuzz
Browse files Browse the repository at this point in the history
Signed-off-by: zeramorphic <[email protected]>
  • Loading branch information
zeramorphic committed Apr 13, 2024
1 parent 4455f27 commit 0b4784a
Showing 1 changed file with 35 additions and 15 deletions.
50 changes: 35 additions & 15 deletions ConNF/Fuzz/Hypotheses.lean
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,10 @@ it here for more convenient use later.
## Main declarations
* `ConNF.ModelData`: Data about the model elements at level `α`, called *t-sets*.
* `ConNF.Tangle`: A t-set together with a support for it.
* `ConNF.PositionedTangles`: A function that gives each type `α` tangle a unique position `ν : μ`.
* `ConNF.TypedObjects`: Allows us to encode atoms and near-litters as type `α` t-sets.
* `ConNF.BasePositions`: The position of typed atoms and typed near-litters in the position function
at any level.
* `ConNF.TypedObjects`: Allows us to encode near-litters as type `α` t-sets.
* `ConNF.BasePositions`: Almost arbitrarily chosen position functions for atoms and near-litters.
* `ConNF.PositionedObjects`: Hypotheses on the positions of typed objects.
-/

Expand All @@ -28,25 +28,27 @@ namespace ConNF

variable [Params.{u}]

/-- Data about the model elements at level `α`. This class asserts the existence of a type of
tangles at level `α`, and a group of allowable permutations at level `α` that act on the
`α`-tangles. We also stipulate that each tangle has a prescribed small support, called its
designated support. -/
/-- Data about the model elements at level `α`. This class asserts the existence of a type of model
elements at level `α` called *t-sets*, and a group of *allowable permutations* at level `α` that act
on the type `α` t-sets. We also stipulate that each t-set has a support. There is a natural
embedding of t-sets into structural sets. -/
class ModelData (α : TypeIndex) where
/-- The type of tangles that we assume were constructed at stage `α`.
/-- The type of model elements that we assume were constructed at stage `α`.
Later in the recursion, we will construct this type explicitly, but for now, we will just assume
that it exists. -/
(TSet : Type u)
/-- The type of allowable permutations that we assume exists on `α`-tangles. -/
(Allowable : Type u)
[allowableGroup : Group Allowable]
/-- An embedding from allowable permutations to structural permutations. -/
allowableToStructPerm : Allowable →* StructPerm α
allowableToStructPerm_injective : Function.Injective allowableToStructPerm
[allowableAction : MulAction Allowable TSet]
has_support (t : TSet) : ∃ S : Support α,
letI : MulAction Allowable (Address α) :=
MulAction.compHom _ allowableToStructPerm
MulAction.Supports Allowable (S : Set (Address α)) t
/-- The embedding that converts a t-sets into its underlying structural set. -/
toStructSet : TSet ↪ StructSet α
toStructSet_smul (ρ : Allowable) (t : TSet) :
letI : MulAction Allowable (StructSet α) :=
Expand Down Expand Up @@ -102,6 +104,8 @@ theorem smul_eq_of_smul_support_eq {S : Support α} {ρ : Allowable α}

variable {ρ ρ' : Allowable α} {c : Address α}

/-- Although we use often this in `simp` invocations, it is not given the `@[simp]` attribute so
that it doesn't get used unnecessarily. -/
theorem smul_address :
ρ • c = ⟨c.path, Allowable.toStructPerm ρ c.path • c.value⟩ :=
rfl
Expand All @@ -123,6 +127,7 @@ theorem ModelData.TSet.has_support {α : TypeIndex} [ModelData α] (t : TSet α)
∃ S : Support α, MulAction.Supports (Allowable α) (S : Set (Address α)) t :=
ModelData.has_support t

/-- The canonical support for an atom. -/
def Atom.support (a : Atom) : Support ⊥ :=
Enumeration.singleton ⟨Quiver.Path.nil, Sum.inl a⟩

Expand All @@ -139,8 +144,8 @@ theorem Atom.support_supports (a : Atom) :
Sum.smul_inl, Sum.inl.injEq] at h
exact h

/-- The tangle data at level `⊥` is constructed by taking the tangles to be the atoms, the allowable
permutations to be near-litter permutations, and the designated supports to be singletons. -/
/-- The model data at level `⊥` is constructed by taking the t-sets to be the atoms, and
the allowable permutations to be the near-litter permutations. -/
instance Bot.modelData : ModelData ⊥
where
TSet := Atom
Expand All @@ -152,16 +157,24 @@ instance Bot.modelData : ModelData ⊥
toStructSet := StructSet.ofBot.toEmbedding
toStructSet_smul _ _ := rfl

/-- A t-set at level `α` together with a support for it. This is a specialisation of the notion
of a tangle which will be defined for arbitrary type indices. -/
@[ext]
structure TangleCoe (α : Λ) [ModelData α] : Type u where
set : TSet α
support : Support α
support_supports : MulAction.Supports (Allowable α) (support : Set (Address α)) set

/-- If `α` is a proper type index, an `α`-tangle is t-set at level `α`,
together with a support for it. If `α = ⊥`, then an `α`-tangle is an atom. -/
def Tangle : (α : TypeIndex) → [ModelData α] → Type u
| (α : Λ), _ => TangleCoe α
| ⊥, _ => Atom

/-- Each tangle comes with a support. Since we could (a priori) have instances for `[ModelData ⊥]`
other than that constructed above, it's possible that this isn't a support under the action of
`⊥`-allowable permutations. We will later define `Tangle.support_supports_lt` which gives the
expected result under suitable hypotheses. -/
def Tangle.support : {α : TypeIndex} → [ModelData α] → Tangle α → Support α
| (α : Λ), _, t => TangleCoe.support t
| ⊥, _i, a => Atom.support a
Expand All @@ -183,23 +196,24 @@ instance (α : Λ) [ModelData α] : MulAction (Allowable α) (TangleCoe α) wher
change ⟨_ • t.set, _ • t.support, _⟩ = (⟨_ • _ • t.set, _ • _ • t.support, _⟩ : Tangle α)
ext : 1 <;> simp only [mul_smul]

/-- Allowable permutations act on tangles. -/
instance : (α : TypeIndex) → [ModelData α] → MulAction (Allowable α) (Tangle α)
| (α : Λ), _ => inferInstanceAs (MulAction (Allowable α) (TangleCoe α))
| ⊥, _ => inferInstanceAs (MulAction (Allowable ⊥) Atom)

/-- Provides a position function for `α`-tangles, giving each tangle a unique position `ν : μ`.
The existence of this injection proves that there are at most `μ` tangles at level `α`, and
therefore at most `μ` t-sets. Since `μ` has a well-ordering, this induces a well-ordering on
`α`-tangles: to compare two tangles, simply compare their images under this map. -/
class PositionedTangles (α : TypeIndex) [ModelData α] where
/-- A position function, giving each tangle a unique position `ν : μ`.
The existence of this injection proves that there are at most `μ` tangles at level `α`.
Since `μ` has a well-ordering, this induces a well-ordering on `α`-tangles: to compare two
tangles, simply compare their images under this map. -/
pos : Tangle α ↪ μ

instance {α : TypeIndex} [ModelData α] [PositionedTangles α] : Position (Tangle α) μ where
pos := PositionedTangles.pos

variable (α : Λ) [ModelData α]

/-- Allows us to encode atoms and near-litters as `α`-tangles. These maps are expected to cohere
/-- Allows us to encode near-litters as `α`-tangles. These maps are expected to cohere
with the conditions given in `BasePositions`, but this requirement is expressed later. -/
class TypedObjects where
/-- Encode a near-litter as an `α`-tangle. The resulting model element has a `⊥`-extension which
Expand All @@ -212,6 +226,9 @@ class TypedObjects where

export TypedObjects (typedNearLitter)

/-- Almost arbitrarily chosen position functions for atoms and near-litters. The only requirements
they satisfy are included in this class. These requirements are later used to prove that the
`Constrains` relation is well-founded. -/
class BasePositions where
posAtom : Atom ↪ μ
posNearLitter : NearLitter ↪ μ
Expand Down Expand Up @@ -241,6 +258,9 @@ theorem lt_pos_symmDiff [BasePositions] (a : Atom) (N : NearLitter) (h : a ∈ l
pos a < pos N :=
BasePositions.lt_pos_symmDiff a N h

/-- The assertion that the position of typed near-litters is at least the position of the
near-litter itself. This is used to prove that the alternative extension relation `↝` is
well-founded. -/
class PositionedObjects [BasePositions] [PositionedTangles α] [TypedObjects α] : Prop where
pos_typedNearLitter (N : NearLitter) (t : Tangle α) :
t.set = typedNearLitter N → pos N ≤ pos t
Expand Down

0 comments on commit 0b4784a

Please sign in to comment.