From 352a6e40a5bdf193b8f9690e76aede4e0650a445 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 30 Jun 2018 07:07:42 +0200 Subject: Equality --- Equal.thy | 83 ++++++++++++++++++--------------------------------- EqualProps.thy | 90 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ HoTT_Methods.thy | 14 +++++++-- 3 files changed, 131 insertions(+), 56 deletions(-) create mode 100644 EqualProps.thy diff --git a/Equal.thy b/Equal.thy index 02fe540..6c18084 100644 --- a/Equal.thy +++ b/Equal.thy @@ -12,7 +12,10 @@ begin axiomatization Equal :: "[Term, Term, Term] \ Term" and refl :: "Term \ Term" ("(refl'(_'))" 1000) and - indEqual :: "[Term, [Term, Term, Term] \ Term] \ Term" ("(indEqual[_])") + indEqual :: "[Term, [Term, Term] \ Typefam, Term \ Term, Term, Term, Term] \ Term" ("(indEqual[_])") + + +section \Syntax\ syntax "_EQUAL" :: "[Term, Term, Term] \ Term" ("(3_ =\<^sub>_/ _)" [101, 101] 100) @@ -21,64 +24,36 @@ translations "a =[A] b" \ "CONST Equal A a b" "a =\<^sub>A b" \ "CONST Equal A a b" + +section \Type rules\ + axiomatization where - Equal_form: "\A a b::Term. \A : U; a : A; b : A\ \ a =\<^sub>A b : U" - (* Should I write a permuted version \\A : U; b : A; a : A\ \ \\? *) + Equal_form: "\A a b. \a : A; b : A\ \ a =\<^sub>A b : U" and - Equal_intro [intro]: "\A x::Term. x : A \ refl(x) : x =\<^sub>A x" + Equal_form_cond1: "\A a b. a =\<^sub>A b : U \ A : U" 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 =\<^sub>A y \ U; - f : \x:A. C(x)(x)(refl(x)); - a : A; - b : A; - p : a =\<^sub>A b \ - \ indEqual[A](C)`f`a`b`p : C(a)(b)(p)" + Equal_form_cond2: "\A a b. a =\<^sub>A b : U \ a : A" 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 =\<^sub>A x)`(\<^bold>\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 =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\x z _. x =\<^sub>A z)`(\<^bold>\x:A. refl(x)))" - -\ \"Natural" composition function\ -abbreviation compose :: "[Term, Term, Term, Term] \ Term" ("(1compose[_,/ _,/ _,/ _])") - where "compose[A,x,y,z] \ \<^bold>\p:x =\<^sub>A y. \<^bold>\q:y =\<^sub>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 =\<^sub>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\ + Equal_form_cond3: "\A a b. a =\<^sub>A b : U \ b : A" +and + Equal_intro: "\A a. a : A \ refl(a) : a =\<^sub>A a" +and + Equal_elim: "\A C f a b p. \ + \x y.\x : A; y : A\ \ C x y: x =\<^sub>A y \ U; + \x. x : A \ f x : C x x refl(x); + a : A; + b : A; + p : a =\<^sub>A b + \ \ indEqual[A] C f a b p : C a b p" +and + Equal_comp: "\A C f a. \ + \x y.\x : A; y : A\ \ C x y: x =\<^sub>A y \ U; + \x. x : A \ f x : C x x refl(x); + a : A + \ \ indEqual[A] C f a a refl(a) \ f a" -abbreviation inv_pretty :: "[Term, Term, Term, Term] \ Term" ("(1_\<^sup>-\<^sup>1[_, _, _])" 500) - where "p\<^sup>-\<^sup>1[A,x,y] \ inv[A,x,y]`p" +lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp +lemmas Equal_form_conds [elim] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 -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 \ No newline at end of file diff --git a/EqualProps.thy b/EqualProps.thy new file mode 100644 index 0000000..3b0de79 --- /dev/null +++ b/EqualProps.thy @@ -0,0 +1,90 @@ +(* Title: HoTT/EqualProps.thy + Author: Josh Chen + Date: Jun 2018 + +Properties of equality. +*) + +theory EqualProps + imports + HoTT_Methods + Equal + Prod +begin + +section \Symmetry / Path inverse\ + +definition inv :: "[Term, Term, Term] \ Term" ("(1inv[_,/ _,/ _])") + where "inv[A,x,y] \ \<^bold>\p: (x =\<^sub>A y). indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) x y p" + +lemma inv_type: + assumes "p : x =\<^sub>A y" + shows "inv[A,x,y]`p : y =\<^sub>A x" + +proof + show "inv[A,x,y] : (x =\<^sub>A y) \ (y =\<^sub>A x)" + proof (unfold inv_def, standard) + fix p assume asm: "p : x =\<^sub>A y" + show "indEqual[A] (\x y _. y =[A] x) refl x y p : y =\<^sub>A x" + proof standard+ + show "x : A" by (wellformed jdgmt: asm) + show "y : A" by (wellformed jdgmt: asm) + qed (assumption | rule | rule asm)+ + qed (wellformed jdgmt: assms) +qed (rule assms) + + +lemma inv_comp: + assumes "a : A" + shows "inv[A,a,a]`refl(a) \ refl(a)" + +proof - + have "inv[A,a,a]`refl(a) \ indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a)" + proof (unfold inv_def, standard) + show "refl(a) : a =\<^sub>A a" using assms .. + + fix p assume asm: "p : a =\<^sub>A a" + show "indEqual[A] (\x y _. y =\<^sub>A x) refl a a p : a =\<^sub>A a" + proof standard+ + show "a : A" by (wellformed jdgmt: asm) + then show "a : A" . \ \The elimination rule requires that both arguments to \indEqual\ be shown to have the correct type.\ + qed (assumption | rule | rule asm)+ + qed + + also have "indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a) \ refl(a)" + by (standard | assumption | rule assms)+ + + finally show "inv[A,a,a]`refl(a) \ refl(a)" . +qed + +section \Transitivity / Path composition\ + +\ \"Raw" composition function\ +definition compose' :: "Term \ Term" ("(1compose''[_])") + where "compose'[A] \ + indEqual[A] (\x y _. \z:A. \q: y =\<^sub>A z. x =\<^sub>A z) (indEqual[A](\x z _. x =\<^sub>A z) (\<^bold>\x:A. refl(x)))" + +\ \"Natural" composition function\ +abbreviation compose :: "[Term, Term, Term, Term] \ Term" ("(1compose[_,/ _,/ _,/ _])") + where "compose[A,x,y,z] \ \<^bold>\p:x =\<^sub>A y. \<^bold>\q:y =\<^sub>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 =\<^sub>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_\<^sup>-\<^sup>1[_, _, _])" 500) + where "p\<^sup>-\<^sup>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" \ No newline at end of file diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index aa6fca2..7886c1a 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -11,6 +11,7 @@ theory HoTT_Methods "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" HoTT_Base + Equal Prod Sum begin @@ -27,16 +28,25 @@ method wellformed uses jdgmt = ( "A : U" for A \ \ match (A) in "\x:?A. ?B x" \ \ - rule Prod.Prod_form_cond1[OF jdgmt] | + print_term "\", + (rule Prod.Prod_form_cond1[OF jdgmt] | rule Prod.Prod_form_cond2[OF jdgmt] | catch \wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\ \fail\ + catch \wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\ \fail\) \ \ "\x:?A. ?B x" \ \ rule Sum.Sum_form_cond1[OF jdgmt] | rule Sum.Sum_form_cond2[OF jdgmt] | catch \wellformed jdgmt: Sum.Sum_form_cond1[OF jdgmt]\ \fail\ | catch \wellformed jdgmt: Sum.Sum_form_cond2[OF jdgmt]\ \fail\ + \ \ + "?a =[?A] ?b" \ \ + rule Equal.Equal_form_cond1[OF jdgmt] | + rule Equal.Equal_form_cond2[OF jdgmt] | + rule Equal.Equal_form_cond3[OF jdgmt] | + catch \wellformed jdgmt: Equal.Equal_form_cond1[OF jdgmt]\ \fail\ | + catch \wellformed jdgmt: Equal.Equal_form_cond2[OF jdgmt]\ \fail\ | + catch \wellformed jdgmt: Equal.Equal_form_cond3[OF jdgmt]\ \fail\ \ \ \ "PROP ?P \ PROP Q" for Q \ \ -- cgit v1.2.3