diff options
Diffstat (limited to 'Algebra/Derivations.lean')
| -rw-r--r-- | Algebra/Derivations.lean | 237 |
1 files changed, 237 insertions, 0 deletions
diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean new file mode 100644 index 0000000..b6e5cb5 --- /dev/null +++ b/Algebra/Derivations.lean @@ -0,0 +1,237 @@ +import Mathlib +import Algebra.Terms + +namespace NominalAlgebra + +section Theories + +variable (πΈ : Type) [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] +variable (sig : Signature) + +@[ext] +structure Equation where + vars : Type + [vars_nominal : NominalSet πΈ vars] + left : Term πΈ sig vars + right : Term πΈ sig vars + +namespace Equation + +instance (eq : Equation πΈ sig) : NominalSet πΈ eq.vars := + eq.vars_nominal + +def HasDepth + {πΈ : Type} [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] {sig : Signature} + (eq : Equation πΈ sig) (n : β) : Prop := + eq.left.HasDepth n β§ eq.right.HasDepth n + +end Equation + +def UniformEquation := + { eq : Equation πΈ sig // β n, eq.HasDepth n } + +structure Theory where + sig : Signature + axioms : Set (UniformEquation πΈ sig) + axioms_orbitFinite : β eq β axioms, OrbitFinite πΈ eq.val.vars + +end Theories + +variable {πΈ : Type} [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] +variable {sig : Signature} + +section Helpers + +def UniformEquation.mk + (X : Type) [NominalSet πΈ X] {n : β} (t u : TermAtDepth πΈ sig X n) : + UniformEquation πΈ sig := + β¨β¨X, t.val, u.valβ©, β¨n, t.prop, u.propβ©β© + +notation:50 X " β’ " lhs " β£ " rhs => UniformEquation.mk X lhs rhs + +end Helpers + +section DerivableEquations + +inductive Derivable (T : Theory πΈ) : (eq : UniformEquation πΈ T.sig) β Prop + | refl {X : Type} [NominalSet πΈ X] {x : X} : + Derivable T (X β’ .var x β£ .var x) + | symm {X : Type} [NominalSet πΈ X] + {m : β} {t u : TermAtDepth πΈ T.sig X m} : + Derivable T (X β’ u β£ t) β + Derivable T (X β’ t β£ u) + | trans {X : Type} [NominalSet πΈ 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] + {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] + {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] + {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 Y : Type} [NominalSet πΈ X] [NominalSet πΈ 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] + {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)) β + Derivable T (X β’ .bound a f ts β£ .bound b f us) + +def DerivableEq (T : Theory πΈ) (X : Type) [NominalSet πΈ X] (n : β) : + Rel (TermAtDepth πΈ T.sig X n) (TermAtDepth πΈ T.sig X n) := + fun t u => Derivable T (X β’ t β£ u) + +variable {X Y : Type} [NominalSet πΈ X] [NominalSet πΈ Y] + +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 + {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.ext; ext + Β· rfl + Β· rfl + Β· exact heq_of_eq ht + Β· exact heq_of_eq hu + rw [β heq]; exact hderiv + +lemma Derivable.equivariant_substitution + {l : β} (Ο : UniformSubstitution πΈ T.sig Y X l) : + Ο.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 h + Β· apply of_eq (.free (Ο β’ a) f (Ο.apply β (Ο β’ Β·) β args)) (.free (Ο β’ a) f ((Ο β’ Β·) β Ο.apply β args)) + apply Derivable.cong_free + exact h + Β· apply of_eq (.bound (Ο β’ a) f (Ο.apply β (Ο β’ Β·) β args)) (.bound (Ο β’ a) f ((Ο β’ Β·) β Ο.apply β args)) + apply Derivable.cong_bound + exact h + +lemma Derivable.equivariant {m : β} {t u : TermAtDepth πΈ T.sig X m} : + β (Ο : FPerm πΈ), Derivable T (X β’ t β£ u) β Derivable T (X β’ Ο β’ t β£ Ο β’ u) := by + intro Ο + 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] {Ο : 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 + Β· rw [rename_eq] + apply Derivable.symm + exact a_ih + Β· rw [rename_eq] at * + apply Derivable.trans + Β· exact a_ih + Β· exact a_ih_1 + Β· apply of_eq (TermAtDepth.pure f ((Ο β’ Β·) β ts)) (TermAtDepth.pure f ((Ο β’ Β·) β us)) + apply Derivable.cong_pure + exact a_ih + Β· apply of_eq (TermAtDepth.free (Ο β’ a) f ((Ο β’ Β·) β ts)) (TermAtDepth.free (Ο β’ a) f ((Ο β’ Β·) β us)) + apply Derivable.cong_free + exact a_ih + Β· apply of_eq (TermAtDepth.bound (Ο β’ a) f ((Ο β’ Β·) β ts)) (TermAtDepth.bound (Ο β’ a) f ((Ο β’ Β·) β us)) + apply Derivable.cong_bound + exact a_ih + Β· 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 [β SemigroupAction.mul_smul, β SemigroupAction.mul_smul] + apply Derivable.ax + Β· exact h + Β· exact h_1 + Β· apply of_eq (TermAtDepth.bound (Ο β’ a) f ((Ο β’ Β·) β ts)) (TermAtDepth.bound (Ο β’ b) f ((Ο β’ Β·) β us)) + 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 [β SemigroupAction.mul_smul, β FPerm.mul_swap_eq_swap_mul, SemigroupAction.mul_smul] + exact a_ih x + +instance DerivableEq.instEquivariant : Rel.Equivariant πΈ (DerivableEq T X n) := by + constructor; intro t u + exact Derivable.equivariant + +@[refl] +lemma DerivableEq.refl (t : TermAtDepth πΈ T.sig X n) : DerivableEq T X n t t := by + induction' t using TermAtDepth.induction <;> 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 + +end NominalAlgebra |