diff options
Diffstat (limited to 'Algebra/Derivations.lean')
| -rw-r--r-- | Algebra/Derivations.lean | 237 |
1 files changed, 0 insertions, 237 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 |