blob: c78af1437de33033a4bab5392c1a05e75f19c3ce (
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
|
(* Title: HoTT/ex/Methods.thy
Author: Josh Chen
HoTT method usage examples
*)
theory Methods
imports "../HoTT"
begin
text "Wellformedness results, metatheorems written into the object theory using the wellformedness rules."
lemma
assumes "A : U(i)" "B: A \<longrightarrow> U(i)" "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)"
shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U(i)"
by (routine lems: assms)
lemma
assumes "\<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z: U(i)"
shows
"A : U(i)" and
"B: A \<longrightarrow> U(i)" and
"\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and
"\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)"
proof -
show
"A : U(i)" and
"B: A \<longrightarrow> U(i)" and
"\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and
"\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)"
by (derive lems: assms)
qed
text "Typechecking and constructing inhabitants:"
\<comment> \<open>Correctly determines the type of the pair\<close>
schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> <a, b> : ?A"
by routine
\<comment> \<open>Finds pair (too easy).\<close>
schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B"
apply (rule Sum_intro)
apply assumption+
done
text "
Function application.
The proof methods are not yet automated as well as I would like; we still often have to explicitly specify types.
"
lemma
assumes "A: U(i)" "a: A"
shows "(\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>"
proof compute
show "\<And>x. x: A \<Longrightarrow> <x,0>: A \<times> \<nat>" by routine
qed (routine lems: assms)
lemma
assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "a: A" "b: B(a)"
shows "(\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>"
proof compute
show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>y. <x,y>: \<Prod>y:B(x). \<Sum>x:A. B(x)" by (routine lems: assms)
show "(\<^bold>\<lambda>b. <a,b>)`b \<equiv> <a, b>"
proof compute
show "\<And>b. b: B(a) \<Longrightarrow> <a, b>: \<Sum>x:A. B(x)" by (routine lems: assms)
qed fact
qed fact
end
|
