From da3ddb5f61bb3dae9978770a26cf276c5265a1b8 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Thu, 4 Dec 2025 19:05:06 +0100 Subject: prove that derivable equality is an equivariant equivalence --- Algebra/Derivations.lean | 147 +++++++++++++++++++++++++++++++++++++---------- 1 file changed, 118 insertions(+), 29 deletions(-) (limited to 'Algebra/Derivations.lean') diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean index 6f81e9a..c037925 100644 --- a/Algebra/Derivations.lean +++ b/Algebra/Derivations.lean @@ -61,75 +61,164 @@ def EquationAtDepth.mk def EquationAtDepth.toUniform {n : β„•} (eq : EquationAtDepth 𝔸 sig n) : UniformEquation 𝔸 sig := ⟨eq.val, ⟨n, eq.prop⟩⟩ -notation:50 X " ⊒ " lhs " ≣ " rhs => EquationAtDepth.mk X lhs rhs +notation:50 X " ⊒ " lhs " ≣ " rhs => Equation.mk X lhs rhs end Helpers section DerivableEquations -inductive Derivable (T : Theory 𝔸) : {m : β„•} β†’ (eq : EquationAtDepth 𝔸 T.sig m) β†’ Prop +inductive Derivable (T : Theory 𝔸) : (eq : Equation 𝔸 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] - {m : β„•} {t u : TermAtDepth 𝔸 T.sig X m} : + {t u : Term 𝔸 T.sig X} : Derivable T (X ⊒ u ≣ t) β†’ Derivable T (X ⊒ t ≣ u) | trans {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] - {m : β„•} {t u v : TermAtDepth 𝔸 T.sig X m} : + {t u v : Term 𝔸 T.sig X} : 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} {m : β„•} {ts us : T.sig.pureArgs f β†’ TermAtDepth 𝔸 T.sig X m} : + {f : T.sig.pure} {ts us : T.sig.pureArgs f β†’ Term 𝔸 T.sig X} : (βˆ€ 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} {m : β„•} {ts us : T.sig.freeArgs f β†’ TermAtDepth 𝔸 T.sig X m} : + {a : 𝔸} {f : T.sig.free} {ts us : T.sig.freeArgs f β†’ Term 𝔸 T.sig X} : (βˆ€ 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} {m : β„•} {ts us : T.sig.boundArgs f β†’ TermAtDepth 𝔸 T.sig X m} : + {a : 𝔸} {f : T.sig.bound} {ts us : T.sig.boundArgs f β†’ Term 𝔸 T.sig X} : (βˆ€ x, Derivable T (X ⊒ ts x ≣ us x)) β†’ Derivable T (X ⊒ .bound a f ts ≣ .bound a f us) - | 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).toUniform ∈ T.axioms) β†’ - (βˆ€ (y : Y) (Ο€ : FPerm 𝔸), Derivable T (X ⊒ Οƒ (Ο€ β€’ y) ≣ Ο€ β€’ (Οƒ y))) β†’ - Derivable T (X ⊒ Οƒ.apply (Ο„ β€’ r) ≣ Οƒ.apply (Ο„ β€’ s)) + | 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)) | perm {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] - {a b : 𝔸} {f : T.sig.bound} {m : β„•} {ts us : T.sig.boundArgs f β†’ TermAtDepth 𝔸 T.sig X m} : + {a b : 𝔸} {f : T.sig.bound} {ts us : T.sig.boundArgs f β†’ Term 𝔸 T.sig X} : a β‰  b β†’ (βˆ€ x, a # us x) β†’ (βˆ€ x, Derivable T (X ⊒ ts x ≣ βΈ¨a, bβΈ© β€’ us x)) β†’ Derivable T (X ⊒ .bound a f ts ≣ .bound b f us) +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) + variable {X Y : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] [NominalSet 𝔸 Y] [OrbitFinite 𝔸 Y] -def UniformSubstitution.DerivablyEquivariant - (T : Theory 𝔸) {l : β„•} (Οƒ : UniformSubstitution 𝔸 T.sig X Y l) : Prop := +def Substitution.DerivablyEquivariant + (T : Theory 𝔸) (Οƒ : Substitution 𝔸 T.sig X Y) : Prop := (βˆ€ (x : X) (Ο€ : FPerm 𝔸), Derivable T (Y ⊒ Οƒ (Ο€ β€’ x) ≣ Ο€ β€’ Οƒ x)) /-- Restated ax' rule using DerivablyEquivariant in the premiss. -/ lemma Derivable.ax {T : Theory 𝔸} - {m : β„•} {r s : TermAtDepth 𝔸 T.sig Y m} - {l : β„•} {Οƒ : UniformSubstitution 𝔸 T.sig Y X l} {Ο„ : FPerm 𝔸} : - ((Y ⊒ r ≣ s).toUniform ∈ T.axioms) β†’ - Οƒ.DerivablyEquivariant T β†’ - Derivable T (X ⊒ Οƒ.apply (Ο„ β€’ r) ≣ Οƒ.apply (Ο„ β€’ s)) := + {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' lemma Derivable.equivariant_substitution (T : Theory 𝔸) - {l : β„•} (Οƒ : UniformSubstitution 𝔸 T.sig Y X l) (hequi : Οƒ.DerivablyEquivariant T) - {m : β„•} (t : TermAtDepth 𝔸 T.sig Y m) {Ο€ : FPerm 𝔸} : - Derivable T (X ⊒ Οƒ.apply (Ο€ β€’ t) ≣ Ο€ β€’ (Οƒ.apply t)) := by - induction' t using TermAtDepth.induction <;> expose_names - Β· sorry - Β· sorry - Β· sorry - Β· sorry + {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] + apply Derivable.cong_pure + exact args_ih + Β· simp only [Term.smul_free, Substitution.apply_free] + apply Derivable.cong_free + exact args_ih + Β· simp only [Term.smul_bound, Substitution.apply_bound] + apply Derivable.cong_bound + exact args_ih + +lemma Derivable.equivariant + (T : Theory 𝔸) {t u : Term 𝔸 T.sig X} : + βˆ€ (Ο€ : 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 + exact this (X ⊒ t ≣ u) + intro eq hderiv + induction' hderiv <;> expose_names + Β· exact .refl + Β· apply Derivable.symm + exact a_ih + Β· apply Derivable.trans + Β· exact a_ih + Β· exact a_ih_1 + Β· apply Derivable.cong_pure + exact a_ih + Β· apply Derivable.cong_free + exact a_ih + Β· apply Derivable.cong_bound + exact a_ih + Β· 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 + Β· intro hcontra + apply Ο€.val.injective at hcontra + contradiction + Β· intro x + show Ο€ β€’ a # Ο€ β€’ (us x) + rw [← Rel.equivariant 𝔸 NominalSet.IsFresh] + exact h_1 x + Β· intro x + show Derivable T (X_1 ⊒ Ο€ β€’ ts x ≣ βΈ¨Ο€ a, Ο€ bβΈ© β€’ Ο€ β€’ us x) + 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 + +@[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 + Β· apply Derivable.refl + Β· apply Derivable.cong_pure; assumption + Β· apply Derivable.cong_free; assumption + Β· apply Derivable.cong_bound; assumption + +@[symm] +lemma DerivableEq.symm {t u : TermAtDepth 𝔸 T.sig X n} : + DerivableEq T X n u t β†’ DerivableEq T X n t u := by + intro h + apply Derivable.symm + exact h + +@[trans] +lemma DerivableEq.trans {t u v : TermAtDepth 𝔸 T.sig X n} : + DerivableEq T X n t v β†’ DerivableEq T X n v u β†’ DerivableEq T X n t u := by + intro htv hvu + apply Derivable.trans + Β· exact htv + Β· exact hvu + +instance TermAtDepth.setoid : Setoid (TermAtDepth 𝔸 T.sig X n) where + r := DerivableEq T X n + iseqv := + { refl := DerivableEq.refl + symm := DerivableEq.symm + trans := DerivableEq.trans } end DerivableEquations -- cgit v1.3.1