diff options
| -rw-r--r-- | Equal.thy | 83 | ||||
| -rw-r--r-- | EqualProps.thy | 90 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 14 |
3 files changed, 131 insertions, 56 deletions
@@ -12,7 +12,10 @@ begin axiomatization Equal :: "[Term, Term, Term] \<Rightarrow> Term" and refl :: "Term \<Rightarrow> Term" ("(refl'(_'))" 1000) and - indEqual :: "[Term, [Term, Term, Term] \<Rightarrow> Term] \<Rightarrow> Term" ("(indEqual[_])") + indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(indEqual[_])") + + +section \<open>Syntax\<close> syntax "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 101] 100) @@ -21,64 +24,36 @@ translations "a =[A] b" \<rightleftharpoons> "CONST Equal A a b" "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b" + +section \<open>Type rules\<close> + axiomatization where - Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U" - (* Should I write a permuted version \<open>\<lbrakk>A : U; b : A; a : A\<rbrakk> \<Longrightarrow> \<dots>\<close>? *) + Equal_form: "\<And>A a b. \<lbrakk>a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U" and - Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x" + Equal_form_cond1: "\<And>A a b. a =\<^sub>A b : U \<Longrightarrow> A : U" and - Equal_elim [elim]: - "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term) (b::Term) (p::Term). - \<lbrakk> \<And>x y::Term. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<rightarrow> U; - f : \<Prod>x:A. C(x)(x)(refl(x)); - a : A; - b : A; - p : a =\<^sub>A b \<rbrakk> - \<Longrightarrow> indEqual[A](C)`f`a`b`p : C(a)(b)(p)" + Equal_form_cond2: "\<And>A a b. a =\<^sub>A b : U \<Longrightarrow> a : A" and - Equal_comp [simp]: - "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \<equiv> f`a" - -lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2] - -subsubsection \<open>Properties of equality\<close> - -text "Symmetry/Path inverse" - -definition inv :: "[Term, Term, Term] \<Rightarrow> Term" ("(1inv[_,/ _,/ _])") - where "inv[A,x,y] \<equiv> indEqual[A](\<lambda>x y _. y =\<^sub>A x)`(\<^bold>\<lambda>x:A. refl(x))`x`y" - -lemma inv_comp: "\<And>A a::Term. a : A \<Longrightarrow> inv[A,a,a]`refl(a) \<equiv> refl(a)" unfolding inv_def by simp - -text "Transitivity/Path composition" - -\<comment> \<open>"Raw" composition function\<close> -definition compose' :: "Term \<Rightarrow> Term" ("(1compose''[_])") - where "compose'[A] \<equiv> indEqual[A](\<lambda>x y _. \<Prod>z:A. \<Prod>q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\<lambda>x z _. x =\<^sub>A z)`(\<^bold>\<lambda>x:A. refl(x)))" - -\<comment> \<open>"Natural" composition function\<close> -abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compose[_,/ _,/ _,/ _])") - where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>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) \<equiv> 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 \<open>using\<close> 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 \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>. - 3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>." - -lemmas Equal_simps [simp] = inv_comp compose_comp - -subsubsection \<open>Pretty printing\<close> + Equal_form_cond3: "\<And>A a b. a =\<^sub>A b : U \<Longrightarrow> b : A" +and + Equal_intro: "\<And>A a. a : A \<Longrightarrow> refl(a) : a =\<^sub>A a" +and + Equal_elim: "\<And>A C f a b p. \<lbrakk> + \<And>x y.\<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<rightarrow> U; + \<And>x. x : A \<Longrightarrow> f x : C x x refl(x); + a : A; + b : A; + p : a =\<^sub>A b + \<rbrakk> \<Longrightarrow> indEqual[A] C f a b p : C a b p" +and + Equal_comp: "\<And>A C f a. \<lbrakk> + \<And>x y.\<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<rightarrow> U; + \<And>x. x : A \<Longrightarrow> f x : C x x refl(x); + a : A + \<rbrakk> \<Longrightarrow> indEqual[A] C f a a refl(a) \<equiv> f a" -abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1_\<^sup>-\<^sup>1[_, _, _])" 500) - where "p\<^sup>-\<^sup>1[A,x,y] \<equiv> 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] \<Rightarrow> Term" ("(1_ \<bullet>[_, _, _, _]/ _)") - where "p \<bullet>[A,x,y,z] q \<equiv> 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 \<open>Symmetry / Path inverse\<close> + +definition inv :: "[Term, Term, Term] \<Rightarrow> Term" ("(1inv[_,/ _,/ _])") + where "inv[A,x,y] \<equiv> \<^bold>\<lambda>p: (x =\<^sub>A y). indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>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) \<rightarrow> (y =\<^sub>A x)" + proof (unfold inv_def, standard) + fix p assume asm: "p : x =\<^sub>A y" + show "indEqual[A] (\<lambda>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) \<equiv> refl(a)" + +proof - + have "inv[A,a,a]`refl(a) \<equiv> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>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] (\<lambda>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" . \<comment> \<open>The elimination rule requires that both arguments to \<open>indEqual\<close> be shown to have the correct type.\<close> + qed (assumption | rule | rule asm)+ + qed + + also have "indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)" + by (standard | assumption | rule assms)+ + + finally show "inv[A,a,a]`refl(a) \<equiv> refl(a)" . +qed + +section \<open>Transitivity / Path composition\<close> + +\<comment> \<open>"Raw" composition function\<close> +definition compose' :: "Term \<Rightarrow> Term" ("(1compose''[_])") + where "compose'[A] \<equiv> + indEqual[A] (\<lambda>x y _. \<Prod>z:A. \<Prod>q: y =\<^sub>A z. x =\<^sub>A z) (indEqual[A](\<lambda>x z _. x =\<^sub>A z) (\<^bold>\<lambda>x:A. refl(x)))" + +\<comment> \<open>"Natural" composition function\<close> +abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compose[_,/ _,/ _,/ _])") + where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>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) \<equiv> 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 \<open>using\<close> 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 \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>. + 3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>." + +lemmas Equal_simps [simp] = inv_comp compose_comp + +subsubsection \<open>Pretty printing\<close> + +abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1_\<^sup>-\<^sup>1[_, _, _])" 500) + where "p\<^sup>-\<^sup>1[A,x,y] \<equiv> inv[A,x,y]`p" + +abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \<Rightarrow> Term" ("(1_ \<bullet>[_, _, _, _]/ _)") + where "p \<bullet>[A,x,y,z] q \<equiv> 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 \<Rightarrow> \<open> match (A) in "\<Prod>x:?A. ?B x" \<Rightarrow> \<open> - rule Prod.Prod_form_cond1[OF jdgmt] | + print_term "\<Pi>", + (rule Prod.Prod_form_cond1[OF jdgmt] | rule Prod.Prod_form_cond2[OF jdgmt] | catch \<open>wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]\<close> \<open>fail\<close> | - catch \<open>wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\<close> \<open>fail\<close> + catch \<open>wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\<close> \<open>fail\<close>) \<close> \<bar> "\<Sum>x:?A. ?B x" \<Rightarrow> \<open> rule Sum.Sum_form_cond1[OF jdgmt] | rule Sum.Sum_form_cond2[OF jdgmt] | catch \<open>wellformed jdgmt: Sum.Sum_form_cond1[OF jdgmt]\<close> \<open>fail\<close> | catch \<open>wellformed jdgmt: Sum.Sum_form_cond2[OF jdgmt]\<close> \<open>fail\<close> + \<close> \<bar> + "?a =[?A] ?b" \<Rightarrow> \<open> + rule Equal.Equal_form_cond1[OF jdgmt] | + rule Equal.Equal_form_cond2[OF jdgmt] | + rule Equal.Equal_form_cond3[OF jdgmt] | + catch \<open>wellformed jdgmt: Equal.Equal_form_cond1[OF jdgmt]\<close> \<open>fail\<close> | + catch \<open>wellformed jdgmt: Equal.Equal_form_cond2[OF jdgmt]\<close> \<open>fail\<close> | + catch \<open>wellformed jdgmt: Equal.Equal_form_cond3[OF jdgmt]\<close> \<open>fail\<close> \<close> \<close> \<bar> "PROP ?P \<Longrightarrow> PROP Q" for Q \<Rightarrow> \<open> |