blob: b0eb87a88ee67af89f23a42342756ed681d632ac (
plain)
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
|
(* Title: HoTT/tests/Test.thy
Author: Josh Chen
Date: Aug 2018
This is an old "test suite" from early implementations of the theory.
It is not always guaranteed to be up to date, or reflect most recent versions of the theory.
*)
theory Test
imports "../HoTT"
begin
text "
A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
Things that *should* be automated:
- Checking that \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>.
- Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
"
declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]]
\<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
section \<open>\<Pi>-type\<close>
subsection \<open>Typing functions\<close>
text "
Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following.
"
proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" by (routine lems: assms)
proposition
assumes "A : U(i)" and "A \<equiv> B"
shows "\<^bold>\<lambda>x. x : B \<rightarrow> A"
proof -
have "A \<rightarrow> A \<equiv> B \<rightarrow> A" using assms by simp
moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (routine lems: assms)
ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp
qed
proposition
assumes "A : U(i)" and "B : U(i)"
shows "\<^bold>\<lambda>x y. x : A \<rightarrow> B \<rightarrow> A"
by (routine lems: assms)
subsection \<open>Function application\<close>
proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (derive lems: assms)
text "Currying:"
lemma
assumes "a : A" and "\<And>x. x: A \<Longrightarrow> B(x): U(i)"
shows "(\<^bold>\<lambda>x y. y)`a \<equiv> \<^bold>\<lambda>y. y"
proof compute
show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. y : B(x) \<rightarrow> B(x)" by (routine lems: assms)
qed fact
lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b" by derive
lemma "\<lbrakk>A: U(i); a : A \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y"
proof compute
show "\<And>x. \<lbrakk>A: U(i); x: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>y. f x y: \<Prod>y:B(x). C x y"
proof
oops
lemma "\<lbrakk>a : A; b : B(a); c : C(a)(b)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. \<^bold>\<lambda>y. \<^bold>\<lambda>z. f x y z)`a`b`c \<equiv> f a b c"
oops
subsection \<open>Currying functions\<close>
proposition curried_function_formation:
fixes A B C
assumes
"A : U(i)" and
"B: A \<longrightarrow> U(i)" and
"\<And>x. C(x): B(x) \<longrightarrow> U(i)"
shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U(i)"
by (routine lems: assms)
proposition higher_order_currying_formation:
assumes
"A: U(i)" and
"B: A \<longrightarrow> U(i)" and
"\<And>x y. y: B(x) \<Longrightarrow> C(x)(y): U(i)" and
"\<And>x y z. z : C(x)(y) \<Longrightarrow> D(x)(y)(z): U(i)"
shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z): U(i)"
by (routine lems: assms)
lemma curried_type_judgment:
assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "\<And>x y. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y"
shows "\<^bold>\<lambda>x y. f x y : \<Prod>x:A. \<Prod>y:B(x). C x y"
by (routine lems: assms)
text "
Polymorphic identity function is now trivial due to lambda expression polymorphism.
(Was more involved in previous monomorphic incarnations.)
"
definition Id :: "Term" where "Id \<equiv> \<^bold>\<lambda>x. x"
lemma "\<lbrakk>x: A\<rbrakk> \<Longrightarrow> Id`x \<equiv> x"
unfolding Id_def by (compute, routine)
section \<open>Natural numbers\<close>
text "Automatic proof methods recognize natural numbers."
proposition "succ(succ(succ 0)): Nat" by routine
end
|
