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, 0 insertions, 628 deletions
diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean deleted file mode 100644 index b6e5cb5..0000000 --- a/Algebra/Derivations.lean +++ /dev/null @@ -1,237 +0,0 @@ -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 deleted file mode 100644 index 13b54a0..0000000 --- a/Algebra/Semantics.lean +++ /dev/null @@ -1,79 +0,0 @@ -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 deleted file mode 100644 index 568f5cb..0000000 --- a/Algebra/Terms.lean +++ /dev/null @@ -1,312 +0,0 @@ -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 |