Merge pull request #44 from leanprover-community/remove-base-positions

leanprover-community · Dec 13, 2023 · 71090af · 71090af
2 parents 1e5905a + 6fdbc39
commit 71090af
Show file tree

Hide file tree

Showing 29 changed files with 313 additions and 268 deletions.
diff --git a/ConNF/BaseType/Atom.lean b/ConNF/BaseType/Atom.lean
@@ -70,6 +70,10 @@ def litterSetEquiv (L : Litter) : litterSet L ≃ κ := ⟨
 theorem mk_litterSet (L : Litter) : #(litterSet L) = #κ :=
   Cardinal.eq.2 ⟨litterSetEquiv L⟩
 
+theorem litterSet_nonempty (L : Litter) : Nonempty (litterSet L) := by
+  rw [← Cardinal.mk_ne_zero_iff, mk_litterSet]
+  exact mk_ne_zero κ
+
 /-- Two litters with different indices have disjoint litter sets. -/
 theorem pairwise_disjoint_litterSet : Pairwise (Disjoint on litterSet) :=
   fun _ _ h => disjoint_left.2 fun _ h₁ h₂ => h <| h₁.symm.trans h₂

diff --git a/ConNF/BaseType/NearLitter.lean b/ConNF/BaseType/NearLitter.lean
@@ -119,6 +119,10 @@ theorem coe_mk (L : Litter) (s : { s // IsNearLitter L s }) :
 theorem ext (h₂ : (N₁ : Set Atom) = N₂) : N₁ = N₂ :=
   SetLike.coe_injective h₂
 
+theorem nonempty (N : NearLitter) : Nonempty N := by
+  obtain ⟨a, ha⟩ := IsNearLitter.nonempty N.2.2
+  exact ⟨a, ha⟩
+
 /-- Reinterpret a near-litter as a product of a litter and a set of atoms. -/
 @[simps]
 def toProd (N : NearLitter) : Litter × Set Atom :=

diff --git a/ConNF/FOA/Action/Complete.lean b/ConNF/FOA/Action/Complete.lean
@@ -12,7 +12,7 @@ universe u
 
 namespace ConNF
 
-variable [Params.{u}] (φ : NearLitterAction) [BasePositions] [Level]
+variable [Params.{u}] (φ : NearLitterAction) [Level]
   [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 [BasePositions] [Level] [FOAAssumptions] {β : Λ} {A : ExtendedIndex β}
+variable [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
@@ -87,7 +87,7 @@ end StructAction
 
 namespace StructAction
 
-variable [BasePositions] [Level] [FOAAssumptions] {β : Λ}
+variable [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
@@ -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 [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 [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 [Level] [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 [BasePositions] [Level] [FOAAssumptions] {β : TypeIndex} (π : NearLitterApprox)
+def Free [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
@@ -27,7 +27,7 @@ def Approximates {β : TypeIndex} (π₀ : StructApprox β) (π : StructPerm β)
 def ExactlyApproximates {β : TypeIndex} (π₀ : StructApprox β) (π : StructPerm β) : Prop :=
   ∀ A, (π₀ A).ExactlyApproximates (π A)
 
-variable [BasePositions] [Level] [FOAAssumptions]
+variable [Level] [FOAAssumptions]
 
 def Free {β : Λ} (π₀ : StructApprox β) : Prop :=
   ∀ A, (π₀ A).Free A