diff --git a/ConNF.lean b/ConNF.lean index 36327659e7..ee739ee1e9 100644 --- a/ConNF.lean +++ b/ConNF.lean @@ -8,9 +8,11 @@ import ConNF.Setup.Atom import ConNF.Setup.BasePerm import ConNF.Setup.Enumeration import ConNF.Setup.Litter +import ConNF.Setup.ModelData import ConNF.Setup.NearLitter import ConNF.Setup.Params import ConNF.Setup.Path +import ConNF.Setup.PathEnumeration import ConNF.Setup.Small import ConNF.Setup.StrPerm import ConNF.Setup.StrSet diff --git a/ConNF/Setup/Enumeration.lean b/ConNF/Setup/Enumeration.lean index b7f9f9ff07..dbbe34e9d0 100644 --- a/ConNF/Setup/Enumeration.lean +++ b/ConNF/Setup/Enumeration.lean @@ -1,5 +1,4 @@ import ConNF.Aux.Rel -import ConNF.Setup.Path import ConNF.Setup.Small /-! @@ -53,6 +52,12 @@ theorem graph'_small (E : Enumeration X) : Small E.rel.graph' := small_graph' E.dom_small E.coe_small +noncomputable def empty : Enumeration X where + bound := 0 + rel _ _ := False + lt_bound _ h := by cases h; contradiction + rel_coinjective := by constructor; intros; contradiction + noncomputable def singleton (x : X) : Enumeration X where bound := 1 rel i y := i = 0 ∧ y = x @@ -168,38 +173,6 @@ theorem mem_invImage {f : Y → X} {hf : f.Injective} (y : Y) : y ∈ E.invImage f hf ↔ f y ∈ E := Iff.rfl -/-! -## Enumerations over paths --/ - -instance (X : Type u) (α β : TypeIndex) : - Derivative (Enumeration (α ↝ ⊥ × X)) (Enumeration (β ↝ ⊥ × X)) α β where - deriv E A := E.invImage (λ x ↦ (x.1 ⇗ A, x.2)) - (λ x y h ↦ Prod.ext (Path.deriv_right_injective - ((Prod.mk.injEq _ _ _ _).mp h).1) ((Prod.mk.injEq _ _ _ _).mp h).2) - -instance (X : Type u) (α β : TypeIndex) : - Coderivative (Enumeration (β ↝ ⊥ × X)) (Enumeration (α ↝ ⊥ × X)) α β where - coderiv E A := E.image (λ x ↦ (x.1 ⇗ A, x.2)) - -instance (X : Type u) (α : TypeIndex) : - BotDerivative (Enumeration (α ↝ ⊥ × X)) (Enumeration X) α where - botDeriv E A := E.invImage (λ x ↦ (A, x)) (Prod.mk.inj_left A) - botSderiv E := E.invImage (λ x ↦ (Path.nil ↘., x)) (Prod.mk.inj_left (Path.nil ↘.)) - botDeriv_single E h := by - cases α using WithBot.recBotCoe with - | bot => cases lt_irrefl ⊥ h - | coe => rfl - -theorem ext_path {X : Type u} {α : TypeIndex} {E F : Enumeration (α ↝ ⊥ × X)} - (h : ∀ A, E ⇘. A = F ⇘. A) : - E = F := by - ext i x - · have := congr_arg bound (h (Path.nil ↘.)) - exact this - · have := congr_arg rel (h x.1) - exact iff_of_eq (congr_fun₂ this i x.2) - -- TODO: Some stuff about the partial order on enumerations and concatenation of enumerations. end Enumeration diff --git a/ConNF/Setup/Litter.lean b/ConNF/Setup/Litter.lean index 37a17efd16..86eeaca341 100644 --- a/ConNF/Setup/Litter.lean +++ b/ConNF/Setup/Litter.lean @@ -55,20 +55,28 @@ theorem card_litter : #Litter = #μ := by cases h rfl -/-- Typeclass for the `ᴸ` notation. -/ +/-- Typeclass for the `ᴸ` notation. Used for converting to litters, or extracting the +"litter part" of an object. -/ class SuperL (X : Type _) (Y : outParam <| Type _) where superL : X → Y -/-- Typeclass for the `ᴬ` notation. -/ +/-- Typeclass for the `ᴬ` notation. Used for converting to atoms, or extracting the +"atom part" of an object. -/ class SuperA (X : Type _) (Y : outParam <| Type _) where superA : X → Y -/-- Typeclass for the `ᴺ` notation. -/ +/-- Typeclass for the `ᴺ` notation. Used for converting to near-litters, or extracting the +"near-litter part" of an object. -/ class SuperN (X : Type _) (Y : outParam <| Type _) where superN : X → Y +/-- Typeclass for the `ᵁ` notation. Used for forgetful operations. -/ +class SuperU (X : Type _) (Y : outParam <| Type _) where + superU : X → Y + postfix:max "ᴸ" => SuperL.superL postfix:max "ᴬ" => SuperA.superA postfix:max "ᴺ" => SuperN.superN +postfix:max "ᵁ" => SuperU.superU end ConNF diff --git a/ConNF/Setup/ModelData.lean b/ConNF/Setup/ModelData.lean new file mode 100644 index 0000000000..67ed049d00 --- /dev/null +++ b/ConNF/Setup/ModelData.lean @@ -0,0 +1,116 @@ +import ConNF.Setup.StrSet +import ConNF.Setup.Support + +/-! +# Model data + +In this file, we define what model data at a type index means. + +## Main declarations + +* `ConNF.ModelData`: The type of model data at a given type index. +-/ + +universe u + +open Cardinal + +namespace ConNF + +variable [Params.{u}] + +/-- The same as `ModelData` but without the propositions. -/ +class PreModelData (α : TypeIndex) where + TSet : Type u + AllPerm : Type u + [allPermGroup : Group AllPerm] + [allAction : MulAction AllPerm TSet] + tSetForget : TSet → StrSet α + allPermForget : AllPerm → StrPerm α + +export PreModelData (TSet AllPerm) + +attribute [instance] PreModelData.allPermGroup PreModelData.allAction + +instance {α : TypeIndex} [PreModelData α] : SuperU (TSet α) (StrSet α) where + superU := PreModelData.tSetForget + +instance {α : TypeIndex} [PreModelData α] : SuperU (AllPerm α) (StrPerm α) where + superU := PreModelData.allPermForget + +structure Support.Supports {X : Type _} {α : TypeIndex} [PreModelData α] [MulAction (AllPerm α) X] + (S : Support α) (x : X) : Prop where + supports (ρ : AllPerm α) : ρᵁ • S = S → ρ • x = x + nearLitters_eq_empty_of_bot : α = ⊥ → Sᴺ = .empty + +class ModelData (α : TypeIndex) extends PreModelData α where + allPermForget_one : (1 : AllPerm)ᵁ = 1 + allPermForget_mul (ρ₁ ρ₂ : AllPerm) : (ρ₁ * ρ₂)ᵁ = ρ₁ᵁ * ρ₂ᵁ + smul_forget (ρ : AllPerm) (x : TSet) : (ρ • x)ᵁ = ρᵁ • xᵁ + exists_support (x : TSet) : ∃ S : Support α, S.Supports x + +@[ext] +structure Tangle (α : TypeIndex) [ModelData α] where + set : TSet α + support : Support α + support_supports : support.Supports set + +/-! +## Criteria for supports +-/ + +theorem Support.supports_coe {α : Λ} {X : Type _} [PreModelData α] [MulAction (AllPerm α) X] + (S : Support α) (x : X) + (h : ∀ ρ : AllPerm α, + (∀ A : α ↝ ⊥, ∀ a ∈ (S ⇘. A)ᴬ, ρᵁ A • a = a) → + (∀ A : α ↝ ⊥, ∀ N ∈ (S ⇘. A)ᴺ, ρᵁ A • N = N) → ρ • x = x) : + S.Supports x := by + constructor + · intro ρ h' + apply h + · intro A a ha + exact Enumeration.smul_eq_of_mem_of_smul_eq (smul_atoms_eq_of_smul_eq h') A a ha + · intro A N hN + exact Enumeration.smul_eq_of_mem_of_smul_eq (smul_nearLitters_eq_of_smul_eq h') A N hN + · intro h + cases h + +theorem Support.supports_bot {X : Type _} [PreModelData ⊥] [MulAction (AllPerm ⊥) X] + (E : Enumeration (⊥ ↝ ⊥ × Atom)) (x : X) + (h : ∀ ρ : AllPerm ⊥, (∀ A : ⊥ ↝ ⊥, ∀ x : Atom, (A, x) ∈ E → ρᵁ A • x = x) → ρ • x = x) : + (⟨E, .empty⟩ : Support ⊥).Supports x := by + constructor + · intro ρ h' + apply h + intro A x hx + exact Enumeration.smul_eq_of_mem_of_smul_eq (smul_atoms_eq_of_smul_eq h') A x hx + · intro + rfl + +/-! +## Model data at level `⊥` +-/ + +def botPreModelData : PreModelData ⊥ where + TSet := Atom + AllPerm := BasePerm + tSetForget := StrSet.botEquiv.symm + allPermForget ρ _ := ρ + +def botModelData : ModelData ⊥ where + allPermForget_one := rfl + allPermForget_mul _ _ := rfl + smul_forget ρ x := by + apply StrSet.botEquiv.injective + have : ∀ x : TSet ⊥, xᵁ = StrSet.botEquiv.symm x := λ _ ↦ rfl + simp only [this, Equiv.apply_symm_apply, StrSet.strPerm_smul_bot] + rfl + exists_support x := by + use ⟨.singleton (Path.nil, x), .empty⟩ + apply Support.supports_bot + intro ρ hc + apply hc Path.nil x + rw [Enumeration.mem_singleton_iff] + __ := botPreModelData + +end ConNF diff --git a/ConNF/Setup/PathEnumeration.lean b/ConNF/Setup/PathEnumeration.lean new file mode 100644 index 0000000000..2ad9a42336 --- /dev/null +++ b/ConNF/Setup/PathEnumeration.lean @@ -0,0 +1,123 @@ +import ConNF.Setup.Enumeration +import ConNF.Setup.StrPerm + +/-! +# Enumerations over paths + +In this file, we provide extra features to `Enumeration`s that take values of the form `α ↝ ⊥ × X`. + +## Main declarations + +* `ConNF.ext_path`: An extensionality principle for such `Enumeration`s. +-/ + +noncomputable section +universe u + +open Cardinal Ordinal + +namespace ConNF + +variable [Params.{u}] + +namespace Enumeration + +instance (X : Type u) (α β : TypeIndex) : + Derivative (Enumeration (α ↝ ⊥ × X)) (Enumeration (β ↝ ⊥ × X)) α β where + deriv E A := E.invImage (λ x ↦ (x.1 ⇗ A, x.2)) + (λ x y h ↦ Prod.ext (Path.deriv_right_injective + ((Prod.mk.injEq _ _ _ _).mp h).1) ((Prod.mk.injEq _ _ _ _).mp h).2) + +@[simp] +theorem deriv_rel {X : Type _} {α β : TypeIndex} (E : Enumeration (α ↝ ⊥ × X)) (A : α ↝ β) + (i : κ) (x : β ↝ ⊥ × X) : + (E ⇘ A).rel i x ↔ E.rel i (x.1 ⇗ A, x.2) := + Iff.rfl + +instance (X : Type u) (α β : TypeIndex) : + Coderivative (Enumeration (β ↝ ⊥ × X)) (Enumeration (α ↝ ⊥ × X)) α β where + coderiv E A := E.image (λ x ↦ (x.1 ⇗ A, x.2)) + +instance (X : Type u) (α : TypeIndex) : + BotDerivative (Enumeration (α ↝ ⊥ × X)) (Enumeration X) α where + botDeriv E A := E.invImage (λ x ↦ (A, x)) (Prod.mk.inj_left A) + botSderiv E := E.invImage (λ x ↦ (Path.nil ↘., x)) (Prod.mk.inj_left (Path.nil ↘.)) + botDeriv_single E h := by + cases α using WithBot.recBotCoe with + | bot => cases lt_irrefl ⊥ h + | coe => rfl + +theorem ext_path {X : Type u} {α : TypeIndex} {E F : Enumeration (α ↝ ⊥ × X)} + (h : ∀ A, E ⇘. A = F ⇘. A) : + E = F := by + ext i x + · have := congr_arg bound (h (Path.nil ↘.)) + exact this + · have := congr_arg rel (h x.1) + exact iff_of_eq (congr_fun₂ this i x.2) + +theorem mulAction_aux {X : Type _} {α : TypeIndex} [MulAction BasePerm X] (π : StrPerm α) : + Function.Injective (λ x : α ↝ ⊥ × X ↦ (x.1, (π x.1)⁻¹ • x.2)) := by + rintro ⟨A₁, x₁⟩ ⟨A₂, x₂⟩ h + rw [Prod.mk.injEq] at h + cases h.1 + exact Prod.ext h.1 (smul_left_cancel _ h.2) + +instance {X : Type _} {α : TypeIndex} [MulAction BasePerm X] : + SMul (StrPerm α) (Enumeration (α ↝ ⊥ × X)) where + smul π E := E.invImage (λ x ↦ (x.1, (π x.1)⁻¹ • x.2)) (mulAction_aux π) + +@[simp] +theorem smul_rel {X : Type _} {α : TypeIndex} [MulAction BasePerm X] + (π : StrPerm α) (E : Enumeration (α ↝ ⊥ × X)) (i : κ) (x : α ↝ ⊥ × X) : + (π • E).rel i x ↔ E.rel i (x.1, (π x.1)⁻¹ • x.2) := + Iff.rfl + +instance {X : Type _} {α : TypeIndex} [MulAction BasePerm X] : + MulAction (StrPerm α) (Enumeration (α ↝ ⊥ × X)) where + one_smul E := by + ext i x + · rfl + · rw [smul_rel, Tree.one_apply, inv_one, one_smul] + mul_smul π₁ π₂ E := by + ext i x + · rfl + · rw [smul_rel, smul_rel, smul_rel, Tree.mul_apply, mul_inv_rev, mul_smul] + +theorem smul_eq_of_forall_smul_eq {X : Type _} {α : TypeIndex} [MulAction BasePerm X] + {π : StrPerm α} {E : Enumeration (α ↝ ⊥ × X)} + (h : ∀ A : α ↝ ⊥, ∀ x : X, (A, x) ∈ E → π A • x = x) : + π • E = E := by + ext i x + · rfl + · obtain ⟨A, x⟩ := x + constructor + · intro hx + have := h A ((π A)⁻¹ • x) ⟨i, hx⟩ + rw [smul_inv_smul] at this + rw [this] + exact hx + · intro hx + have := h A x ⟨i, hx⟩ + rw [← this] + rwa [smul_rel, inv_smul_smul] + +theorem smul_eq_of_mem_of_smul_eq {X : Type _} {α : TypeIndex} [MulAction BasePerm X] + {π : StrPerm α} {E : Enumeration (α ↝ ⊥ × X)} + (h : π • E = E) (A : α ↝ ⊥) (x : X) (hx : (A, x) ∈ E) : + π A • x = x := by + obtain ⟨i, hx⟩ := hx + have := congr_fun₂ (congr_arg rel h) i (A, x) + simp only [smul_rel, eq_iff_iff] at this + have := E.rel_coinjective.coinjective hx (this.mpr hx) + rw [Prod.mk.injEq, eq_inv_smul_iff] at this + exact this.2 + +theorem smul_eq_iff {X : Type _} {α : TypeIndex} [MulAction BasePerm X] + (π : StrPerm α) (E : Enumeration (α ↝ ⊥ × X)) : + π • E = E ↔ ∀ A : α ↝ ⊥, ∀ x : X, (A, x) ∈ E → π A • x = x := + ⟨smul_eq_of_mem_of_smul_eq, smul_eq_of_forall_smul_eq⟩ + +end Enumeration + +end ConNF diff --git a/ConNF/Setup/Support.lean b/ConNF/Setup/Support.lean index 30449d026b..515c1dbf13 100644 --- a/ConNF/Setup/Support.lean +++ b/ConNF/Setup/Support.lean @@ -1,5 +1,4 @@ -import ConNF.Setup.StrPerm -import ConNF.Setup.Enumeration +import ConNF.Setup.PathEnumeration /-! # Supports @@ -82,6 +81,16 @@ instance : SuperA (Support α) (Enumeration (α ↝ ⊥ × Atom)) where instance : SuperN (Support α) (Enumeration (α ↝ ⊥ × NearLitter)) where superN := nearLitters +@[simp] +theorem mk_atoms (E : Enumeration (α ↝ ⊥ × Atom)) (F : Enumeration (α ↝ ⊥ × NearLitter)) : + (⟨E, F⟩ : Support α)ᴬ = E := + rfl + +@[simp] +theorem mk_nearLitters (E : Enumeration (α ↝ ⊥ × Atom)) (F : Enumeration (α ↝ ⊥ × NearLitter)) : + (⟨E, F⟩ : Support α)ᴺ = F := + rfl + instance : Derivative (Support α) (Support β) α β where deriv S A := ⟨Sᴬ ⇘ A, Sᴺ ⇘ A⟩ @@ -93,6 +102,13 @@ instance : BotDerivative (Support α) BaseSupport α where botSderiv S := ⟨Sᴬ ↘., Sᴺ ↘.⟩ botDeriv_single S h := by dsimp only; rw [botDeriv_single, botDeriv_single] +theorem ext' {S T : Support α} (h₁ : Sᴬ = Tᴬ) (h₂ : Sᴺ = Tᴺ) : S = T := by + obtain ⟨SA, SN⟩ := S + obtain ⟨TA, TN⟩ := T + cases h₁ + cases h₂ + rfl + @[ext] theorem ext {S T : Support α} (h : ∀ A, S ⇘. A = T ⇘. A) : S = T := by obtain ⟨SA, SN⟩ := S @@ -106,6 +122,41 @@ theorem ext {S T : Support α} (h : ∀ A, S ⇘. A = T ⇘. A) : S = T := by intro A exact BaseSupport.nearLitters_congr (h A) +instance {α : TypeIndex} : SMul (StrPerm α) (Support α) where + smul π S := ⟨π • Sᴬ, π • Sᴺ⟩ + +@[simp] +theorem smul_atoms {α : TypeIndex} (π : StrPerm α) (S : Support α) : + (π • S)ᴬ = π • Sᴬ := + rfl + +@[simp] +theorem smul_nearLitters {α : TypeIndex} (π : StrPerm α) (S : Support α) : + (π • S)ᴺ = π • Sᴺ := + rfl + +@[simp] +theorem smul_atoms_eq_of_smul_eq {α : TypeIndex} {π : StrPerm α} {S : Support α} + (h : π • S = S) : + π • Sᴬ = Sᴬ := by + rw [← smul_atoms, h] + +@[simp] +theorem smul_nearLitters_eq_of_smul_eq {α : TypeIndex} {π : StrPerm α} {S : Support α} + (h : π • S = S) : + π • Sᴺ = Sᴺ := by + rw [← smul_nearLitters, h] + +instance {α : TypeIndex} : MulAction (StrPerm α) (Support α) where + one_smul S := by + apply ext' + · rw [smul_atoms, one_smul] + · rw [smul_nearLitters, one_smul] + mul_smul π₁ π₂ S := by + apply ext' + · rw [smul_atoms, smul_atoms, smul_atoms, mul_smul] + · rw [smul_nearLitters, smul_nearLitters, smul_nearLitters, mul_smul] + end Support def supportEquiv {α : TypeIndex} : Support α ≃ diff --git a/blueprint/src/chapters/environment.tex b/blueprint/src/chapters/environment.tex index c485034a4a..ad71dbe1c4 100644 --- a/blueprint/src/chapters/environment.tex +++ b/blueprint/src/chapters/environment.tex @@ -212,6 +212,7 @@ \section{The structural hierarchy} \label{def:Enumeration} \uses{def:Small} \lean{ConNF.Enumeration} + \leanok Let \( \tau \) be a type. An \emph{enumeration} of \( \tau \) is a pair \( E = (i, f) \) where \( i : \kappa \) and \( f \) is a partial function \( \kappa \to \tau \), such that all domain elements of \( f \) are strictly less than \( i \).\footnote{This should be encoded as a coinjective relation \( \kappa \to \tau \to \Prop \); see \cref{def:relation_props}.} If \( x : \tau \), we write \( x \in E \) for \( x \in \ran f \). @@ -342,6 +343,8 @@ \section{Hypotheses of the recursion} \begin{definition}[model data] \label{def:ModelData} \uses{def:StrSupport,def:StrSet} + \lean{ConNF.ModelData} + \leanok Let \( \alpha \) be a type index. \emph{Model data} at type \( \alpha \) consists of:\footnote{A type theory problem with \texttt{export}ing this data is that under different assumptions, things like different spellings of \( \TSet_\alpha \) might require case splitting on \( \alpha \) before they become defeq (e.g.\ see the old version of \texttt{Model/FOA.lean}). There doesn't seem to be an easy way around this.} \begin{itemize} @@ -351,12 +354,14 @@ \section{Hypotheses of the recursion} such that \begin{itemize} \item if \( \rho : \AllPerm_\alpha \) and \( x : \TSet_\alpha \), then \( \rho(U_\alpha(x)) = U_\alpha(\rho(x)) \); - \item every t-set of type \( \alpha \) has an \( \alpha \)-support (\cref{def:StrSupport}) for its action under the \( \alpha \)-allowable permutations; + \item every t-set of type \( \alpha \) has an \( \alpha \)-support (\cref{def:StrSupport}) for its action under the \( \alpha \)-allowable permutations. \end{itemize} \end{definition} \begin{definition}[tangle] \label{def:Tangle} \uses{def:ModelData} + \lean{ConNF.Tangle} + \leanok Let \( \alpha \) be a type index with model data. An \emph{\( \alpha \)-tangle} is a pair \( t = (x, S) \) where \( x \) is a tangled set of type \( \alpha \) and \( S \) is an \( \alpha \)-support for \( x \). We define \( \set(t) = x \) and \( \supp(t) = S \). @@ -366,7 +371,7 @@ \section{Hypotheses of the recursion} \end{definition} \begin{proposition}[fuzz maps] \label{prop:fuzz} - \uses{def:Tangle} + \uses{def:Tangle,def:Position} Let \( \beta \) be a type index with model data, and suppose that \( \Tang_\beta \) has a position function. Let \( \gamma \) be any proper type index not equal to \( \beta \). Then there is an injective \emph{fuzz map} \( f_{\beta,\gamma} : \Tang_\beta \to \Litter \) such that \( \iota(t) < \iota(f_{\beta,\gamma}(t)) \), and the different \( f_{\beta,\gamma} \) all have disjoint ranges.