blob: e48b3e66a4a6afdfc7050275ed382a7919514064 (
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
|
(* Title: HoTT/ProdProps.thy
Author: Josh Chen
Date: Aug 2018
Properties of the dependent product.
*)
theory ProdProps
imports
HoTT_Methods
Prod
begin
section \<open>Composition\<close>
text "
The proof of associativity is surprisingly intricate; it involves telling Isabelle to use the correct rule for \<Pi>-type judgmental equality, and the correct substitutions in the subgoals thereafter, among other things.
"
lemma compose_assoc:
assumes
"A \<rightarrow> B: U(i)" "B \<rightarrow> C: U(i)" and
"\<Prod>x:C. D(x): U(i)" and
"f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D(x)"
shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)"
proof (subst (0 1 2 3) compose_def)
text "Compute the different bracketings and show they are equivalent:"
show "\<^bold>\<lambda>x. (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)"
proof (subst Prod_eq)
show "\<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)" by simp
show "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)"
proof compute
show "\<And>x. x: A \<Longrightarrow> h`(g`(f`x)) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)"
proof compute
show "\<And>x. x: A \<Longrightarrow> g`(f`x): C" by (simple lems: assms)
qed
show "\<And>x. x: B \<Longrightarrow> h`(g`x): D(g`x)" by (simple lems: assms)
qed (simple lems: assms)
qed (wellformed lems: assms)
text "
Finish off any remaining subgoals that Isabelle can't prove automatically.
These typically require the application of specific substitutions or computation rules.
"
show "g \<circ> f: A \<rightarrow> C" by (subst compose_def) (derive lems: assms)
show "h \<circ> g: \<Prod>x:B. D(g`x)"
proof (subst compose_def)
show "\<^bold>\<lambda>x. h`(g`x): \<Prod>x:B. D(g`x)"
proof
show "\<And>x. x: B \<Longrightarrow> h`(g`x): D(g`x)"
proof
show "\<And>x. x: B \<Longrightarrow> g`x: C" by (simple lems: assms)
qed (simple lems: assms)
qed (wellformed lems: assms)
qed fact+
show "\<Prod>x:B. D (g`x): U(i)"
proof
show "\<And>x. x: B \<Longrightarrow> D(g`x): U(i)"
proof -
have *: "D: C \<longrightarrow> U(i)" by (wellformed lems: assms)
fix x assume asm: "x: B"
have "g`x: C" by (simple lems: assms asm)
then show "D(g`x): U(i)" by (rule *)
qed
qed (wellformed lems: assms)
have "A: U(i)" by (wellformed lems: assms)
moreover have "C: U(i)" by (wellformed lems: assms)
ultimately show "A \<rightarrow> C: U(i)" ..
qed (simple lems: assms)
text "The following rule is correct, but we cannot prove it using just the rules of the theory."
lemma compose_comp':
assumes "A: U(i)" and "\<And>x. x: A \<Longrightarrow> b(x): B" and "\<And>x. x: B \<Longrightarrow> c(x): C(x)"
shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))"
oops
text "However we can derive a variant with more explicit premises:"
lemma compose_comp:
assumes
"A: U(i)" "B: U(i)" "C: B \<longrightarrow> U(i)" and
"\<And>x. x: A \<Longrightarrow> b(x): B" and
"\<And>x. x: B \<Longrightarrow> c(x): C(x)"
shows "(\<^bold>\<lambda>x. c(x)) \<circ> (\<^bold>\<lambda>x. b(x)) \<equiv> \<^bold>\<lambda>x. c(b(x))"
proof (subst compose_def)
show "\<^bold>\<lambda>x. (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`x) \<equiv> \<^bold>\<lambda>x. c(b(x))"
proof
show "\<And>a. a: A \<Longrightarrow> (\<^bold>\<lambda>x. c(x))`((\<^bold>\<lambda>x. b(x))`a) \<equiv> c(b(a))"
proof compute
show "\<And>a. a: A \<Longrightarrow> c((\<^bold>\<lambda>x. b(x))`a) \<equiv> c(b(a))" by compute (simple lems: assms)
qed (simple lems: assms)
qed fact
qed (simple lems: assms)
lemmas compose_comps [comp] = compose_def compose_comp
end
|
