From 283a1129b490cfc8bd9cb391d276c95b3e4c5333 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Tue, 12 Dec 2023 12:14:20 +0000 Subject: [PATCH] Rename `Foa` to `FOA` Signed-off-by: zeramorphic --- ConNF.lean | 2 +- ConNF/FOA.lean | 6 ++++++ ConNF/FOA/Action.lean | 6 ++++++ ConNF/{Foa => FOA}/Action/Complete.lean | 4 ++-- ConNF/{Foa => FOA}/Action/FillAtomOrbits.lean | 2 +- ConNF/{Foa => FOA}/Action/FillAtomRange.lean | 2 +- .../{Foa => FOA}/Action/NearLitterAction.lean | 8 ++++---- ConNF/{Foa => FOA}/Action/Refine.lean | 10 +++++----- ConNF/{Foa => FOA}/Action/StructAction.lean | 12 +++++------ ConNF/FOA/Approximation.lean | 2 ++ .../Approximation/NearLitterApprox.lean | 6 +++--- .../Approximation/StructApprox.lean | 4 ++-- ConNF/FOA/Basic.lean | 6 ++++++ ConNF/{Foa => FOA}/Basic/CompleteOrbit.lean | 0 ConNF/{Foa => FOA}/Basic/Constrains.lean | 4 ++-- ConNF/{Foa => FOA}/Basic/Flexible.lean | 4 ++-- ConNF/{Foa => FOA}/Basic/Hypotheses.lean | 20 +++++++++---------- ConNF/{Foa => FOA}/Basic/Reduction.lean | 4 ++-- ConNF/{Foa => FOA}/Basic/Sublitter.lean | 0 ConNF/FOA/Complete.lean | 6 ++++++ .../{Foa => FOA}/Complete/AtomCompletion.lean | 6 +++--- .../{Foa => FOA}/Complete/CompleteAction.lean | 6 +++--- .../Complete/FlexibleCompletion.lean | 4 ++-- ConNF/{Foa => FOA}/Complete/HypAction.lean | 4 ++-- .../Complete/LitterCompletion.lean | 14 ++++++------- .../Complete/NearLitterCompletion.lean | 4 ++-- ConNF/FOA/Properties.lean | 4 ++++ ConNF/{Foa => FOA}/Properties/Bijective.lean | 6 +++--- .../Properties/ConstrainedAction.lean | 4 ++-- ConNF/{Foa => FOA}/Properties/Injective.lean | 4 ++-- ConNF/{Foa => FOA}/Properties/Surjective.lean | 4 ++-- ConNF/{Foa => FOA}/Result.lean | 8 ++++---- ConNF/Foa.lean | 6 ------ ConNF/Foa/Action.lean | 6 ------ ConNF/Foa/Approximation.lean | 2 -- ConNF/Foa/Basic.lean | 6 ------ ConNF/Foa/Complete.lean | 6 ------ ConNF/Foa/Properties.lean | 4 ---- README.md | 2 +- docs/index.md | 2 +- 40 files changed, 105 insertions(+), 105 deletions(-) create mode 100644 ConNF/FOA.lean create mode 100644 ConNF/FOA/Action.lean rename ConNF/{Foa => FOA}/Action/Complete.lean (98%) rename ConNF/{Foa => FOA}/Action/FillAtomOrbits.lean (99%) rename ConNF/{Foa => FOA}/Action/FillAtomRange.lean (99%) rename ConNF/{Foa => FOA}/Action/NearLitterAction.lean (98%) rename ConNF/{Foa => FOA}/Action/Refine.lean (95%) rename ConNF/{Foa => FOA}/Action/StructAction.lean (91%) create mode 100644 ConNF/FOA/Approximation.lean rename ConNF/{Foa => FOA}/Approximation/NearLitterApprox.lean (98%) rename ConNF/{Foa => FOA}/Approximation/StructApprox.lean (92%) create mode 100644 ConNF/FOA/Basic.lean rename ConNF/{Foa => FOA}/Basic/CompleteOrbit.lean (100%) rename ConNF/{Foa => FOA}/Basic/Constrains.lean (99%) rename ConNF/{Foa => FOA}/Basic/Flexible.lean (99%) rename ConNF/{Foa => FOA}/Basic/Hypotheses.lean (96%) rename ConNF/{Foa => FOA}/Basic/Reduction.lean (98%) rename ConNF/{Foa => FOA}/Basic/Sublitter.lean (100%) create mode 100644 ConNF/FOA/Complete.lean rename ConNF/{Foa => FOA}/Complete/AtomCompletion.lean (89%) rename ConNF/{Foa => FOA}/Complete/CompleteAction.lean (98%) rename ConNF/{Foa => FOA}/Complete/FlexibleCompletion.lean (96%) rename ConNF/{Foa => FOA}/Complete/HypAction.lean (95%) rename ConNF/{Foa => FOA}/Complete/LitterCompletion.lean (95%) rename ConNF/{Foa => FOA}/Complete/NearLitterCompletion.lean (96%) create mode 100644 ConNF/FOA/Properties.lean rename ConNF/{Foa => FOA}/Properties/Bijective.lean (85%) rename ConNF/{Foa => FOA}/Properties/ConstrainedAction.lean (99%) rename ConNF/{Foa => FOA}/Properties/Injective.lean (99%) rename ConNF/{Foa => FOA}/Properties/Surjective.lean (99%) rename ConNF/{Foa => FOA}/Result.lean (98%) delete mode 100644 ConNF/Foa.lean delete mode 100644 ConNF/Foa/Action.lean delete mode 100644 ConNF/Foa/Approximation.lean delete mode 100644 ConNF/Foa/Basic.lean delete mode 100644 ConNF/Foa/Complete.lean delete mode 100644 ConNF/Foa/Properties.lean diff --git a/ConNF.lean b/ConNF.lean index e327ea79fa..ea02ac8039 100644 --- a/ConNF.lean +++ b/ConNF.lean @@ -3,4 +3,4 @@ import ConNF.BaseType import ConNF.Structural import ConNF.Fuzz import ConNF.NewTangle -import ConNF.Foa +import ConNF.FOA diff --git a/ConNF/FOA.lean b/ConNF/FOA.lean new file mode 100644 index 0000000000..84dd3b8656 --- /dev/null +++ b/ConNF/FOA.lean @@ -0,0 +1,6 @@ +import ConNF.FOA.Basic +import ConNF.FOA.Approximation +import ConNF.FOA.Action +import ConNF.FOA.Complete +import ConNF.FOA.Properties +import ConNF.FOA.Result diff --git a/ConNF/FOA/Action.lean b/ConNF/FOA/Action.lean new file mode 100644 index 0000000000..04229105d4 --- /dev/null +++ b/ConNF/FOA/Action.lean @@ -0,0 +1,6 @@ +import ConNF.FOA.Action.NearLitterAction +import ConNF.FOA.Action.Complete +import ConNF.FOA.Action.FillAtomOrbits +import ConNF.FOA.Action.FillAtomRange +import ConNF.FOA.Action.StructAction +import ConNF.FOA.Action.Refine diff --git a/ConNF/Foa/Action/Complete.lean b/ConNF/FOA/Action/Complete.lean similarity index 98% rename from ConNF/Foa/Action/Complete.lean rename to ConNF/FOA/Action/Complete.lean index 6883c65552..347b756243 100644 --- a/ConNF/Foa/Action/Complete.lean +++ b/ConNF/FOA/Action/Complete.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Action.NearLitterAction +import ConNF.FOA.Action.NearLitterAction /-! # Completed permutations @@ -13,7 +13,7 @@ universe u namespace ConNF variable [Params.{u}] (φ : NearLitterAction) [BasePositions] [Level] - [FoaAssumptions] {β : Λ} {A : ExtendedIndex β} + [FOAAssumptions] {β : Λ} {A : ExtendedIndex β} namespace NearLitterAction diff --git a/ConNF/Foa/Action/FillAtomOrbits.lean b/ConNF/FOA/Action/FillAtomOrbits.lean similarity index 99% rename from ConNF/Foa/Action/FillAtomOrbits.lean rename to ConNF/FOA/Action/FillAtomOrbits.lean index 90c9e4b9f7..d29c47245a 100644 --- a/ConNF/Foa/Action/FillAtomOrbits.lean +++ b/ConNF/FOA/Action/FillAtomOrbits.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Action.NearLitterAction +import ConNF.FOA.Action.NearLitterAction open Cardinal Quiver Set Sum WithBot diff --git a/ConNF/Foa/Action/FillAtomRange.lean b/ConNF/FOA/Action/FillAtomRange.lean similarity index 99% rename from ConNF/Foa/Action/FillAtomRange.lean rename to ConNF/FOA/Action/FillAtomRange.lean index 3412c31fb0..cf254e0f35 100644 --- a/ConNF/Foa/Action/FillAtomRange.lean +++ b/ConNF/FOA/Action/FillAtomRange.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Action.NearLitterAction +import ConNF.FOA.Action.NearLitterAction open Cardinal Quiver Set Sum WithBot diff --git a/ConNF/Foa/Action/NearLitterAction.lean b/ConNF/FOA/Action/NearLitterAction.lean similarity index 98% rename from ConNF/Foa/Action/NearLitterAction.lean rename to ConNF/FOA/Action/NearLitterAction.lean index 45f69eaf88..59379043ee 100644 --- a/ConNF/Foa/Action/NearLitterAction.lean +++ b/ConNF/FOA/Action/NearLitterAction.lean @@ -1,6 +1,6 @@ -import ConNF.Foa.Basic.CompleteOrbit -import ConNF.Foa.Basic.Reduction -import ConNF.Foa.Approximation.NearLitterApprox +import ConNF.FOA.Basic.CompleteOrbit +import ConNF.FOA.Basic.Reduction +import ConNF.FOA.Approximation.NearLitterApprox open Cardinal Quiver Set Sum WithBot @@ -246,7 +246,7 @@ theorem roughLitterMapOrElse_injOn (hφ : φ.Lawful) : rw [φ.roughLitterMapOrElse_of_dom hL₁, φ.roughLitterMapOrElse_of_dom hL₂] at h exact hφ.litterMap_injective hL₁ hL₂ (NearLitter.inter_nonempty_of_fst_eq_fst h) -variable [BasePositions] [Level] [FoaAssumptions] {β : Λ} {A : ExtendedIndex β} +variable [BasePositions] [Level] [FOAAssumptions] {β : Λ} {A : ExtendedIndex β} theorem mk_not_bannedLitter_and_flexible : #{L | ¬φ.BannedLitter L ∧ Flexible A L} = #μ := by refine' le_antisymm ((mk_subtype_le _).trans mk_litter.le) _ diff --git a/ConNF/Foa/Action/Refine.lean b/ConNF/FOA/Action/Refine.lean similarity index 95% rename from ConNF/Foa/Action/Refine.lean rename to ConNF/FOA/Action/Refine.lean index fba34522d4..ae9705ea21 100644 --- a/ConNF/Foa/Action/Refine.lean +++ b/ConNF/FOA/Action/Refine.lean @@ -1,7 +1,7 @@ -import ConNF.Foa.Basic.Flexible -import ConNF.Foa.Action.StructAction -import ConNF.Foa.Action.FillAtomRange -import ConNF.Foa.Action.FillAtomOrbits +import ConNF.FOA.Basic.Flexible +import ConNF.FOA.Action.StructAction +import ConNF.FOA.Action.FillAtomRange +import ConNF.FOA.Action.FillAtomOrbits open Quiver Set @@ -87,7 +87,7 @@ end StructAction namespace StructAction -variable [BasePositions] [Level] [FoaAssumptions] {β : Λ} +variable [BasePositions] [Level] [FOAAssumptions] {β : Λ} /-- Refine and complete this action into a structural approximation. -/ noncomputable def rc (φ : StructAction β) (h : φ.Lawful) : StructApprox β := diff --git a/ConNF/Foa/Action/StructAction.lean b/ConNF/FOA/Action/StructAction.lean similarity index 91% rename from ConNF/Foa/Action/StructAction.lean rename to ConNF/FOA/Action/StructAction.lean index 88c995e284..cd440e3327 100644 --- a/ConNF/Foa/Action/StructAction.lean +++ b/ConNF/FOA/Action/StructAction.lean @@ -1,6 +1,6 @@ -import ConNF.Foa.Basic.Flexible -import ConNF.Foa.Approximation.StructApprox -import ConNF.Foa.Action.Complete +import ConNF.FOA.Basic.Flexible +import ConNF.FOA.Approximation.StructApprox +import ConNF.FOA.Action.Complete open Cardinal Quiver Set Sum WithBot @@ -27,7 +27,7 @@ def Lawful {β : TypeIndex} (φ : StructAction β) : Prop := ∀ B, (φ B).Lawful /-- This structural action maps flexible litters to flexible litters. -/ -def MapFlexible [BasePositions] [Level] [FoaAssumptions] {β : Λ} (φ : StructAction β) : +def MapFlexible [BasePositions] [Level] [FOAAssumptions] {β : Λ} (φ : StructAction β) : Prop := ∀ (B) (L : Litter) (hL), Flexible B L → Flexible B (((φ B).litterMap L).get hL).1 @@ -36,7 +36,7 @@ section Precise def Precise {β : TypeIndex} (φ : StructAction β) : Prop := ∀ B, (φ B).Precise -variable [BasePositions] [Level] [FoaAssumptions] {β : Λ} (φ : StructAction β) +variable [BasePositions] [Level] [FOAAssumptions] {β : Λ} (φ : StructAction β) noncomputable def complete (hφ : φ.Lawful) : StructApprox β := fun B => (φ B).complete (hφ B) B @@ -67,7 +67,7 @@ theorem smul_nearLitter_eq_of_precise {hφ : φ.Lawful} (hφp : φ.Precise) {π end Precise -variable [BasePositions] [Level] [FoaAssumptions] {β : Λ} +variable [BasePositions] [Level] [FOAAssumptions] {β : Λ} instance {β : TypeIndex} : PartialOrder (StructAction β) where diff --git a/ConNF/FOA/Approximation.lean b/ConNF/FOA/Approximation.lean new file mode 100644 index 0000000000..ee252437b1 --- /dev/null +++ b/ConNF/FOA/Approximation.lean @@ -0,0 +1,2 @@ +import ConNF.FOA.Approximation.NearLitterApprox +import ConNF.FOA.Approximation.StructApprox diff --git a/ConNF/Foa/Approximation/NearLitterApprox.lean b/ConNF/FOA/Approximation/NearLitterApprox.lean similarity index 98% rename from ConNF/Foa/Approximation/NearLitterApprox.lean rename to ConNF/FOA/Approximation/NearLitterApprox.lean index 0ead3063be..dc4cacda50 100644 --- a/ConNF/Foa/Approximation/NearLitterApprox.lean +++ b/ConNF/FOA/Approximation/NearLitterApprox.lean @@ -1,6 +1,6 @@ import ConNF.Mathlib.Logic.Equiv.LocalPerm -import ConNF.Foa.Basic.Flexible -import ConNF.Foa.Basic.Sublitter +import ConNF.FOA.Basic.Flexible +import ConNF.FOA.Basic.Sublitter open Quiver Set Sum @@ -196,7 +196,7 @@ theorem ExactlyApproximates.mem_litterSet_inv {π₀ : NearLitterApprox} {π : N (hπ : π₀.ExactlyApproximates π) (a : Atom) (ha : a ∉ π₀.atomPerm.domain) : π⁻¹ • a ∈ litterSet (π⁻¹ • a.1) := by contrapose! ha; exact hπ.exception_mem _ (Or.inr ha) -def Free [BasePositions] [Level] [FoaAssumptions] {β : TypeIndex} (π : NearLitterApprox) +def Free [BasePositions] [Level] [FOAAssumptions] {β : TypeIndex} (π : NearLitterApprox) (A : ExtendedIndex β) : Prop := ∀ L ∈ π.litterPerm.domain, Flexible A L diff --git a/ConNF/Foa/Approximation/StructApprox.lean b/ConNF/FOA/Approximation/StructApprox.lean similarity index 92% rename from ConNF/Foa/Approximation/StructApprox.lean rename to ConNF/FOA/Approximation/StructApprox.lean index fea9028746..65052d9b53 100644 --- a/ConNF/Foa/Approximation/StructApprox.lean +++ b/ConNF/FOA/Approximation/StructApprox.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Approximation.NearLitterApprox +import ConNF.FOA.Approximation.NearLitterApprox open Quiver Set Sum @@ -27,7 +27,7 @@ def Approximates {β : TypeIndex} (π₀ : StructApprox β) (π : StructPerm β) def ExactlyApproximates {β : TypeIndex} (π₀ : StructApprox β) (π : StructPerm β) : Prop := ∀ A, (π₀ A).ExactlyApproximates (π A) -variable [BasePositions] [Level] [FoaAssumptions] +variable [BasePositions] [Level] [FOAAssumptions] def Free {β : Λ} (π₀ : StructApprox β) : Prop := ∀ A, (π₀ A).Free A diff --git a/ConNF/FOA/Basic.lean b/ConNF/FOA/Basic.lean new file mode 100644 index 0000000000..a5ad54c35c --- /dev/null +++ b/ConNF/FOA/Basic.lean @@ -0,0 +1,6 @@ +import ConNF.FOA.Basic.CompleteOrbit +import ConNF.FOA.Basic.Sublitter +import ConNF.FOA.Basic.Hypotheses +import ConNF.FOA.Basic.Constrains +import ConNF.FOA.Basic.Reduction +import ConNF.FOA.Basic.Flexible diff --git a/ConNF/Foa/Basic/CompleteOrbit.lean b/ConNF/FOA/Basic/CompleteOrbit.lean similarity index 100% rename from ConNF/Foa/Basic/CompleteOrbit.lean rename to ConNF/FOA/Basic/CompleteOrbit.lean diff --git a/ConNF/Foa/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean similarity index 99% rename from ConNF/Foa/Basic/Constrains.lean rename to ConNF/FOA/Basic/Constrains.lean index cde1e33707..511a997619 100644 --- a/ConNF/Foa/Basic/Constrains.lean +++ b/ConNF/FOA/Basic/Constrains.lean @@ -1,6 +1,6 @@ import Mathlib.Data.Prod.Lex import ConNF.Fuzz -import ConNF.Foa.Basic.Hypotheses +import ConNF.FOA.Basic.Hypotheses /-! # Constraints @@ -58,7 +58,7 @@ theorem pos_atomNearLitter_inr (N : NearLitter) : end ExtendedIndex -variable [BasePositions] [Level] [FoaAssumptions] {β : Λ} +variable [BasePositions] [Level] [FOAAssumptions] {β : Λ} /-- Support conditions can be said to *constrain* each other in a number of ways. 1. `(L, A) ≺ (a, A)` when `a ∈ L` and `L` is a litter. We can say that an atom is constrained by the diff --git a/ConNF/Foa/Basic/Flexible.lean b/ConNF/FOA/Basic/Flexible.lean similarity index 99% rename from ConNF/Foa/Basic/Flexible.lean rename to ConNF/FOA/Basic/Flexible.lean index 5d298e0c65..7570fc5122 100644 --- a/ConNF/Foa/Basic/Flexible.lean +++ b/ConNF/FOA/Basic/Flexible.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Basic.Constrains +import ConNF.FOA.Basic.Constrains open Quiver Set Sum WithBot @@ -8,7 +8,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : TypeIndex} +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : TypeIndex} /-- A litter is *inflexible* if it is the image of some f-map. -/ @[mk_iff] diff --git a/ConNF/Foa/Basic/Hypotheses.lean b/ConNF/FOA/Basic/Hypotheses.lean similarity index 96% rename from ConNF/Foa/Basic/Hypotheses.lean rename to ConNF/FOA/Basic/Hypotheses.lean index 4eb7cca048..6547b84e4c 100644 --- a/ConNF/Foa/Basic/Hypotheses.lean +++ b/ConNF/FOA/Basic/Hypotheses.lean @@ -9,8 +9,8 @@ This file contains the inductive hypotheses required for proving the freedom of * `ConNF.PositionedTypedObjects`: Asserts that the positions of typed objects agree with the position functions defined on atoms and near-litters in `BasePositions`. -* `ConNF.FoaData`: Contains various kinds of tangle data for all levels below `α`. -* `ConNF.FoaAssumptions`: Describes how the type levels in the `FoaData` tangle together. +* `ConNF.FOAData`: Contains various kinds of tangle data for all levels below `α`. +* `ConNF.FOAAssumptions`: Describes how the type levels in the `FOAData` tangle together. -/ open Set WithBot @@ -49,15 +49,15 @@ This structure combines the following data: * `pos : Tangle β ↪ μ` * `typedAtom` and `typedNearLitter` -/ -class FoaData where +class FOAData where lowerTangleData : ∀ β : Λ, [LeLevel β] → TangleData β lowerPositionedTangles : ∀ β : Λ, [LtLevel β] → PositionedTangles β lowerTypedObjects : ∀ β : Λ, [LeLevel β] → TypedObjects β lowerPositionedTypedObjects : ∀ β : Λ, [LtLevel β] → PositionedTypedObjects β -namespace FoaData +namespace FOAData -variable [FoaData] {β : Λ} [LeLevel β] {γ : Λ} [LtLevel γ] +variable [FOAData] {β : Λ} [LeLevel β] {γ : Λ} [LtLevel γ] instance tangleData : TangleData β := lowerTangleData β @@ -79,10 +79,10 @@ noncomputable instance iioBotPositionedTangles : ∀ β : TypeIndex, [LtLevel β | ⊥, _ => Bot.positionedTangles | (β : Λ), _ => lowerPositionedTangles β -end FoaData +end FOAData /-- Assumptions detailing how the different levels of the tangled structure interact. -/ -class FoaAssumptions extends FoaData where +class FOAAssumptions extends FOAData where /-- The one-step derivative map between types of allowable permutations. We can think of this map as `cons`ing a single morphism on a path. -/ allowableCons : @@ -117,12 +117,12 @@ class FoaAssumptions extends FoaData where (γ : TypeIndex) [LtLevel γ] (hγ : γ < β) : allowableCons hγ (allowableOfSmulFuzz β ρs h) = ρs γ hγ -export FoaAssumptions (allowableCons allowableCons_eq designatedSupport_smul +export FOAAssumptions (allowableCons allowableCons_eq designatedSupport_smul smul_fuzz allowableOfSmulFuzz allowableOfSmulFuzz_comp_eq) attribute [simp] designatedSupport_smul allowableOfSmulFuzz_comp_eq -variable [FoaAssumptions] +variable [FOAAssumptions] /-- A primitive version of `Allowable.comp` with different arguments. This is always the wrong spelling to use. -/ @@ -148,7 +148,7 @@ def Allowable.comp {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (A : Quiver.Pat Allowable.comp' A /-! We prove that `Allowable.comp` is functorial. In addition, we prove a number of lemmas about -`FoaAssumptions`. -/ +`FOAAssumptions`. -/ @[simp] theorem Allowable.comp_nil {β : TypeIndex} [LeLevel β] : diff --git a/ConNF/Foa/Basic/Reduction.lean b/ConNF/FOA/Basic/Reduction.lean similarity index 98% rename from ConNF/Foa/Basic/Reduction.lean rename to ConNF/FOA/Basic/Reduction.lean index f346ef40a2..15145e667e 100644 --- a/ConNF/Foa/Basic/Reduction.lean +++ b/ConNF/FOA/Basic/Reduction.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Basic.Constrains +import ConNF.FOA.Basic.Constrains /-! # Reductions of supports @@ -25,7 +25,7 @@ open scoped Cardinal Pointwise namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] variable {β : Λ} {G : Type _} {τ : Type _} [SMul G (SupportCondition β)] [SMul G τ] {x : τ} /-- A support condition is *reduced* if it is an atom or a litter. -/ diff --git a/ConNF/Foa/Basic/Sublitter.lean b/ConNF/FOA/Basic/Sublitter.lean similarity index 100% rename from ConNF/Foa/Basic/Sublitter.lean rename to ConNF/FOA/Basic/Sublitter.lean diff --git a/ConNF/FOA/Complete.lean b/ConNF/FOA/Complete.lean new file mode 100644 index 0000000000..c9cdf13d80 --- /dev/null +++ b/ConNF/FOA/Complete.lean @@ -0,0 +1,6 @@ +import ConNF.FOA.Complete.HypAction +import ConNF.FOA.Complete.AtomCompletion +import ConNF.FOA.Complete.FlexibleCompletion +import ConNF.FOA.Complete.LitterCompletion +import ConNF.FOA.Complete.NearLitterCompletion +import ConNF.FOA.Complete.CompleteAction diff --git a/ConNF/Foa/Complete/AtomCompletion.lean b/ConNF/FOA/Complete/AtomCompletion.lean similarity index 89% rename from ConNF/Foa/Complete/AtomCompletion.lean rename to ConNF/FOA/Complete/AtomCompletion.lean index 0bc593454f..6ed14443e3 100644 --- a/ConNF/Foa/Complete/AtomCompletion.lean +++ b/ConNF/FOA/Complete/AtomCompletion.lean @@ -1,5 +1,5 @@ -import ConNF.Foa.Complete.HypAction -import ConNF.Foa.Approximation +import ConNF.FOA.Complete.HypAction +import ConNF.FOA.Approximation open Set Sum @@ -9,7 +9,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} (π : StructApprox β) +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} (π : StructApprox β) namespace StructApprox diff --git a/ConNF/Foa/Complete/CompleteAction.lean b/ConNF/FOA/Complete/CompleteAction.lean similarity index 98% rename from ConNF/Foa/Complete/CompleteAction.lean rename to ConNF/FOA/Complete/CompleteAction.lean index 4477dcbfa4..0fe120a504 100644 --- a/ConNF/Foa/Complete/CompleteAction.lean +++ b/ConNF/FOA/Complete/CompleteAction.lean @@ -1,6 +1,6 @@ import Mathlib.Order.Extension.Well -import ConNF.Foa.Complete.AtomCompletion -import ConNF.Foa.Complete.NearLitterCompletion +import ConNF.FOA.Complete.AtomCompletion +import ConNF.FOA.Complete.NearLitterCompletion open Equiv Function Quiver Set Sum WithBot @@ -12,7 +12,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] /-! diff --git a/ConNF/Foa/Complete/FlexibleCompletion.lean b/ConNF/FOA/Complete/FlexibleCompletion.lean similarity index 96% rename from ConNF/Foa/Complete/FlexibleCompletion.lean rename to ConNF/FOA/Complete/FlexibleCompletion.lean index bd560465df..45f84fc7b1 100644 --- a/ConNF/Foa/Complete/FlexibleCompletion.lean +++ b/ConNF/FOA/Complete/FlexibleCompletion.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Approximation.NearLitterApprox +import ConNF.FOA.Approximation.NearLitterApprox open Set @@ -8,7 +8,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : TypeIndex} +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : TypeIndex} (π : NearLitterApprox) (A : ExtendedIndex β) namespace NearLitterApprox diff --git a/ConNF/Foa/Complete/HypAction.lean b/ConNF/FOA/Complete/HypAction.lean similarity index 95% rename from ConNF/Foa/Complete/HypAction.lean rename to ConNF/FOA/Complete/HypAction.lean index 0055e7ae5f..d4aca30719 100644 --- a/ConNF/Foa/Complete/HypAction.lean +++ b/ConNF/FOA/Complete/HypAction.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Basic.Constrains +import ConNF.FOA.Basic.Constrains open Quiver Set Sum @@ -8,7 +8,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] /-! # Induction on support conditions diff --git a/ConNF/Foa/Complete/LitterCompletion.lean b/ConNF/FOA/Complete/LitterCompletion.lean similarity index 95% rename from ConNF/Foa/Complete/LitterCompletion.lean rename to ConNF/FOA/Complete/LitterCompletion.lean index 85b6e35ee1..1c092e7875 100644 --- a/ConNF/Foa/Complete/LitterCompletion.lean +++ b/ConNF/FOA/Complete/LitterCompletion.lean @@ -1,7 +1,7 @@ -import ConNF.Foa.Basic.Reduction -import ConNF.Foa.Complete.HypAction -import ConNF.Foa.Action.Refine -import ConNF.Foa.Complete.FlexibleCompletion +import ConNF.FOA.Basic.Reduction +import ConNF.FOA.Complete.HypAction +import ConNF.FOA.Action.Refine +import ConNF.FOA.Complete.FlexibleCompletion open Quiver Set Sum WithBot @@ -13,16 +13,16 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] /-- The inductive hypothesis used for proving freedom of action: Every free approximation exactly approximates some allowable permutation. -/ -def FoaIh (β : Λ) [LeLevel β] : Prop := +def FOAIh (β : Λ) [LeLevel β] : Prop := ∀ π₀ : StructApprox β, π₀.Free → ∃ π : Allowable β, π₀.ExactlyApproximates (Allowable.toStructPerm π) class FreedomOfActionHypothesis (β : Λ) [LeLevel β] : Prop where - freedomOfAction_of_lt : ∀ γ < β, [LeLevel γ] → FoaIh γ + freedomOfAction_of_lt : ∀ γ < β, [LeLevel γ] → FOAIh γ export FreedomOfActionHypothesis (freedomOfAction_of_lt) diff --git a/ConNF/Foa/Complete/NearLitterCompletion.lean b/ConNF/FOA/Complete/NearLitterCompletion.lean similarity index 96% rename from ConNF/Foa/Complete/NearLitterCompletion.lean rename to ConNF/FOA/Complete/NearLitterCompletion.lean index dbd16d2e61..0140fc3640 100644 --- a/ConNF/Foa/Complete/NearLitterCompletion.lean +++ b/ConNF/FOA/Complete/NearLitterCompletion.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Complete.LitterCompletion +import ConNF.FOA.Complete.LitterCompletion open Set Sum @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] def nearLitterHypothesis (A : ExtendedIndex β) (N : NearLitter) (H : HypAction ⟨A, inr N⟩) : diff --git a/ConNF/FOA/Properties.lean b/ConNF/FOA/Properties.lean new file mode 100644 index 0000000000..958175e469 --- /dev/null +++ b/ConNF/FOA/Properties.lean @@ -0,0 +1,4 @@ +import ConNF.FOA.Properties.ConstrainedAction +import ConNF.FOA.Properties.Injective +import ConNF.FOA.Properties.Surjective +import ConNF.FOA.Properties.Bijective diff --git a/ConNF/Foa/Properties/Bijective.lean b/ConNF/FOA/Properties/Bijective.lean similarity index 85% rename from ConNF/Foa/Properties/Bijective.lean rename to ConNF/FOA/Properties/Bijective.lean index dcdac87483..ac49f461fd 100644 --- a/ConNF/Foa/Properties/Bijective.lean +++ b/ConNF/FOA/Properties/Bijective.lean @@ -1,5 +1,5 @@ -import ConNF.Foa.Properties.Injective -import ConNF.Foa.Properties.Surjective +import ConNF.FOA.Properties.Injective +import ConNF.FOA.Properties.Surjective open Equiv Function Quiver Set Sum WithBot @@ -11,7 +11,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] {π : StructApprox β} theorem completeAtomMap_bijective (hπf : π.Free) (A : ExtendedIndex β) : diff --git a/ConNF/Foa/Properties/ConstrainedAction.lean b/ConNF/FOA/Properties/ConstrainedAction.lean similarity index 99% rename from ConNF/Foa/Properties/ConstrainedAction.lean rename to ConNF/FOA/Properties/ConstrainedAction.lean index 1101ddb219..13f09d0797 100644 --- a/ConNF/Foa/Properties/ConstrainedAction.lean +++ b/ConNF/FOA/Properties/ConstrainedAction.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Complete +import ConNF.FOA.Complete open Equiv Function Quiver Set Sum WithBot @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] def transConstrained (c d : SupportCondition β) : Set (SupportCondition β) := diff --git a/ConNF/Foa/Properties/Injective.lean b/ConNF/FOA/Properties/Injective.lean similarity index 99% rename from ConNF/Foa/Properties/Injective.lean rename to ConNF/FOA/Properties/Injective.lean index 3cc9d1f78b..de279845c8 100644 --- a/ConNF/Foa/Properties/Injective.lean +++ b/ConNF/FOA/Properties/Injective.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Properties.ConstrainedAction +import ConNF.FOA.Properties.ConstrainedAction open Equiv Function Quiver Set Sum WithBot @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] {π : StructApprox β} theorem atom_injective_extends {c d : SupportCondition β} (hcd : (ihsAction π c d).Lawful) diff --git a/ConNF/Foa/Properties/Surjective.lean b/ConNF/FOA/Properties/Surjective.lean similarity index 99% rename from ConNF/Foa/Properties/Surjective.lean rename to ConNF/FOA/Properties/Surjective.lean index 286769ec07..2e3d71231f 100644 --- a/ConNF/Foa/Properties/Surjective.lean +++ b/ConNF/FOA/Properties/Surjective.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Properties.Injective +import ConNF.FOA.Properties.Injective open Equiv Function Quiver Set Sum WithBot @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] {π : StructApprox β} theorem completeNearLitterMap_subset_range (A : ExtendedIndex β) (L : Litter) : diff --git a/ConNF/Foa/Result.lean b/ConNF/FOA/Result.lean similarity index 98% rename from ConNF/Foa/Result.lean rename to ConNF/FOA/Result.lean index 1053145d02..05e8f1f114 100644 --- a/ConNF/Foa/Result.lean +++ b/ConNF/FOA/Result.lean @@ -1,4 +1,4 @@ -import ConNF.Foa.Properties.Bijective +import ConNF.FOA.Properties.Bijective open Equiv Function Quiver Set Sum WithBot @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FoaAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] {π : StructApprox β} noncomputable def completeAtomPerm (hπf : π.Free) (A : ExtendedIndex β) : Perm Atom := @@ -265,7 +265,7 @@ theorem completeAllowable_exactlyApproximates (hπf : π.Free) : rw [completeAllowable_comp] at ha exact complete_exception_mem hπf A a ha -def foa_extends : FoaIh β := fun _ hπf => +def foa_extends : FOAIh β := fun _ hπf => ⟨completeAllowable hπf, completeAllowable_exactlyApproximates hπf⟩ theorem freedom_of_action (β : Λ) [i : LeLevel β] (π₀ : StructApprox β) (h : π₀.Free) : @@ -274,7 +274,7 @@ theorem freedom_of_action (β : Λ) [i : LeLevel β] (π₀ : StructApprox β) ( have := WellFounded.induction (C := fun β => ∀ (i : LeLevel β) (π₀ : StructApprox β), Free π₀ → ∃ π : Allowable β, - ExactlyApproximates π₀ (@Allowable.toStructPerm _ _ FoaData.tangleData π)) Λwo.wf β + ExactlyApproximates π₀ (@Allowable.toStructPerm _ _ FOAData.tangleData π)) Λwo.wf β refine fun i => this ?_ i π₀ h intro β ih _ π₀ h have : FreedomOfActionHypothesis β diff --git a/ConNF/Foa.lean b/ConNF/Foa.lean deleted file mode 100644 index 0a1729b7dd..0000000000 --- a/ConNF/Foa.lean +++ /dev/null @@ -1,6 +0,0 @@ -import ConNF.Foa.Basic -import ConNF.Foa.Approximation -import ConNF.Foa.Action -import ConNF.Foa.Complete -import ConNF.Foa.Properties -import ConNF.Foa.Result diff --git a/ConNF/Foa/Action.lean b/ConNF/Foa/Action.lean deleted file mode 100644 index e66e9b2775..0000000000 --- a/ConNF/Foa/Action.lean +++ /dev/null @@ -1,6 +0,0 @@ -import ConNF.Foa.Action.NearLitterAction -import ConNF.Foa.Action.Complete -import ConNF.Foa.Action.FillAtomOrbits -import ConNF.Foa.Action.FillAtomRange -import ConNF.Foa.Action.StructAction -import ConNF.Foa.Action.Refine diff --git a/ConNF/Foa/Approximation.lean b/ConNF/Foa/Approximation.lean deleted file mode 100644 index b42a715771..0000000000 --- a/ConNF/Foa/Approximation.lean +++ /dev/null @@ -1,2 +0,0 @@ -import ConNF.Foa.Approximation.NearLitterApprox -import ConNF.Foa.Approximation.StructApprox diff --git a/ConNF/Foa/Basic.lean b/ConNF/Foa/Basic.lean deleted file mode 100644 index 58e2486651..0000000000 --- a/ConNF/Foa/Basic.lean +++ /dev/null @@ -1,6 +0,0 @@ -import ConNF.Foa.Basic.CompleteOrbit -import ConNF.Foa.Basic.Sublitter -import ConNF.Foa.Basic.Hypotheses -import ConNF.Foa.Basic.Constrains -import ConNF.Foa.Basic.Reduction -import ConNF.Foa.Basic.Flexible diff --git a/ConNF/Foa/Complete.lean b/ConNF/Foa/Complete.lean deleted file mode 100644 index 452ac6be5e..0000000000 --- a/ConNF/Foa/Complete.lean +++ /dev/null @@ -1,6 +0,0 @@ -import ConNF.Foa.Complete.HypAction -import ConNF.Foa.Complete.AtomCompletion -import ConNF.Foa.Complete.FlexibleCompletion -import ConNF.Foa.Complete.LitterCompletion -import ConNF.Foa.Complete.NearLitterCompletion -import ConNF.Foa.Complete.CompleteAction diff --git a/ConNF/Foa/Properties.lean b/ConNF/Foa/Properties.lean deleted file mode 100644 index a34536551d..0000000000 --- a/ConNF/Foa/Properties.lean +++ /dev/null @@ -1,4 +0,0 @@ -import ConNF.Foa.Properties.ConstrainedAction -import ConNF.Foa.Properties.Injective -import ConNF.Foa.Properties.Surjective -import ConNF.Foa.Properties.Bijective diff --git a/README.md b/README.md index e57f23250e..60ee096659 100644 --- a/README.md +++ b/README.md @@ -63,7 +63,7 @@ This allows us to satisfy TTT's extensionality axiom. Each type α can only be constructed under the assumption that all types β < α are of size exactly μ. It is easy to prove that the type of α-tangles has cardinality at least μ, so we need to show that there are at most μ elements of this set. We do this by showing that there are not that many fundamentally different descriptions of tangles under the action of allowable permutations. -This requires the [freedom of action theorem](https://leanprover-community.github.io/con-nf/doc/ConNF/Foa/Result.html#ConNF.StructApprox.freedom_of_action), which is a technical lemma that allows us to construct allowable permutations. +This requires the [freedom of action theorem](https://leanprover-community.github.io/con-nf/doc/ConNF/FOA/Result.html#ConNF.StructApprox.freedom_of_action), which is a technical lemma that allows us to construct allowable permutations. ### Finishing the induction diff --git a/docs/index.md b/docs/index.md index b80bd279e3..b1f03c4b10 100644 --- a/docs/index.md +++ b/docs/index.md @@ -68,7 +68,7 @@ This allows us to satisfy TTT's extensionality axiom. Each type α can only be constructed under the assumption that all types β < α are of size exactly μ. It is easy to prove that the type of α-tangles has cardinality at least μ, so we need to show that there are at most μ elements of this set. We do this by showing that there are not that many fundamentally different descriptions of tangles under the action of allowable permutations. -This requires the [freedom of action theorem](https://leanprover-community.github.io/con-nf/doc/ConNF/Foa/Result.html#ConNF.StructApprox.freedom_of_action), which is a technical lemma that allows us to construct allowable permutations. +This requires the [freedom of action theorem](https://leanprover-community.github.io/con-nf/doc/ConNF/FOA/Result.html#ConNF.StructApprox.freedom_of_action), which is a technical lemma that allows us to construct allowable permutations. ### Finishing the induction