Reintroduce base positions

Signed-off-by: zeramorphic <[email protected]>
leanprover-community · Mar 19, 2024 · 33668f5 · 33668f5
1 parent 5ea4ef8
commit 33668f5
Show file tree

Hide file tree

Showing 45 changed files with 204 additions and 326 deletions.
diff --git a/ConNF/Counting/CodingFunction.lean b/ConNF/Counting/CodingFunction.lean
@@ -182,16 +182,17 @@ theorem code_eq_code_iff (S S' : Support β) (t t' : Tangle β)
     refine ext (ρ • S) ⟨ρ, rfl⟩ ⟨1, by rw [one_smul]⟩ ?_
     simp only [code_decode, Part.get_some, decode_smul]
 
-def Strong [FOAAssumptions] {β : Λ} [LeLevel β] (χ : CodingFunction β) : Prop :=
+def Strong [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β] (χ : CodingFunction β) : Prop :=
   ∀ S ∈ χ.decode.Dom, S.Strong
 
-theorem strong_of_strong_mem [FOAAssumptions] {β : Λ} [LeLevel β]
+theorem strong_of_strong_mem [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β]
     (χ : CodingFunction β) (S : Support β) (hS : S.Strong) (hSχ : S ∈ χ.decode.Dom) : χ.Strong := by
   intro T hTχ
   obtain ⟨ρ, rfl⟩ := (χ.dom_iff S T hSχ).mp hTχ
   exact hS.smul ρ
 
-theorem code_strong [FOAAssumptions] {β : Λ} [LeLevel β] (S : Support β) (t : Tangle β)
+theorem code_strong [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β]
+    (S : Support β) (t : Tangle β)
     (ht : Supports (Allowable β) (S : Set (Address β)) t) (hS : S.Strong) :
     (code S t ht).Strong :=
   strong_of_strong_mem _ S hS mem_code_self

diff --git a/ConNF/Counting/Conclusions.lean b/ConNF/Counting/Conclusions.lean
@@ -11,7 +11,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [CountingAssumptions]
+variable [Params.{u}] [Level] [BasePositions] [CountingAssumptions]
 
 theorem mk_codingFunction (β : Λ) [i : LeLevel β] : #(CodingFunction β) < #μ := by
   revert i

diff --git a/ConNF/Counting/CountCodingFunction.lean b/ConNF/Counting/CountCodingFunction.lean
@@ -11,7 +11,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ]
+variable [Params.{u}] [Level] [BasePositions] [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ]
   (hγ : (γ : TypeIndex) < β)
 
 def RecodeType (S : Support β) : Type u :=

diff --git a/ConNF/Counting/CountRaisedSingleton.lean b/ConNF/Counting/CountRaisedSingleton.lean
@@ -13,7 +13,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ]
+variable [Params.{u}] [Level] [BasePositions] [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ]
     (hγ : (γ : TypeIndex) < β)
 
 noncomputable def RaisedSingleton.code (S : Support β) (r : RaisedSingleton hγ S) :

diff --git a/ConNF/Counting/CountSpec.lean b/ConNF/Counting/CountSpec.lean
@@ -8,7 +8,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
+variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β]
 
 def SpecCondition' (β : Λ) :=
   (ExtendedIndex β × Set κ × Set κ) ⊕

diff --git a/ConNF/Counting/CountStrongOrbit.lean b/ConNF/Counting/CountStrongOrbit.lean
@@ -11,7 +11,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
+variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β]
 
 /-- A morphism of supports `S → T`. -/
 structure SupportHom (S T : Support β) : Type u where

diff --git a/ConNF/Counting/ExistsSpec.lean b/ConNF/Counting/ExistsSpec.lean
@@ -8,7 +8,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ}
+variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ}
 
 noncomputable def Support.spec (S : Support β) (hS : S.Strong) : Spec β where
   max := S.max

diff --git a/ConNF/Counting/Hypotheses.lean b/ConNF/Counting/Hypotheses.lean
@@ -14,7 +14,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level]
+variable [Params.{u}] [Level] [BasePositions]
 
 instance : LeLevel (0 : Λ) := ⟨WithBot.coe_le_coe.mpr (Params.Λ_zero_le _)⟩
 

diff --git a/ConNF/Counting/Recode.lean b/ConNF/Counting/Recode.lean
@@ -12,7 +12,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ]
+variable [Params.{u}] [Level] [BasePositions] [CountingAssumptions] {β γ : Λ} [LeLevel β] [LeLevel γ]
   (hγ : (γ : TypeIndex) < β)
 
 def raiseIndex (A : ExtendedIndex (γ : TypeIndex)) : ExtendedIndex β :=

