diff options
| -rw-r--r-- | Algebra.lean | 3 | ||||
| -rw-r--r-- | Algebra/Derivations.lean | 0 | ||||
| -rw-r--r-- | Algebra/Terms.lean (renamed from Algebra/Term.lean) | 140 |
3 files changed, 95 insertions, 48 deletions
diff --git a/Algebra.lean b/Algebra.lean index 73c5f4e..26109ba 100644 --- a/Algebra.lean +++ b/Algebra.lean @@ -1 +1,2 @@ -import Algebra.Term +import Algebra.Terms +import Algebra.Derivations diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/Algebra/Derivations.lean diff --git a/Algebra/Term.lean b/Algebra/Terms.lean index fe7e742..aa853a8 100644 --- a/Algebra/Term.lean +++ b/Algebra/Terms.lean @@ -3,7 +3,7 @@ import Nominal namespace Algebra -variable (πΈ : Type) [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] +section Definitions /-- A graded signature. -/ structure Signature where @@ -33,17 +33,20 @@ def Signature.pureDepth (sig : Signature) (f : sig.pure) : β := sig.depth (.in 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 {sig : Signature} -variable {X : Type} [NominalSet πΈ X] -variable {Y : Type} [NominalSet πΈ Y] +variable (πΈ : Type) [Infinite πΈ] [Countable πΈ] [DecidableEq πΈ] +variable (sig : Signature) -inductive Term (sig : Signature) (X : Type) [NominalSet πΈ X] - | var (x : X) : Term sig X - | pure (f : sig.pure) (args : sig.pureArgs f β Term sig X) : Term sig X - | free (a : πΈ) (f : sig.free) (args : sig.freeArgs f β Term sig X) : Term sig X - | bound (a : πΈ) (f : sig.bound) (args : sig.boundArgs f β Term sig X) : Term sig X +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 : Term πΈ sig X β β β Prop +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) @@ -52,8 +55,23 @@ inductive Term.HasDepth : Term πΈ sig X β β β Prop | 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 (sig : Signature) (X : Type) [NominalSet πΈ X] (n : β) := - { t : Term πΈ sig X // t.HasDepth πΈ n } +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β© @@ -69,8 +87,9 @@ def TermAtDepth.bound {n : β} (a : πΈ) (f : sig.bound) (args : sig.boundArgs TermAtDepth πΈ sig X (n + sig.boundDepth f) := β¨.bound a f (Subtype.val β args), by constructor; intro arg; exact (args arg).propβ© -def Substitution (sig : Signature) (X : Type) [NominalSet πΈ X] (Y : Type) [NominalSet πΈ Y] := - X β Term πΈ sig Y +end ConvenienceConstructors + +section Substitution def Substitution.apply (Ο : Substitution πΈ sig X Y) : Term πΈ sig X β Term πΈ sig Y | .var x => Ο x @@ -79,30 +98,27 @@ def Substitution.apply (Ο : Substitution πΈ sig X Y) : Term πΈ sig X β Te | .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 + Ο.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 + Ο.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 + Ο.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 (sig : Signature) (X : Type) [NominalSet πΈ X] (Y : Type) [NominalSet πΈ Y] (l : β) := - X β TermAtDepth πΈ sig Y l + Ο.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 + β¨Ο.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 @@ -116,22 +132,28 @@ def UniformSubstitution.apply {n l : β} (Ο : UniformSubstitution πΈ sig X Y @[simp] lemma UniformSubstitution.apply_var {x : X} {l : β} {Ο : UniformSubstitution πΈ sig X Y l} : - (Ο.apply πΈ (.var πΈ x)).val = (Ο x).val := rfl + (Ο.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 + (Ο.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 + (Ο.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 + (Ο.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) @@ -139,37 +161,37 @@ private def rename (Ο : FPerm πΈ) : Term πΈ sig X β Term πΈ sig 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) : rename πΈ 1 t = t := by +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) : - rename πΈ (Ο * Ο) t = rename πΈ Ο (rename πΈ Ο t) := by + 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 πΈ + smul := rename + one_smul := one_rename + mul_smul := mul_rename @[simp] lemma smul_var {Ο : FPerm πΈ} {x : X} : - Ο β’ (Term.var x : Term πΈ sig X) = Term.var (Ο β’ x) := rfl + Ο β’ (.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 = Term.pure f ((Ο β’ Β·) β args) := rfl + Ο β’ 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 = Term.free (Ο β’ a) f ((Ο β’ Β·) β args) := rfl + Ο β’ 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 = Term.bound (Ο β’ a) f ((Ο β’ Β·) β args) := rfl + Ο β’ 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 => ββ {atoms (args x) | x : sig.pureArgs f} - | .free a f args => {a} βͺ ββ {atoms (args x) | x : sig.freeArgs f} - | .bound a f args => {a} βͺ ββ {atoms (args x) | x : sig.boundArgs f} + | .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) : (atoms πΈ t).Finite := by +private lemma atoms_finite (t : Term πΈ sig X) : t.atoms.Finite := by fun_induction atoms <;> all_goals expose_names Β· exact NominalSet.supp_finite πΈ Β· have hfin := (sig.pureArgs_fintype f).finite @@ -198,7 +220,7 @@ private lemma atoms_finite (t : Term πΈ sig X) : (atoms πΈ t).Finite := by rw [β hS] exact ih1 x -private lemma atoms_support (t : Term πΈ sig X) : PermSet.HasSupport πΈ t (atoms πΈ t) := by +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 πΈ @@ -231,13 +253,13 @@ private lemma atoms_support (t : Term πΈ sig X) : PermSet.HasSupport πΈ t (a instance : NominalSet πΈ (Term πΈ sig X) where fin_supp t := by - use atoms πΈ t - exact β¨atoms_support πΈ t, atoms_finite πΈ tβ© + use t.atoms + exact β¨t.atoms_support, t.atoms_finiteβ© -instance Term.instHasDepthEquivariant {n : β} : - Set.Equivariant πΈ {t : Term πΈ sig X | HasDepth πΈ t n} := by +instance instHasDepthEquivariant {n : β} : + Set.Equivariant πΈ {t : Term πΈ sig X | t.HasDepth n} := by constructor; intro t Ο ht - suffices β t n, t.HasDepth πΈ n β (rename πΈ Ο t).HasDepth πΈ n by + 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 @@ -247,7 +269,31 @@ instance Term.instHasDepthEquivariant {n : β} : 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 | Term.HasDepth πΈ t 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 Algebra |