blob: 871964fb3db0d3850a74ced6a130bde341fc4155 (
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
|
(* Title: HoTT/ex/Methods.thy
Author: Josh Chen
Date: Aug 2018
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 ⟶ U(i)" "⋀x. x : A ⟹ C x: B x ⟶ U(i)"
shows "∑x:A. ∏y:B x. ∑z:C x y. ∏w:A. x =⇩A w : U(i)"
by (simple lems: assms)
lemma
assumes "∑x:A. ∏y: B x. ∑z: C x y. D x y z: U(i)"
shows
"A : U(i)" and
"B: A ⟶ U(i)" and
"⋀x. x : A ⟹ C x: B x ⟶ U(i)" and
"⋀x y. ⟦x : A; y : B x⟧ ⟹ D x y: C x y ⟶ U(i)"
proof -
show
"A : U(i)" and
"B: A ⟶ U(i)" and
"⋀x. x : A ⟹ C x: B x ⟶ U(i)" and
"⋀x y. ⟦x : A; y : B x⟧ ⟹ D x y: C x y ⟶ U(i)"
by (derive lems: assms)
qed
text "Typechecking and constructing inhabitants:"
― ‹Correctly determines the type of the pair›
schematic_goal "⟦A: U(i); B: U(i); a : A; b : B⟧ ⟹ <a, b> : ?A"
by simple
― ‹Finds pair (too easy).›
schematic_goal "⟦A: U(i); B: U(i); a : A; b : B⟧ ⟹ ?x : A × 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 "(❙λx. <x,0>)`a ≡ <a,0>"
proof compute
show "⋀x. x: A ⟹ <x,0>: A × ℕ" by simple
qed (simple lems: assms)
lemma
assumes "A: U(i)" "B: A ⟶ U(i)" "a: A" "b: B(a)"
shows "(❙λx y. <x,y>)`a`b ≡ <a,b>"
proof compute
show "⋀x. x: A ⟹ ❙λy. <x,y>: ∏y:B(x). ∑x:A. B(x)" by (simple lems: assms)
show "(❙λb. <a,b>)`b ≡ <a, b>"
proof compute
show "⋀b. b: B(a) ⟹ <a, b>: ∑x:A. B(x)" by (simple lems: assms)
qed fact
qed fact
end
|
