blob: 6f9f996c0bd5fc3a9874d4de1d580e3e46baf351 (
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
|
(*
Title: tests/Test.thy
Author: Joshua Chen
Date: 2018
This is an old test suite from early implementations.
It is not always guaranteed to be up to date or to reflect most recent versions of the theory.
*)
theory Test
imports "../HoTT"
begin
text \<open>
A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
Things that *should* be automated:
\<^item> Checking that @{term A} is a well-formed type, when writing things like @{prop "x: A"} and @{prop "A: U i"}.
\<^item> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
\<close>
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>\<Prod>-type\<close>
subsection \<open>Typing functions\<close>
text \<open>Declaring @{thm Prod_intro} with the @{attribute intro} attribute enables @{method rule} to prove the following.\<close>
proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A"
by (routine add: 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 add: 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 add: assms)
subsection \<open>Function application\<close>
proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a"
by (derive lems: assms)
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"
by (derive lems: assms)
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 derive
oops \<comment> \<open>Missing some premises.\<close>
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"
proof derive
oops
subsection \<open>Currying functions\<close>
proposition curried_function_formation:
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 add: 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 add: assms)
lemma curried_type_judgment:
assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "\<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 add: assms)
text \<open>
Polymorphic identity function is now trivial due to lambda expression polymorphism.
It was more involved in previous monomorphic incarnations.
\<close>
lemma "x: A \<Longrightarrow> id`x \<equiv> x"
by derive
section \<open>Natural numbers\<close>
text \<open>Automatic proof methods recognize natural numbers.\<close>
proposition "succ(succ(succ 0)): \<nat>" by routine
end
|
