blob: da044b42cdde3f569c88ab65410c9c87780329e8 (
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/HoTT_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 HoTT_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" using 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" using assms(1) ..
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 (simple lems: assms)
subsection \<open>Function application\<close>
proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (simple 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
show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. y : B(x) \<rightarrow> B(x)" by (simple 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 (compute, simple)
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 (simple 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 (simple 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 (simple lems: assms)
text "
Polymorphic identity function. 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, simple)
section \<open>Natural numbers\<close>
text "Automatic proof methods recognize natural numbers."
proposition "succ(succ(succ 0)): Nat" by simple
end
|
