From 7a89ec1e72f61179767c6488177c6d12e69388c5 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 12 Aug 2018 13:04:16 +0200 Subject: Commit before testing polymorphic equality eliminator --- Coprod.thy | 10 +++++----- Equal.thy | 20 ++++++++++---------- EqualProps.thy | 29 ++++++++++++++++------------- HoTT_Base.thy | 1 + HoTT_Methods.thy | 4 ++-- Prod.thy | 22 ++++++++++++---------- Proj.thy | 45 +++++++++++++++++++++++++++++++++++++++++++-- Sum.thy | 27 +++++++++++++-------------- scratch.thy | 6 ++++++ 9 files changed, 108 insertions(+), 56 deletions(-) diff --git a/Coprod.thy b/Coprod.thy index a301e7e..d47c24e 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -44,17 +44,17 @@ and \y. y: B \ d(y): C(inr(y)); b: B \ \ ind\<^sub>+(c)(d)(inr(b)) \ d(b)" - +(* text "Admissible formation inference rules:" axiomatization where Coprod_form_cond1: "\i A B. A + B: U(i) \ A: U(i)" and Coprod_form_cond2: "\i A B. A + B: U(i) \ B: U(i)" - -lemmas Coprod_rules [intro] = Coprod_form Coprod_intro1 Coprod_intro2 - Coprod_elim Coprod_comp1 Coprod_comp2 -lemmas Coprod_form_conds [intro] = Coprod_form_cond1 Coprod_form_cond2 +*) +lemmas Coprod_rules [intro] = + Coprod_form Coprod_intro1 Coprod_intro2 Coprod_elim Coprod_comp1 Coprod_comp2 +(*lemmas Coprod_form_conds [intro] = Coprod_form_cond1 Coprod_form_cond2 *) lemmas Coprod_comps [comp] = Coprod_comp1 Coprod_comp2 diff --git a/Equal.thy b/Equal.thy index 8bd7875..d910bb8 100644 --- a/Equal.thy +++ b/Equal.thy @@ -28,11 +28,11 @@ translations section \Type rules\ axiomatization where - Equal_form: "\i A a b. \A: U(i); a: A; b: A\ \ a =\<^sub>A b : U(i)" + Equal_form: "\A: U(i); a: A; b: A\ \ a =\<^sub>A b : U(i)" and - Equal_intro: "\A a. a : A \ refl(a): a =\<^sub>A a" + Equal_intro: "a : A \ refl(a): a =\<^sub>A a" and - Equal_elim: "\i A C f a b p. \ + Equal_elim: "\ \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i); \x. x: A \ f(x) : C(x)(x)(refl x); a: A; @@ -40,23 +40,23 @@ and p: a =\<^sub>A b \ \ ind\<^sub>=(f)(a)(b)(p) : C(a)(b)(p)" and - Equal_comp: "\i A C f a. \ + Equal_comp: "\ \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i); \x. x: A \ f(x) : C(x)(x)(refl x); a: A \ \ ind\<^sub>=(f)(a)(a)(refl(a)) \ f(a)" text "Admissible inference rules for equality type formation:" - +(* axiomatization where - Equal_form_cond1: "\i A a b. a =\<^sub>A b: U(i) \ A: U(i)" + Equal_form_cond1: "a =\<^sub>A b: U(i) \ A: U(i)" and - Equal_form_cond2: "\i A a b. a =\<^sub>A b: U(i) \ a: A" + Equal_form_cond2: "a =\<^sub>A b: U(i) \ a: A" and - Equal_form_cond3: "\i A a b. a =\<^sub>A b: U(i) \ b: A" - + Equal_form_cond3: "a =\<^sub>A b: U(i) \ b: A" +*) lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -lemmas Equal_form_conds [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 +(*lemmas Equal_form_conds [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3*) lemmas Equal_comps [comp] = Equal_comp diff --git a/EqualProps.thy b/EqualProps.thy index 17c7fa6..9d23a99 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -15,20 +15,25 @@ 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" +definition inv :: "[Term, Term] \ (Term \ Term)" ("(1inv[_,/ _])") + where "inv[x,y] \ \p. ind\<^sub>= (\x. refl(x)) x y p" lemma inv_type: - assumes "A : U(i)" and "x : A" and "y : A" shows "inv[A,x,y] : x =\<^sub>A y \ y =\<^sub>A x" - unfolding inv_def - by (derive lems: assms) + assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "inv[x,y](p): y =\<^sub>A x" +unfolding inv_def +proof + show "\x y. \x: A; y: A\ \ y =\<^sub>A x: U(i)" using assms(1) .. + show "\x. x: A \ refl x: x =\<^sub>A x" .. +qed (fact assms)+ -corollary assumes "x =\<^sub>A y : U(i)" and "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x" - by (derive lems: inv_type assms) -lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[A,a,a]`refl(a) \ refl(a)" - unfolding inv_def by (simplify lems: assms) +lemma inv_comp: assumes "A : U(i)" and "a : A" shows "inv[a,a](refl(a)) \ refl(a)" +unfolding inv_def +proof + show "\x. x: A \ refl x: x =\<^sub>A x" .. + show "\x. x: A \ x =\<^sub>A x: U(i)" using assms(1) .. +qed (fact assms) section \Transitivity / Path composition\ @@ -42,10 +47,8 @@ definition rcompose :: "Term \ Term" ("(1rcompose[_])") x y p" -text "``Natural'' composition function, of type \\x,y,z:A. x =\<^sub>A y \ y =\<^sub>A z \ x =\<^sub>A z\." - -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). rcompose[A]`x`y`p`z`q" +definition compose :: "[Term, Term, Term] \ [Term, Term] \ Term" ("(1compose[ _,/ _,/ _])") + where "compose[x,y,z] \ \p." lemma compose_type: diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 614419e..e94ca5c 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -56,6 +56,7 @@ and U_cumulative: "\A i j. \A: U(i); i <- j\ \ A: U(j)" \ \WARNING: \rule Universe_cumulative\ can result in an infinite rewrite loop!\ + section \Type families\ text " diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 8351c3c..f80b99b 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -57,9 +57,9 @@ method derive uses lems unfolds = ( unfold unfolds | simple lems: lems | match lems in lem: "?X : ?Y" \ \wellformed jdgmt: lem\ | - rule U_hierarchy | + rule U_hierarchy (*| (rule U_cumulative, simple lems: lems) | - (rule U_cumulative, match lems in lem: "?X : ?Y" \ \wellformed jdgmt: lem\) + (rule U_cumulative, match lems in lem: "?X : ?Y" \ \wellformed jdgmt: lem\)*) )+ diff --git a/Prod.thy b/Prod.thy index 01cd006..5391943 100644 --- a/Prod.thy +++ b/Prod.thy @@ -41,20 +41,21 @@ abbreviation Function :: "[Term, Term] \ Term" (infixr "\Type rules\ axiomatization where - Prod_form: "\i A B. \A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" + Prod_form: "\A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" and - Prod_intro: "\i A B b. \A: U(i); B: A \ U(i); \x. x: A \ b(x): B(x)\ \ \<^bold>\x:A. b(x): \x:A. B(x)" + Prod_intro: "\A: U(i); \x. x: A \ b(x): B(x)\ \ \<^bold>\x:A. b(x): \x:A. B(x)" and - Prod_elim: "\A B f a. \f: \x:A. B(x); a: A\ \ f`a: B(a)" + Prod_elim: "\f: \x:A. B(x); a: A\ \ f`a: B(a)" and - Prod_comp: "\i A B b a. \A: U(i); B: A \ U(i); \x. x: A \ b(x): B(x); a: A\ \ (\<^bold>\x:A. b(x))`a \ b(a)" + Prod_comp: "\a: A; \x. x: A \ b(x): B(x)\ \ (\<^bold>\x:A. b(x))`a \ b(a)" and - Prod_uniq: "\A B f. f : \x:A. B(x) \ \<^bold>\x:A. (f`x) \ f" + Prod_uniq: "f : \x:A. B(x) \ \<^bold>\x:A. (f`x) \ f" 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 addition to the usual type rules, it is a meta-theorem (*PROVE THIS!*) that whenever \\x:A. B x: U(i)\ is derivable from some set of premises \, then so are \A: U(i)\ and \B: A \ U(i)\. @@ -62,14 +63,15 @@ text " " axiomatization where - Prod_form_cond1: "\i A B. (\x:A. B(x): U(i)) \ A: U(i)" + Prod_form_cond1: "(\x:A. B(x): U(i)) \ A: U(i)" and - Prod_form_cond2: "\i A B. (\x:A. B(x): U(i)) \ B: A \ U(i)" + Prod_form_cond2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" +*) text "Set up the standard reasoner to use the type rules:" lemmas Prod_rules = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq -lemmas Prod_form_conds [intro (*elim, wellform*)] = Prod_form_cond1 Prod_form_cond2 +(*lemmas Prod_form_conds [intro (*elim, wellform*)] = Prod_form_cond1 Prod_form_cond2*) lemmas Prod_comps [comp] = Prod_comp Prod_uniq @@ -84,9 +86,9 @@ where and Unit_intro: "\: \" and - Unit_elim: "\i C c a. \C: \ \ U(i); c: C(\); a: \\ \ ind\<^sub>\(c)(a) : C(a)" + Unit_elim: "\C: \ \ U(i); c: C(\); a: \\ \ ind\<^sub>\(c)(a) : C(a)" and - Unit_comp: "\i C c. \C: \ \ U(i); c: C(\)\ \ ind\<^sub>\(c)(\) \ c" + Unit_comp: "\C: \ \ U(i); c: C(\)\ \ ind\<^sub>\(c)(\) \ c" lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp lemmas Unit_comps [comp] = Unit_comp diff --git a/Proj.thy b/Proj.thy index 717df65..b1c21c1 100644 --- a/Proj.thy +++ b/Proj.thy @@ -18,8 +18,49 @@ abbreviation snd :: "Term \ Term" where "snd \ \p. in text "Typing judgments and computation rules for the dependent and non-dependent projection functions." -lemma assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "fst(p): A" - by (derive lems: assms + +lemma fst_type: + assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "fst(p): A" +proof + show "A: U(i)" using assms(1) by (rule Sum_forms) +qed (fact assms | assumption)+ + + +lemma fst_comp: + assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "fst() \ a" +proof + show "\x. x: A \ x: A" . +qed (rule assms)+ + + +lemma snd_type: + assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "snd(p): B(fst p)" +proof + show "\p. p: \x:A. B(x) \ B(fst p): U(i)" + proof - + have "\p. p: \x:A. B(x) \ fst(p): A" using assms(1) by (rule fst_type) + with assms(1) show "\p. p: \x:A. B(x) \ B(fst p): U(i)" by (rule Sum_forms) + qed + + fix x y + assume asm: "x: A" "y: B(x)" + show "y: B(fst )" + proof (subst fst_comp) + show "A: U(i)" using assms(1) by (rule Sum_forms) + show "\x. x: A \ B(x): U(i)" using assms(1) by (rule Sum_forms) + qed (rule asm)+ +qed (fact assms) + + +lemma snd_comp: + assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "snd() \ b" +proof + show "\x y. y: B(x) \ y: B(x)" . + show "a: A" by (fact assms) + show "b: B(a)" by (fact assms) + show *: "B(a): U(i)" using assms(3) by (rule assms(2)) + show "B(a): U(i)" by (fact *) +qed end \ No newline at end of file diff --git a/Sum.thy b/Sum.thy index cdfe5bd..eddb464 100644 --- a/Sum.thy +++ b/Sum.thy @@ -14,7 +14,7 @@ section \Constants and syntax\ axiomatization Sum :: "[Term, Typefam] \ Term" and - pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and + pair :: "[Term, Term] \ Term" ("(1<_,/ _>)") and indSum :: "[[Term, Term] \ Term, Term] \ Term" ("(1ind\<^sub>\)") syntax @@ -34,34 +34,33 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) section \Type rules\ axiomatization where - Sum_form: "\i A B. \A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" + Sum_form: "\A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" and - Sum_intro: "\i A B a b. \A: U(i); B: A \ U(i); a: A; b: B(a)\ \ (a,b) : \x:A. B(x)" + Sum_intro: "\B: A \ U(i); a: A; b: B(a)\ \ : \x:A. B(x)" and - Sum_elim: "\i A B C f p. \ + Sum_elim: "\ C: \x:A. B(x) \ U(i); - \x y. \x: A; y: B(x)\ \ f(x)(y) : C((x,y)); + \x y. \x: A; y: B(x)\ \ f(x)(y) : C(); p : \x:A. B(x) \ \ ind\<^sub>\(f)(p) : C(p)" (* What does writing \x y. f(x, y) change? *) and - Sum_comp: "\i A B C f a b. \ - A: U(i); - B: A \ U(i); + Sum_comp: "\ C: \x:A. B(x) \ U(i); - \x y. \x: A; y :B(x)\ \ f(x)(y) : C((x,y)); + B: A \ U(i); + \x y. \x: A; y: B(x)\ \ f(x)(y) : C(); a: A; b: B(a) - \ \ ind\<^sub>\(f)((a,b)) \ f(a)(b)" + \ \ ind\<^sub>\(f)() \ f(a)(b)" text "Admissible inference rules for sum formation:" axiomatization where - Sum_form_cond1: "\i A B. (\x:A. B(x): U(i)) \ A: U(i)" + Sum_form_cond1: "(\x:A. B(x): U(i)) \ A: U(i)" and - Sum_form_cond2: "\i A B. (\x:A. B(x): U(i)) \ B: A \ U(i)" + Sum_form_cond2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp -lemmas Sum_form_conds [intro (*elim, wellform*)] = Sum_form_cond1 Sum_form_cond2 +lemmas Sum_forms = Sum_form Sum_form_cond1 Sum_form_cond2 lemmas Sum_comps [comp] = Sum_comp @@ -73,7 +72,7 @@ axiomatization where Empty_form: "\ : U(O)" and - Empty_elim: "\i C z. \C: \ \ U(i); z: \\ \ ind\<^sub>\(z): C(z)" + Empty_elim: "\C: \ \ U(i); z: \\ \ ind\<^sub>\(z): C(z)" lemmas Empty_rules [intro] = Empty_form Empty_elim diff --git a/scratch.thy b/scratch.thy index e06fb7e..3141120 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,6 +3,12 @@ theory scratch begin + +lemma "U(O): U(O)" +proof (rule inhabited_implies_type) + show "\: U(O)" .. +qed + lemma assumes "\x:A. B(x): U(i)" "(a,b): \x:A. B(x)" shows "a : A" -- cgit v1.2.3