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
137
|
import Mathlib
import Nominal.Support
import Nominal.Equivariance
import Nominal.Category
import Nominal.Permutations
import Nominal.Instances.Basic
/-!
# Name Abstractions
Given a nominal set X, we define the set `[𝔸]X` of abstractions as pairs in 𝔸 × X modulo alpha-equivalence.
-/
variable (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸]
/-!
## Raw Structure
We first define the raw type of name abstractions as a pair (𝔸, X).
This structure, along with the obvious permutation action, forms a nominal set where supp (a, x) = supp x ∪ {a}.
-/
section RawStructure
variable (X : Type) [NominalSet 𝔸 X]
/-- The structure forming a name abstraction. -/
structure NameAbstraction' where
/-- The atom that is abstracted away. -/
atom : 𝔸
/-- The body from which the atom is abstracted. -/
body : X
attribute [ext] NameAbstraction'
namespace NameAbstraction'
instance : SMul (FPerm 𝔸) (NameAbstraction' 𝔸 X) where
smul π x := .mk (π x.atom) (π • x.body)
@[simp] lemma smul_atom (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).atom = π x.atom := rfl
@[simp] lemma smul_body (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).body = π • x.body := rfl
instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where
smul π x := .mk (π x.atom) (π • x.body)
one_smul := by intro _; ext <;> simp [one_smul]
mul_smul := by intro _ _ _; ext <;> simp [mul_smul]
instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) where
fin_supp := sorry
@[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by sorry
@[simp] lemma fresh {a : 𝔸} {x : NameAbstraction' 𝔸 X} : a # x ↔ a ≠ x.atom ∧ a # x.body := by
simp [NominalSet.IsFresh]
end NameAbstraction'
end RawStructure
/-!
## Alpha-Equivalence
We continue to define alpha-equivalence on this structure.
-/
section AlphaEquivalence
namespace NameAbstraction
variable {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X]
/-- (a, x) ≈ (b, y) if (c a) x = (c b) y for some fresh c. -/
def AlphaEq (x y : NameAbstraction' 𝔸 X) : Prop :=
И c, ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body
lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by sorry
lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by sorry
lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by sorry
private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by sorry
private lemma alpha_eq_symm {x y : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y x := by sorry
private lemma alpha_eq_trans {x y z : NameAbstraction' 𝔸 X} : AlphaEq x y → AlphaEq y z → AlphaEq x z := by sorry
lemma alpha_eq_equivariant : EquivariantRelation 𝔸 (AlphaEq : NameAbstraction' 𝔸 X → NameAbstraction' 𝔸 X → Prop) := by sorry
end NameAbstraction
end AlphaEquivalence
/-!
## Quotient Type
We then define `NameAbstraction` as the quotient type of this structure modulo alpha-equivalence.
-/
section Quotient
variable (X : Type) [NominalSet 𝔸 X]
/-- Associate the name abstraction structure with alpha-equivalence. -/
instance NameAbstraction.setoid : Setoid (NameAbstraction' 𝔸 X) where
r := AlphaEq
iseqv := ⟨alpha_eq_refl, alpha_eq_symm, alpha_eq_trans⟩
/-- Define name abstractions as the quotient set (𝔸 × X)/≈. -/
def NameAbstraction := Quotient (NameAbstraction.setoid 𝔸 X)
/-- The equivalence class of a name abstraction (a, x), often written `⟪a⟫ x` -/
def NameAbstraction.mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : NameAbstraction 𝔸 X :=
Quotient.mk (setoid 𝔸 X) (.mk a x)
/-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/
notation "⟪" a "⟫ " t => NameAbstraction.mk a t
end Quotient
/-!
## Nominal Set Instance
The equivalence classes of name abstractions form a nominal set where supp (⟪a⟫ x) = supp x \ {a}.
-/
section NominalSet
end NominalSet
/-!
## Abstraction Functor
Name abstraction can also be considered as a functor `Nom → Nom`.
-/
section Functor
end Functor
|
