1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
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
|
