implement derivable equality

4 files changed, 191 insertions, 0 deletions

diff --git a/Algebra/Derivations.lean b/Algebra/Derivations.lean
index e69de29..6f81e9a 100644
--- a/Algebra/Derivations.lean
+++ b/Algebra/Derivations.lean
@@ -0,0 +1,136 @@
+import Mathlib
+import Algebra.Terms
+
+namespace Algebra
+
+section Theories
+
+variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable (sig : Signature)
+
+structure Equation where
+  vars : Type
+  [vars_nominal : NominalSet 𝔸 vars]
+  [vars_orbitFinite : OrbitFinite 𝔸 vars]
+  left : Term 𝔸 sig vars
+  right : Term 𝔸 sig vars
+
+namespace Equation
+
+instance (eq : Equation 𝔸 sig) : NominalSet 𝔸 eq.vars :=
+  eq.vars_nominal
+
+instance (eq : Equation 𝔸 sig) : OrbitFinite 𝔸 eq.vars :=
+  eq.vars_orbitFinite
+
+def HasDepth
+    {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {sig : Signature}
+    (eq : Equation 𝔸 sig) (n : ℕ) : Prop :=
+  eq.left.HasDepth n ∧ eq.right.HasDepth n
+
+end Equation
+
+def EquationAtDepth (n : ℕ) :=
+  { eq : Equation 𝔸 sig // eq.HasDepth n }
+
+def UniformEquation :=
+  { eq : Equation 𝔸 sig // ∃ n, eq.HasDepth n }
+
+structure Theory where
+  sig : Signature
+  axioms : Set (UniformEquation 𝔸 sig)
+
+end Theories
+
+variable {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
+variable {sig : Signature}
+
+section Helpers
+
+def EquationAtDepth.left {n : ℕ} (eq : EquationAtDepth 𝔸 sig n) : TermAtDepth 𝔸 sig eq.val.vars n :=
+  ⟨eq.val.left, eq.prop.left⟩
+
+def EquationAtDepth.right {n : ℕ} (eq : EquationAtDepth 𝔸 sig n) : TermAtDepth 𝔸 sig eq.val.vars n :=
+  ⟨eq.val.right, eq.prop.right⟩
+
+def EquationAtDepth.mk
+    (X : Type) [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] {n : ℕ} (t u : TermAtDepth 𝔸 sig X n) :
+    EquationAtDepth 𝔸 sig n :=
+  ⟨⟨X, t.val, u.val⟩, ⟨t.prop, u.prop⟩⟩
+
+def EquationAtDepth.toUniform {n : ℕ} (eq : EquationAtDepth 𝔸 sig n) : UniformEquation 𝔸 sig :=
+  ⟨eq.val, ⟨n, eq.prop⟩⟩
+
+notation:50 X " ⊢ " lhs " ≣ " rhs => EquationAtDepth.mk X lhs rhs
+
+end Helpers
+
+section DerivableEquations
+
+inductive Derivable (T : Theory 𝔸) : {m : ℕ} → (eq : EquationAtDepth 𝔸 T.sig m) → Prop
+  | refl {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] {x : X} :
+      Derivable T (X ⊢ .var x ≣ .var x)
+  | symm {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X]
+      {m : ℕ} {t u : TermAtDepth 𝔸 T.sig X m} :
+      Derivable T (X ⊢ u ≣ t) →
+      Derivable T (X ⊢ t ≣ u)
+  | trans {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 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] [OrbitFinite 𝔸 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] [OrbitFinite 𝔸 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] [OrbitFinite 𝔸 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] [OrbitFinite 𝔸 X] [NominalSet 𝔸 Y] [OrbitFinite 𝔸 Y]
+      {m : ℕ} {r s : TermAtDepth 𝔸 T.sig Y m}
+      {l : ℕ} {σ : UniformSubstitution 𝔸 T.sig Y X l} {τ : FPerm 𝔸} :
+      ((Y ⊢ r ≣ s).toUniform ∈ T.axioms) →
+      (∀ (y : Y) (π : FPerm 𝔸), Derivable T (X ⊢ σ (π • y) ≣ π • (σ y))) →
+      Derivable T (X ⊢ σ.apply (τ • r) ≣ σ.apply (τ • s))
+  | perm {X : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 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)
+
+variable {X Y : Type} [NominalSet 𝔸 X] [OrbitFinite 𝔸 X] [NominalSet 𝔸 Y] [OrbitFinite 𝔸 Y]
+
+def UniformSubstitution.DerivablyEquivariant
+    (T : Theory 𝔸) {l : ℕ} (σ : UniformSubstitution 𝔸 T.sig X Y l) : Prop :=
+  (∀ (x : X) (π : FPerm 𝔸), Derivable T (Y ⊢ σ (π • x) ≣ π • σ x))
+
+/-- Restated ax' rule using DerivablyEquivariant in the premiss. -/
+lemma Derivable.ax
+    {T : Theory 𝔸}
+    {m : ℕ} {r s : TermAtDepth 𝔸 T.sig Y m}
+    {l : ℕ} {σ : UniformSubstitution 𝔸 T.sig Y X l} {τ : FPerm 𝔸} :
+    ((Y ⊢ r ≣ s).toUniform ∈ T.axioms) →
+    σ.DerivablyEquivariant T →
+    Derivable T (X ⊢ σ.apply (τ • r) ≣ σ.apply (τ • s)) :=
+  .ax'
+
+lemma Derivable.equivariant_substitution
+    (T : Theory 𝔸)
+    {l : ℕ} (σ : UniformSubstitution 𝔸 T.sig Y X l) (hequi : σ.DerivablyEquivariant T)
+    {m : ℕ} (t : TermAtDepth 𝔸 T.sig Y m) {π : FPerm 𝔸} :
+    Derivable T (X ⊢ σ.apply (π • t) ≣ π • (σ.apply t)) := by
+  induction' t using TermAtDepth.induction <;> expose_names
+  · sorry
+  · sorry
+  · sorry
+  · sorry
+
+end DerivableEquations
+
+end Algebra
diff --git a/Algebra/Terms.lean b/Algebra/Terms.lean
index aa853a8..997dca4 100644
--- a/Algebra/Terms.lean
+++ b/Algebra/Terms.lean
@@ -87,6 +87,29 @@ 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⟩
 
+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
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean
index dcca75b..64b6425 100644
--- a/Nominal/Instances/Basic.lean
+++ b/Nominal/Instances/Basic.lean
@@ -70,6 +70,21 @@ def NominalSet.mkDiscrete (X : Type) : NominalSet.Discrete 𝔸 X where
     · intro π hπ; simp only [PermSet.fix', Set.mem_setOf_eq]; rfl
     · exact Set.finite_empty
 
+instance {X : Type} [NominalSet.Discrete 𝔸 X] [Finite X] : OrbitFinite 𝔸 X where
+  fin_orbits := Finite.of_equiv X
+    { toFun x := Quotient.mk _ x
+      invFun x := x.out
+      left_inv x := by
+        suffices ∀ (x y : X), MulAction.orbitRel (FPerm 𝔸) X x y → x = y by
+          apply this
+          rw [← Quotient.eq]
+          apply Quotient.out_eq
+        intro x y ⟨π, hπ⟩
+        simp only [NominalSet.Discrete.is_discrete] at hπ
+        exact hπ.symm
+      right_inv x := by simp
+    }
+
 @[simp] lemma NominalSet.Discrete.supp {X : Type} [NominalSet.Discrete 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
   rw [← Set.subset_empty_iff]
   apply Set.sInter_subset_of_mem
diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean
index 79a5042..0a4974a 100644
--- a/Nominal/Permutations.lean
+++ b/Nominal/Permutations.lean
@@ -187,12 +187,29 @@ class PermSet (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
 variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
 
+/-- An (FPerm 𝔸)-set is orbit-finite if there are only finitely many different orbits. -/
+class OrbitFinite (X : Type) [PermSet 𝔸 X] where
+  fin_orbits : Finite (Quotient (MulAction.orbitRel (FPerm 𝔸) X))
+
 /-- The set of atoms itself forms an (FPerm 𝔸)-Set. -/
 instance : PermSet 𝔸 𝔸 where
   smul π a := π a
   one_smul := by intro; rfl
   mul_smul := by intro _ _ _; rfl
 
+instance : OrbitFinite 𝔸 𝔸 where
+  fin_orbits := Finite.of_equiv Unit
+    { toFun _ := Quotient.mk _ (inferInstanceAs (Nonempty 𝔸)).some
+      invFun _ := ()
+      right_inv := by
+        let chosen := (inferInstanceAs (Nonempty 𝔸)).some
+        apply Quotient.ind; intro a
+        rw [Quotient.eq]
+        show chosen ∈ MulAction.orbit (FPerm 𝔸) a
+        use ⸨chosen, a⸩
+        exact FPerm.swap_apply_right chosen a
+    }
+
 /-- The set of finite permutations forms an (FPerm 𝔸)-Set. -/
 instance : PermSet 𝔸 (FPerm 𝔸) where
   smul π τ := π * τ