From 3cac8d0aeeee5f04297760f76c4ef79164e199af Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Wed, 13 Dec 2023 12:10:31 +0000 Subject: [PATCH 1/5] Remove `BasePositions` Signed-off-by: zeramorphic --- 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 | 4 +- ConNF/FOA/Basic/Flexible.lean | 2 +- ConNF/FOA/Basic/Hypotheses.lean | 2 +- 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/Properties/Bijective.lean | 2 +- ConNF/FOA/Properties/ConstrainedAction.lean | 2 +- ConNF/FOA/Properties/Injective.lean | 2 +- ConNF/FOA/Properties/Surjective.lean | 2 +- ConNF/FOA/Result.lean | 2 +- ConNF/Fuzz/Construction.lean | 2 +- ConNF/Fuzz/Hypotheses.lean | 70 ++----------------- ConNF/NewTangle/Cloud.lean | 2 +- ConNF/NewTangle/CodeEquiv.lean | 2 +- ConNF/NewTangle/NewAllowable.lean | 2 +- ConNF/NewTangle/NewTangle.lean | 2 +- 27 files changed, 34 insertions(+), 94 deletions(-) diff --git a/ConNF/FOA/Action/Complete.lean b/ConNF/FOA/Action/Complete.lean index 08e468f071..b1391e5a8a 100644 --- 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 index 48b9decb66..a76ca86590 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 [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 index ae9705ea21..166e970528 100644 --- 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 index cd440e3327..e6eb000810 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 [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 index dc4cacda50..9201a03180 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 [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 index 65052d9b53..c79feefaef 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 [BasePositions] [Level] [FOAAssumptions] +variable [Level] [FOAAssumptions] def Free {β : Λ} (π₀ : StructApprox β) : Prop := ∀ A, (π₀ A).Free A diff --git a/ConNF/FOA/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean index 511a997619..9a2b0065cc 100644 --- a/ConNF/FOA/Basic/Constrains.lean +++ b/ConNF/FOA/Basic/Constrains.lean @@ -26,7 +26,7 @@ variable [Params.{u}] section ExtendedIndex -variable [BasePositions] +variable instance : Position (Atom ⊕ NearLitter) μ where pos := { @@ -58,7 +58,7 @@ theorem pos_atomNearLitter_inr (N : NearLitter) : end ExtendedIndex -variable [BasePositions] [Level] [FOAAssumptions] {β : Λ} +variable [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 index 7570fc5122..f2401274a7 100644 --- a/ConNF/FOA/Basic/Flexible.lean +++ b/ConNF/FOA/Basic/Flexible.lean @@ -8,7 +8,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : TypeIndex} +variable [Params.{u}] [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 index 6547b84e4c..52ddaece97 100644 --- a/ConNF/FOA/Basic/Hypotheses.lean +++ b/ConNF/FOA/Basic/Hypotheses.lean @@ -21,7 +21,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] +variable [Params.{u}] [Level] /-- Asserts that the positions of typed objects agree with the position functions defined on atoms and near-litters in `BasePositions`. -/ diff --git a/ConNF/FOA/Basic/Reduction.lean b/ConNF/FOA/Basic/Reduction.lean index d092244f6f..1d5252fe5b 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}] [BasePositions] [Level] [FOAAssumptions] +variable [Params.{u}] [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/Complete/AtomCompletion.lean b/ConNF/FOA/Complete/AtomCompletion.lean index 6ed14443e3..fed818ff74 100644 --- a/ConNF/FOA/Complete/AtomCompletion.lean +++ b/ConNF/FOA/Complete/AtomCompletion.lean @@ -9,7 +9,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} (π : StructApprox β) +variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} (π : StructApprox β) namespace StructApprox diff --git a/ConNF/FOA/Complete/CompleteAction.lean b/ConNF/FOA/Complete/CompleteAction.lean index 0fe120a504..7509436a3c 100644 --- a/ConNF/FOA/Complete/CompleteAction.lean +++ b/ConNF/FOA/Complete/CompleteAction.lean @@ -12,7 +12,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] /-! diff --git a/ConNF/FOA/Complete/FlexibleCompletion.lean b/ConNF/FOA/Complete/FlexibleCompletion.lean index 45f84fc7b1..1026c4a4eb 100644 --- a/ConNF/FOA/Complete/FlexibleCompletion.lean +++ b/ConNF/FOA/Complete/FlexibleCompletion.lean @@ -8,7 +8,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : TypeIndex} +variable [Params.{u}] [Level] [FOAAssumptions] {β : TypeIndex} (π : NearLitterApprox) (A : ExtendedIndex β) namespace NearLitterApprox diff --git a/ConNF/FOA/Complete/HypAction.lean b/ConNF/FOA/Complete/HypAction.lean index d4aca30719..a7b2e6dbce 100644 --- a/ConNF/FOA/Complete/HypAction.lean +++ b/ConNF/FOA/Complete/HypAction.lean @@ -8,7 +8,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] +variable [Params.{u}] [Level] [FOAAssumptions] /-! # Induction on support conditions diff --git a/ConNF/FOA/Complete/LitterCompletion.lean b/ConNF/FOA/Complete/LitterCompletion.lean index 1c092e7875..cfee365d53 100644 --- a/ConNF/FOA/Complete/LitterCompletion.lean +++ b/ConNF/FOA/Complete/LitterCompletion.lean @@ -13,7 +13,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] +variable [Params.{u}] [Level] [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 0140fc3640..0f419ef426 100644 --- a/ConNF/FOA/Complete/NearLitterCompletion.lean +++ b/ConNF/FOA/Complete/NearLitterCompletion.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] def nearLitterHypothesis (A : ExtendedIndex β) (N : NearLitter) (H : HypAction ⟨A, inr N⟩) : diff --git a/ConNF/FOA/Properties/Bijective.lean b/ConNF/FOA/Properties/Bijective.lean index ac49f461fd..d050498958 100644 --- a/ConNF/FOA/Properties/Bijective.lean +++ b/ConNF/FOA/Properties/Bijective.lean @@ -11,7 +11,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [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 index 13f09d0797..f2651721b4 100644 --- a/ConNF/FOA/Properties/ConstrainedAction.lean +++ b/ConNF/FOA/Properties/ConstrainedAction.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [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 index de279845c8..8673def5bb 100644 --- a/ConNF/FOA/Properties/Injective.lean +++ b/ConNF/FOA/Properties/Injective.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [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 index 2e3d71231f..e98009bc4d 100644 --- a/ConNF/FOA/Properties/Surjective.lean +++ b/ConNF/FOA/Properties/Surjective.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [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 index f597dc13ff..9fb179d02d 100644 --- a/ConNF/FOA/Result.lean +++ b/ConNF/FOA/Result.lean @@ -10,7 +10,7 @@ namespace ConNF namespace StructApprox -variable [Params.{u}] [BasePositions] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] +variable [Params.{u}] [Level] [FOAAssumptions] {β : Λ} [LeLevel β] [FreedomOfActionHypothesis β] {π : StructApprox β} noncomputable def completeAtomPerm (hπf : π.Free) (A : ExtendedIndex β) : Perm Atom := diff --git a/ConNF/Fuzz/Construction.lean b/ConNF/Fuzz/Construction.lean index 8ef4a8ff1f..7d7fe7ffea 100644 --- a/ConNF/Fuzz/Construction.lean +++ b/ConNF/Fuzz/Construction.lean @@ -112,7 +112,7 @@ such that we could run out of available values for the function. -/ variable [Params.{u}] {β : TypeIndex} {γ : Λ} [TangleData β] [PositionedTangles β] - [BasePositions] [TangleData γ] [PositionedTangles γ] [TypedObjects γ] (hβγ : β ≠ γ) + [TangleData γ] [PositionedTangles γ] [TypedObjects γ] (hβγ : β ≠ γ) -- TODO: Refactor to use near-litters directly instead of `IsNearLitter`. /-- The requirements to be satisfied by the f-maps. diff --git a/ConNF/Fuzz/Hypotheses.lean b/ConNF/Fuzz/Hypotheses.lean index 967f848874..f273477a63 100644 --- a/ConNF/Fuzz/Hypotheses.lean +++ b/ConNF/Fuzz/Hypotheses.lean @@ -132,68 +132,6 @@ theorem smul_typedNearLitter (ρ : Allowable α) (N : NearLitter) : end Allowable -/-- This class stores the position of typed atoms and typed near-litters in the position function -at any level, along with some conditions on these maps. -/ -class BasePositions where - /-- Gives the positions of typed atoms at any level. -/ - typedAtomPosition : Atom ↪ μ - /-- Gives the positions of typed near-litters at any level. -/ - typedNearLitterPosition : NearLitter ↪ μ - /-- Typed litters precede typed atoms they contain. -/ - litter_lt_atom : - ∀ (L : Litter), - ∀ a ∈ litterSet L, typedNearLitterPosition L.toNearLitter < typedAtomPosition a - /-- Typed litters precede near-litters to them. -/ - litter_le_nearLitter : - ∀ N : NearLitter, typedNearLitterPosition N.fst.toNearLitter ≤ typedNearLitterPosition N - /-- Atoms in the symmetric difference between a near-litter and its corresponding litter - precede the near-litter. -/ - symmDiff_lt_nearLitter : - ∀ (N : NearLitter), - ∀ a ∈ litterSet N.fst ∆ N.snd, typedAtomPosition a < typedNearLitterPosition N - typedAtomPosition_ne_typedNearLitterPosition : - ∀ a N, typedAtomPosition a ≠ typedNearLitterPosition N - -instance [BasePositions] : Position Atom μ where - pos := BasePositions.typedAtomPosition - -instance [BasePositions] : Position NearLitter μ where - pos := BasePositions.typedNearLitterPosition - -instance [BasePositions] : Position Litter μ where - pos := { - toFun := fun L => pos L.toNearLitter - inj' := fun _ _ h => Litter.toNearLitter_injective (pos_injective h) - } - -/-- Typed litters precede typed atoms they contain. -/ -theorem litter_lt_atom [BasePositions] : - ∀ L : Litter, ∀ a ∈ litterSet L, pos L < pos a := - BasePositions.litter_lt_atom - -/-- Typed litters precede near-litters to them. -/ -theorem litter_le_nearLitter [BasePositions] : - ∀ N : NearLitter, pos N.1 ≤ pos N := - BasePositions.litter_le_nearLitter - -/-- Typed litters precede near-litters to them. -/ -theorem litter_lt_nearLitter [BasePositions] (N : NearLitter) (hN : ¬N.IsLitter) : - pos N.1 < pos N := - lt_of_le_of_ne - (litter_le_nearLitter N) - (pos_injective.ne (f := (pos : NearLitter → μ)) (NearLitter.not_isLitter' hN)) - -/-- Atoms in the symmetric difference between a near-litter and its corresponding litter -precede the near-litter. -/ -theorem symmDiff_lt_nearLitter [BasePositions] : - ∀ N : NearLitter, ∀ a ∈ litterSet N.fst ∆ N.snd, pos a < pos N := - BasePositions.symmDiff_lt_nearLitter - -/-- Atoms and near-litters cannot be assigned the same position. -/ -theorem pos_atom_ne_pos_nearLitter [BasePositions] : - ∀ a : Atom, ∀ N : NearLitter, pos a ≠ pos N := - BasePositions.typedAtomPosition_ne_typedNearLitterPosition - /-- The tangle data at level `⊥` is constructed by taking the tangles to be the atoms, the allowable permutations to be near-litter permutations, and the designated supports to be singletons. -/ instance Bot.tangleData : TangleData ⊥ @@ -211,11 +149,13 @@ instance Bot.tangleData : TangleData ⊥ exact h small := small_singleton _ } -/-- The position function at level `⊥`, which is chosen arbitrarily. -/ -noncomputable instance Bot.positionedTangles : PositionedTangles ⊥ := +/-- A position function for atoms, which is chosen arbitrarily. -/ +noncomputable instance instPositionAtom : Position Atom μ := ⟨Nonempty.some mk_atom.le⟩ --- TODO: Require coherence between `pos : Tangle ⊥ → μ` and `pos : Atom → μ`? +/-- The position function at level `⊥`, which is chosen arbitrarily. -/ +noncomputable instance Bot.positionedTangles : PositionedTangles ⊥ := + ⟨instPositionAtom.pos⟩ /-- The identity equivalence between `⊥`-allowable permutations and near-litter permutations. This equivalence is a group isomorphism. -/ diff --git a/ConNF/NewTangle/Cloud.lean b/ConNF/NewTangle/Cloud.lean index cbfa447dd0..c53d4fc99b 100644 --- a/ConNF/NewTangle/Cloud.lean +++ b/ConNF/NewTangle/Cloud.lean @@ -36,7 +36,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] +variable [Params.{u}] [Level] open Code diff --git a/ConNF/NewTangle/CodeEquiv.lean b/ConNF/NewTangle/CodeEquiv.lean index d64b5f0c6b..85523abe8f 100644 --- a/ConNF/NewTangle/CodeEquiv.lean +++ b/ConNF/NewTangle/CodeEquiv.lean @@ -38,7 +38,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] {β : TypeIndex} [LtLevel β] {γ : Λ} [LtLevel γ] +variable [Params.{u}] [Level] {β : TypeIndex} [LtLevel β] {γ : Λ} [LtLevel γ] [TangleDataLt] [TypedObjectsLt] [PositionedTanglesLt] namespace Code diff --git a/ConNF/NewTangle/NewAllowable.lean b/ConNF/NewTangle/NewAllowable.lean index 6fc5fafe85..d8de43e894 100644 --- a/ConNF/NewTangle/NewAllowable.lean +++ b/ConNF/NewTangle/NewAllowable.lean @@ -197,7 +197,7 @@ instance : MulAction SemiallowablePerm NonemptyCode := end SemiallowablePerm -variable [BasePositions] [PositionedTanglesLt] [TypedObjectsLt] [TangleData α] +variable [PositionedTanglesLt] [TypedObjectsLt] [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 f6f67276a2..780dbfe978 100644 --- a/ConNF/NewTangle/NewTangle.lean +++ b/ConNF/NewTangle/NewTangle.lean @@ -28,7 +28,7 @@ universe u namespace ConNF -variable [Params.{u}] [BasePositions] [Level] [TangleDataLt] +variable [Params.{u}] [Level] [TangleDataLt] {β : TypeIndex} [LtLevel β] {γ : Λ} [LtLevel γ] open Code From 7caf1c08e221488444b8c5d223417a32ba3e28f5 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Wed, 13 Dec 2023 12:15:08 +0000 Subject: [PATCH 2/5] Sorry out well-foundedness Signed-off-by: zeramorphic --- ConNF/FOA/Basic/Constrains.lean | 70 +-------------------------------- ConNF/FOA/Basic/Hypotheses.lean | 14 +------ ConNF/FOA/Basic/Reduction.lean | 8 ---- 3 files changed, 3 insertions(+), 89 deletions(-) diff --git a/ConNF/FOA/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean index 9a2b0065cc..204229c0a9 100644 --- a/ConNF/FOA/Basic/Constrains.lean +++ b/ConNF/FOA/Basic/Constrains.lean @@ -22,43 +22,7 @@ universe u namespace ConNF -variable [Params.{u}] - -section ExtendedIndex - -variable - -instance : Position (Atom ⊕ NearLitter) μ where - pos := { - toFun := fun x => match x with - | inl a => pos a - | inr N => pos N - inj' := by - rintro (a₁ | N₁) (a₂ | N₂) h - · exact congr_arg _ (pos_injective h) - · cases pos_atom_ne_pos_nearLitter a₁ N₂ h - · cases pos_atom_ne_pos_nearLitter a₂ N₁ h.symm - · exact congr_arg _ (pos_injective h) - } - -/-- Override the default instance for `LT (α ⊕ β)`. -/ -@[default_instance 1500] -instance : LT (Atom ⊕ NearLitter) := - ⟨InvImage (· < ·) pos⟩ - -@[simp] -theorem pos_atomNearLitter_inl (a : Atom) : - pos (inl a : Atom ⊕ NearLitter) = pos a := - rfl - -@[simp] -theorem pos_atomNearLitter_inr (N : NearLitter) : - pos (inr N : Atom ⊕ NearLitter) = pos N := - rfl - -end ExtendedIndex - -variable [Level] [FOAAssumptions] {β : Λ} +variable [Params.{u}] [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 @@ -90,31 +54,10 @@ inductive Constrains : SupportCondition β → SupportCondition β → Prop @[inherit_doc] infix:50 " ≺ " => Constrains -theorem constrains_subrelation : Subrelation - ((· ≺ ·) : SupportCondition β → _ → Prop) - (InvImage (· < ·) SupportCondition.value) := by - intro c d h - obtain ⟨A, a⟩ | ⟨A, N, hN⟩ | ⟨A, N, a, ha⟩ | ⟨hδ, hε, hδε, A, t, c, hc⟩ | ⟨hδ, A, a⟩ := h - · exact litter_lt_atom a.1 a rfl - · exact litter_lt_nearLitter N hN - · exact symmDiff_lt_nearLitter N a ha - · have := fuzz_pos hδε t ?_ ?_ - rw [PositionedTypedObjects.pos_nearLitter_eq] at this - refine' lt_of_le_of_lt _ this - obtain ⟨B, a | N⟩ := c - · exact PositionedTypedObjects.pos_atom_le t B a hc - · exact PositionedTypedObjects.pos_nearLitter_le t B N hc - · rfl - · simp only [InvImage, elim_inr] - convert pos_atom_lt_fuzz a - simp only [← pos_lt_pos, pos_atomNearLitter_inl, pos_atomNearLitter_inr] - rw [@PositionedTypedObjects.pos_nearLitter_eq _ _ _ ?_ ?_ ?_ ?_ _] - infer_instance - /-- The `≺` relation is well-founded. By the conditions on orderings, if we have `(x, A) ≺ (y, B)`, then `x < y` in `µ`, under the `typedNearLitter` or `typedAtom` maps. -/ theorem constrains_wf (β : Λ) : WellFounded ((· ≺ · ) : SupportCondition β → _ → Prop) := - Subrelation.wf constrains_subrelation IsWellFounded.wf + sorry @[simp] theorem constrains_atom {c : SupportCondition β} {A : ExtendedIndex β} {a : Atom} : @@ -160,15 +103,6 @@ instance : PartialOrder (SupportCondition β) where · exact h₂ cases (constrains_wf β).transGen.isIrrefl.irrefl c (h₁.trans h₂) -theorem lt_subrelation : Subrelation - ((· < ·) : SupportCondition β → _ → Prop) - (InvImage (· < ·) SupportCondition.value) := by - intro c d h - change pos c.value < pos d.value - induction h with - | single hcd => exact constrains_subrelation hcd - | tail _ h ih => exact ih.trans (constrains_subrelation h) - instance : WellFoundedLT (SupportCondition β) where wf := (constrains_wf β).transGen diff --git a/ConNF/FOA/Basic/Hypotheses.lean b/ConNF/FOA/Basic/Hypotheses.lean index 52ddaece97..2945bce7b9 100644 --- a/ConNF/FOA/Basic/Hypotheses.lean +++ b/ConNF/FOA/Basic/Hypotheses.lean @@ -27,19 +27,7 @@ variable [Params.{u}] [Level] and near-litters in `BasePositions`. -/ class PositionedTypedObjects (β : Λ) [TangleData β] [TypedObjects β] [PositionedTangles β] : Prop where - pos_atom_eq : ∀ a : Atom, pos (typedAtom a : Tangle β) = pos a - pos_nearLitter_eq : - ∀ N : NearLitter, pos (typedNearLitter N : Tangle β) = pos N - /-- All tangles are positioned later than all of the support conditions in their designated - support. -/ - pos_atom_le : - ∀ (t : Tangle β) (A : ExtendedIndex β) (a : Atom), - ⟨A, Sum.inl a⟩ ∈ designatedSupport t → pos a ≤ pos t - /-- All tangles are positioned later than all of the support conditions in their designated - support. -/ - pos_nearLitter_le : - ∀ (t : Tangle β) (A : ExtendedIndex β) (N : NearLitter), - ⟨A, Sum.inr N⟩ ∈ designatedSupport t → pos N ≤ pos t + -- TODO: Fill with what we need. /-- The data that we will use when proving the freedom of action theorem. This structure combines the following data: diff --git a/ConNF/FOA/Basic/Reduction.lean b/ConNF/FOA/Basic/Reduction.lean index 1d5252fe5b..3a5ff2ac8f 100644 --- a/ConNF/FOA/Basic/Reduction.lean +++ b/ConNF/FOA/Basic/Reduction.lean @@ -209,12 +209,4 @@ theorem lt_of_mem_reducedSupport obtain ⟨⟨d, hd, hcd⟩, _⟩ := h exact Relation.TransGen.tail' (le_comp hcd _) (Constrains.fuzz hδ hε hδε B t d hd) -theorem pos_lt_of_mem_reducedSupport - {β γ δ ε : Λ} [LeLevel β] [LeLevel γ] [LtLevel δ] [LtLevel ε] - (hδ : (δ : TypeIndex) < γ) (hε : (ε : TypeIndex) < γ) (hδε : (δ : TypeIndex) ≠ ε) - (B : Path (β : TypeIndex) γ) (t : Tangle δ) - (c : SupportCondition δ) (h : c ∈ reducedSupport t) : - pos c.value < pos (fuzz hδε t) := - lt_subrelation (lt_of_mem_reducedSupport hδ hε hδε B t c h) - end ConNF From 15acd97f33660c53d31196c26c39c25539aa708b Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Wed, 13 Dec 2023 13:19:24 +0000 Subject: [PATCH 3/5] Create litter constrains relation Signed-off-by: zeramorphic --- ConNF/FOA/Basic/Constrains.lean | 135 +++++++++++++++++++++++++++++++- ConNF/FOA/Basic/Hypotheses.lean | 25 +++--- ConNF/Fuzz/Construction.lean | 9 +-- 3 files changed, 148 insertions(+), 21 deletions(-) diff --git a/ConNF/FOA/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean index 204229c0a9..e3f54de378 100644 --- a/ConNF/FOA/Basic/Constrains.lean +++ b/ConNF/FOA/Basic/Constrains.lean @@ -54,9 +54,138 @@ inductive Constrains : SupportCondition β → SupportCondition β → Prop @[inherit_doc] infix:50 " ≺ " => Constrains -/-- The `≺` relation is well-founded. By the conditions on orderings, if we have `(x, A) ≺ (y, B)`, -then `x < y` in `µ`, under the `typedNearLitter` or `typedAtom` maps. -/ -theorem constrains_wf (β : Λ) : WellFounded ((· ≺ · ) : SupportCondition β → _ → Prop) := +inductive LitterConstrains : Litter → Litter → Prop + | fuzz_atom ⦃δ : Λ⦄ [LtLevel δ] ⦃ε : Λ⦄ [LtLevel ε] (hδε : (δ : TypeIndex) ≠ ε) + (t : Tangle δ) {B : ExtendedIndex δ} {a : Atom} : ⟨B, inl a⟩ ∈ designatedSupport t → + LitterConstrains a.1 (fuzz hδε t) + | fuzz_nearLitter ⦃δ : Λ⦄ [LtLevel δ] ⦃ε : Λ⦄ [LtLevel ε] (hδε : (δ : TypeIndex) ≠ ε) + (t : Tangle δ) {B : ExtendedIndex δ} {N : NearLitter} : ⟨B, inr N⟩ ∈ designatedSupport t → + LitterConstrains N.1 (fuzz hδε t) + | fuzz_bot ⦃ε : Λ⦄ [LtLevel ε] (a : Atom) : + LitterConstrains a.1 (fuzz (bot_ne_coe (a := ε)) a) + +@[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) + +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 + +theorem hasPosition_of_litterConstrains {L₁ L₂ : Litter} (h : LitterConstrains L₁ L₂) : + ∃ ν, HasPosition L₂ ν := 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_of_atom_mem_designatedSupport t ht t' hδε ht' + | inr h => + obtain ⟨ε, _, a, h, rfl⟩ := h + exact pos_lt_pos_of_atom_mem_designatedSupport t ht + (show Tangle ⊥ from a) bot_ne_coe h + | fuzz_nearLitter 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_of_nearLitter_mem_designatedSupport t ht t' hδε ht' + | inr h => + obtain ⟨ε, _, a, h, rfl⟩ := h + exact pos_lt_pos_of_nearLitter_mem_designatedSupport t ht + (show Tangle ⊥ from a) bot_ne_coe 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 ⊥ + +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 ((· ≺ ·) : SupportCondition β → _ → Prop) := sorry @[simp] diff --git a/ConNF/FOA/Basic/Hypotheses.lean b/ConNF/FOA/Basic/Hypotheses.lean index 2945bce7b9..8a622b1b8a 100644 --- a/ConNF/FOA/Basic/Hypotheses.lean +++ b/ConNF/FOA/Basic/Hypotheses.lean @@ -7,8 +7,6 @@ This file contains the inductive hypotheses required for proving the freedom of ## Main declarations -* `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. -/ @@ -23,12 +21,6 @@ namespace ConNF variable [Params.{u}] [Level] -/-- Asserts that the positions of typed objects agree with the position functions defined on atoms -and near-litters in `BasePositions`. -/ -class PositionedTypedObjects (β : Λ) [TangleData β] [TypedObjects β] [PositionedTangles β] : Prop - where - -- TODO: Fill with what we need. - /-- The data that we will use when proving the freedom of action theorem. This structure combines the following data: * `Tangle` @@ -41,7 +33,6 @@ class FOAData where lowerTangleData : ∀ β : Λ, [LeLevel β] → TangleData β lowerPositionedTangles : ∀ β : Λ, [LtLevel β] → PositionedTangles β lowerTypedObjects : ∀ β : Λ, [LeLevel β] → TypedObjects β - lowerPositionedTypedObjects : ∀ β : Λ, [LtLevel β] → PositionedTypedObjects β namespace FOAData @@ -56,9 +47,6 @@ instance positionedTangles : PositionedTangles γ := instance typedObjects : TypedObjects β := lowerTypedObjects β -instance positionedTypedObjects : PositionedTypedObjects γ := - lowerPositionedTypedObjects γ - noncomputable instance iicBotTangleData : ∀ β : TypeIndex, [LeLevel β] → TangleData β | ⊥, _ => Bot.tangleData | (β : Λ), _ => lowerTangleData β @@ -85,6 +73,18 @@ class FOAAssumptions extends FOAData where /-- Designated supports commute with allowable permutations. -/ designatedSupport_smul {β : Λ} [LeLevel β] (t : Tangle β) (ρ : Allowable β) : designatedSupport (ρ • t) = ρ • (designatedSupport t : Set (SupportCondition β)) + /-- Inflexible litters whose atoms occur in designated supports have position less than the + original tangle. -/ + pos_lt_pos_of_atom_mem_designatedSupport {β : Λ} [LtLevel β] (t : Tangle β) + {A : ExtendedIndex β} {a : Atom} (ht : ⟨A, Sum.inl a⟩ ∈ designatedSupport t) + {γ : TypeIndex} [LtLevel γ] (s : Tangle γ) {δ : Λ} [LtLevel δ] (hγδ : γ ≠ δ) + (ha : a.1 = fuzz hγδ s) : pos s < pos t + /-- Inflexible litters with near-litters in designated supports have position less than the + original tangle. -/ + pos_lt_pos_of_nearLitter_mem_designatedSupport {β : Λ} [LtLevel β] (t : Tangle β) + {A : ExtendedIndex β} {N : NearLitter} (ht : ⟨A, Sum.inr N⟩ ∈ designatedSupport t) + {γ : TypeIndex} [LtLevel γ] (s : Tangle γ) {δ : Λ} [LtLevel δ] (hγδ : γ ≠ δ) + (hN : N.1 = fuzz hγδ s) : pos s < pos t /-- The `fuzz` map commutes with allowable permutations. -/ smul_fuzz {β : TypeIndex} [LeLevel β] {γ : TypeIndex} [LtLevel γ] {δ : Λ} [LtLevel δ] (hγ : γ < β) (hδ : (δ : TypeIndex) < β) (hγδ : γ ≠ δ) (ρ : Allowable β) (t : Tangle γ) : @@ -106,6 +106,7 @@ class FOAAssumptions extends FOAData where allowableCons hγ (allowableOfSmulFuzz β ρs h) = ρs γ hγ export FOAAssumptions (allowableCons allowableCons_eq designatedSupport_smul + pos_lt_pos_of_atom_mem_designatedSupport pos_lt_pos_of_nearLitter_mem_designatedSupport smul_fuzz allowableOfSmulFuzz allowableOfSmulFuzz_comp_eq) attribute [simp] designatedSupport_smul allowableOfSmulFuzz_comp_eq diff --git a/ConNF/Fuzz/Construction.lean b/ConNF/Fuzz/Construction.lean index 7d7fe7ffea..38e24aa8bb 100644 --- a/ConNF/Fuzz/Construction.lean +++ b/ConNF/Fuzz/Construction.lean @@ -266,11 +266,8 @@ theorem fuzz_pos (t : Tangle β) (N : NearLitter) (h : N.1 = fuzz hβγ t) : have := fuzz_pos' hβγ t N ((NearLitter.isNearLitter _ _).mpr h) exact lt_of_lt_of_eq this (congr_arg _ (congr_arg _ (NearLitter.ext rfl))) -theorem pos_atom_lt_fuzz (t : Tangle ⊥) : - pos (show Atom from t) < - pos (typedNearLitter (fuzz (bot_ne_coe : (⊥ : TypeIndex) ≠ γ) t).toNearLitter : Tangle γ) := by - have := fuzz_not_mem_deny (bot_ne_coe : (⊥ : TypeIndex) ≠ γ) t - contrapose! this - exact FuzzCondition.bot t rfl HEq.rfl this +theorem pos_lt_pos_fuzz (t : Tangle β) (a : Atom) (ha : a.1 = fuzz hβγ t) : + pos t < pos a := by + sorry end ConNF From f63ac5b00d4515ac1f15c37ac5f9621d120d40c1 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Wed, 13 Dec 2023 15:25:03 +0000 Subject: [PATCH 4/5] Constrains relation is well-founded Signed-off-by: zeramorphic --- ConNF/BaseType/Atom.lean | 4 ++ ConNF/BaseType/NearLitter.lean | 4 ++ ConNF/FOA/Basic/Constrains.lean | 118 ++++++++++++++++++++++++++++---- ConNF/FOA/Basic/Hypotheses.lean | 10 +-- 4 files changed, 117 insertions(+), 19 deletions(-) diff --git a/ConNF/BaseType/Atom.lean b/ConNF/BaseType/Atom.lean index 0845aebff0..ccc7778637 100644 --- 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 index 9c2c352251..c4bec709f8 100644 --- 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/Basic/Constrains.lean b/ConNF/FOA/Basic/Constrains.lean index e3f54de378..3444543b29 100644 --- a/ConNF/FOA/Basic/Constrains.lean +++ b/ConNF/FOA/Basic/Constrains.lean @@ -38,7 +38,7 @@ inductive Constrains : SupportCondition β → SupportCondition β → Prop | nearLitter (A : ExtendedIndex β) (N : NearLitter) (hN : ¬N.IsLitter) : Constrains ⟨A, inr N.fst.toNearLitter⟩ ⟨A, inr N⟩ | symmDiff (A : ExtendedIndex β) (N : NearLitter) (a : Atom) : - a ∈ litterSet N.fst ∆ N.snd → Constrains ⟨A, inl a⟩ ⟨A, inr N⟩ + a ∈ litterSet N.fst ∆ N → Constrains ⟨A, inl a⟩ ⟨A, inr N⟩ | fuzz ⦃γ : Λ⦄ [LeLevel γ] ⦃δ : Λ⦄ [LtLevel δ] ⦃ε : Λ⦄ [LtLevel ε] (hδ : (δ : TypeIndex) < γ) (hε : (ε : TypeIndex) < γ) (hδε : (δ : TypeIndex) ≠ ε) (A : Path (β : TypeIndex) γ) (t : Tangle δ) (c : SupportCondition δ) : @@ -59,8 +59,9 @@ inductive LitterConstrains : Litter → Litter → Prop (t : Tangle δ) {B : ExtendedIndex δ} {a : Atom} : ⟨B, inl a⟩ ∈ designatedSupport t → LitterConstrains a.1 (fuzz hδε t) | fuzz_nearLitter ⦃δ : Λ⦄ [LtLevel δ] ⦃ε : Λ⦄ [LtLevel ε] (hδε : (δ : TypeIndex) ≠ ε) - (t : Tangle δ) {B : ExtendedIndex δ} {N : NearLitter} : ⟨B, inr N⟩ ∈ designatedSupport t → - LitterConstrains N.1 (fuzz hδε t) + (t : Tangle δ) {B : ExtendedIndex δ} {N : NearLitter} (h : ⟨B, inr N⟩ ∈ designatedSupport t) + {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) @@ -124,12 +125,11 @@ theorem hasPosition_lt_of_litterConstrains {L₁ L₂ : Litter} (h : LitterConst cases h₁ with | inl h => obtain ⟨δ, _, ε, _, hδε, t', ht', rfl⟩ := h - exact pos_lt_pos_of_atom_mem_designatedSupport t ht t' hδε ht' + exact pos_lt_pos_atom t ht t' hδε ht' | inr h => obtain ⟨ε, _, a, h, rfl⟩ := h - exact pos_lt_pos_of_atom_mem_designatedSupport t ht - (show Tangle ⊥ from a) bot_ne_coe h - | fuzz_nearLitter hδε t ht => + 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 @@ -142,11 +142,10 @@ theorem hasPosition_lt_of_litterConstrains {L₁ L₂ : Litter} (h : LitterConst cases h₁ with | inl h => obtain ⟨δ, _, ε, _, hδε, t', ht', rfl⟩ := h - exact pos_lt_pos_of_nearLitter_mem_designatedSupport t ht t' hδε ht' + exact pos_lt_pos_nearLitter t ht t' hδε ⟨_, ha, ht'⟩ | inr h => obtain ⟨ε, _, a, h, rfl⟩ := h - exact pos_lt_pos_of_nearLitter_mem_designatedSupport t ht - (show Tangle ⊥ from a) bot_ne_coe 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 => @@ -184,10 +183,6 @@ theorem litterConstrains_subrelation : theorem litterConstrains_wf : WellFounded LitterConstrains := Subrelation.wf litterConstrains_subrelation IsWellFounded.wf -/-- The `≺` relation is well-founded. -/ -theorem constrains_wf (β : Λ) : WellFounded ((· ≺ ·) : SupportCondition β → _ → Prop) := - sorry - @[simp] theorem constrains_atom {c : SupportCondition β} {A : ExtendedIndex β} {a : Atom} : c ≺ ⟨A, inl a⟩ ↔ c = ⟨A, inr a.1.toNearLitter⟩ := by @@ -197,6 +192,101 @@ theorem constrains_atom {c : SupportCondition β} {A : ExtendedIndex β} {a : At · rintro rfl exact Constrains.atom A a +theorem constrains_nearLitter {c : SupportCondition β} {A : ExtendedIndex β} + {N : NearLitter} (hN : ¬N.IsLitter) : + c ≺ ⟨A, inr N⟩ ↔ c = ⟨A, inr N.1.toNearLitter⟩ ∨ + ∃ a ∈ litterSet N.fst ∆ N.snd, c = ⟨A, inl a⟩ := by + constructor + · intro h + rw [Constrains_iff] at h + obtain ⟨A, a, rfl, hc⟩ | ⟨A, N, hN, rfl, hc⟩ | ⟨A, N, a, ha, rfl, hc⟩ | + ⟨γ, _, δ, _, ε, _, hδ, hε, hδε, A, t, c, _, rfl, hc'⟩ | + ⟨γ, _, ε, _, hγ, A, a, rfl, hc⟩ := h + · cases hc + · cases hc + exact Or.inl rfl + · cases hc + exact Or.inr ⟨a, ha, rfl⟩ + · cases hc' + cases hN (NearLitter.IsLitter.mk _) + · cases hc + cases hN (NearLitter.IsLitter.mk _) + · rintro (rfl | ⟨a, ha, rfl⟩) + · exact Constrains.nearLitter A N hN + · exact Constrains.symmDiff A N a ha + +theorem acc_atom {a : Atom} {A : ExtendedIndex β} + (h : Acc ((· ≺ ·) : SupportCondition β → _ → Prop) ⟨A, inr a.1.toNearLitter⟩) : + Acc ((· ≺ ·) : SupportCondition β → _ → 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 ((· ≺ ·) : SupportCondition β → _ → Prop) ⟨A, inr a.1.toNearLitter⟩) : + Acc ((· ≺ ·) : SupportCondition β → _ → 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 ((· ≺ ·) : SupportCondition β → _ → Prop) := by + have : ∀ L : Litter, ∀ A : ExtendedIndex β, + Acc ((· ≺ ·) : SupportCondition β → _ → 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 [SupportCondition.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 [SupportCondition.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 : SupportCondition γ} (h : c ≺ d) (B : Path (β : TypeIndex) γ) : ⟨B.comp c.path, c.value⟩ ≺ ⟨B.comp d.path, d.value⟩ := by diff --git a/ConNF/FOA/Basic/Hypotheses.lean b/ConNF/FOA/Basic/Hypotheses.lean index 8a622b1b8a..7677ccfbec 100644 --- a/ConNF/FOA/Basic/Hypotheses.lean +++ b/ConNF/FOA/Basic/Hypotheses.lean @@ -75,16 +75,16 @@ class FOAAssumptions extends FOAData where designatedSupport (ρ • t) = ρ • (designatedSupport t : Set (SupportCondition β)) /-- Inflexible litters whose atoms occur in designated supports have position less than the original tangle. -/ - pos_lt_pos_of_atom_mem_designatedSupport {β : Λ} [LtLevel β] (t : Tangle β) + pos_lt_pos_atom {β : Λ} [LtLevel β] (t : Tangle β) {A : ExtendedIndex β} {a : Atom} (ht : ⟨A, Sum.inl a⟩ ∈ designatedSupport t) {γ : TypeIndex} [LtLevel γ] (s : Tangle γ) {δ : Λ} [LtLevel δ] (hγδ : γ ≠ δ) (ha : a.1 = fuzz hγδ s) : pos s < pos t - /-- Inflexible litters with near-litters in designated supports have position less than the + /-- Inflexible litters touching near-litters in designated supports have position less than the original tangle. -/ - pos_lt_pos_of_nearLitter_mem_designatedSupport {β : Λ} [LtLevel β] (t : Tangle β) + pos_lt_pos_nearLitter {β : Λ} [LtLevel β] (t : Tangle β) {A : ExtendedIndex β} {N : NearLitter} (ht : ⟨A, Sum.inr N⟩ ∈ designatedSupport t) {γ : TypeIndex} [LtLevel γ] (s : Tangle γ) {δ : Λ} [LtLevel δ] (hγδ : γ ≠ δ) - (hN : N.1 = fuzz hγδ s) : pos s < pos t + (h : Set.Nonempty ((N : Set Atom) ∩ (fuzz hγδ s).toNearLitter)) : pos s < pos t /-- The `fuzz` map commutes with allowable permutations. -/ smul_fuzz {β : TypeIndex} [LeLevel β] {γ : TypeIndex} [LtLevel γ] {δ : Λ} [LtLevel δ] (hγ : γ < β) (hδ : (δ : TypeIndex) < β) (hγδ : γ ≠ δ) (ρ : Allowable β) (t : Tangle γ) : @@ -106,7 +106,7 @@ class FOAAssumptions extends FOAData where allowableCons hγ (allowableOfSmulFuzz β ρs h) = ρs γ hγ export FOAAssumptions (allowableCons allowableCons_eq designatedSupport_smul - pos_lt_pos_of_atom_mem_designatedSupport pos_lt_pos_of_nearLitter_mem_designatedSupport + pos_lt_pos_atom pos_lt_pos_nearLitter smul_fuzz allowableOfSmulFuzz allowableOfSmulFuzz_comp_eq) attribute [simp] designatedSupport_smul allowableOfSmulFuzz_comp_eq From 6fdbc396fed44f38c6164e9b8add0f8eae51f1d1 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Wed, 13 Dec 2023 15:59:48 +0000 Subject: [PATCH 5/5] New fuzz construction works Signed-off-by: zeramorphic --- ConNF/Fuzz/Construction.lean | 100 ++++++++++++----------------------- 1 file changed, 33 insertions(+), 67 deletions(-) diff --git a/ConNF/Fuzz/Construction.lean b/ConNF/Fuzz/Construction.lean index 38e24aa8bb..82c8437452 100644 --- a/ConNF/Fuzz/Construction.lean +++ b/ConNF/Fuzz/Construction.lean @@ -114,21 +114,13 @@ such that we could run out of available values for the function. variable [Params.{u}] {β : TypeIndex} {γ : Λ} [TangleData β] [PositionedTangles β] [TangleData γ] [PositionedTangles γ] [TypedObjects γ] (hβγ : β ≠ γ) --- TODO: Refactor to use near-litters directly instead of `IsNearLitter`. -/-- The requirements to be satisfied by the f-maps. -If `FuzzCondition` applied to a litter indexed by `ν` is true, -then `ν` is *not* a valid output to `fuzz _ t`. -/ -inductive FuzzCondition (t : Tangle β) (ν : μ) : Prop - | any (N : Set Atom) (hN : IsNearLitter ⟨ν, β, γ, hβγ⟩ N) : - pos (typedNearLitter ⟨⟨ν, β, γ, hβγ⟩, N, hN⟩ : Tangle γ) ≤ pos t → FuzzCondition t ν - | bot (a : Atom) : - β = ⊥ → -- this condition should only trigger for type `⊥` - HEq a t → -- using `HEq` instead of induction on `β` or the instance deals with some problems - pos (typedNearLitter (Litter.toNearLitter ⟨ν, ⊥, γ, bot_ne_coe⟩) : Tangle γ) ≤ pos a → - FuzzCondition t ν - 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 } ∪ + { ν : μ | ∃ (a : Atom), pos a ≤ pos t ∧ ν = a.1.1 } + theorem mk_invImage_lt (t : Tangle β) : #{ t' // t' < t } < #μ := by refine lt_of_le_of_lt ?_ (show #{ ν // ν < pos t } < #μ from card_Iio_lt _) refine ⟨⟨fun t' => ⟨_, t'.prop⟩, ?_⟩⟩ @@ -145,47 +137,27 @@ theorem mk_invImage_le (t : Tangle β) : #{ t' : Tangle γ // pos t' ≤ pos t } variable {γ} -theorem mk_fuzz_deny (hβγ : β ≠ γ) (t : Tangle β) : - #{ t' // t' < t } + #{ ν // FuzzCondition hβγ t ν } < #μ := by - have h₁ := mk_invImage_lt t - suffices h₂ : #{ ν // FuzzCondition hβγ t ν } < #μ - · exact add_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le h₁ h₂ - have : ∀ ν, FuzzCondition hβγ t ν → - (∃ (N : Set Atom) (hN : IsNearLitter ⟨ν, β, γ, hβγ⟩ N), - pos (typedNearLitter ⟨_, N, hN⟩ : Tangle γ) ≤ pos t) ∨ - (β = ⊥ ∧ ∃ a : Atom, HEq a t ∧ - pos (typedNearLitter (Litter.toNearLitter ⟨ν, β, γ, hβγ⟩) : Tangle γ) ≤ pos a) - · intro i hi - obtain ⟨N, hN₁, hN₂⟩ | ⟨a, h₁, h₂, h₃⟩ := hi - · left; exact ⟨N, hN₁, hN₂⟩ - · right; refine' ⟨h₁, a, h₂, _⟩; simp_rw [h₁]; exact h₃ - refine lt_of_le_of_lt (mk_subtype_mono this) ?_ +theorem mk_fuzzDeny (t : Tangle β) : + #{ 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 => ⟨_, i.prop.choose_spec.choose_spec⟩, ?_⟩⟩ - intro i j h - simp only [Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq] at h - apply_fun Sigma.fst at h - simp only [Litter.mk.injEq, Subtype.coe_inj, and_self, and_true] at h - exact h - · by_cases h : β = ⊥ ∧ ∃ a : Atom, HEq a t - · obtain ⟨_, a, hat⟩ := h - refine lt_of_le_of_lt ?_ (card_Iic_lt (pos a)) - refine ⟨⟨fun i => ⟨pos (typedNearLitter - (Litter.toNearLitter ⟨i, β, γ, hβγ⟩) : Tangle γ), ?_⟩, ?_⟩⟩ - · obtain ⟨ν, _, b, hb, _⟩ := i - rw [eq_of_heq (hat.trans hb.symm)] - assumption - · intro i j h - simp only [Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq, - Litter.toNearLitter_injective.eq_iff, - Litter.mk.injEq, Subtype.coe_inj, and_self, and_true] at h - exact h - · refine' lt_of_eq_of_lt _ (lt_of_lt_of_le aleph0_pos Params.μ_isStrongLimit.isLimit.aleph0_le) - rw [mk_eq_zero_iff, isEmpty_coe_sort, Set.eq_empty_iff_forall_not_mem] - rintro i ⟨hb, a, ha, _⟩ - exact h ⟨hb, a, ha⟩ + 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 : #{ 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⟩, ?_⟩⟩ + 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⟩ /-! We're done with proving technical results, now we can define the `fuzz` maps. @@ -209,7 +181,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 (FuzzCondition hβγ) (mk_fuzz_deny hβγ) t, β, γ, hβγ⟩ + ⟨chooseWf (fuzzDeny γ) mk_fuzzDeny t, β, γ, hβγ⟩ @[simp] theorem fuzz_β (t : Tangle β) : (fuzz hβγ t).β = β := @@ -247,27 +219,21 @@ 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).ν ∉ {ν | FuzzCondition hβγ t ν} := +theorem fuzz_not_mem_deny (t : Tangle β) : (fuzz hβγ t).ν ∉ fuzzDeny γ t := chooseWf_not_mem_deny t -theorem fuzz_pos' (t : Tangle β) (N : Set Atom) (h : IsNearLitter (fuzz hβγ t) N) : - pos t < pos (typedNearLitter ⟨fuzz hβγ t, N, h⟩ : Tangle γ) := by - have h' := fuzz_not_mem_deny hβγ t - contrapose! h' - -- Generalise the instances. - revert β - intro β - induction β using WithBot.recBotCoe <;> - · intros _ _ hβγ t h h' - exact FuzzCondition.any _ h h' - theorem fuzz_pos (t : Tangle β) (N : NearLitter) (h : N.1 = fuzz hβγ t) : pos t < pos (typedNearLitter N : Tangle γ) := by - have := fuzz_pos' hβγ t N ((NearLitter.isNearLitter _ _).mpr h) - exact lt_of_lt_of_eq this (congr_arg _ (congr_arg _ (NearLitter.ext rfl))) + 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) : pos t < pos a := by - sorry + have h' := fuzz_not_mem_deny hβγ t + contrapose! h' + refine Or.inr ⟨a, h', ?_⟩ + rw [ha] end ConNF