From 39c33b4a743bea62dbcc549548b712ffd38ca65c Mon Sep 17 00:00:00 2001 From: Sky Wilshaw Date: Thu, 5 Dec 2024 10:07:03 +0000 Subject: [PATCH] More refactoring Signed-off-by: Sky Wilshaw --- ConNF.lean | 20 +++++++++---------- ConNF/Construction/Code.lean | 2 +- ConNF/Counting/CodingFunction.lean | 2 +- ConNF/Counting/Twist.lean | 2 +- ConNF/FOA/BaseApprox.lean | 2 +- ConNF/FOA/Coherent.lean | 2 +- ConNF/FOA/Inflexible.lean | 2 +- ConNF/FOA/StrApprox.lean | 2 +- ConNF/Model/InductionStatement.lean | 2 +- .../{Coherent => ModelData}/CoherentData.lean | 8 ++++---- .../{Coherent => ModelData}/Enumeration.lean | 0 ConNF/{Coherent => ModelData}/Fuzz.lean | 4 ++-- ConNF/{Levels => ModelData}/Level.lean | 0 ConNF/{Coherent => ModelData}/ModelData.lean | 2 +- .../PathEnumeration.lean | 2 +- ConNF/{Coherent => ModelData}/Support.lean | 2 +- ConNF/{Levels => Position}/BasePositions.lean | 2 +- ConNF/{Levels => Position}/Deny.lean | 2 +- ConNF/{Base => Position}/Position.lean | 0 19 files changed, 29 insertions(+), 29 deletions(-) rename ConNF/{Coherent => ModelData}/CoherentData.lean (97%) rename ConNF/{Coherent => ModelData}/Enumeration.lean (100%) rename ConNF/{Coherent => ModelData}/Fuzz.lean (95%) rename ConNF/{Levels => ModelData}/Level.lean (100%) rename ConNF/{Coherent => ModelData}/ModelData.lean (99%) rename ConNF/{Coherent => ModelData}/PathEnumeration.lean (99%) rename ConNF/{Coherent => ModelData}/Support.lean (99%) rename ConNF/{Levels => Position}/BasePositions.lean (98%) rename ConNF/{Levels => Position}/Deny.lean (99%) rename ConNF/{Base => Position}/Position.lean (100%) diff --git a/ConNF.lean b/ConNF.lean index 35073869be..402b492397 100644 --- a/ConNF.lean +++ b/ConNF.lean @@ -12,15 +12,8 @@ import ConNF.Base.BasePerm import ConNF.Base.Litter import ConNF.Base.NearLitter import ConNF.Base.Params -import ConNF.Base.Position import ConNF.Base.Small import ConNF.Base.TypeIndex -import ConNF.Coherent.CoherentData -import ConNF.Coherent.Enumeration -import ConNF.Coherent.Fuzz -import ConNF.Coherent.ModelData -import ConNF.Coherent.PathEnumeration -import ConNF.Coherent.Support import ConNF.Construction.Code import ConNF.Construction.NewModelData import ConNF.Counting.BaseCoding @@ -39,9 +32,6 @@ import ConNF.FOA.StrAction import ConNF.FOA.StrActionFOA import ConNF.FOA.StrApprox import ConNF.FOA.StrApproxFOA -import ConNF.Levels.BasePositions -import ConNF.Levels.Deny -import ConNF.Levels.Level import ConNF.Levels.Path import ConNF.Levels.StrPerm import ConNF.Levels.StrSet @@ -55,6 +45,16 @@ import ConNF.Model.RaiseStrong import ConNF.Model.Result import ConNF.Model.RunInduction import ConNF.Model.TTT +import ConNF.ModelData.CoherentData +import ConNF.ModelData.Enumeration +import ConNF.ModelData.Fuzz +import ConNF.ModelData.Level +import ConNF.ModelData.ModelData +import ConNF.ModelData.PathEnumeration +import ConNF.ModelData.Support +import ConNF.Position.BasePositions +import ConNF.Position.Deny +import ConNF.Position.Position import ConNF.Strong.SMulSpec import ConNF.Strong.Spec import ConNF.Strong.SpecSame diff --git a/ConNF/Construction/Code.lean b/ConNF/Construction/Code.lean index 5a5d76ba1c..9d3982b8d5 100644 --- a/ConNF/Construction/Code.lean +++ b/ConNF/Construction/Code.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.CoherentData +import ConNF.ModelData.CoherentData /-! # Codes diff --git a/ConNF/Counting/CodingFunction.lean b/ConNF/Counting/CodingFunction.lean index 9f4df6531a..71b18d4cbf 100644 --- a/ConNF/Counting/CodingFunction.lean +++ b/ConNF/Counting/CodingFunction.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.CoherentData +import ConNF.ModelData.CoherentData /-! # Coding functions diff --git a/ConNF/Counting/Twist.lean b/ConNF/Counting/Twist.lean index dcb18d97bd..3a0a71ac4a 100644 --- a/ConNF/Counting/Twist.lean +++ b/ConNF/Counting/Twist.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.ModelData +import ConNF.ModelData.ModelData /-! # Twisting sets diff --git a/ConNF/FOA/BaseApprox.lean b/ConNF/FOA/BaseApprox.lean index 96d97b0500..549061ab03 100644 --- a/ConNF/FOA/BaseApprox.lean +++ b/ConNF/FOA/BaseApprox.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.Support +import ConNF.ModelData.Support import ConNF.FOA.Coherent /-! diff --git a/ConNF/FOA/Coherent.lean b/ConNF/FOA/Coherent.lean index a7142e79ac..18d5dd13e0 100644 --- a/ConNF/FOA/Coherent.lean +++ b/ConNF/FOA/Coherent.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.CoherentData +import ConNF.ModelData.CoherentData import ConNF.FOA.Inflexible /-! diff --git a/ConNF/FOA/Inflexible.lean b/ConNF/FOA/Inflexible.lean index 6e2a42e704..3177471b14 100644 --- a/ConNF/FOA/Inflexible.lean +++ b/ConNF/FOA/Inflexible.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.CoherentData +import ConNF.ModelData.CoherentData /-! # New file diff --git a/ConNF/FOA/StrApprox.lean b/ConNF/FOA/StrApprox.lean index 3c481a8dfb..f9fa1140eb 100644 --- a/ConNF/FOA/StrApprox.lean +++ b/ConNF/FOA/StrApprox.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.CoherentData +import ConNF.ModelData.CoherentData import ConNF.FOA.BaseApprox /-! diff --git a/ConNF/Model/InductionStatement.lean b/ConNF/Model/InductionStatement.lean index 6f67760e09..1468952ccd 100644 --- a/ConNF/Model/InductionStatement.lean +++ b/ConNF/Model/InductionStatement.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.CoherentData +import ConNF.ModelData.CoherentData import ConNF.Construction.Code /-! diff --git a/ConNF/Coherent/CoherentData.lean b/ConNF/ModelData/CoherentData.lean similarity index 97% rename from ConNF/Coherent/CoherentData.lean rename to ConNF/ModelData/CoherentData.lean index f32fa11c33..802645c7bd 100644 --- a/ConNF/Coherent/CoherentData.lean +++ b/ConNF/ModelData/CoherentData.lean @@ -1,6 +1,6 @@ -import ConNF.Coherent.Fuzz -import ConNF.Levels.Level -import ConNF.Coherent.ModelData +import ConNF.ModelData.Fuzz +import ConNF.ModelData.Level +import ConNF.ModelData.ModelData /-! # Coherent data @@ -9,7 +9,7 @@ In this file, we define the type of coherent data below a particular proper type ## Main declarations -* `ConNF.CoherentData`: Coherent data below a given level `α`. +* `ConNF.ModelDataData`: Coherent data below a given level `α`. -/ noncomputable section diff --git a/ConNF/Coherent/Enumeration.lean b/ConNF/ModelData/Enumeration.lean similarity index 100% rename from ConNF/Coherent/Enumeration.lean rename to ConNF/ModelData/Enumeration.lean diff --git a/ConNF/Coherent/Fuzz.lean b/ConNF/ModelData/Fuzz.lean similarity index 95% rename from ConNF/Coherent/Fuzz.lean rename to ConNF/ModelData/Fuzz.lean index 4db6f8ded6..36c93c3ad6 100644 --- a/ConNF/Coherent/Fuzz.lean +++ b/ConNF/ModelData/Fuzz.lean @@ -1,5 +1,5 @@ -import ConNF.Levels.BasePositions -import ConNF.Coherent.ModelData +import ConNF.Position.BasePositions +import ConNF.ModelData.ModelData /-! # The `fuzz` map diff --git a/ConNF/Levels/Level.lean b/ConNF/ModelData/Level.lean similarity index 100% rename from ConNF/Levels/Level.lean rename to ConNF/ModelData/Level.lean diff --git a/ConNF/Coherent/ModelData.lean b/ConNF/ModelData/ModelData.lean similarity index 99% rename from ConNF/Coherent/ModelData.lean rename to ConNF/ModelData/ModelData.lean index f084ad6bcc..09f4c444a3 100644 --- a/ConNF/Coherent/ModelData.lean +++ b/ConNF/ModelData/ModelData.lean @@ -1,5 +1,5 @@ import ConNF.Levels.StrSet -import ConNF.Coherent.Support +import ConNF.ModelData.Support /-! # Model data diff --git a/ConNF/Coherent/PathEnumeration.lean b/ConNF/ModelData/PathEnumeration.lean similarity index 99% rename from ConNF/Coherent/PathEnumeration.lean rename to ConNF/ModelData/PathEnumeration.lean index 0df30e0d51..0dad8bd086 100644 --- a/ConNF/Coherent/PathEnumeration.lean +++ b/ConNF/ModelData/PathEnumeration.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.Enumeration +import ConNF.ModelData.Enumeration import ConNF.Levels.StrPerm /-! diff --git a/ConNF/Coherent/Support.lean b/ConNF/ModelData/Support.lean similarity index 99% rename from ConNF/Coherent/Support.lean rename to ConNF/ModelData/Support.lean index 9963ff550b..8d46511911 100644 --- a/ConNF/Coherent/Support.lean +++ b/ConNF/ModelData/Support.lean @@ -1,4 +1,4 @@ -import ConNF.Coherent.PathEnumeration +import ConNF.ModelData.PathEnumeration /-! # Supports diff --git a/ConNF/Levels/BasePositions.lean b/ConNF/Position/BasePositions.lean similarity index 98% rename from ConNF/Levels/BasePositions.lean rename to ConNF/Position/BasePositions.lean index 34612912af..75f295d00a 100644 --- a/ConNF/Levels/BasePositions.lean +++ b/ConNF/Position/BasePositions.lean @@ -1,4 +1,4 @@ -import ConNF.Levels.Deny +import ConNF.Position.Deny import ConNF.Base.NearLitter /-! diff --git a/ConNF/Levels/Deny.lean b/ConNF/Position/Deny.lean similarity index 99% rename from ConNF/Levels/Deny.lean rename to ConNF/Position/Deny.lean index e5aa1638bf..8548fee96b 100644 --- a/ConNF/Levels/Deny.lean +++ b/ConNF/Position/Deny.lean @@ -1,4 +1,4 @@ -import ConNF.Base.Position +import ConNF.Position.Position /-! # Injective functions from denied sets diff --git a/ConNF/Base/Position.lean b/ConNF/Position/Position.lean similarity index 100% rename from ConNF/Base/Position.lean rename to ConNF/Position/Position.lean