From ba0205cddb0205dcc5d9f7bba5702b11a791e6c7 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 27 Jun 2018 16:11:20 +0200 Subject: Move projection function definitions out of Sum.thy --- Proj.thy | 196 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Sum.thy | 171 +------------------------------------------------------ 2 files changed, 197 insertions(+), 170 deletions(-) create mode 100644 Proj.thy diff --git a/Proj.thy b/Proj.thy new file mode 100644 index 0000000..9387ffb --- /dev/null +++ b/Proj.thy @@ -0,0 +1,196 @@ +(* Title: HoTT/Proj.thy + Author: Josh Chen + Date: Jun 2018 + +Projection functions \fst\ and \snd\ for the dependent sum type. +*) + +theory Proj + imports + HoTT_Methods + Prod + Sum +begin + +consts + fst :: "[Term, 'a] \ Term" ("(1fst[/_,/ _])") + snd :: "[Term, 'a] \ Term" ("(1snd[/_,/ _])") + + +section \Overloaded syntax for dependent and nondependent pairs\ + +overloading + fst_dep \ fst + fst_nondep \ fst +begin + definition fst_dep :: "[Term, Typefam] \ Term" where + "fst_dep A B \ \<^bold>\p: (\x:A. B x). indSum[A,B] (\_. A) (\x y. x) p" + + definition fst_nondep :: "[Term, Term] \ Term" where + "fst_nondep A B \ \<^bold>\p: A \ B. indSum[A, \_. B] (\_. A) (\x y. x) p" +end + +overloading + snd_dep \ snd + snd_nondep \ snd +begin + definition snd_dep :: "[Term, Typefam] \ Term" where + "snd_dep A B \ \<^bold>\p: (\x:A. B x). indSum[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p" + + definition snd_nondep :: "[Term, Term] \ Term" where + "snd_nondep A B \ \<^bold>\p: A \ B. indSum[A, \_. B] (\_. B) (\x y. y) p" +end + + +section \Properties\ + +text "Typing judgments and computation rules for the dependent and non-dependent projection functions." + +lemma fst_dep_type: + assumes "p : \x:A. B x" + shows "fst[A,B]`p : A" + +proof \ \The standard reasoner knows to backchain with the product elimination rule here...\ + \ \Also write about this proof: compare the effect of letting the standard reasoner do simplifications, as opposed to using the minus switch and writing everything out explicitly from first principles.\ + + have *: "\x:A. B x : U" using assms .. + + show "fst[A,B]: (\x:A. B x) \ A" + + proof (unfold fst_dep_def, standard) \ \...and with the product introduction rule here...\ + show "\p. p : \x:A. B x \ indSum[A,B] (\_. A) (\x y. x) p : A" + + proof \ \...and with sum elimination here.\ + show "A : U" using * .. + qed + + qed (rule *) + +qed (rule assms) + + +lemma fst_dep_comp: (* Potential for automation *) + assumes "B: A \ U" and "a : A" and "b : B a" + shows "fst[A,B]`(a,b) \ a" + +proof - + \ "Write about this proof: unfolding, how we set up the introduction rules (explain \..\), do a trace of the proof, explain the meaning of keywords, etc." + + have *: "A : U" using assms(2) .. (* I keep thinking this should not have to be done explicitly, but rather automated. *) + + have "fst[A,B]`(a,b) \ indSum[A,B] (\_. A) (\x y. x) (a,b)" + proof (unfold fst_dep_def, standard) + show "\p. p : \x:A. B x \ indSum[A,B] (\_. A) (\x y. x) p : A" using * .. + show "(a,b) : \x:A. B x" using assms .. + qed + + also have "indSum[A,B] (\_. A) (\x y. x) (a,b) \ a" + by (rule Sum_comp) (rule *, assumption, (rule assms)+) + + finally show "fst[A,B]`(a,b) \ a" . +qed + + +text "In proving results about the second dependent projection function we often use the following two lemmas." + +lemma snd_dep_welltyped: + assumes "p : \x:A. B x" + shows "B (fst[A,B]`p) : U" + +proof - + have "\x:A. B x : U" using assms .. + then have *: "B: A \ U" .. + + have "fst[A,B]`p : A" using assms by (rule fst_dep_type) + then show "B (fst[A,B]`p) : U" by (rule *) +qed + + +lemma snd_dep_const_type: + assumes "B: A \ U" and "x : A" and "y : B x" + shows "y : B (fst[A,B]`(x,y))" + +proof - + have "fst[A,B]`(x,y) \ x" using assms by (rule fst_dep_comp) + then show "y : B (fst[A,B]`(x,y))" using assms by simp +qed + + +lemma snd_dep_type: + assumes "p : \x:A. B x" + shows "snd[A,B]`p : B (fst[A,B]`p)" + +proof + have *: "\x:A. B x : U" using assms .. + + show "snd[A, B] : \p:(\x:A. B x). B (fst[A,B]`p)" + + proof (unfold snd_dep_def, standard) + show "\p. p : \x:A. B x \ indSum[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p : B (fst[A,B]`p)" + + proof (standard, elim snd_dep_welltyped) + fix x y assume 1: "x : A" and 2: "y : B x" + show "y : B (fst[A,B]`(x,y))" + proof - + have "B: A \ U" using * .. + then show "y : B (fst[A,B]`(x,y))" using 1 2 by (rule snd_dep_const_type) + qed + qed + + qed (rule *) + +qed (rule assms) + + +lemma snd_dep_comp: + assumes "B: A \ U" and "a : A" and "b : B a" + shows "snd[A,B]`(a,b) \ b" + +proof - + have "snd[A,B]`(a,b) \ indSum[A, B] (\q. B (fst[A,B]`q)) (\x y. y) (a,b)" + proof (unfold snd_dep_def, standard) + show "(a,b) : \x:A. B x" using assms .. + + fix p assume *: "p : \x:A. B x" + show "indSum[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p : B (fst[A,B]`p)" + proof (standard, elim snd_dep_welltyped) + show "\x y. \x : A; y : B x\ \ y : B (fst[A,B]`(x,y))" using assms + by (elim snd_dep_const_type) + qed (rule *) + qed + + also have "indSum[A, B] (\q. B (fst[A,B]`q)) (\x y. y) (a,b) \ b" + proof (standard, elim snd_dep_welltyped) + show "\x y. \x : A; y : B x\ \ y : B (fst[A,B]`(x,y))" using assms + by (elim snd_dep_const_type) + qed (rule assms)+ + + finally show "snd[A,B]`(a,b) \ b" . +qed + + +text "For non-dependent projection functions:" + +print_statement fst_dep_type +print_statement fst_dep_type[where ?p = p and ?A = A and ?B = "\_. B"] + + +lemma fst_nondep_type: "p : A \ B \ fst[A,B]`p : A" +by (rule fst_dep_type[where ?B = "\_. B"]) + + +lemma fst_nondep_comp: + assumes "a : A" and "b : B" + shows "fst[A,B]`(a,b) \ a" +proof (unfold fst_nondep_def) + have "A : U" using assms(1) .. + then show "fst[A,B]`(a,b) \ a" unfolding fst_nondep_def +qed + +lemma snd_nondep_comp: "\a : A; b : B\ \ snd[A,B]`(a,b) \ b" +proof - + assume "a : A" and "b : B" + then have "(a, b) : A \ B" .. + then show "snd[A,B]`(a,b) \ b" unfolding snd_nondep_def by simp +qed + diff --git a/Sum.thy b/Sum.thy index 08c0de0..d5704ba 100644 --- a/Sum.thy +++ b/Sum.thy @@ -6,7 +6,7 @@ Dependent sum type. *) theory Sum - imports Prod + imports HoTT_Base begin axiomatization @@ -58,173 +58,4 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) where "A \ B \ \_:A. B" -section \Projection functions\ - -consts - fst :: "[Term, 'a] \ Term" ("(1fst[/_,/ _])") - snd :: "[Term, 'a] \ Term" ("(1snd[/_,/ _])") - -overloading - fst_dep \ fst - fst_nondep \ fst -begin - definition fst_dep :: "[Term, Typefam] \ Term" where - "fst_dep A B \ \<^bold>\p: (\x:A. B x). indSum[A,B] (\_. A) (\x y. x) p" - - definition fst_nondep :: "[Term, Term] \ Term" where - "fst_nondep A B \ \<^bold>\p: A \ B. indSum[A, \_. B] (\_. A) (\x y. x) p" -end - -overloading - snd_dep \ snd - snd_nondep \ snd -begin - definition snd_dep :: "[Term, Typefam] \ Term" where - "snd_dep A B \ \<^bold>\p: (\x:A. B x). indSum[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p" - - definition snd_nondep :: "[Term, Term] \ Term" where - "snd_nondep A B \ \<^bold>\p: A \ B. indSum[A, \_. B] (\_. B) (\x y. y) p" -end - -text "Typing judgments and computation rules for the dependent and non-dependent projection functions." - -lemma fst_dep_type: - assumes "p : \x:A. B x" - shows "fst[A,B]`p : A" - -proof \ \The standard reasoner knows to backchain with the product elimination rule here...\ - \ \Also write about this proof: compare the effect of letting the standard reasoner do simplifications, as opposed to using the minus switch and writing everything out explicitly from first principles.\ - - have *: "\x:A. B x : U" using assms .. - - show "fst[A,B]: (\x:A. B x) \ A" - - proof (unfold fst_dep_def, standard) \ \...and with the product introduction rule here...\ - show "\p. p : \x:A. B x \ indSum[A,B] (\_. A) (\x y. x) p : A" - - proof \ \...and with sum elimination here.\ - show "A : U" using * .. - qed - - qed (rule *) - -qed (rule assms) - - -lemma fst_dep_comp: (* Potential for automation *) - assumes "B: A \ U" and "a : A" and "b : B a" - shows "fst[A,B]`(a,b) \ a" - -proof - - \ "Write about this proof: unfolding, how we set up the introduction rules (explain \..\), do a trace of the proof, explain the meaning of keywords, etc." - - have *: "A : U" using assms(2) .. (* I keep thinking this should not have to be done explicitly, but rather automated. *) - - have "fst[A,B]`(a,b) \ indSum[A,B] (\_. A) (\x y. x) (a,b)" - proof (unfold fst_dep_def, standard) - show "\p. p : \x:A. B x \ indSum[A,B] (\_. A) (\x y. x) p : A" using * .. - show "(a,b) : \x:A. B x" using assms .. - qed - - also have "indSum[A,B] (\_. A) (\x y. x) (a,b) \ a" - by (rule Sum_comp) (rule *, assumption, (rule assms)+) - - finally show "fst[A,B]`(a,b) \ a" . -qed - - -text "In proving results about the second dependent projection function we often use the following two lemmas." - -lemma snd_dep_welltyped: - assumes "p : \x:A. B x" - shows "B (fst[A,B]`p) : U" -proof - - have "\x:A. B x : U" using assms .. - then have *: "B: A \ U" .. - - have "fst[A,B]`p : A" using assms by (rule fst_dep_type) - then show "B (fst[A,B]`p) : U" by (rule *) -qed - -lemma snd_dep_const_type: - assumes "B: A \ U" and "x : A" and "y : B x" - shows "y : B (fst[A,B]`(x,y))" -proof - - have "fst[A,B]`(x,y) \ x" using assms by (rule fst_dep_comp) - then show "y : B (fst[A,B]`(x,y))" using assms by simp -qed - - -lemma snd_dep_type: - assumes "p : \x:A. B x" - shows "snd[A,B]`p : B (fst[A,B]`p)" -proof - have *: "\x:A. B x : U" using assms .. - - show "snd[A, B] : \p:(\x:A. B x). B (fst[A,B]`p)" - - proof (unfold snd_dep_def, standard) - show "\p. p : \x:A. B x \ indSum[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p : B (fst[A,B]`p)" - - proof (standard, elim snd_dep_welltyped) - fix x y assume 1: "x : A" and 2: "y : B x" - show "y : B (fst[A,B]`(x,y))" - - proof - - have "B: A \ U" using * .. - then show "y : B (fst[A,B]`(x,y))" using 1 2 by (rule snd_dep_const_type) - qed - - qed - - qed (rule *) - -qed (rule assms) - - -lemma snd_dep_comp: - assumes "B: A \ U" and "a : A" and "b : B a" - shows "snd[A,B]`(a,b) \ b" -proof - - have "snd[A,B]`(a,b) \ indSum[A, B] (\q. B (fst[A,B]`q)) (\x y. y) (a,b)" - proof (unfold snd_dep_def, standard) - show "(a,b) : \x:A. B x" using assms .. - - fix p assume *: "p : \x:A. B x" - show "indSum[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p : B (fst[A,B]`p)" - proof (standard, elim snd_dep_welltyped) - show "\x y. \x : A; y : B x\ \ y : B (fst[A,B]`(x,y))" using assms - by (elim snd_dep_const_type) - qed (rule *) - qed - - also have "indSum[A, B] (\q. B (fst[A,B]`q)) (\x y. y) (a,b) \ b" - proof (standard, elim snd_dep_welltyped) - show "\x y. \x : A; y : B x\ \ y : B (fst[A,B]`(x,y))" using assms - by (elim snd_dep_const_type) - qed (rule assms)+ - - finally show "snd[A,B]`(a,b) \ b" . -qed - - -text "For non-dependent projection functions:" - -lemma fst_nondep_comp: - assumes "a : A" and "b : B" - shows "fst[A,B]`(a,b) \ a" -proof (unfold fst_nondep_def) - have "A : U" using assms(1) .. - then show "fst[A,B]`(a,b) \ a" unfolding fst_nondep_def -qed - -lemma snd_nondep_comp: "\a : A; b : B\ \ snd[A,B]`(a,b) \ b" -proof - - assume "a : A" and "b : B" - then have "(a, b) : A \ B" .. - then show "snd[A,B]`(a,b) \ b" unfolding snd_nondep_def by simp -qed - - - end \ No newline at end of file -- cgit v1.2.3