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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
|
theory HoTT
imports Pure
begin
section \<open>Setup\<close>
text "For ML files, routines and setup."
section \<open>Basic definitions\<close>
text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
We do not implement universes, but simply follow the informal notation in the HoTT book."
typedecl Term
section \<open>Judgments\<close>
consts
is_a_type :: "Term \<Rightarrow> prop" ("(_ : U)" [0] 1000)
is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(3_ :/ _)" [0, 0] 1000)
section \<open>Definitional equality\<close>
text "We take the meta-equality \<open>\<equiv>\<close>, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory.
Note that the Pure framework already provides axioms and results for various properties of \<open>\<equiv>\<close>, which we make use of and extend where necessary."
theorem equal_types:
assumes "A \<equiv> B" and "A : U"
shows "B : U" using assms by simp
theorem equal_type_element:
assumes "A \<equiv> B" and "x : A"
shows "x : B" using assms by simp
lemmas type_equality [intro, simp] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated]
section \<open>Type families\<close>
text "Type families are implemented using meta-level lambda expressions \<open>P::Term \<Rightarrow> Term\<close> that further satisfy the following property."
abbreviation is_type_family :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> prop" ("(3_:/ _ \<rightarrow> U)")
where "P: A \<rightarrow> U \<equiv> (\<And>x::Term. x : A \<Longrightarrow> P(x) : U)"
section \<open>Types\<close>
subsection \<open>Dependent function/product\<close>
axiomatization
Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
syntax
"_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 30)
"_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<^bold>\<lambda>_:_./ _)" 30)
"_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3PROD _:_./ _)" 30)
"_LAMBDA_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3%%_:_./ _)" 30)
translations
"\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
"\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
"PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
"%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
(* The above syntax translations bind the x in the expressions B, b. *)
abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40)
where "A\<rightarrow>B \<equiv> \<Prod>_:A. B"
axiomatization
appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60)
where
Prod_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U"
and
Prod_intro [intro]:
"\<And>(A::Term) (B::Term \<Rightarrow> Term) (b::Term \<Rightarrow> Term). (\<And>x::Term. x : A \<Longrightarrow> b(x) : B(x)) \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : \<Prod>x:A. B(x)"
and
Prod_elim [elim]:
"\<And>(A::Term) (B::Term \<Rightarrow> Term) (f::Term) (a::Term). \<lbrakk>f : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> f`a : B(a)"
and
Prod_comp [simp]: "\<And>(A::Term) (b::Term \<Rightarrow> Term) (a::Term). a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)"
and
Prod_uniq [simp]: "\<And>A f::Term. \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
lemmas Prod_formation [intro] = Prod_form Prod_form[rotated]
text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)."
subsection \<open>Dependent pair/sum\<close>
axiomatization
Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
syntax
"_SUM" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20)
"_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3SUM _:_./ _)" 20)
translations
"\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
"SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)"
abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50)
where "A\<times>B \<equiv> \<Sum>_:A. B"
axiomatization
pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and
indSum :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"
where
Sum_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) : U"
and
Sum_intro [intro]:
"\<And>(A::Term) (B::Term \<Rightarrow> Term) (a::Term) (b::Term). \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> (a, b) : \<Sum>x:A. B(x)"
and
Sum_elim [elim]:
"\<And>(A::Term) (B::Term \<Rightarrow> Term) (C::Term \<Rightarrow> Term) (f::Term) (p::Term).
\<lbrakk>C: \<Sum>x:A. B(x) \<rightarrow> U; f : \<Prod>x:A. \<Prod>y:B(x). C((x,y)); p : \<Sum>x:A. B(x)\<rbrakk> \<Longrightarrow> indSum(C)`f`p : C(p)"
and
Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \<equiv> f`a`b"
lemmas Sum_formation [intro] = Sum_form Sum_form[rotated]
text "We choose to formulate the elimination rule by using the object-level function type and function application as much as possible.
Hence only the type family \<open>C\<close> is left as a meta-level argument to the inductor indSum."
subsubsection \<open>Projections\<close>
consts
fst :: "[Term, 'a] \<Rightarrow> Term" ("(1fst[/_,/ _])")
snd :: "[Term, 'a] \<Rightarrow> Term" ("(1snd[/_,/ _])")
overloading
fst_dep \<equiv> fst
snd_dep \<equiv> snd
fst_nondep \<equiv> fst
snd_nondep \<equiv> snd
begin
definition fst_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
"fst_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)"
definition snd_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where
"snd_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)"
definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where
"fst_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)"
definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where
"snd_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)"
end
lemma fst_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def by simp
lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by simp
lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp
lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp
\<comment> \<open>Simplification rules for projections\<close>
lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
subsection \<open>Equality type\<close>
axiomatization
Equal :: "[Term, Term, Term] \<Rightarrow> Term"
syntax
"_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 101] 100)
"_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =[_]/ _)" [101, 101] 100)
translations
"a =\<^sub>A b" \<rightleftharpoons> "CONST Equal A a b"
"a =[A] b" \<rightharpoonup> "CONST Equal A a b"
axiomatization
refl :: "Term \<Rightarrow> Term" ("(refl'(_'))") and
indEqual :: "[Term, [Term, Term, Term] \<Rightarrow> Term] \<Rightarrow> Term" ("(indEqual[_])")
where
Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U"
(* Should I write a permuted version \<open>\<lbrakk>A : U; b : A; a : A\<rbrakk> \<Longrightarrow> \<dots>\<close>? *)
and
Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x"
and
Equal_elim [elim]:
"\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term) (b::Term) (p::Term).
\<lbrakk> \<And>x y::Term. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<rightarrow> U;
f : \<Prod>x:A. C(x)(x)(refl(x));
a : A;
b : A;
p : a =\<^sub>A b \<rbrakk>
\<Longrightarrow> indEqual[A](C)`f`a`b`p : C(a)(b)(p)"
and
Equal_comp [simp]:
"\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \<equiv> f`a"
lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2]
subsubsection \<open>Properties of equality\<close>
text "Symmetry/Path inverse"
definition inv :: "[Term, Term, Term] \<Rightarrow> Term" ("(1inv[_,/ _,/ _])")
where "inv[A,x,y] \<equiv> indEqual[A](\<lambda>x y _. y =\<^sub>A x)`(\<^bold>\<lambda>x:A. refl(x))`x`y"
lemma inv_comp: "\<And>A a::Term. a : A \<Longrightarrow> inv[A,a,a]`refl(a) \<equiv> refl(a)" unfolding inv_def by simp
text "Transitivity/Path composition"
\<comment> \<open>"Raw" composition function\<close>
abbreviation compose' :: "Term \<Rightarrow> Term" ("(1compose''[_])")
where "compose'[A] \<equiv> indEqual[A](\<lambda>x y _. \<Prod>z:A. \<Prod>q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\<lambda>x z _. x =\<^sub>A z)`(\<^bold>\<lambda>x:A. refl(x)))"
\<comment> \<open>"Natural" composition function\<close>
abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compose[_,/ _,/ _,/ _])")
where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>q:y =\<^sub>A z. compose'[A]`x`y`p`z`q"
(**** GOOD CANDIDATE FOR AUTOMATION ****)
lemma compose_comp:
assumes "a : A"
shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" using assms Equal_intro[OF assms] by simp
text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \<open>using\<close> clause in the proof.
This would likely involve something like:
1. Recognizing that there is a function application that can be simplified.
2. Noting that the obstruction to applying \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>.
3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>."
lemmas Equal_simps [simp] = inv_comp compose_comp
subsubsection \<open>Pretty printing\<close>
abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1_\<^sup>-\<^sup>1\<^sub>_\<^sub>,\<^sub>_\<^sub>,\<^sub>_)" 500)
where "p\<^sup>-\<^sup>1\<^sub>A\<^sub>,\<^sub>x\<^sub>,\<^sub>y \<equiv> inv[A,x,y]`p"
abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \<Rightarrow> Term" ("(1_ \<bullet>\<^sub>_\<^sub>,\<^sub>_\<^sub>,\<^sub>_\<^sub>,\<^sub>_/ _)")
where "p \<bullet>\<^sub>A\<^sub>,\<^sub>x\<^sub>,\<^sub>y\<^sub>,\<^sub>z q \<equiv> compose[A,x,y,z]`p`q"
end
(*
subsubsection \<open>Empty type\<close>
axiomatization
Null :: Term and
ind_Null :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(ind'_Null'(_,/ _'))")
where
Null_form: "Null : U" and
Null_elim: "\<And>C x a. \<lbrakk>x : Null \<Longrightarrow> C(x) : U; a : Null\<rbrakk> \<Longrightarrow> ind_Null(C(x), a) : C(a)"
subsubsection \<open>Natural numbers\<close>
axiomatization
Nat :: Term and
zero :: Term ("0") and
succ :: "Term \<Rightarrow> Term" and (* how to enforce \<open>succ : Nat\<rightarrow>Nat\<close>? *)
ind_Nat :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term"
where
Nat_form: "Nat : U" and
Nat_intro1: "0 : Nat" and
Nat_intro2: "\<And>n. n : Nat \<Longrightarrow> succ n : Nat"
(* computation rules *)
*)
|