diff options
Diffstat (limited to 'Algebra')
| -rw-r--r-- | Algebra/Derivations.lean | 237 | ||||
| -rw-r--r-- | Algebra/Semantics.lean | 79 | ||||
| -rw-r--r-- | Algebra/Terms.lean | 312 |
3 files changed, 628 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 diff --git a/Algebra/Semantics.lean b/Algebra/Semantics.lean new file mode 100644 index 0000000..13b54a0 --- /dev/null +++ b/Algebra/Semantics.lean @@ -0,0 +1,79 @@ +import Mathlib +import Algebra.Terms +import Algebra.Derivations + +open CategoryTheory + +namespace NominalAlgebra + +section AlgebraDefinition + +variable (πΈ : Type) [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] +variable (sig : Signature) + +structure Algebra where + carrier : β β Nom πΈ + pure (f : sig.pure) {m : β} : + (sig.pureArgs f β carrier m) ββ[πΈ] carrier (m + sig.pureDepth f) + free (f : sig.free) {m : β} : + (πΈ Γ (sig.freeArgs f β carrier m)) ββ[πΈ] carrier (m + sig.freeDepth f) + bound (f : sig.bound) {m : β} : + NameAbstraction πΈ (sig.boundArgs f β carrier m) ββ[πΈ] carrier (m + sig.boundDepth f) + +instance : CoeFun (Algebra πΈ sig) (fun _ => β β Nom πΈ) where + coe A := A.carrier + +@[ext] +structure Algebra.Hom (A B : Algebra πΈ sig) where + toFun : (n : β) β (A n ββ[πΈ] B n) + preserve_pure : β (f : sig.pure) {m : β} (args : sig.pureArgs f β A m), + toFun (m + sig.pureDepth f) (A.pure f args) = B.pure f (toFun m β args) + preserve_free : β (a : πΈ) (f : sig.free) {m : β} (args : sig.freeArgs f β A m), + toFun (m + sig.freeDepth f) (A.free f β¨a, argsβ©) = B.free f β¨a, toFun m β argsβ© + preserve_bound : β (a : πΈ) (f : sig.bound) {m : β} (args : sig.boundArgs f β A m), + toFun (m + sig.boundDepth f) (A.bound f (βͺaβ« args)) = B.bound f (βͺaβ« toFun m β args) + +instance {A B : Algebra πΈ sig} : CoeFun (Algebra.Hom πΈ sig A B) (fun _ => (n : β) β (A n ββ[πΈ] B n)) where + coe h := h.toFun + +end AlgebraDefinition + +section Algebra + +variable {πΈ : Type} [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] +variable {sig : Signature} + +namespace Algebra + +def Hom.id (A : Algebra πΈ sig) : Hom πΈ sig A A where + toFun _ := EquivariantMap.id πΈ + preserve_pure _ _ _ := rfl + preserve_free _ _ _ _ := rfl + preserve_bound _ _ _ _ := rfl + +def Hom.comp {A B C : Algebra πΈ sig} (h : Hom πΈ sig B C) (g : Hom πΈ sig A B) : Hom πΈ sig A C where + toFun n := EquivariantMap.comp πΈ (h n) (g n) + preserve_pure f m args := by + rw [EquivariantMap.comp_app, g.preserve_pure, h.preserve_pure] + rfl + preserve_free a f m args := by + rw [EquivariantMap.comp_app, g.preserve_free, h.preserve_free] + rfl + preserve_bound a f m args := by + rw [EquivariantMap.comp_app, g.preserve_bound, h.preserve_bound] + rfl + +instance : Category (Algebra πΈ sig) where + Hom := Hom πΈ sig + id := Hom.id + comp h g := Hom.comp g h + +def forgetfulFunctor : Algebra πΈ sig β₯€ Nom πΈ where + obj X := X 0 + map f := f.toFun 0 + +end Algebra + +end Algebra + +end NominalAlgebra diff --git a/Algebra/Terms.lean b/Algebra/Terms.lean new file mode 100644 index 0000000..568f5cb --- /dev/null +++ b/Algebra/Terms.lean @@ -0,0 +1,312 @@ +import Mathlib +import Nominal + +namespace NominalAlgebra + +section Definitions + +/-- A graded signature. -/ +structure Signature where + pure : Type + free : Type + bound : Type + /-- Type representing the arguments required for an operation. -/ + args : pure β free β bound β Type + args_fintype : β f, Fintype (args f) := by intro; infer_instance + /-- Depth of an operation. -/ + depth : pure β free β bound β β + +def Signature.pureArgs (sig : Signature) (f : sig.pure) : Type := sig.args (.inl f) +def Signature.freeArgs (sig : Signature) (f : sig.free) : Type := sig.args (.inr (.inl f)) +def Signature.boundArgs (sig : Signature) (f : sig.bound) : Type := sig.args (.inr (.inr f)) + +instance Signature.instPureArgsFintype (sig : Signature) (f : sig.pure) : Fintype (sig.pureArgs f) := sig.args_fintype (.inl f) +instance Signature.instFreeArgsFintype (sig : Signature) (f : sig.free) : Fintype (sig.freeArgs f) := sig.args_fintype (.inr (.inl f)) +instance Signature.instBoundArgsFintype (sig : Signature) (f : sig.bound) : Fintype (sig.boundArgs f) := sig.args_fintype (.inr (.inr f)) + +def Signature.arity (sig : Signature) (f : sig.pure β sig.free β sig.bound) : β := (sig.args_fintype f).card +def Signature.pureArity (sig : Signature) (f : sig.pure) : β := sig.arity (.inl f) +def Signature.freeArity (sig : Signature) (f : sig.free) : β := sig.arity (.inr (.inl f)) +def Signature.boundArity (sig : Signature) (f : sig.bound) : β := sig.arity (.inr (.inr f)) + +def Signature.pureDepth (sig : Signature) (f : sig.pure) : β := sig.depth (.inl f) +def Signature.freeDepth (sig : Signature) (f : sig.free) : β := sig.depth (.inr (.inl f)) +def Signature.boundDepth (sig : Signature) (f : sig.bound) : β := sig.depth (.inr (.inr f)) + +variable (πΈ : Type) [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] +variable (sig : Signature) + +inductive Term (X : Type) [NominalSet πΈ X] + | var (x : X) : Term X + | pure (f : sig.pure) (args : sig.pureArgs f β Term X) : Term X + | free (a : πΈ) (f : sig.free) (args : sig.freeArgs f β Term X) : Term X + | bound (a : πΈ) (f : sig.bound) (args : sig.boundArgs f β Term X) : Term X + +inductive Term.HasDepth + {πΈ : Type} [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] + {sig : Signature} + {X : Type} [NominalSet πΈ X] + : Term πΈ sig X β β β Prop + | var (x : X) : HasDepth (.var x) 0 + | pure (f : sig.pure) (args : sig.pureArgs f β Term πΈ sig X) (k : β) : + (β arg : sig.pureArgs f, HasDepth (args arg) k) β HasDepth (.pure f args) (k + sig.pureDepth f) + | free (a : πΈ) (f : sig.free) (args : sig.freeArgs f β Term πΈ sig X) (k : β) : + (β arg : sig.freeArgs f, HasDepth (args arg) k) β HasDepth (.free a f args) (k + sig.freeDepth f) + | bound (a : πΈ) (f : sig.bound) (args : sig.boundArgs f β Term πΈ sig X) (k : β) : + (β arg : sig.boundArgs f, HasDepth (args arg) k) β HasDepth (.bound a f args) (k + sig.boundDepth f) + +def TermAtDepth (X : Type) [NominalSet πΈ X] (n : β) := + { t : Term πΈ sig X // t.HasDepth n } + +def Substitution (X : Type) [NominalSet πΈ X] (Y : Type) [NominalSet πΈ Y] := + X β Term πΈ sig Y + +def UniformSubstitution (X : Type) [NominalSet πΈ X] (Y : Type) [NominalSet πΈ Y] (l : β) := + X β TermAtDepth πΈ sig Y l + +end Definitions + +variable {πΈ : Type} [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] +variable {sig : Signature} +variable {X : Type} [NominalSet πΈ X] +variable {Y : Type} [NominalSet πΈ Y] + +section ConvenienceConstructors + +def TermAtDepth.var (x : X) : TermAtDepth πΈ sig X 0 := β¨.var x, by constructorβ© + +def TermAtDepth.pure {n : β} (f : sig.pure) (args : sig.pureArgs f β TermAtDepth πΈ sig X n) : + TermAtDepth πΈ sig X (n + sig.pureDepth f) := + β¨.pure f (Subtype.val β args), by constructor; intro arg; exact (args arg).propβ© + +def TermAtDepth.free {n : β} (a : πΈ) (f : sig.free) (args : sig.freeArgs f β TermAtDepth πΈ sig X n) : + TermAtDepth πΈ sig X (n + sig.freeDepth f) := + β¨.free a f (Subtype.val β args), by constructor; intro arg; exact (args arg).propβ© + +def TermAtDepth.bound {n : β} (a : πΈ) (f : sig.bound) (args : sig.boundArgs f β TermAtDepth πΈ sig X n) : + TermAtDepth πΈ sig X (n + sig.boundDepth f) := + β¨.bound a f (Subtype.val β args), by constructor; intro arg; exact (args arg).propβ© + +theorem TermAtDepth.induction + {motive : {n : β} β TermAtDepth πΈ sig X n β Prop} + (var : β (x : X), motive (.var x)) + (pure : β {n : β} (f : sig.pure) (args : sig.pureArgs f β TermAtDepth πΈ sig X n), + (β x, motive (args x)) β motive (.pure f args)) + (free : β {n : β} (a : πΈ) (f : sig.free) (args : sig.freeArgs f β TermAtDepth πΈ sig X n), + (β x, motive (args x)) β motive (.free a f args)) + (bound : β {n : β} (a : πΈ) (f : sig.bound) (args : sig.boundArgs f β TermAtDepth πΈ sig X n), + (β x, motive (args x)) β motive (.bound a f args)) + : β {n : β} (t : TermAtDepth πΈ sig X n), motive t := by + intro n β¨t, htβ© + induction' t generalizing n <;> cases ht <;> expose_names + Β· exact var x + Β· let args' : sig.pureArgs f β TermAtDepth πΈ sig X k := fun x => β¨args x, h xβ© + have args_ih' : β x, motive (args' x) := fun x => args_ih x (h x) + exact pure f args' args_ih' + Β· let args' : sig.freeArgs f β TermAtDepth πΈ sig X k := fun x => β¨args x, h xβ© + have args_ih' : β x, motive (args' x) := fun x => args_ih x (h x) + exact free a f args' args_ih' + Β· let args' : sig.boundArgs f β TermAtDepth πΈ sig X k := fun x => β¨args x, h xβ© + have args_ih' : β x, motive (args' x) := fun x => args_ih x (h x) + exact bound a f args' args_ih' + +end ConvenienceConstructors + +section Substitution + +def Substitution.apply (Ο : Substitution πΈ sig X Y) : Term πΈ sig X β Term πΈ sig Y + | .var x => Ο x + | .pure f args => .pure f (fun x => Ο.apply (args x)) + | .free a f args => .free a f (fun x => Ο.apply (args x)) + | .bound a f args => .bound a f (fun x => Ο.apply (args x)) + +@[simp] lemma Substitution.apply_var {x : X} {Ο : Substitution πΈ sig X Y} : + Ο.apply (.var x) = (Ο x) := rfl + +@[simp] lemma Substitution.apply_pure + {f : sig.pure} {args : sig.pureArgs f β Term πΈ sig X} {Ο : Substitution πΈ sig X Y} : + Ο.apply (.pure f args) = .pure f (Ο.apply β args) := rfl + +@[simp] lemma Substitution.apply_free + {a : πΈ} {f : sig.free} {args : sig.freeArgs f β Term πΈ sig X} {Ο : Substitution πΈ sig X Y} : + Ο.apply (.free a f args) = .free a f (Ο.apply β args) := rfl + +@[simp] lemma Substitution.apply_bound + {a : πΈ} {f : sig.bound} {args : sig.boundArgs f β Term πΈ sig X} {Ο : Substitution πΈ sig X Y} : + Ο.apply (.bound a f args) = .bound a f (Ο.apply β args) := rfl + +def UniformSubstitution.toSubstitution {l : β} (Ο : UniformSubstitution πΈ sig X Y l) : Substitution πΈ sig X Y := + fun x => (Ο x).val + +def UniformSubstitution.apply {n l : β} (Ο : UniformSubstitution πΈ sig X Y l) (t : TermAtDepth πΈ sig X n) : + TermAtDepth πΈ sig Y (n + l) := + β¨Ο.toSubstitution.apply t.val, by + suffices β t n, t.HasDepth n β (Ο.toSubstitution.apply t).HasDepth (n + l) by + exact this t.val n t.prop + intro t; fun_induction Substitution.apply + Β· intro n h; cases h + rw [Nat.zero_add] + exact (Ο _).prop + all_goals + intro n h; cases h; expose_names + rw [Nat.add_right_comm] + constructor; intro arg + apply ih1; exact h argβ© + +@[simp] lemma UniformSubstitution.apply_var + {x : X} {l : β} {Ο : UniformSubstitution πΈ sig X Y l} : + (Ο.apply (.var x)).val = (Ο x).val := rfl + +@[simp] lemma UniformSubstitution.apply_pure + {n : β} {f : sig.pure} {args : sig.pureArgs f β TermAtDepth πΈ sig X n} + {l : β} {Ο : UniformSubstitution πΈ sig X Y l} : + (Ο.apply (.pure f args)).val = (TermAtDepth.pure f (Ο.apply β args)).val := rfl + +@[simp] lemma UniformSubstitution.apply_free + {n : β} {a : πΈ} {f : sig.free} {args : sig.freeArgs f β TermAtDepth πΈ sig X n} + {l : β} {Ο : UniformSubstitution πΈ sig X Y l} : + (Ο.apply (.free a f args)).val = (TermAtDepth.free a f (Ο.apply β args)).val := rfl + +@[simp] lemma UniformSubstitution.apply_bound + {n : β} {a : πΈ} {f : sig.bound} {args : sig.boundArgs f β TermAtDepth πΈ sig X n} + {l : β} {Ο : UniformSubstitution πΈ sig X Y l} : + (Ο.apply (.bound a f args)).val = (TermAtDepth.bound a f (Ο.apply β args)).val := rfl + +end Substitution + +section NominalSet + +namespace Term + +private def rename (Ο : FPerm πΈ) : Term πΈ sig X β Term πΈ sig X + | .var x => .var (Ο β’ x) + | .pure f args => .pure f (fun x => rename Ο (args x)) + | .free a f args => .free (Ο β’ a) f (fun x => rename Ο (args x)) + | .bound a f args => .bound (Ο β’ a) f (fun x => rename Ο (args x)) + +private lemma one_rename (t : Term πΈ sig X) : t.rename 1 = t := by + induction' t <;> all_goals simp [rename, *] + +private lemma mul_rename (Ο Ο : FPerm πΈ) (t : Term πΈ sig X) : + t.rename (Ο * Ο) = (t.rename Ο).rename Ο := by + induction' t <;> all_goals simp [rename, mul_smul, *] + +instance : PermSet πΈ (Term πΈ sig X) where + smul := rename + one_smul := one_rename + mul_smul := mul_rename + +@[simp] lemma smul_var {Ο : FPerm πΈ} {x : X} : + Ο β’ (.var x : Term πΈ sig X) = .var (Ο β’ x) := rfl + +@[simp] lemma smul_pure {Ο : FPerm πΈ} {f : sig.pure} {args : sig.pureArgs f β Term πΈ sig X} : + Ο β’ Term.pure f args = .pure f ((Ο β’ Β·) β args) := rfl + +@[simp] lemma smul_free {Ο : FPerm πΈ} {a : πΈ} {f : sig.free} {args : sig.freeArgs f β Term πΈ sig X} : + Ο β’ Term.free a f args = .free (Ο β’ a) f ((Ο β’ Β·) β args) := rfl + +@[simp] lemma smul_bound {Ο : FPerm πΈ} {a : πΈ} {f : sig.bound} {args : sig.boundArgs f β Term πΈ sig X} : + Ο β’ Term.bound a f args = .bound (Ο β’ a) f ((Ο β’ Β·) β args) := rfl + +private def atoms : Term πΈ sig X β Set πΈ + | .var x => NominalSet.supp πΈ x + | .pure f args => ββ {(args x).atoms | x : sig.pureArgs f} + | .free a f args => {a} βͺ ββ {(args x).atoms | x : sig.freeArgs f} + | .bound a f args => {a} βͺ ββ {(args x).atoms | x : sig.boundArgs f} + +private lemma atoms_finite (t : Term πΈ sig X) : t.atoms.Finite := by + fun_induction atoms <;> all_goals expose_names + Β· exact NominalSet.supp_finite πΈ + Β· apply Set.Finite.sUnion + Β· simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range] + apply Set.finite_range + Β· intro S β¨x, hSβ© + rw [β hS] + exact ih1 x + all_goals + apply Set.Finite.union + Β· exact Set.finite_singleton a + Β· apply Set.Finite.sUnion + Β· simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range] + apply Set.finite_range + Β· intro S β¨x, hSβ© + rw [β hS] + exact ih1 x + +private lemma atoms_support (t : Term πΈ sig X) : PermSet.HasSupport πΈ t t.atoms := by + intro Ο + fun_induction atoms <;> all_goals expose_names + Β· have hsupp : PermSet.HasSupport πΈ x (NominalSet.supp πΈ x) := NominalSet.supp_is_support πΈ + intro hΟ + simp only [PermSet.fix', smul_var, Term.var.injEq, Set.mem_setOf_eq] + exact hsupp hΟ + Β· intro hΟ + simp only [PermSet.fix', smul_pure, Term.pure.injEq, heq_eq_eq, true_and, Set.mem_setOf_eq] + ext x + rw [Function.comp_apply] + apply ih1 + apply PermSet.fix_antitone_mem πΈ hΟ + apply Set.subset_sUnion_of_mem + use x + all_goals + intro hΟ + simp only [PermSet.fix', smul_free, smul_bound, Term.free.injEq, Term.bound.injEq, heq_eq_eq, + true_and, Set.mem_setOf_eq] + constructor + Β· apply PermSet.fix_antitone_mem πΈ hΟ + apply Set.subset_union_left + rfl + Β· ext x + rw [Function.comp_apply] + apply ih1 + apply PermSet.fix_antitone_mem πΈ hΟ + apply Set.subset_union_of_subset_right + apply Set.subset_sUnion_of_mem + use x + +instance : NominalSet πΈ (Term πΈ sig X) where + fin_supp t := by + use t.atoms + exact β¨t.atoms_support, t.atoms_finiteβ© + +instance instHasDepthEquivariant {n : β} : + Set.Equivariant πΈ {t : Term πΈ sig X | t.HasDepth n} := by + constructor; intro t Ο ht + suffices β (t : Term πΈ sig X) n, t.HasDepth n β (t.rename Ο).HasDepth n by + exact this t n ht + intro t; fun_induction rename + Β· intro n h; cases h; constructor + all_goals + intro n h; cases h + expose_names + constructor; intro arg + apply ih1; exact h arg + +end Term + +namespace TermAtDepth + +instance {n : β} : NominalSet πΈ (TermAtDepth πΈ sig X n) := + (Subtype.instNominalSetElem πΈ : NominalSet πΈ {t : Term πΈ sig X | t.HasDepth n}) + +@[simp] lemma smul_var + {Ο : FPerm πΈ} {x : X} : + (Ο β’ (.var x : TermAtDepth πΈ sig X 0)).val = (TermAtDepth.var (Ο β’ x)).val := rfl + +@[simp] lemma smul_pure + {Ο : FPerm πΈ} {n : β} {f : sig.pure} {args : sig.pureArgs f β TermAtDepth πΈ sig X n} : + (Ο β’ TermAtDepth.pure f args).val = (TermAtDepth.pure f ((Ο β’ Β·) β args)).val := rfl + +@[simp] lemma smul_free + {Ο : FPerm πΈ} {n : β} {a : πΈ} {f : sig.free} {args : sig.freeArgs f β TermAtDepth πΈ sig X n} : + (Ο β’ TermAtDepth.free a f args).val = (TermAtDepth.free (Ο β’ a) f ((Ο β’ Β·) β args)).val := rfl + +@[simp] lemma smul_bound + {Ο : FPerm πΈ} {n : β} {a : πΈ} {f : sig.bound} {args : sig.boundArgs f β TermAtDepth πΈ sig X n} : + (Ο β’ TermAtDepth.bound a f args).val = (TermAtDepth.bound (Ο β’ a) f ((Ο β’ Β·) β args)).val := rfl + +end TermAtDepth + +end NominalSet + +end NominalAlgebra |