blob: 2145bf904fad9ffbaa0d2c83df19181ccd9fed23 (
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
|
(* Title: HoTT/ProdProps.thy
Author: Josh Chen
Date: Aug 2018
Properties of the dependent product.
*)
theory ProdProps
imports
HoTT_Methods
Prod
begin
section ‹Composition›
text "
The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for Π-type definitional equality, and the correct substitutions in the subgoals thereafter.
"
lemma compose_assoc:
assumes "A: U(i)" and "f: A → B" "g: B → C" "h: ∏x:C. D(x)"
shows "(h ∘ g) ∘ f ≡ h ∘ (g ∘ f)"
proof (subst (0 1 2 3) compose_def)
show "❙λx. (❙λy. h`(g`y))`(f`x) ≡ ❙λx. h`((❙λy. g`(f`y))`x)"
proof (subst Prod_eq)
― ‹Todo: set the Simplifier (or other simplification methods) up to use ‹Prod_eq›!›
show "⋀x. x: A ⟹ (❙λy. h`(g`y))`(f`x) ≡ h`((❙λy. g`(f`y))`x)"
proof compute
show "⋀x. x: A ⟹ h`(g`(f`x)) ≡ h`((❙λy. g`(f`y))`x)"
proof compute
show "⋀x. x: A ⟹ g`(f`x): C" by (simple lems: assms)
qed
show "⋀x. x: B ⟹ h`(g`x): D(g`x)" by (simple lems: assms)
qed (simple lems: assms)
qed fact
qed
lemma compose_comp':
assumes "A: U(i)" and "⋀x. x: A ⟹ b(x): B" and "⋀x. x: B ⟹ c(x): C(x)"
shows "(❙λx. c(x)) ∘ (❙λx. b(x)) ≡ ❙λx. c(b(x))"
proof (subst compose_def, subst Prod_eq)
show "⋀x. x: A ⟹ (❙λx. c(x))`((❙λx. b(x))`x) ≡ ❙λx. c (b x)"
proof compute
text "However we can derive a variant with more explicit premises:"
lemma compose_comp:
assumes
"A: U(i)" "B: U(i)" "C: B ⟶ U(i)" and
"⋀x. x: A ⟹ b(x): B" and
"⋀x. x: B ⟹ c(x): C(x)"
shows "(❙λx. c(x)) ∘ (❙λx. b(x)) ≡ ❙λx. c(b(x))"
proof (subst compose_def)
show "❙λx. (❙λx. c(x))`((❙λx. b(x))`x) ≡ ❙λx. c(b(x))"
proof
show "⋀a. a: A ⟹ (❙λx. c(x))`((❙λx. b(x))`a) ≡ c(b(a))"
proof compute
show "⋀a. a: A ⟹ c((❙λx. b(x))`a) ≡ 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
|
