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
|
(* Title: HoTT/Equal.thy
Author: Josh Chen
Date: Jun 2018
Equality type.
*)
theory Equal
imports HoTT_Base
begin
axiomatization
Equal :: "[Term, Term, Term] ⇒ Term" and
refl :: "Term ⇒ Term" ("(refl'(_'))" 1000) and
indEqual :: "[Term, [Term, Term, Term] ⇒ Term] ⇒ Term" ("(indEqual[_])")
syntax
"_EQUAL" :: "[Term, Term, Term] ⇒ Term" ("(3_ =⇩_/ _)" [101, 101] 100)
"_EQUAL_ASCII" :: "[Term, Term, Term] ⇒ Term" ("(3_ =[_]/ _)" [101, 0, 101] 100)
translations
"a =[A] b" ⇌ "CONST Equal A a b"
"a =⇩A b" ⇀ "CONST Equal A a b"
axiomatization where
Equal_form: "⋀A a b::Term. ⟦A : U; a : A; b : A⟧ ⟹ a =⇩A b : U"
(* Should I write a permuted version ‹⟦A : U; b : A; a : A⟧ ⟹ …›? *)
and
Equal_intro [intro]: "⋀A x::Term. x : A ⟹ refl(x) : x =⇩A x"
and
Equal_elim [elim]:
"⋀(A::Term) (C::[Term, Term, Term] ⇒ Term) (f::Term) (a::Term) (b::Term) (p::Term).
⟦ ⋀x y::Term. ⟦x : A; y : A⟧ ⟹ C(x)(y): x =⇩A y → U;
f : ∏x:A. C(x)(x)(refl(x));
a : A;
b : A;
p : a =⇩A b ⟧
⟹ indEqual[A](C)`f`a`b`p : C(a)(b)(p)"
and
Equal_comp [simp]:
"⋀(A::Term) (C::[Term, Term, Term] ⇒ Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) ≡ f`a"
lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2]
subsubsection ‹Properties of equality›
text "Symmetry/Path inverse"
definition inv :: "[Term, Term, Term] ⇒ Term" ("(1inv[_,/ _,/ _])")
where "inv[A,x,y] ≡ indEqual[A](λx y _. y =⇩A x)`(❙λx:A. refl(x))`x`y"
lemma inv_comp: "⋀A a::Term. a : A ⟹ inv[A,a,a]`refl(a) ≡ refl(a)" unfolding inv_def by simp
text "Transitivity/Path composition"
― ‹"Raw" composition function›
definition compose' :: "Term ⇒ Term" ("(1compose''[_])")
where "compose'[A] ≡ indEqual[A](λx y _. ∏z:A. ∏q: y =⇩A z. x =⇩A z)`(indEqual[A](λx z _. x =⇩A z)`(❙λx:A. refl(x)))"
― ‹"Natural" composition function›
abbreviation compose :: "[Term, Term, Term, Term] ⇒ Term" ("(1compose[_,/ _,/ _,/ _])")
where "compose[A,x,y,z] ≡ ❙λp:x =⇩A y. ❙λq:y =⇩A z. compose'[A]`x`y`p`z`q"
(**** GOOD CANDIDATE FOR AUTOMATION ****)
lemma compose_comp:
assumes "a : A"
shows "compose[A,a,a,a]`refl(a)`refl(a) ≡ refl(a)" using assms Equal_intro[OF assms] unfolding compose'_def by simp
text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the ‹using› clause in the proof.
This would likely involve something like:
1. Recognizing that there is a function application that can be simplified.
2. Noting that the obstruction to applying ‹Prod_comp› is the requirement that ‹refl(a) : a =⇩A a›.
3. Obtaining such a condition, using the known fact ‹a : A› and the introduction rule ‹Equal_intro›."
lemmas Equal_simps [simp] = inv_comp compose_comp
subsubsection ‹Pretty printing›
abbreviation inv_pretty :: "[Term, Term, Term, Term] ⇒ Term" ("(1_⇧-⇧1[_, _, _])" 500)
where "p⇧-⇧1[A,x,y] ≡ inv[A,x,y]`p"
abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] ⇒ Term" ("(1_ ∙[_, _, _, _]/ _)")
where "p ∙[A,x,y,z] q ≡ compose[A,x,y,z]`p`q"
end
|