diff --git a/ConNF/Counting/Spec.lean b/ConNF/Counting/Spec.lean
@@ -14,7 +14,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ}
+variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ}
 
 inductive SpecCondition (β : Λ)
   | atom (A : ExtendedIndex β) (s : Set κ) (t : Set κ)

diff --git a/ConNF/Counting/SpecSMul.lean b/ConNF/Counting/SpecSMul.lean
@@ -12,7 +12,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
+variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β]
   {S T : Support β} {hS : S.Strong} {σ : Spec β} (hσS : σ.Specifies S hS) (ρ : Allowable β)
 
 theorem Spec.Specifies.smul : σ.Specifies (ρ • S) (hS.smul ρ) := by

diff --git a/ConNF/Counting/SpecSame.lean b/ConNF/Counting/SpecSame.lean
@@ -33,7 +33,7 @@ end PFun
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
+variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β]
   {S T : Support β} {hS : S.Strong} {hT : T.Strong}
   {σ : Spec β} (hσS : σ.Specifies S hS) (hσT : σ.Specifies T hT)
 

diff --git a/ConNF/Counting/StrongSupport.lean b/ConNF/Counting/StrongSupport.lean
@@ -17,7 +17,7 @@ namespace ConNF
 
 namespace Support
 
-variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ}
+variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ}
 
 @[mk_iff]
 inductive Interferes (a : Atom) (N₁ N₂ : NearLitter) : Prop
@@ -68,7 +68,7 @@ theorem Precedes.lt {c d : Address β} :
   case fuzzBot A N h =>
     refine lt_nearLitter (Relation.TransGen.single ?_)
     simp_rw [h.hL]
-    exact Constrains.fuzz_bot h.path.hε _ _
+    exact Constrains.fuzzBot h.path.hε _ _
 
 theorem Precedes.wellFounded : WellFounded (Precedes : Address β → Address β → Prop) := by
   have : Subrelation Precedes ((· < ·) : Address β → Address β → Prop) := Precedes.lt

diff --git a/ConNF/Counting/SupportOrbit.lean b/ConNF/Counting/SupportOrbit.lean
@@ -9,7 +9,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β]
+variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β]
 
 def SupportOrbit (β : Λ) [LeLevel β] : Type u :=
   MulAction.orbitRel.Quotient (Allowable β) (Support β)

diff --git a/ConNF/FOA/Action/Complete.lean b/ConNF/FOA/Action/Complete.lean
@@ -13,7 +13,7 @@ universe u
 namespace ConNF
 
 variable [Params.{u}] (φ : NearLitterAction) [Level]
-  [FOAAssumptions] {β : Λ} {A : ExtendedIndex β}
+  [BasePositions] [FOAAssumptions] {β : Λ} {A : ExtendedIndex β}
 
 namespace NearLitterAction
 

diff --git a/ConNF/FOA/Action/NearLitterAction.lean b/ConNF/FOA/Action/NearLitterAction.lean
@@ -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 [Level] [FOAAssumptions] {β : Λ} {A : ExtendedIndex β}
+variable [Level] [BasePositions] [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
@@ -87,7 +87,7 @@ end StructAction
 
 namespace StructAction
 
-variable [Level] [FOAAssumptions] {β : Λ}
+variable [Level] [BasePositions] [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
@@ -27,7 +27,7 @@ def Lawful {β : TypeIndex} (φ : StructAction β) : Prop :=
   ∀ B, (φ B).Lawful
 
 /-- This structural action maps flexible litters to flexible litters. -/
-def MapFlexible [Level] [FOAAssumptions] {β : Λ} (φ : StructAction β) :
+def MapFlexible [Level] [BasePositions] [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 [Level] [FOAAssumptions] {β : Λ} (φ : StructAction β)
+variable [Level] [BasePositions] [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 [Level] [FOAAssumptions] {β : Λ}
+variable [Level] [BasePositions] [FOAAssumptions] {β : Λ}
 
 instance {β : TypeIndex} : PartialOrder (StructAction β)
     where

diff --git a/ConNF/FOA/Approximation/NearLitterApprox.lean b/ConNF/FOA/Approximation/NearLitterApprox.lean
@@ -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 [Level] [FOAAssumptions] {β : TypeIndex} (π : NearLitterApprox)
+def Free [Level] [BasePositions] [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
@@ -27,7 +27,7 @@ def Approximates {β : TypeIndex} (π₀ : StructApprox β) (π : StructPerm β)
 def ExactlyApproximates {β : TypeIndex} (π₀ : StructApprox β) (π : StructPerm β) : Prop :=
   ∀ A, (π₀ A).ExactlyApproximates (π A)
 
-variable [Level] [FOAAssumptions]
+variable [Level] [BasePositions] [FOAAssumptions]
 
 def Free {β : Λ} (π₀ : StructApprox β) : Prop :=
   ∀ A, (π₀ A).Free A