From 33668f5e99a0b4a00916aacf28f7a8208b984252 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Tue, 19 Mar 2024 16:10:17 +0000 Subject: [PATCH] Reintroduce base positions Signed-off-by: zeramorphic --- ConNF/Counting/CodingFunction.lean | 7 +- ConNF/Counting/Conclusions.lean | 2 +- ConNF/Counting/CountCodingFunction.lean | 2 +- ConNF/Counting/CountRaisedSingleton.lean | 2 +- ConNF/Counting/CountSpec.lean | 2 +- ConNF/Counting/CountStrongOrbit.lean | 2 +- ConNF/Counting/ExistsSpec.lean | 2 +- ConNF/Counting/Hypotheses.lean | 2 +- ConNF/Counting/Recode.lean | 2 +- ConNF/Counting/Spec.lean | 2 +- ConNF/Counting/SpecSMul.lean | 2 +- ConNF/Counting/SpecSame.lean | 2 +- ConNF/Counting/StrongSupport.lean | 4 +- ConNF/Counting/SupportOrbit.lean | 2 +- ConNF/FOA/Action/Complete.lean | 2 +- ConNF/FOA/Action/NearLitterAction.lean | 2 +- ConNF/FOA/Action/Refine.lean | 2 +- ConNF/FOA/Action/StructAction.lean | 6 +- ConNF/FOA/Approximation/NearLitterApprox.lean | 2 +- ConNF/FOA/Approximation/StructApprox.lean | 2 +- ConNF/FOA/Basic/Constrains.lean | 242 ++++-------------- ConNF/FOA/Basic/Flexible.lean | 4 +- ConNF/FOA/Basic/Hypotheses.lean | 35 +-- ConNF/FOA/Basic/Reduction.lean | 2 +- ConNF/FOA/Complete/AtomCompletion.lean | 2 +- ConNF/FOA/Complete/CompleteAction.lean | 2 +- ConNF/FOA/Complete/FlexibleCompletion.lean | 2 +- ConNF/FOA/Complete/HypAction.lean | 2 +- ConNF/FOA/Complete/LitterCompletion.lean | 2 +- ConNF/FOA/Complete/NearLitterCompletion.lean | 2 +- ConNF/FOA/Corollaries.lean | 4 +- ConNF/FOA/Properties/Bijective.lean | 2 +- ConNF/FOA/Properties/ConstrainedAction.lean | 2 +- ConNF/FOA/Properties/Injective.lean | 14 +- ConNF/FOA/Properties/Surjective.lean | 4 +- ConNF/FOA/Result.lean | 5 +- ConNF/Fuzz/Construction.lean | 39 ++- ConNF/Fuzz/Hypotheses.lean | 49 +++- ConNF/Model/Construction.lean | 4 +- ConNF/NewTangle/Cloud.lean | 13 +- ConNF/NewTangle/CodeEquiv.lean | 31 ++- ConNF/NewTangle/Hypotheses.lean | 7 +- ConNF/NewTangle/NewAllowable.lean | 2 +- ConNF/NewTangle/NewTangle.lean | 4 +- ConNF/NewTangle/Position.lean | 4 +- 45 files changed, 204 insertions(+), 326 deletions(-) diff --git a/ConNF/Counting/CodingFunction.lean b/ConNF/Counting/CodingFunction.lean index 9a6e3aeffa..1e6b0086a9 100644 --- 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 index ecc5fddc3d..8eb0887ffa 100644 --- 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 index d6ad67f7d0..9da7ab8099 100644 --- 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 index 9d92b0ddf5..0bdae43e35 100644 --- 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 index b77369ce00..0778b2f405 100644 --- 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 index 4f328abda6..aaa6ea8a35 100644 --- 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 index b8a9c547c2..37ce3f76fe 100644 --- 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 index 657c560e63..92c526df5e 100644 --- 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 index e42be723f8..50ae63a949 100644 --- 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 index 7578afd727..e9fb498c89 100644 --- 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 index b9bd94859f..9bfb80f66f 100644 --- 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 index cd2f6f99f9..ca41505de3 100644 --- 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 index 853f08fe62..fd160ecbe1 100644 --- 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 index 4a4e292319..fb651eeac1 100644 --- 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 index 2435fbc5db..fade682748 100644 --- 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 index 0ebc324fb7..155c7f04a5 100644 --- 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 index f9a6353043..720704e9fb 100644 --- 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 index 5a85b5cd7b..427d7c4246 100644 --- 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 index 54a65541a4..86f22cccfa 100644 --- 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 index c79feefaef..6aa664d5dc 100644 --- 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 diff --git a/ConNF/FOA/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean index e6ac23302a..5409892505 100644 --- a/ConNF/FOA/Basic/Constrains.lean +++ b/ConNF/FOA/Basic/Constrains.lean @@ -22,7 +22,7 @@ universe u namespace ConNF -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} /-- addresses 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 @@ -45,7 +45,7 @@ inductive Constrains : Address β → Address β → Prop c ∈ t.support → Constrains ⟨(A.cons hδ).comp c.path, c.value⟩ ⟨(A.cons hε).cons (bot_lt_coe _), inr (fuzz hδε t).toNearLitter⟩ - | fuzz_bot ⦃γ : Λ⦄ [LeLevel γ] ⦃ε : Λ⦄ [LtLevel ε] + | fuzzBot ⦃γ : Λ⦄ [LeLevel γ] ⦃ε : Λ⦄ [LtLevel ε] (hε : (ε : TypeIndex) < γ) (A : Path (β : TypeIndex) γ) (a : Atom) : Constrains ⟨A.cons (bot_lt_coe _), inl a⟩ ⟨(A.cons hε).cons (bot_lt_coe _), inr (fuzz (bot_ne_coe (a := ε)) a).toNearLitter⟩ @@ -54,134 +54,52 @@ inductive Constrains : Address β → Address β → Prop @[inherit_doc] infix:50 " ≺ " => Constrains -inductive LitterConstrains : Litter → Litter → Prop - | fuzz_atom ⦃δ : Λ⦄ [LtLevel δ] ⦃ε : Λ⦄ [LtLevel ε] (hδε : (δ : TypeIndex) ≠ ε) - (t : Tangle δ) {B : ExtendedIndex δ} {a : Atom} : ⟨B, inl a⟩ ∈ t.support → - LitterConstrains a.1 (fuzz hδε t) - | fuzz_nearLitter ⦃δ : Λ⦄ [LtLevel δ] ⦃ε : Λ⦄ [LtLevel ε] (hδε : (δ : TypeIndex) ≠ ε) - (t : Tangle δ) {B : ExtendedIndex δ} {N : NearLitter} (h : ⟨B, inr N⟩ ∈ t.support) - {a : Atom} (ha : a ∈ N) : - LitterConstrains a.1 (fuzz hδε t) - | fuzz_bot ⦃ε : Λ⦄ [LtLevel ε] (a : Atom) : - LitterConstrains a.1 (fuzz (bot_ne_coe (a := ε)) a) +def Address.pos (c : Address β) : μ := + c.2.elim Position.pos Position.pos -@[mk_iff] -inductive HasPosition : Litter → μ → Prop - | fuzz ⦃δ : Λ⦄ [LtLevel δ] ⦃ε : Λ⦄ [LtLevel ε] (hδε : (δ : TypeIndex) ≠ ε) (t : Tangle δ) : - HasPosition (fuzz hδε t) (pos t) - | fuzz_bot ⦃ε : Λ⦄ [LtLevel ε] (a : Atom) : - HasPosition (fuzz (bot_ne_coe (a := ε)) a) (pos a) +@[simp] +theorem Address.pos_atom (A : ExtendedIndex β) (a : Atom) : + Address.pos ⟨A, inl a⟩ = Position.pos a := + rfl -theorem hasPosition_subsingleton {L : Litter} {ν₁ ν₂ : μ} - (h₁ : HasPosition L ν₁) (h₂ : HasPosition L ν₂) : ν₁ = ν₂ := by - rw [hasPosition_iff] at h₁ h₂ - cases h₁ with - | inl h₁ => - obtain ⟨δ, _, ε, _, hδε, t, rfl, rfl⟩ := h₁ - cases h₂ with - | inl h₂ => - obtain ⟨_, _, _, _, _, t, ht, rfl⟩ := h₂ - cases fuzz_congr_β ht - cases fuzz_congr_γ ht - cases fuzz_injective _ ht - rfl - | inr h₂ => - obtain ⟨_, _, a, ha, rfl⟩ := h₂ - cases fuzz_congr_β ha - | inr h₁ => - obtain ⟨_, _, a, rfl, rfl⟩ := h₁ - cases h₂ with - | inl h₂ => - obtain ⟨_, _, _, _, _, t, ht, rfl⟩ := h₂ - cases fuzz_congr_β ht - | inr h₂ => - obtain ⟨_, _, a, ha, rfl⟩ := h₂ - cases fuzz_congr_γ ha - cases fuzz_injective _ ha - rfl +@[simp] +theorem Address.pos_nearLitter (A : ExtendedIndex β) (N : NearLitter) : + Address.pos ⟨A, inr N⟩ = Position.pos N := + rfl -theorem hasPosition_of_litterConstrains {L₁ L₂ : Litter} (h : LitterConstrains L₁ L₂) : - ∃ ν, HasPosition L₂ ν := by +theorem Constrains.hasPosition_lt {c d : Address β} (h : c ≺ d) : + c.pos < d.pos := by cases h - · exact ⟨_, HasPosition.fuzz _ _⟩ - · exact ⟨_, HasPosition.fuzz _ _⟩ - · exact ⟨_, HasPosition.fuzz_bot _⟩ - -theorem hasPosition_lt_of_litterConstrains {L₁ L₂ : Litter} (h : LitterConstrains L₁ L₂) - {ν₁ ν₂ : μ} (h₁ : HasPosition L₁ ν₁) (h₂ : HasPosition L₂ ν₂) : - ν₁ < ν₂ := by - rw [hasPosition_iff] at h₁ h₂ - cases h with - | fuzz_atom hδε t ht => - cases h₂ with - | inr h => - obtain ⟨_, _, _, h, rfl⟩ := h - cases fuzz_congr_β h - | inl h => - obtain ⟨δ, _, ε, _, _, t', ht', rfl⟩ := h - cases fuzz_congr_β ht' - cases fuzz_congr_γ ht' - cases fuzz_injective _ ht' - cases h₁ with - | inl h => - obtain ⟨δ, _, ε, _, hδε, t', ht', rfl⟩ := h - exact pos_lt_pos_atom t ht t' hδε ht' - | inr h => - obtain ⟨ε, _, a, h, rfl⟩ := h - exact pos_lt_pos_atom t ht (show Tangle ⊥ from a) bot_ne_coe h - | fuzz_nearLitter hδε t ht ha => - cases h₂ with - | inr h => - obtain ⟨_, _, _, h, rfl⟩ := h - cases fuzz_congr_β h - | inl h => - obtain ⟨δ, _, ε, _, _, t', ht', rfl⟩ := h - cases fuzz_congr_β ht' - cases fuzz_congr_γ ht' - cases fuzz_injective _ ht' - cases h₁ with - | inl h => - obtain ⟨δ, _, ε, _, hδε, t', ht', rfl⟩ := h - exact pos_lt_pos_nearLitter t ht t' hδε ⟨_, ha, ht'⟩ - | inr h => - obtain ⟨ε, _, a, h, rfl⟩ := h - exact pos_lt_pos_nearLitter t ht (show Tangle ⊥ from a) bot_ne_coe ⟨_, ha, h⟩ - | fuzz_bot a => - cases h₂ with - | inl h => - obtain ⟨_, _, _, _, _, _, h, rfl⟩ := h - cases fuzz_congr_β h - | inr h => - obtain ⟨ε, _, a, ha, rfl⟩ := h - cases fuzz_congr_γ ha - cases fuzz_injective _ ha - cases h₁ with - | inl h => - obtain ⟨δ, _, ε, _, hδε, t', ht', rfl⟩ := h - exact pos_lt_pos_fuzz _ t' a ht' - | inr h => - obtain ⟨ε, _, a', ha', rfl⟩ := h - exact pos_lt_pos_fuzz _ (show Tangle ⊥ from a') a ha' - -open scoped Classical in -noncomputable def positionOrBot (L : Litter) : WithBot μ := - if h : ∃ ν, HasPosition L ν then h.choose else ⊥ + case atom A a => exact BasePositions.lt_pos_atom a + case nearLitter A N hN => exact BasePositions.lt_pos_litter N hN + case symmDiff A N a ha => exact BasePositions.lt_pos_symmDiff a N ha + case fuzz γ _ δ _ ε _ hδ hε hδε A t c hc' => + have := pos_lt_pos_fuzz_nearLitter hδε t (ConNF.fuzz hδε t).toNearLitter rfl + obtain ⟨B, a | N⟩ := c + · simp only [Address.pos_atom, Address.pos_nearLitter] + by_cases h : t = typedAtom a + · subst h + rw [pos_typedAtom] at this + exact this + · exact (pos_lt_pos_atom _ hc' h).trans this + · simp only [Address.pos_nearLitter] + by_cases h : t = typedNearLitter N + · subst h + rw [pos_typedNearLitter] at this + exact this + · exact (pos_lt_pos_nearLitter _ hc' h).trans this + case fuzzBot γ _ ε _ hε A a => + simp only [Address.pos_atom, Address.pos_nearLitter] + exact pos_lt_pos_fuzz_nearLitter (bot_ne_coe (a := ε)) a + (ConNF.fuzz (bot_ne_coe (a := ε)) a).toNearLitter rfl + +theorem constrains_subrelation (β : Λ) : + Subrelation ((· ≺ ·) : Address β → _ → Prop) (InvImage (· < ·) Address.pos) := + Constrains.hasPosition_lt -theorem litterConstrains_subrelation : - Subrelation LitterConstrains (InvImage (· < ·) positionOrBot) := by - intro L₁ L₂ h - obtain ⟨ν₂, hν₂⟩ := hasPosition_of_litterConstrains h - by_cases h₁ : ∃ ν₁, HasPosition L₁ ν₁ - · obtain ⟨ν₁, hν₁⟩ := h₁ - rw [InvImage, positionOrBot, positionOrBot, dif_pos ⟨ν₁, hν₁⟩, dif_pos ⟨ν₂, hν₂⟩, - hasPosition_subsingleton (Exists.choose_spec ⟨ν₁, hν₁⟩) hν₁, - hasPosition_subsingleton (Exists.choose_spec ⟨ν₂, hν₂⟩) hν₂] - exact WithBot.coe_lt_coe.mpr (hasPosition_lt_of_litterConstrains h hν₁ hν₂) - · rw [InvImage, positionOrBot, positionOrBot, dif_neg h₁, dif_pos ⟨ν₂, hν₂⟩] - exact bot_lt_coe _ - -theorem litterConstrains_wf : WellFounded LitterConstrains := - Subrelation.wf litterConstrains_subrelation IsWellFounded.wf +/-- The `≺` relation is well-founded. -/ +theorem constrains_wf (β : Λ) : WellFounded ((· ≺ ·) : Address β → _ → Prop) := + Subrelation.wf (constrains_subrelation β) (InvImage.wf _ Params.μ_isWellOrder.wf) @[simp] theorem constrains_atom {c : Address β} {A : ExtendedIndex β} {a : Atom} : @@ -215,78 +133,6 @@ theorem constrains_nearLitter {c : Address β} {A : ExtendedIndex β} · exact Constrains.nearLitter A N hN · exact Constrains.symmDiff A N a ha -theorem acc_atom {a : Atom} {A : ExtendedIndex β} - (h : Acc ((· ≺ ·) : Address β → _ → Prop) ⟨A, inr a.1.toNearLitter⟩) : - Acc ((· ≺ ·) : Address β → _ → Prop) ⟨A, inl a⟩ := by - constructor - intro c - rw [constrains_atom] - rintro rfl - exact h - -theorem acc_nearLitter {N : NearLitter} {A : ExtendedIndex β} - (h : ∀ a ∈ N, Acc ((· ≺ ·) : Address β → _ → Prop) ⟨A, inr a.1.toNearLitter⟩) : - Acc ((· ≺ ·) : Address β → _ → Prop) ⟨A, inr N⟩ := by - by_cases hN : N.IsLitter - · obtain ⟨L, rfl⟩ := hN.exists_litter_eq - obtain ⟨⟨a, rfl⟩⟩ := litterSet_nonempty L - exact h _ rfl - constructor - intro d hd - rw [constrains_nearLitter hN] at hd - obtain (rfl | ⟨a, ha, rfl⟩) := hd - · obtain ⟨a, ha⟩ := NearLitter.inter_nonempty_of_fst_eq_fst (N₁ := N) (N₂ := N.1.toNearLitter) rfl - have := h a ha.1 - rw [ha.2] at this - exact this - · refine acc_atom ?_ - obtain (ha | ha) := ha - · obtain ⟨b, hb⟩ := NearLitter.inter_nonempty_of_fst_eq_fst (N₁ := N) (N₂ := N.1.toNearLitter) rfl - have := h b hb.1 - rw [hb.2, ← ha.1] at this - exact this - · exact h a ha.1 - -/-- The `≺` relation is well-founded. -/ -theorem constrains_wf (β : Λ) : WellFounded ((· ≺ ·) : Address β → _ → Prop) := by - have : ∀ L : Litter, ∀ A : ExtendedIndex β, - Acc ((· ≺ ·) : Address β → _ → Prop) ⟨A, inr L.toNearLitter⟩ - · intro L - refine litterConstrains_wf.induction - (C := fun L => ∀ A : ExtendedIndex β, Acc (· ≺ ·) ⟨A, inr L.toNearLitter⟩) L ?_ - clear L - intro L ih A - constructor - intro c hc - rw [constrains_iff] at hc - obtain ⟨A, a, rfl, hc⟩ | ⟨A, N, hN, rfl, hc⟩ | ⟨A, N, a, ha, rfl, hc⟩ | - ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, A, t, c, hc, rfl, hc'⟩ | - ⟨γ, _, ε, _, hγ, A, a, rfl, hc⟩ := hc - · cases hc - · cases hc - cases hN (NearLitter.IsLitter.mk _) - · cases hc - cases ha with - | inl ha => cases ha.2 ha.1 - | inr ha => cases ha.2 ha.1 - · simp only [Address.mk.injEq, inr.injEq, Litter.toNearLitter_injective.eq_iff] at hc' - cases hc'.1 - cases hc'.2 - obtain ⟨B, a | N⟩ := c - · exact acc_atom (ih a.1 (LitterConstrains.fuzz_atom _ _ hc) _) - · refine acc_nearLitter ?_ - intro a ha - exact ih _ (LitterConstrains.fuzz_nearLitter hδε t hc ha) _ - · simp only [Address.mk.injEq, inr.injEq, Litter.toNearLitter_injective.eq_iff] at hc - cases hc.1 - cases hc.2 - refine acc_atom (ih _ (LitterConstrains.fuzz_bot _) _) - constructor - intro c - obtain ⟨B, a | N⟩ := c - · exact acc_atom (this _ _) - · exact acc_nearLitter (fun _ _ => this _ _) - /-- The constrains relation is stable under composition of paths. -/ theorem constrains_comp {β γ : Λ} {c d : Address γ} (h : c ≺ d) (B : Path (β : TypeIndex) γ) : ⟨B.comp c.path, c.value⟩ ≺ ⟨B.comp d.path, d.value⟩ := by @@ -297,7 +143,7 @@ theorem constrains_comp {β γ : Λ} {c d : Address γ} (h : c ≺ d) · rw [Path.comp_cons, ← Path.comp_assoc, Path.comp_cons] exact Constrains.fuzz hδ hε hδε (B.comp A) t c hc · rw [Path.comp_cons] - exact Constrains.fuzz_bot hδ (B.comp A) a + exact Constrains.fuzzBot hδ (B.comp A) a instance : PartialOrder (Address β) where le := Relation.ReflTransGen (· ≺ ·) diff --git a/ConNF/FOA/Basic/Flexible.lean b/ConNF/FOA/Basic/Flexible.lean index 4ac83bba0a..65f34bceb2 100644 --- a/ConNF/FOA/Basic/Flexible.lean +++ b/ConNF/FOA/Basic/Flexible.lean @@ -8,7 +8,7 @@ universe u namespace ConNF -variable [Params.{u}] [Level] [FOAAssumptions] {β : TypeIndex} +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : TypeIndex} /-- A litter is *inflexible* if it is the image of some f-map. -/ @[mk_iff] @@ -232,7 +232,7 @@ end Comp theorem InflexibleBot.constrains {β : Λ} {A : ExtendedIndex β} {L : Litter} (h : InflexibleBot A L) : (⟨h.path.B.cons (bot_lt_coe _), inl h.a⟩ : Address β) < ⟨A, inr L.toNearLitter⟩ := by - have := Constrains.fuzz_bot h.path.hε h.path.B h.a + have := Constrains.fuzzBot h.path.hε h.path.B h.a rw [← h.hL, ← h.path.hA] at this exact Relation.TransGen.single this diff --git a/ConNF/FOA/Basic/Hypotheses.lean b/ConNF/FOA/Basic/Hypotheses.lean index 35b0cde5d9..ee475e722c 100644 --- a/ConNF/FOA/Basic/Hypotheses.lean +++ b/ConNF/FOA/Basic/Hypotheses.lean @@ -19,7 +19,7 @@ universe u namespace ConNF -variable [Params.{u}] [Level] +variable [Params.{u}] [Level] [BasePositions] /-- The data that we will use when proving the freedom of action theorem. This structure combines the following data: @@ -33,25 +33,29 @@ class FOAData where lowerTangleData : ∀ β : Λ, [LeLevel β] → TangleData β lowerPositionedTangles : ∀ β : Λ, [LtLevel β] → PositionedTangles β lowerTypedObjects : ∀ β : Λ, [LeLevel β] → TypedObjects β + lowerPositionedObjects : ∀ β : Λ, [LtLevel β] → PositionedObjects β namespace FOAData variable [FOAData] {β : Λ} [LeLevel β] {γ : Λ} [LtLevel γ] -instance tangleData : TangleData β := +instance : TangleData β := lowerTangleData β -instance positionedTangles : PositionedTangles γ := +instance : PositionedTangles γ := lowerPositionedTangles γ -instance typedObjects : TypedObjects β := +instance : TypedObjects β := lowerTypedObjects β -instance iicBotTangleData : ∀ β : TypeIndex, [LeLevel β] → TangleData β +instance : PositionedObjects γ := + lowerPositionedObjects γ + +instance : ∀ β : TypeIndex, [LeLevel β] → TangleData β | ⊥, _ => Bot.tangleData | (β : Λ), _ => lowerTangleData β -noncomputable instance iioBotPositionedTangles : ∀ β : TypeIndex, [LtLevel β] → PositionedTangles β +instance : ∀ β : TypeIndex, [LtLevel β] → PositionedTangles β | ⊥, _ => Bot.positionedTangles | (β : Λ), _ => lowerPositionedTangles β @@ -76,16 +80,12 @@ class FOAAssumptions extends FOAData where (ρ • t).support = ρ • t.support /-- Inflexible litters whose atoms occur in designated supports have position less than the original tangle. -/ - pos_lt_pos_atom {β : Λ} [LtLevel β] (t : Tangle β) - {A : ExtendedIndex β} {a : Atom} (ht : ⟨A, Sum.inl a⟩ ∈ t.support) - {γ : TypeIndex} [LtLevel γ] (s : Tangle γ) {δ : Λ} [LtLevel δ] (hγδ : γ ≠ δ) - (ha : a.1 = fuzz hγδ s) : pos s < pos t + pos_lt_pos_atom {β : Λ} [LtLevel β] (t : Tangle β) {A : ExtendedIndex β} {a : Atom} : + ⟨A, Sum.inl a⟩ ∈ t.support → t ≠ typedAtom a → pos a < pos t /-- Inflexible litters touching near-litters in designated supports have position less than the original tangle. -/ - pos_lt_pos_nearLitter {β : Λ} [LtLevel β] (t : Tangle β) - {A : ExtendedIndex β} {N : NearLitter} (ht : ⟨A, Sum.inr N⟩ ∈ t.support) - {γ : TypeIndex} [LtLevel γ] (s : Tangle γ) {δ : Λ} [LtLevel δ] (hγδ : γ ≠ δ) - (h : Set.Nonempty ((N : Set Atom) ∩ (fuzz hγδ s).toNearLitter)) : pos s < pos t + pos_lt_pos_nearLitter {β : Λ} [LtLevel β] (t : Tangle β) {A : ExtendedIndex β} {N : NearLitter} : + ⟨A, Sum.inr N⟩ ∈ t.support → t ≠ typedNearLitter N → pos N < pos t /-- The `fuzz` map commutes with allowable permutations. -/ smul_fuzz {β : TypeIndex} [LeLevel β] {γ : TypeIndex} [LtLevel γ] {δ : Λ} [LtLevel δ] (hγ : γ < β) (hδ : (δ : TypeIndex) < β) (hγδ : γ ≠ δ) (ρ : Allowable β) (t : Tangle γ) : @@ -214,13 +214,6 @@ theorem NearLitterPerm.ofBot_comp' {β : TypeIndex} [LeLevel β] {hβ : ⊥ < β NearLitterPerm.ofBot (allowableCons hβ ρ) = Allowable.toStructPerm ρ (Quiver.Hom.toPath hβ) := (congr_fun (allowableCons_eq β ⊥ hβ ρ) Quiver.Path.nil).symm -theorem exists_cons_of_length_ne_zero {V : Type _} [Quiver V] {x y : V} - (p : Quiver.Path x y) (h : p.length ≠ 0) : - ∃ t : V, ∃ q : Quiver.Path x t, ∃ e : t ⟶ y, p = q.cons e := by - cases p - · cases h rfl - · exact ⟨_, _, _, rfl⟩ - @[simp] theorem ofBot_smul {X : Type _} [MulAction NearLitterPerm X] (π : Allowable ⊥) (x : X) : π • x = NearLitterPerm.ofBot π • x := diff --git a/ConNF/FOA/Basic/Reduction.lean b/ConNF/FOA/Basic/Reduction.lean index b0740eae6f..eb139f09f9 100644 --- a/ConNF/FOA/Basic/Reduction.lean +++ b/ConNF/FOA/Basic/Reduction.lean @@ -25,7 +25,7 @@ open scoped Cardinal Pointwise namespace ConNF -variable [Params.{u}] [Level] [FOAAssumptions] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] variable {β : Λ} {G : Type _} {τ : Type _} [SMul G (Address β)] [SMul G τ] {x : τ} /-- An address is *reduced* if it is an atom or a litter. -/ diff --git a/ConNF/FOA/Complete/AtomCompletion.lean b/ConNF/FOA/Complete/AtomCompletion.lean index fed818ff74..1a1e36ee38 100644 --- a/ConNF/FOA/Complete/AtomCompletion.lean +++ b/ConNF/FOA/Complete/AtomCompletion.lean @@ -9,7 +9,7 @@ universe u namespace ConNF -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} (π : StructApprox β) +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} (π : StructApprox β) namespace StructApprox diff --git a/ConNF/FOA/Complete/CompleteAction.lean b/ConNF/FOA/Complete/CompleteAction.lean index cca4541237..6eadea22c3 100644 --- a/ConNF/FOA/Complete/CompleteAction.lean +++ b/ConNF/FOA/Complete/CompleteAction.lean @@ -12,7 +12,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] /-! diff --git a/ConNF/FOA/Complete/FlexibleCompletion.lean b/ConNF/FOA/Complete/FlexibleCompletion.lean index 6410a798d1..1c471cb8ef 100644 --- a/ConNF/FOA/Complete/FlexibleCompletion.lean +++ b/ConNF/FOA/Complete/FlexibleCompletion.lean @@ -8,7 +8,7 @@ universe u namespace ConNF -variable [Params.{u}] [Level] [FOAAssumptions] {β : TypeIndex} +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : TypeIndex} (π : NearLitterApprox) (A : ExtendedIndex β) namespace NearLitterApprox diff --git a/ConNF/FOA/Complete/HypAction.lean b/ConNF/FOA/Complete/HypAction.lean index a824e8125e..48b9452691 100644 --- a/ConNF/FOA/Complete/HypAction.lean +++ b/ConNF/FOA/Complete/HypAction.lean @@ -8,7 +8,7 @@ universe u namespace ConNF -variable [Params.{u}] [Level] [FOAAssumptions] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] /-! # Induction on addresses diff --git a/ConNF/FOA/Complete/LitterCompletion.lean b/ConNF/FOA/Complete/LitterCompletion.lean index afe418c153..dde2c40ab7 100644 --- a/ConNF/FOA/Complete/LitterCompletion.lean +++ b/ConNF/FOA/Complete/LitterCompletion.lean @@ -13,7 +13,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [Level] [FOAAssumptions] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] /-- The inductive hypothesis used for proving freedom of action: Every free approximation exactly approximates some allowable permutation. -/ diff --git a/ConNF/FOA/Complete/NearLitterCompletion.lean b/ConNF/FOA/Complete/NearLitterCompletion.lean index ed03604fd3..4da89dedc5 100644 --- a/ConNF/FOA/Complete/NearLitterCompletion.lean +++ b/ConNF/FOA/Complete/NearLitterCompletion.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] def nearLitterHypothesis (A : ExtendedIndex β) (N : NearLitter) (H : HypAction ⟨A, inr N⟩) : diff --git a/ConNF/FOA/Corollaries.lean b/ConNF/FOA/Corollaries.lean index fdb0b0eb73..3de3008b20 100644 --- a/ConNF/FOA/Corollaries.lean +++ b/ConNF/FOA/Corollaries.lean @@ -9,7 +9,7 @@ universe u namespace ConNF -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β] -- TODO: Reverse equalities of NearLitterApprox.map_atom @@ -113,7 +113,7 @@ theorem foaMotive_litter (ψ : StructAction β) (h₁ : ψ.Lawful) (h₂ : ψ.Co Allowable.toStructPerm_apply] rw [toStructPerm_smul_fuzz, comp_bot_smul_atom] · have := ih ⟨A.cons (bot_lt_coe _), inl a⟩ - (Relation.TransGen.single (Constrains.fuzz_bot hε A a)) + (Relation.TransGen.single (Constrains.fuzzBot hε A a)) (h₂.atom_bot_dom A hε hL) simp only [Allowable.toStructPerm_comp, Tree.comp_apply, Hom.comp_toPath] exact this.symm diff --git a/ConNF/FOA/Properties/Bijective.lean b/ConNF/FOA/Properties/Bijective.lean index d050498958..c904462575 100644 --- a/ConNF/FOA/Properties/Bijective.lean +++ b/ConNF/FOA/Properties/Bijective.lean @@ -11,7 +11,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [BasePositions] [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 index 192449d410..cd0d210792 100644 --- a/ConNF/FOA/Properties/ConstrainedAction.lean +++ b/ConNF/FOA/Properties/ConstrainedAction.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] def transConstrained (c d : Address β) : Set (Address β) := diff --git a/ConNF/FOA/Properties/Injective.lean b/ConNF/FOA/Properties/Injective.lean index 0dcc9b31a2..02cde76b59 100644 --- a/ConNF/FOA/Properties/Injective.lean +++ b/ConNF/FOA/Properties/Injective.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] {π : StructApprox β} theorem atom_injective_extends {c d : Address β} (hcd : (ihsAction π c d).Lawful) @@ -156,9 +156,9 @@ theorem Biexact.smul_eq_smul {β : Λ} [LeLevel β] {π π' : Allowable β} {c : have := ih ⟨B.cons <| bot_lt_coe _, inl a⟩ ?_ ?_ · simp only [smul_inl, inl.injEq] at this exact this - · exact Constrains.fuzz_bot hε _ _ + · exact Constrains.fuzzBot hε _ _ · refine' h.constrains (Relation.ReflTransGen.single _) - exact Constrains.fuzz_bot hε _ _ + exact Constrains.fuzzBot hε _ _ theorem Biexact.smul_eq_smul_nearLitter {β : Λ} [LeLevel β] {π π' : Allowable β} {A : ExtendedIndex β} {N : NearLitter} @@ -372,11 +372,11 @@ theorem ConNF.StructApprox.extracted_1 refine Eq.trans ?_ this.symm rw [← (h <| C.cons (bot_lt_coe _)).map_atom a (Or.inl (Or.inl (Or.inl (Or.inl - ⟨c, hc₁, Relation.ReflTransGen.head (Constrains.fuzz_bot hε _ _) hc₂'⟩))))] + ⟨c, hc₁, Relation.ReflTransGen.head (Constrains.fuzzBot hε _ _) hc₂'⟩))))] rw [StructAction.rc_smul_atom_eq] · rfl · simp only [Tree.comp_apply, constrainedAction_atomMap] - exact ⟨c, hc₁, Relation.ReflTransGen.head (Constrains.fuzz_bot hε _ _) hc₂'⟩ + exact ⟨c, hc₁, Relation.ReflTransGen.head (Constrains.fuzzBot hε _ _) hc₂'⟩ theorem ConNF.StructApprox.extracted_2 (hπf : π.Free) {γ : Λ} [LeLevel γ] (A : Path (β : TypeIndex) γ) @@ -792,10 +792,10 @@ theorem litter_injective_extends (hπf : π.Free) {c d : Address β} cases coe_injective (Path.obj_eq_of_cons_eq_cons (Path.heq_of_cons_eq_cons hB).eq) cases (Path.heq_of_cons_eq_cons (Path.heq_of_cons_eq_cons hB).eq).eq refine' congr_arg _ ((hcd _).atomMap_injective _ _ (fuzz_injective bot_ne_coe h)) - · have := Constrains.fuzz_bot hγε₁ B₁ a₁ + · have := Constrains.fuzzBot hγε₁ B₁ a₁ exact transConstrained_of_reflTransConstrained_of_trans_constrains h₁ (Relation.TransGen.single this) - · have := Constrains.fuzz_bot hγε₁ B₁ a₂ + · have := Constrains.fuzzBot hγε₁ B₁ a₂ exact transConstrained_of_reflTransConstrained_of_trans_constrains h₂ (Relation.TransGen.single this) · obtain ⟨h₁'⟩ := h₁' diff --git a/ConNF/FOA/Properties/Surjective.lean b/ConNF/FOA/Properties/Surjective.lean index a5b07a5c88..4b59ce9fd8 100644 --- a/ConNF/FOA/Properties/Surjective.lean +++ b/ConNF/FOA/Properties/Surjective.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] {π : StructApprox β} theorem completeNearLitterMap_subset_range (A : ExtendedIndex β) (L : Litter) : @@ -151,7 +151,7 @@ theorem completeLitterMap_surjective_extends (hπf : π.Free) (A : ExtendedIndex exact h · exact NearLitterApprox.flexibleCompletion_symm_smul_flexible (π A) A (hπf A) L h · obtain ⟨⟨γ, ε, hε, C, rfl⟩, a, rfl⟩ := h - obtain ⟨b, rfl⟩ := ha _ a (Constrains.fuzz_bot hε _ a) + obtain ⟨b, rfl⟩ := ha _ a (Constrains.fuzzBot hε _ a) refine' ⟨fuzz (show ⊥ ≠ (ε : TypeIndex) from bot_ne_coe) b, _⟩ rw [completeLitterMap_eq_of_inflexibleBot ⟨⟨γ, ε, hε, C, rfl⟩, b, rfl⟩] · obtain ⟨⟨γ, δ, ε, hδ, hε, hδε, B, rfl⟩, t, rfl⟩ := h diff --git a/ConNF/FOA/Result.lean b/ConNF/FOA/Result.lean index 43bae7287b..60911d167f 100644 --- a/ConNF/FOA/Result.lean +++ b/ConNF/FOA/Result.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [BasePositions] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] {π : StructApprox β} noncomputable def completeAtomPerm (hπf : π.Free) (A : ExtendedIndex β) : Perm Atom := @@ -276,8 +276,7 @@ theorem freedom_of_action {β : Λ} [i : LeLevel β] (π₀ : StructApprox β) ( revert i have := WellFounded.induction (C := fun β => ∀ (i : LeLevel β) (π₀ : StructApprox β), - Free π₀ → ∃ π : Allowable β, - ExactlyApproximates π₀ (@Allowable.toStructPerm _ _ FOAData.tangleData π)) + Free π₀ → ∃ π : Allowable β, ExactlyApproximates π₀ (Allowable.toStructPerm π)) (inferInstanceAs (IsWellFounded Λ (· < ·))).wf β refine fun i => this ?_ i π₀ h intro β ih _ π₀ h diff --git a/ConNF/Fuzz/Construction.lean b/ConNF/Fuzz/Construction.lean index 58ccb5f22a..8faf53e776 100644 --- a/ConNF/Fuzz/Construction.lean +++ b/ConNF/Fuzz/Construction.lean @@ -111,14 +111,14 @@ The majority of this section is spent proving that the set of values to deny isn such that we could run out of available values for the function. -/ -variable [Params.{u}] {β : TypeIndex} {γ : Λ} [TangleData β] [PositionedTangles β] +variable [Params.{u}] [BasePositions] {β : TypeIndex} {γ : Λ} [TangleData β] [PositionedTangles β] [TangleData γ] [PositionedTangles γ] [TypedObjects γ] (hβγ : β ≠ γ) variable (γ) /-- The set of elements of `ν` that `fuzz _ t` cannot be. -/ def fuzzDeny (t : Tangle β) : Set μ := - { ν : μ | ∃ (N : NearLitter), pos (typedNearLitter N : Tangle γ) ≤ pos t ∧ ν = N.1.1 } ∪ + { ν : μ | ∃ (N : NearLitter), pos N ≤ pos t ∧ ν = N.1.1 } ∪ { ν : μ | ∃ (a : Atom), pos a ≤ pos t ∧ ν = a.1.1 } theorem mk_invImage_lt (t : Tangle β) : #{ t' // t' < t } < #μ := by @@ -128,27 +128,22 @@ theorem mk_invImage_lt (t : Tangle β) : #{ t' // t' < t } < #μ := by simp only [Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq, Subtype.coe_inj] at h exact h -theorem mk_invImage_le (t : Tangle β) : #{ t' : Tangle γ // pos t' ≤ pos t } < #μ := by - refine lt_of_le_of_lt ?_ (show #{ ν // ν ≤ pos t } < #μ from card_Iic_lt _) - refine ⟨⟨fun t' => ⟨_, t'.prop⟩, ?_⟩⟩ - intro y₁ y₂ h - simp only [Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq, Subtype.coe_inj] at h - exact h - variable {γ} theorem mk_fuzzDeny (t : Tangle β) : - #{ t' // t' < t } + #(fuzzDeny γ t) < #μ := by + #{ t' // t' < t } + #(fuzzDeny t) < #μ := by refine add_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le (mk_invImage_lt t) ?_ refine lt_of_le_of_lt (mk_union_le _ _) ?_ refine add_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le ?_ ?_ - · refine lt_of_le_of_lt ?_ (mk_invImage_le γ t) - refine ⟨⟨fun i => ⟨typedNearLitter i.prop.choose, i.prop.choose_spec.1⟩, ?_⟩⟩ - intro ν₁ ν₂ h - have h' := typedNearLitter.injective (Subtype.coe_inj.mpr h) - have := ν₁.2.choose_spec.2 - rw [h', ← ν₂.2.choose_spec.2] at this - exact Subtype.coe_inj.mp this + · have : #{ N : NearLitter | pos N ≤ pos t } < #μ + · refine lt_of_le_of_lt ?_ (card_Iic_lt (pos t)) + refine ⟨⟨fun a => ⟨pos a.1, a.2⟩, ?_⟩⟩ + intro a b h + exact Subtype.coe_inj.mp (pos_injective (Subtype.coe_inj.mpr h)) + refine lt_of_le_of_lt ?_ this + refine mk_le_of_surjective (f := fun a => ⟨_, a.1, a.2, rfl⟩) ?_ + rintro ⟨_, a, ha, rfl⟩ + exact ⟨⟨a, ha⟩, rfl⟩ · have : #{ a : Atom | pos a ≤ pos t } < #μ · refine lt_of_le_of_lt ?_ (card_Iic_lt (pos t)) refine ⟨⟨fun a => ⟨pos a.1, a.2⟩, ?_⟩⟩ @@ -181,7 +176,7 @@ the pos of the input to the function. This ensures a well-foundedness condition in many places later. -/ noncomputable def fuzz (t : Tangle β) : Litter := - ⟨chooseWf (fuzzDeny γ) mk_fuzzDeny t, β, γ, hβγ⟩ + ⟨chooseWf fuzzDeny mk_fuzzDeny t, β, γ, hβγ⟩ @[simp] theorem fuzz_β (t : Tangle β) : (fuzz hβγ t).β = β := @@ -219,17 +214,17 @@ theorem fuzz_injective : Injective (fuzz hβγ) := by simp only [fuzz, Litter.mk.injEq, chooseWf_injective.eq_iff, and_self, and_true] at h exact h -theorem fuzz_not_mem_deny (t : Tangle β) : (fuzz hβγ t).ν ∉ fuzzDeny γ t := +theorem fuzz_not_mem_deny (t : Tangle β) : (fuzz hβγ t).ν ∉ fuzzDeny t := chooseWf_not_mem_deny t -theorem fuzz_pos (t : Tangle β) (N : NearLitter) (h : N.1 = fuzz hβγ t) : - pos t < pos (typedNearLitter N : Tangle γ) := by +theorem pos_lt_pos_fuzz_nearLitter (t : Tangle β) (N : NearLitter) (h : N.1 = fuzz hβγ t) : + pos t < pos N := by have h' := fuzz_not_mem_deny hβγ t contrapose! h' refine Or.inl ⟨N, h', ?_⟩ rw [h] -theorem pos_lt_pos_fuzz (t : Tangle β) (a : Atom) (ha : a.1 = fuzz hβγ t) : +theorem pos_lt_pos_fuzz_atom (t : Tangle β) (a : Atom) (ha : a.1 = fuzz hβγ t) : pos t < pos a := by have h' := fuzz_not_mem_deny hβγ t contrapose! h' diff --git a/ConNF/Fuzz/Hypotheses.lean b/ConNF/Fuzz/Hypotheses.lean index 3614c43f95..6355c50350 100644 --- a/ConNF/Fuzz/Hypotheses.lean +++ b/ConNF/Fuzz/Hypotheses.lean @@ -19,7 +19,7 @@ it here for more convenient use later. open Function Set WithBot -open scoped Pointwise +open scoped Pointwise symmDiff universe u @@ -146,6 +146,43 @@ class TypedObjects where export TypedObjects (typedAtom typedNearLitter) +class BasePositions where + posAtom : Atom ↪ μ + posNearLitter : NearLitter ↪ μ + lt_pos_atom (a : Atom) : + posNearLitter a.1.toNearLitter < posAtom a + lt_pos_litter (N : NearLitter) (hN : ¬N.IsLitter) : + posNearLitter N.1.toNearLitter < posNearLitter N + lt_pos_symmDiff (a : Atom) (N : NearLitter) (h : a ∈ litterSet N.1 ∆ N) : + posAtom a < posNearLitter N + +/-- A position function for atoms. -/ +instance [BasePositions] : Position Atom μ := + ⟨BasePositions.posAtom⟩ + +/-- A position function for near-litters. -/ +instance [BasePositions] : Position NearLitter μ := + ⟨BasePositions.posNearLitter⟩ + +theorem lt_pos_atom [BasePositions] (a : Atom) : pos a.1.toNearLitter < pos a := + BasePositions.lt_pos_atom a + +theorem lt_pos_litter [BasePositions] (N : NearLitter) (hN : ¬N.IsLitter) : + pos N.1.toNearLitter < pos N := + BasePositions.lt_pos_litter N hN + +theorem lt_pos_symmDiff [BasePositions] (a : Atom) (N : NearLitter) (h : a ∈ litterSet N.1 ∆ N) : + pos a < pos N := + BasePositions.lt_pos_symmDiff a N h + +class PositionedObjects [BasePositions] [PositionedTangles α] [TypedObjects α] where + pos_typedAtom (a : Atom) : pos (typedAtom a : Tangle α) = pos a + pos_typedNearLitter (N : NearLitter) : pos (typedNearLitter N : Tangle α) = pos N + +export PositionedObjects (pos_typedAtom pos_typedNearLitter) + +attribute [simp] pos_typedAtom pos_typedNearLitter + namespace Allowable variable {α} @@ -174,13 +211,9 @@ instance Bot.tangleData : TangleData ⊥ NearLitterPerm.smul_address_eq_iff, forall_eq, Sum.smul_inl, Sum.inl.injEq] at h exact h -/-- A position function for atoms, which is chosen arbitrarily. -/ -noncomputable instance instPositionAtom : Position Atom μ := - ⟨Nonempty.some mk_atom.le⟩ - -/-- The position function at level `⊥`, which is chosen arbitrarily. -/ -noncomputable instance Bot.positionedTangles : PositionedTangles ⊥ := - ⟨instPositionAtom.pos⟩ +/-- The position function at level `⊥`, taken from the `BasePositions`. -/ +instance Bot.positionedTangles [BasePositions] : PositionedTangles ⊥ := + ⟨BasePositions.posAtom⟩ /-- The identity equivalence between `⊥`-allowable permutations and near-litter permutations. This equivalence is a group isomorphism. -/ diff --git a/ConNF/Model/Construction.lean b/ConNF/Model/Construction.lean index b0060d0552..eeb9e52e88 100644 --- a/ConNF/Model/Construction.lean +++ b/ConNF/Model/Construction.lean @@ -9,7 +9,9 @@ universe u namespace ConNF.Construction -variable [Params.{u}] +variable [Params.{u}] [BasePositions] + +#exit /-- The data for the main inductive hypothesis, containing the things we need to construct at each level `α`. -/ diff --git a/ConNF/NewTangle/Cloud.lean b/ConNF/NewTangle/Cloud.lean index 26dfdff9c5..bf562f90ae 100644 --- a/ConNF/NewTangle/Cloud.lean +++ b/ConNF/NewTangle/Cloud.lean @@ -37,14 +37,15 @@ universe u namespace ConNF -variable [Params.{u}] [Level] +variable [Params.{u}] [Level] [BasePositions] open Code section Cloud variable {γ : TypeIndex} [LtLevel γ] [TangleData γ] [PositionedTangles γ] - {β : Λ} [LtLevel β] [TangleData β] [PositionedTangles β] [TypedObjects β] (hγβ : γ ≠ β) + {β : Λ} [LtLevel β] [TangleData β] [PositionedTangles β] [TypedObjects β] [PositionedObjects β] + (hγβ : γ ≠ β) /-- The cloud map. We map each tangle to all typed near-litters near the `fuzz`ed tangle, and take the union over all tangles in the input. -/ @@ -141,8 +142,8 @@ theorem minTangle_lt_minTangle_cloud (s : Set (Tangle γ)) (hs : s.Nonempty) : pos (minTangle s hs) < pos (minTangle (cloud hγβ s) hs.cloud) := by obtain ⟨t, ht, N, hN, h⟩ := mem_cloud.1 (minTangle_mem (cloud hγβ s) hs.cloud) refine (minTangle_le s hs ht).trans_lt ?_ - rw [h] - exact fuzz_pos hγβ t _ hN + rw [h, pos_typedNearLitter] + exact pos_lt_pos_fuzz_nearLitter hγβ t _ hN end Cloud @@ -184,7 +185,8 @@ theorem extension_ne (hβγ : β ≠ γ) : extension s γ = cloud hβγ s := end Extension -variable [TypedObjectsLt] (γ : TypeIndex) [LtLevel γ] (β : Λ) [LtLevel β] (c d : Code) +variable [TypedObjectsLt] [PositionedObjectsLt] + (γ : TypeIndex) [LtLevel γ] (β : Λ) [LtLevel β] (c d : Code) /-- The `cloud` map, phrased as a function on `α`-codes, but if the code's level matches `β`, this is the identity function. This is written in a weird way in order to make `(cloudCode β c).1` @@ -259,6 +261,7 @@ theorem codeMinMap_lt_codeMinMap_cloudCode (c : NonemptyCode) (hcβ : c.1.1 ≠ convert minTangle_lt_minTangle_cloud c.1.members c.2 using 1 congr exact snd_cloudCode β c hcβ + infer_instance /-- This relation on `α`-codes allows us to state that there are only finitely many iterated images under the inverse `cloud` map. Note that we require the map to actually change the data, by diff --git a/ConNF/NewTangle/CodeEquiv.lean b/ConNF/NewTangle/CodeEquiv.lean index f5a70f9466..597549909d 100644 --- a/ConNF/NewTangle/CodeEquiv.lean +++ b/ConNF/NewTangle/CodeEquiv.lean @@ -38,8 +38,8 @@ universe u namespace ConNF -variable [Params.{u}] [Level] {β : TypeIndex} [LtLevel β] {γ : Λ} [LtLevel γ] - [TangleDataLt] [TypedObjectsLt] [PositionedTanglesLt] +variable [Params.{u}] [Level] [BasePositions] {β : TypeIndex} [LtLevel β] {γ : Λ} [LtLevel γ] + [TangleDataLt] [TypedObjectsLt] [PositionedTanglesLt] [PositionedObjectsLt] namespace Code @@ -116,20 +116,19 @@ theorem isEven_empty_iff : IsEven (mk β ∅) ↔ (β : TypeIndex) = ⊥ := theorem isOdd_empty_iff : IsOdd (mk β ∅) ↔ (β : TypeIndex) ≠ ⊥ := IsEmpty.isOdd_iff rfl -private theorem not_isOdd_nonempty : ∀ c : NonemptyCode, ¬c.1.IsOdd ↔ c.1.IsEven - | c => by - rw [isOdd_iff, isEven_iff] - push_neg - apply forall_congr' _ - intro d - apply imp_congr_right _ - intro h - rw [Iff.comm, ← not_iff_not, Classical.not_not] - obtain hd | hd := d.members.eq_empty_or_nonempty - · rw [IsEmpty.isOdd_iff hd, IsEmpty.isEven_iff hd, Classical.not_not] - · let _ : ⟨d, hd⟩ ↝ c := cloudRel_coe_coe.1 h - exact not_isOdd_nonempty ⟨d, hd⟩ -termination_by c => c +private theorem not_isOdd_nonempty (c : NonemptyCode) : ¬c.1.IsOdd ↔ c.1.IsEven := by + refine cloudRel'_wellFounded.induction (C := fun c => ¬c.1.IsOdd ↔ c.1.IsEven) c ?_ + intro c ih + rw [isOdd_iff, isEven_iff] + push_neg + apply forall_congr' _ + intro d + apply imp_congr_right _ + intro h + rw [Iff.comm, ← not_iff_not, Classical.not_not] + obtain hd | hd := d.members.eq_empty_or_nonempty + · rw [IsEmpty.isOdd_iff hd, IsEmpty.isEven_iff hd, Classical.not_not] + · exact ih ⟨d, hd⟩ (cloudRel_coe_coe.1 h) /-- A code is not odd iff it is even. -/ @[simp] diff --git a/ConNF/NewTangle/Hypotheses.lean b/ConNF/NewTangle/Hypotheses.lean index 4ddd4df458..4e2eb3248a 100644 --- a/ConNF/NewTangle/Hypotheses.lean +++ b/ConNF/NewTangle/Hypotheses.lean @@ -39,7 +39,8 @@ class PositionedTanglesLt [TangleDataLt] where data : ∀ β : Λ, [LtLevel β] → PositionedTangles β noncomputable instance PositionedTanglesLt.toPositionedTangles - [TangleDataLt] [PositionedTanglesLt] : ∀ β : TypeIndex, [LtLevel β] → PositionedTangles β + [BasePositions] [TangleDataLt] [PositionedTanglesLt] : + ∀ β : TypeIndex, [LtLevel β] → PositionedTangles β | ⊥, _ => Bot.positionedTangles | (β : Λ), _ => PositionedTanglesLt.data β @@ -47,4 +48,8 @@ noncomputable instance PositionedTanglesLt.toPositionedTangles abbrev TypedObjectsLt [TangleDataLt] := ∀ β : Λ, [LtLevel β] → TypedObjects β +/-- The `PositionedObjects` for each `β < α`. -/ +abbrev PositionedObjectsLt [BasePositions] [TangleDataLt] [PositionedTanglesLt] [TypedObjectsLt] := + ∀ β : Λ, [LtLevel β] → PositionedObjects β + end ConNF diff --git a/ConNF/NewTangle/NewAllowable.lean b/ConNF/NewTangle/NewAllowable.lean index 2200c4daf2..f6296e66b5 100644 --- a/ConNF/NewTangle/NewAllowable.lean +++ b/ConNF/NewTangle/NewAllowable.lean @@ -225,7 +225,7 @@ instance : MulAction SemiallowablePerm NonemptyCode := end SemiallowablePerm -variable [PositionedTanglesLt] [TypedObjectsLt] [TangleData α] +variable [BasePositions] [PositionedTanglesLt] [TypedObjectsLt] [PositionedObjectsLt] [TangleData α] /-- We say that a semiallowable permutation is allowable if its one-step derivatives commute with the `fuzz` maps. -/ diff --git a/ConNF/NewTangle/NewTangle.lean b/ConNF/NewTangle/NewTangle.lean index 24018d000e..27e5c77a96 100644 --- a/ConNF/NewTangle/NewTangle.lean +++ b/ConNF/NewTangle/NewTangle.lean @@ -28,7 +28,7 @@ universe u namespace ConNF -variable [Params.{u}] [Level] [TangleDataLt] +variable [Params.{u}] [Level] [BasePositions] [TangleDataLt] {β : TypeIndex} [LtLevel β] {γ : Λ} [LtLevel γ] open Code @@ -81,7 +81,7 @@ end Semitangle open Semitangle -variable [PositionedTanglesLt] [TypedObjectsLt] +variable [PositionedTanglesLt] [TypedObjectsLt] [PositionedObjectsLt] /-- A *semitangle* is a collection of `β`-tangles for each lower level `β < α`, together with a preference for one of these extensions. -/ diff --git a/ConNF/NewTangle/Position.lean b/ConNF/NewTangle/Position.lean index b67e64ba35..0afc0a204d 100644 --- a/ConNF/NewTangle/Position.lean +++ b/ConNF/NewTangle/Position.lean @@ -12,7 +12,9 @@ universe u namespace ConNF.NewTangle -variable [Params.{u}] [Level] [TangleDataLt] [PositionedTanglesLt] [TypedObjectsLt] +variable [Params.{u}] [Level] [BasePositions] [TangleDataLt] [PositionedTanglesLt] [TypedObjectsLt] + +#exit def posBound (t : NewTangle) : Set μ := {ν | ∃ (A : ExtendedIndex α) (a : Atom), ⟨A, inl a⟩ ∈ t.S ∧