From 21077433667f6c2281aa522f170b93bb0c8c23ea Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 18 Jun 2018 17:16:30 +0200 Subject: Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Added type formation rules expressing necessity of the conditions. --- HoTT_Base.thy | 3 +- Prod.thy | 18 ++++++++--- Sum.thy | 97 +++++++++++++++++++++++++++++++++++++++++++++++++---------- 3 files changed, 95 insertions(+), 23 deletions(-) diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 7794601..a0078fa 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -7,7 +7,6 @@ Basic setup and definitions of a homotopy type theory object logic without unive theory HoTT_Base imports Pure - begin section \Setup\ @@ -34,7 +33,7 @@ consts is_of_type :: "[Term, Term] \ prop" ("(1_ :/ _)" [0, 0] 1000) axiomatization where - inhabited_implies_type [intro]: "\a A. a : A \ A : U" + inhabited_implies_type [intro, elim]: "\a A. a : A \ A : U" section \Type families\ diff --git a/Prod.thy b/Prod.thy index bfb4f42..7facc27 100644 --- a/Prod.thy +++ b/Prod.thy @@ -7,7 +7,6 @@ Dependent product (function) type for the HoTT logic. theory Prod imports HoTT_Base - begin axiomatization @@ -37,7 +36,11 @@ translations section \Type rules\ axiomatization where - Prod_form: "\A B. \A : U; B : A \ U\ \ \x:A. B x : U" + Prod_form: "\A B. \A : U; B: A \ U\ \ \x:A. B x : U" +and + Prod_form_cond1: "\A B. (\x:A. B x : U) \ A : U" +and + Prod_form_cond2: "\A B. (\x:A. B x : U) \ B: A \ U" and Prod_intro: "\A B b. \A : U; \x. x : A \ b x : B x\ \ \<^bold>\x:A. b x : \x:A. B x" and @@ -47,11 +50,16 @@ and and Prod_uniq: "\A B f. f : \x:A. B x \ \<^bold>\x:A. (f`x) \ f" -text "The type rules should be able to be used as introduction rules by the standard reasoner:" +text "Note that the syntax \\<^bold>\\ (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \
2.5.2 of the Isabelle/Isar Implementation)." + +text "In textbook presentations it is usual to present type formation as a forward implication, stating conditions sufficient for the formation of the type. +It is however implicit that the premises of the rule are also necessary, so that for example the only way for one to have that \\x:A. B x : U\ is for \A : U\ and \B: A \ U\ in the first place. +This is what the additional formation rules \Prod_form_cond1\ and \Prod_form_cond2\ express." -lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq +text "The type rules should be able to be used as introduction and elimination rules by the standard reasoner:" -text "Note that the syntax \\<^bold>\\ (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \
2.5.2 of the Isabelle/Isar Implementation)." +lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq +lemmas Prod_form_conds [elim] = Prod_form_cond1 Prod_form_cond2 text "Nondependent functions are a special case." diff --git a/Sum.thy b/Sum.thy index 8e7ccd6..0a062cf 100644 --- a/Sum.thy +++ b/Sum.thy @@ -7,7 +7,6 @@ Dependent sum type. theory Sum imports Prod - begin axiomatization @@ -31,6 +30,10 @@ section \Type rules\ axiomatization where Sum_form: "\A B. \A : U; B: A \ U\ \ \x:A. B x : U" +and + Sum_form_cond1: "\A B. (\x:A. B x : U) \ A : U" +and + Sum_form_cond2: "\A B. (\x:A. B x : U) \ B: A \ U" and Sum_intro: "\A B a b. \B: A \ U; a : A; b : B a\ \ (a,b) : \x:A. B x" and @@ -48,6 +51,7 @@ and \ \ indSum[A,B] C f (a,b) \ f a b" lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp +lemmas Sum_form_conds [elim] = Sum_form_cond1 Sum_form_cond2 \ \Nondependent pair\ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) @@ -76,44 +80,104 @@ overloading snd_nondep \ snd begin definition snd_dep :: "[Term, Typefam] \ Term" where - "snd_dep A B \ \<^bold>\p: (\x:A. B x). indSum[A,B] (\p. B fst[A,B]`p) (\x y. y) p" + "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 "Simplifying projections:" +text "Results about projections:" + +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 (unfold fst_dep_def) + +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. *) - - then have "\p. p : \x:A. B x \ indSum[A,B] (\_. A) (\x y. x) p : A" .. - - moreover have "(a,b) : \x:A. B x" using assms .. - - ultimately have "(\<^bold>\p: (\x:A. B x). indSum[A,B] (\_. A) (\x y. x) p)`(a,b) \ - indSum[A,B] (\_. A) (\x y. x) (a,b)" .. + + 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 "(\<^bold>\p: (\x:A. B x). indSum[A,B] (\_. A) (\x y. x) p)`(a,b) \ a" . + finally show "fst[A,B]`(a,b) \ a" . qed + +lemma snd_dep_type: + assumes "p : \x:A. B x" + shows "snd[A,B]`p : B (fst[A,B]`p)" +oops +\ \Do we need this for the following lemma?\ + + lemma snd_dep_comp: - assumes "a : A" and "b : B a" + assumes "B: A \ U" and "a : A" and "b : B a" shows "snd[A,B]`(a,b) \ b" proof - - have "\p. B fst[A,B]`p: \x:A. B x \ U" - - show "snd[A,B]`(a,b) \ b" unfolding fst_dep_def + \ \We use the following two lemmas:\ + + have lemma1: "\p. p : \x:A. B x \ B (fst[A,B]`p) : U" + proof - + fix p assume "p : \x:A. B x" + then have "fst[A,B]`p : A" by (rule fst_dep_type) + then show "B (fst[A,B]`p) : U" by (rule assms(1)) + qed + + have lemma2: "\x y. \x : A; y : B x\ \ y : B (fst[A,B]`(x, y))" + proof - + fix x y assume "x : A" and "y : B x" + moreover with assms(1) have "fst[A,B]`(x,y) \ x" by (rule fst_dep_comp) + ultimately show "y : B (fst[A,B]`(x,y))" by simp + qed + + \ \And now the 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)" + by (standard, elim lemma1, elim lemma2) (assumption, rule *) + qed + + also have "indSum[A, B] (\q. B (fst[A,B]`q)) (\x y. y) (a,b) \ b" + by (standard, elim lemma1, elim lemma2) (assumption, (rule assms)+) + + finally show "snd[A,B]`(a,b) \ b" . qed + lemma fst_nondep_comp: assumes "a : A" and "b : B" shows "fst[A,B]`(a,b) \ a" @@ -131,4 +195,5 @@ qed lemmas proj_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp + end \ No newline at end of file -- cgit v1.2.3