From cc3483496781b10b6acd2450117b443d03957dc4 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Thu, 4 Dec 2025 21:18:00 +0100 Subject: fix depth --- Algebra/Derivations.lean | 151 ++++++++++++++++++++++++++--------------------- 1 file changed, 83 insertions(+), 68 deletions(-) (limited to 'Algebra/Derivations.lean') diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean index c037925..142c49c 100644 --- a/Algebra/Derivations.lean +++ b/Algebra/Derivations.lean @@ -8,6 +8,7 @@ section Theories variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] variable (sig : Signature) +@[ext] structure Equation where vars : Type [vars_nominal : NominalSet 𝔸 vars] @@ -30,9 +31,6 @@ def HasDepth end Equation -def EquationAtDepth (n : ℕ) := - { eq : Equation 𝔸 sig // eq.HasDepth n } - def UniformEquation := { eq : Equation 𝔸 sig // ∃ n, eq.HasDepth n } @@ -47,58 +45,49 @@ variable {sig : Signature} section Helpers -def EquationAtDepth.left {n : ℕ} (eq : EquationAtDepth 𝔸 sig n) : TermAtDepth 𝔸 sig eq.val.vars n := - ⟨eq.val.left, eq.prop.left⟩ - -def EquationAtDepth.right {n : ℕ} (eq : EquationAtDepth 𝔸 sig n) : TermAtDepth 𝔸 sig eq.val.vars n := - ⟨eq.val.right, eq.prop.right⟩ - -def EquationAtDepth.mk +def UniformEquation.mk (X : Type) [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] {n : ℕ} (t u : TermAtDepth 𝔸 sig X n) : - EquationAtDepth 𝔸 sig n := - ⟨⟨X, t.val, u.val⟩, ⟨t.prop, u.prop⟩⟩ + UniformEquation 𝔸 sig := + ⟨⟨X, t.val, u.val⟩, ⟨n, t.prop, u.prop⟩⟩ -def EquationAtDepth.toUniform {n : ℕ} (eq : EquationAtDepth 𝔸 sig n) : UniformEquation 𝔸 sig := - ⟨eq.val, ⟨n, eq.prop⟩⟩ - -notation:50 X " ⊢ " lhs " ≣ " rhs => Equation.mk X lhs rhs +notation:50 X " ⊢ " lhs " ≣ " rhs => UniformEquation.mk X lhs rhs end Helpers section DerivableEquations -inductive Derivable (T : Theory 𝔸) : (eq : Equation 𝔸 T.sig) → Prop +inductive Derivable (T : Theory 𝔸) : (eq : UniformEquation 𝔸 T.sig) → Prop | refl {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] {x : X} : Derivable T (X ⊢ .var x ≣ .var x) | symm {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] - {t u : Term 𝔸 T.sig X} : + {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} : Derivable T (X ⊢ u ≣ t) → Derivable T (X ⊢ t ≣ u) | trans {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] - {t u v : Term 𝔸 T.sig X} : + {m : ℕ} {t u v : TermAtDepth 𝔸 T.sig X m} : Derivable T (X ⊢ t ≣ v) → Derivable T (X ⊢ v ≣ u) → Derivable T (X ⊢ t ≣ u) | cong_pure {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] - {f : T.sig.pure} {ts us : T.sig.pureArgs f → Term 𝔸 T.sig X} : + {f : T.sig.pure} {m : ℕ} {ts us : T.sig.pureArgs f → TermAtDepth 𝔸 T.sig X m} : (∀ x, Derivable T (X ⊢ ts x ≣ us x)) → Derivable T (X ⊢ .pure f ts ≣ .pure f us) | cong_free {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] - {a : 𝔸} {f : T.sig.free} {ts us : T.sig.freeArgs f → Term 𝔸 T.sig X} : + {a : 𝔸} {f : T.sig.free} {m : ℕ} {ts us : T.sig.freeArgs f → TermAtDepth 𝔸 T.sig X m} : (∀ x, Derivable T (X ⊢ ts x ≣ us x)) → Derivable T (X ⊢ .free a f ts ≣ .free a f us) | cong_bound {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] - {a : 𝔸} {f : T.sig.bound} {ts us : T.sig.boundArgs f → Term 𝔸 T.sig X} : + {a : 𝔸} {f : T.sig.bound} {m : ℕ} {ts us : T.sig.boundArgs f → TermAtDepth 𝔸 T.sig X m} : (∀ x, Derivable T (X ⊢ ts x ≣ us x)) → Derivable T (X ⊢ .bound a f ts ≣ .bound a f us) - | ax' {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] - {eq : UniformEquation 𝔸 T.sig} - {l : ℕ} {σ : UniformSubstitution 𝔸 T.sig eq.val.vars X l} {τ : FPerm 𝔸} : - (eq ∈ T.axioms) → - (∀ (y : eq.val.vars) (π : FPerm 𝔸), Derivable T (X ⊢ σ.toSubstitution (π • y) ≣ π • (σ.toSubstitution y))) → - Derivable T (X ⊢ σ.toSubstitution.apply (τ • eq.val.left) ≣ σ.toSubstitution.apply (τ • eq.val.right)) + | ax' {X Y : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] [NominalSet 𝔸 Y] [OrbitFinite 𝔸 Y] + {m : ℕ} {r s : TermAtDepth 𝔸 T.sig Y m} + {l : ℕ} {σ : UniformSubstitution 𝔸 T.sig Y X l} {τ : FPerm 𝔸} : + ((Y ⊢ r ≣ s) ∈ T.axioms) → + (∀ (y : Y) (π : FPerm 𝔸), Derivable T (X ⊢ σ (π • y) ≣ π • (σ y))) → + Derivable T (X ⊢ σ.apply (τ • r) ≣ σ.apply (τ • s)) | perm {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] - {a b : 𝔸} {f : T.sig.bound} {ts us : T.sig.boundArgs f → Term 𝔸 T.sig X} : + {a b : 𝔸} {f : T.sig.bound} {m : ℕ} {ts us : T.sig.boundArgs f → TermAtDepth 𝔸 T.sig X m} : a ≠ b → (∀ x, a # us x) → (∀ x, Derivable T (X ⊢ ts x ≣ ⸨a, b⸩ • us x)) → @@ -106,70 +95,100 @@ inductive Derivable (T : Theory 𝔸) : (eq : Equation 𝔸 T.sig) → Prop def DerivableEq (T : Theory 𝔸) (X : Type) [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] (n : ℕ) : Rel (TermAtDepth 𝔸 T.sig X n) (TermAtDepth 𝔸 T.sig X n) := - fun t u => Derivable T (X ⊢ t.val ≣ u.val) + fun t u => Derivable T (X ⊢ t ≣ u) variable {X Y : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] [NominalSet 𝔸 Y] [OrbitFinite 𝔸 Y] -def Substitution.DerivablyEquivariant - (T : Theory 𝔸) (σ : Substitution 𝔸 T.sig X Y) : Prop := +def UniformSubstitution.DerivablyEquivariant + (T : Theory 𝔸) {l : ℕ} (σ : UniformSubstitution 𝔸 T.sig X Y l) : Prop := (∀ (x : X) (π : FPerm 𝔸), Derivable T (Y ⊢ σ (π • x) ≣ π • σ x)) +variable {T : Theory 𝔸} {n : ℕ} + /-- Restated ax' rule using DerivablyEquivariant in the premiss. -/ lemma Derivable.ax - {T : Theory 𝔸} - {eq : UniformEquation 𝔸 T.sig} - {l : ℕ} {σ : UniformSubstitution 𝔸 T.sig eq.val.vars X l} {τ : FPerm 𝔸} : - (eq ∈ T.axioms) → - σ.toSubstitution.DerivablyEquivariant T → - Derivable T (X ⊢ σ.toSubstitution.apply (τ • eq.val.left) ≣ σ.toSubstitution.apply (τ • eq.val.right)) := - .ax' + {m : ℕ} {r s : TermAtDepth 𝔸 T.sig Y m} + {l : ℕ} {σ : UniformSubstitution 𝔸 T.sig Y X l} {τ : FPerm 𝔸} : + ((Y ⊢ r ≣ s) ∈ T.axioms) → + σ.DerivablyEquivariant T → + Derivable T (X ⊢ σ.apply (τ • r) ≣ σ.apply (τ • s)) := .ax' + +lemma Derivable.of_eq + {m : ℕ} {eq : UniformEquation 𝔸 T.sig} (t u : TermAtDepth 𝔸 T.sig eq.val.vars m) + (ht : t.val = eq.val.left := by rfl) + (hu : u.val = eq.val.right := by rfl) : + Derivable T (eq.val.vars ⊢ t ≣ u) → + Derivable T eq := by + intro hderiv + have heq : (eq.val.vars ⊢ t ≣ u) = eq := by + apply Subtype.eq; ext + · rfl + · rfl + · rw [heq_eq_eq]; exact ht + · rw [heq_eq_eq]; exact hu + rw [← heq]; exact hderiv lemma Derivable.equivariant_substitution - (T : Theory 𝔸) {l : ℕ} (σ : UniformSubstitution 𝔸 T.sig Y X l) : - σ.toSubstitution.DerivablyEquivariant T → - ∀ (t : Term 𝔸 T.sig Y) (π : FPerm 𝔸), - Derivable T (X ⊢ σ.toSubstitution.apply (π • t) ≣ π • (σ.toSubstitution.apply t)) := by - intro hequi t π - induction' t <;> expose_names - · exact hequi x π - · simp only [Term.smul_pure, Substitution.apply_pure] + σ.DerivablyEquivariant T → + ∀ {n : ℕ} (t : TermAtDepth 𝔸 T.sig Y n) (π : FPerm 𝔸), + Derivable T (X ⊢ σ.apply (π • t) ≣ π • (σ.apply t)) := by + intro hequi n t π + induction' t using TermAtDepth.induction <;> expose_names + · apply of_eq (σ (π • x)) (π • σ x) + exact hequi x π + · apply of_eq (.pure f (σ.apply ∘ (π • ·) ∘ args)) (.pure f ((π • ·) ∘ σ.apply ∘ args)) apply Derivable.cong_pure - exact args_ih - · simp only [Term.smul_free, Substitution.apply_free] + exact h + · apply of_eq (.free (π • a) f (σ.apply ∘ (π • ·) ∘ args)) (.free (π • a) f ((π • ·) ∘ σ.apply ∘ args)) apply Derivable.cong_free - exact args_ih - · simp only [Term.smul_bound, Substitution.apply_bound] + exact h + · apply of_eq (.bound (π • a) f (σ.apply ∘ (π • ·) ∘ args)) (.bound (π • a) f ((π • ·) ∘ σ.apply ∘ args)) apply Derivable.cong_bound - exact args_ih + exact h -lemma Derivable.equivariant - (T : Theory 𝔸) {t u : Term 𝔸 T.sig X} : +lemma Derivable.equivariant {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} : ∀ (π : FPerm 𝔸), Derivable T (X ⊢ t ≣ u) → Derivable T (X ⊢ π • t ≣ π • u) := by intro π - suffices ∀ eq, Derivable T eq → Derivable T (eq.vars ⊢ π • eq.left ≣ π • eq.right) by + let rename (π : FPerm 𝔸) (eq : UniformEquation 𝔸 T.sig) : UniformEquation 𝔸 T.sig := + ⟨⟨eq.val.vars, π • eq.val.left, π • eq.val.right⟩, by + obtain ⟨n, ⟨hn₁, hn₂⟩⟩ := eq.prop + let left : TermAtDepth 𝔸 T.sig eq.val.vars n := ⟨eq.val.left, hn₁⟩ + let right : TermAtDepth 𝔸 T.sig eq.val.vars n := ⟨eq.val.right, hn₂⟩ + use n; exact ⟨(π • left).prop, (π • right).prop⟩⟩ + have rename_eq + {Y : Type} [NominalSet 𝔸 Y] [OrbitFinite 𝔸 Y] {π : FPerm 𝔸} {k : ℕ} + {r s : TermAtDepth 𝔸 T.sig Y k} : rename π (Y ⊢ r ≣ s) = (Y ⊢ π • r ≣ π • s) := rfl + suffices ∀ eq, Derivable T eq → Derivable T (rename π eq) by exact this (X ⊢ t ≣ u) intro eq hderiv induction' hderiv <;> expose_names · exact .refl - · apply Derivable.symm + · rw [rename_eq] + apply Derivable.symm exact a_ih - · apply Derivable.trans + · rw [rename_eq] at * + apply Derivable.trans · exact a_ih · exact a_ih_1 - · apply Derivable.cong_pure + · apply of_eq (TermAtDepth.pure f ((π • ·) ∘ ts)) (TermAtDepth.pure f ((π • ·) ∘ us)) + apply Derivable.cong_pure exact a_ih - · apply Derivable.cong_free + · apply of_eq (TermAtDepth.free (π • a) f ((π • ·) ∘ ts)) (TermAtDepth.free (π • a) f ((π • ·) ∘ us)) + apply Derivable.cong_free exact a_ih - · apply Derivable.cong_bound + · apply of_eq (TermAtDepth.bound (π • a) f ((π • ·) ∘ ts)) (TermAtDepth.bound (π • a) f ((π • ·) ∘ us)) + apply Derivable.cong_bound exact a_ih - · apply Derivable.trans (by apply Derivable.symm; apply equivariant_substitution; exact h_1) _ + · rw [rename_eq] + apply Derivable.trans (by apply Derivable.symm; apply equivariant_substitution; exact h_1) _ apply Derivable.trans _ (by apply equivariant_substitution; exact h_1) rw [← MulAction.mul_smul, ← MulAction.mul_smul] apply Derivable.ax · exact h · exact h_1 - · apply Derivable.perm + · apply of_eq (TermAtDepth.bound (π • a) f ((π • ·) ∘ ts)) (TermAtDepth.bound (π • b) f ((π • ·) ∘ us)) + apply Derivable.perm · intro hcontra apply π.val.injective at hcontra contradiction @@ -182,17 +201,13 @@ lemma Derivable.equivariant rw [← MulAction.mul_smul, ← FPerm.mul_swap_eq_swap_mul, MulAction.mul_smul] exact a_ih x -variable {T : Theory 𝔸} {n : ℕ} - instance DerivableEq.instEquivariant : Rel.Equivariant 𝔸 (DerivableEq T X n) := by constructor; intro t u - exact Derivable.equivariant T + exact Derivable.equivariant @[refl] lemma DerivableEq.refl (t : TermAtDepth 𝔸 T.sig X n) : DerivableEq T X n t t := by - suffices ∀ t, Derivable T (X ⊢ t ≣ t) by exact this t.val - intro t - induction' t <;> expose_names + induction' t using TermAtDepth.induction <;> expose_names · apply Derivable.refl · apply Derivable.cong_pure; assumption · apply Derivable.cong_free; assumption -- cgit v1.3.1