From e1be5f97bb2a42b3179bc24b118d69af137f8e5d Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 18 Aug 2018 21:28:21 +0200 Subject: Regrouping type rules --- Coprod.thy | 26 +++++++++++++------------- Equal.thy | 28 +++++++++++++--------------- EqualProps.thy | 3 +-- HoTT.thy | 21 ++++++++++++++++----- HoTT_Base.thy | 1 - HoTT_Methods.thy | 5 ++--- Nat.thy | 19 +++++++++---------- Prod.thy | 24 ++++++++++++------------ ProdProps.thy | 3 +-- Proj.thy | 9 ++++----- Sum.thy | 36 +++++++++++++++++++----------------- ex/HoTT book/Ch1.thy | 3 +-- ex/Methods.thy | 3 +-- ex/Synthesis.thy | 7 +++---- tests/Subgoal.thy | 10 +--------- tests/Test.thy | 12 ++++++------ 16 files changed, 102 insertions(+), 108 deletions(-) diff --git a/Coprod.thy b/Coprod.thy index a444c89..f62bb06 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -1,8 +1,7 @@ (* Title: HoTT/Coprod.thy Author: Josh Chen - Date: Aug 2018 -Coproduct type. +Coproduct type *) theory Coprod @@ -20,9 +19,9 @@ axiomatization where Coprod_form: "\A: U(i); B: U(i)\ \ A + B: U(i)" and - Coprod_intro1: "\a: A; B: U(i)\ \ inl(a): A + B" + Coprod_intro_inl: "\a: A; B: U(i)\ \ inl(a): A + B" and - Coprod_intro2: "\b: B; A: U(i)\ \ inr(b): A + B" + Coprod_intro_inr: "\b: B; A: U(i)\ \ inr(b): A + B" and Coprod_elim: "\ C: A + B \ U(i); @@ -31,14 +30,14 @@ and u: A + B \ \ ind\<^sub>+(c)(d)(u) : C(u)" and - Coprod_comp1: "\ + Coprod_comp_inl: "\ C: A + B \ U(i); \x. x: A \ c(x): C(inl(x)); \y. y: B \ d(y): C(inr(y)); a: A \ \ ind\<^sub>+(c)(d)(inl(a)) \ c(a)" and - Coprod_comp2: "\ + Coprod_comp_inr: "\ C: A + B \ U(i); \x. x: A \ c(x): C(inl(x)); \y. y: B \ d(y): C(inr(y)); @@ -49,17 +48,18 @@ and text "Admissible formation inference rules:" axiomatization where - Coprod_form_cond1: "A + B: U(i) \ A: U(i)" + Coprod_wellform1: "A + B: U(i) \ A: U(i)" and - Coprod_form_cond2: "A + B: U(i) \ B: U(i)" + Coprod_wellform2: "A + B: U(i) \ B: U(i)" -text "Rule declarations:" +text "Rule attribute declarations:" -lemmas Coprod_intro = Coprod_intro1 Coprod_intro2 -lemmas Coprod_rules [intro] = Coprod_form Coprod_intro Coprod_elim Coprod_comp1 Coprod_comp2 -lemmas Coprod_form_conds [wellform] = Coprod_form_cond1 Coprod_form_cond2 -lemmas Coprod_comps [comp] = Coprod_comp1 Coprod_comp2 +lemmas Coprod_intro = Coprod_intro_inl Coprod_intro_inr + +lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr +lemmas Coprod_wellform [wellform] = Coprod_wellform1 Coprod_wellform2 +lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_comp Coprod_elim end diff --git a/Equal.thy b/Equal.thy index 11a966b..722a9b9 100644 --- a/Equal.thy +++ b/Equal.thy @@ -1,8 +1,7 @@ (* Title: HoTT/Equal.thy Author: Josh Chen - Date: Jun 2018 -Equality type. +Equality type *) theory Equal @@ -33,36 +32,35 @@ and Equal_intro: "a : A \ refl(a): a =\<^sub>A a" and 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); x: A; y: A; - p: x =\<^sub>A y + p: x =\<^sub>A y; + \x. x: A \ f(x) : C(x)(x)(refl x); + \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i) \ \ ind\<^sub>=(f)(p) : C(x)(y)(p)" and Equal_comp: "\ - \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i); + a: A; \x. x: A \ f(x) : C(x)(x)(refl x); - a: A + \x y. \x: A; y: A\ \ C(x)(y): x =\<^sub>A y \ U(i) \ \ ind\<^sub>=(f)(refl(a)) \ f(a)" text "Admissible inference rules for equality type formation:" axiomatization where - Equal_form_cond1: "a =\<^sub>A b: U(i) \ A: U(i)" + Equal_wellform1: "a =\<^sub>A b: U(i) \ A: U(i)" and - Equal_form_cond2: "a =\<^sub>A b: U(i) \ a: A" + Equal_wellform2: "a =\<^sub>A b: U(i) \ a: A" and - Equal_form_cond3: "a =\<^sub>A b: U(i) \ b: A" - + Equal_wellform3: "a =\<^sub>A b: U(i) \ b: A" -text "Rule declarations:" -lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -lemmas Equal_wellform [wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 -lemmas Equal_comps [comp] = Equal_comp +text "Rule attribute declarations:" +lemmas Equal_comp [comp] +lemmas Equal_wellform [wellform] = Equal_wellform1 Equal_wellform2 Equal_wellform3 +lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_comp Equal_elim end diff --git a/EqualProps.thy b/EqualProps.thy index 3c9b971..8b83c5b 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -1,8 +1,7 @@ (* Title: HoTT/EqualProps.thy Author: Josh Chen - Date: Aug 2018 -Properties of equality. +Properties of equality *) theory EqualProps diff --git a/HoTT.thy b/HoTT.thy index 724eebc..789eed2 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -1,7 +1,7 @@ (* Title: HoTT/HoTT.thy Author: Josh Chen -Load all the component modules for the HoTT logic. +Homotopy type theory *) theory HoTT @@ -12,15 +12,26 @@ HoTT_Base HoTT_Methods (* Types *) -Prod -Sum -Equal Coprod +Equal Nat +Prod +Sum -(* Additional properties *) +(* Derived definitions and properties *) EqualProps +ProdProps Proj begin + +lemmas form_rules = + Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form +lemmas intro_rules = + Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro +lemmas elim_rules = + Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim +lemmas routine_rules = + Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine + end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 1b8c526..a229e83 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,6 +1,5 @@ (* Title: HoTT/HoTT_Base.thy Author: Josh Chen - Date: Aug 2018 Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell. *) diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 316841d..4d2174b 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -1,6 +1,5 @@ (* Title: HoTT/HoTT_Methods.thy Author: Josh Chen - Date: Jun 2018 Method setup for the HoTT library. Relies heavily on Eisbach. *) @@ -18,7 +17,7 @@ section \Method definitions\ subsection \Simple type rule proof search\ text " - Prove type judgments \A : U\ and inhabitation judgments \a : A\ using the type rules declared [intro] and [elim] (in the respective theory files), as well as additional provided lemmas. + Prove type judgments \A : U\ and inhabitation judgments \a : A\ using the type rules declared [intro] in the respective theory files, as well as additional provided lemmas. Can also perform typechecking, and search for elements of a type. " @@ -62,7 +61,7 @@ ML_file "~~/src/Tools/eqsubst.ML" text "Perform basic single-step computations:" -method compute uses lems = (subst lems comp) +method compute uses lems = (subst lems comp | rule lems comp) end diff --git a/Nat.thy b/Nat.thy index 05b0bfe..b48804a 100644 --- a/Nat.thy +++ b/Nat.thy @@ -1,8 +1,7 @@ (* Title: HoTT/Nat.thy Author: Josh Chen - Date: Aug 2018 -Natural numbers. +Natural numbers *) theory Nat @@ -20,9 +19,9 @@ axiomatization where Nat_form: "\: U(O)" and - Nat_intro1: "0: \" + Nat_intro_0: "0: \" and - Nat_intro2: "n: \ \ succ(n): \" + Nat_intro_succ: "n: \ \ succ(n): \" and Nat_elim: "\ C: \ \ U(i); @@ -31,13 +30,13 @@ and n: \ \ \ ind\<^sub>\(f)(a)(n): C(n)" and - Nat_comp1: "\ + Nat_comp_0: "\ C: \ \ U(i); \n c. \n: \; c: C(n)\ \ f(n)(c): C(succ n); a: C(0) \ \ ind\<^sub>\(f)(a)(0) \ a" and - Nat_comp2: "\ + Nat_comp_succ: "\ C: \ \ U(i); \n c. \n: \; c: C(n)\ \ f(n)(c): C(succ n); a: C(0); @@ -45,11 +44,11 @@ and \ \ ind\<^sub>\(f)(a)(succ n) \ f(n)(ind\<^sub>\ f a n)" -text "Rule declarations:" +text "Rule attribute declarations:" -lemmas Nat_intro = Nat_intro1 Nat_intro2 -lemmas Nat_rules [intro] = Nat_form Nat_intro Nat_elim Nat_comp1 Nat_comp2 -lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 +lemmas Nat_intro = Nat_intro_0 Nat_intro_succ +lemmas Nat_comp [comp] = Nat_comp_0 Nat_comp_succ +lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_comp Nat_elim end diff --git a/Prod.thy b/Prod.thy index 8c94ec6..323bef4 100644 --- a/Prod.thy +++ b/Prod.thy @@ -1,8 +1,7 @@ (* Title: HoTT/Prod.thy Author: Josh Chen - Date: Aug 2018 -Dependent product (function) type. +Dependent product (function) type *) theory Prod @@ -39,11 +38,11 @@ section \Type rules\ axiomatization where Prod_form: "\A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" and - Prod_intro: "\A: U(i); \x. x: A \ b(x): B(x)\ \ \<^bold>\x. b(x): \x:A. B(x)" + Prod_intro: "\\x. x: A \ b(x): B(x); A: U(i)\ \ \<^bold>\x. b(x): \x:A. B(x)" and Prod_elim: "\f: \x:A. B(x); a: A\ \ f`a: B(a)" and - Prod_comp: "\\x. x: A \ b(x): B(x); a: A\ \ (\<^bold>\x. b(x))`a \ b(a)" + Prod_appl: "\\x. x: A \ b(x): B(x); a: A\ \ (\<^bold>\x. b(x))`a \ b(a)" and Prod_uniq: "f : \x:A. B(x) \ \<^bold>\x. (f`x) \ f" and @@ -62,15 +61,16 @@ text " " axiomatization where - Prod_form_cond1: "(\x:A. B(x): U(i)) \ A: U(i)" + Prod_wellform1: "(\x:A. B(x): U(i)) \ A: U(i)" and - Prod_form_cond2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" + Prod_wellform2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" -text "Set up the standard reasoner to use the type rules:" -lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq Prod_eq -lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2 -lemmas Prod_comps [comp] = Prod_comp Prod_uniq Prod_eq +text "Rule attribute declarations---set up various methods to use the type rules." + +lemmas Prod_comp [comp] = Prod_appl Prod_uniq +lemmas Prod_wellform [wellform] = Prod_wellform1 Prod_wellform2 +lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_comp Prod_elim section \Function composition\ @@ -96,8 +96,8 @@ and and 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 +lemmas Unit_comp [comp] +lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_comp Unit_elim end diff --git a/ProdProps.thy b/ProdProps.thy index adadb29..3e51102 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -1,8 +1,7 @@ (* Title: HoTT/ProdProps.thy Author: Josh Chen - Date: Aug 2018 -Properties of the dependent product. +Properties of the dependent product *) theory ProdProps diff --git a/Proj.thy b/Proj.thy index 291113d..dffc127 100644 --- a/Proj.thy +++ b/Proj.thy @@ -1,6 +1,5 @@ (* Title: HoTT/Proj.thy Author: Josh Chen - Date: Jun 2018 Projection functions \fst\ and \snd\ for the dependent sum type. *) @@ -27,7 +26,7 @@ lemma fst_comp: unfolding fst_def proof show "a: A" and "b: B(a)" by fact+ -qed (rule assms)+ +qed (simple lems: assms)+ lemma snd_type: assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "snd(p): B(fst p)" @@ -54,10 +53,10 @@ proof qed (simple lems: assms) -text "Rule declarations:" +text "Rule attribute declarations:" -lemmas Proj_types [intro] = fst_type snd_type -lemmas Proj_comps [comp] = fst_comp snd_comp +lemmas Proj_type [intro] = fst_type snd_type +lemmas Proj_comp [comp] = fst_comp snd_comp end diff --git a/Sum.thy b/Sum.thy index 8522af1..dce5834 100644 --- a/Sum.thy +++ b/Sum.thy @@ -1,8 +1,7 @@ (* Title: HoTT/Sum.thy Author: Josh Chen - Date: Jun 2018 -Dependent sum type. +Dependent sum type *) theory Sum @@ -36,32 +35,35 @@ section \Type rules\ axiomatization where Sum_form: "\A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" and - Sum_intro: "\B: A \ U(i); a: A; b: B(a)\ \ : \x:A. B(x)" + Sum_intro: "\B: A \ U(i); a: A; b: B(a)\ \ : \x:A. B(x)" and Sum_elim: "\ - C: \x:A. B(x) \ U(i); - \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? *) + p: \x:A. B(x); + \x y. \x: A; y: B(x)\ \ f(x)(y): C(); + C: \x:A. B(x) \ U(i) + \ \ ind\<^sub>\(f)(p): C(p)" (* What does writing \x y. f(x, y) change? *) and Sum_comp: "\ - C: \x:A. B(x) \ U(i); - B: A \ U(i); - \x y. \x: A; y: B(x)\ \ f(x)(y) : C(); a: A; - b: B(a) + b: B(a); + \x y. \x: A; y: B(x)\ \ f(x)(y): C(); + B: A \ U(i); + C: \x:A. B(x) \ U(i) \ \ ind\<^sub>\(f)() \ f(a)(b)" text "Admissible inference rules for sum formation:" axiomatization where - Sum_form_cond1: "(\x:A. B(x): U(i)) \ A: U(i)" + Sum_wellform1: "(\x:A. B(x): U(i)) \ A: U(i)" and - Sum_form_cond2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" + Sum_wellform2: "(\x:A. B(x): U(i)) \ B: A \ U(i)" + + +text "Rule attribute declarations:" -lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp -lemmas Sum_wellform [wellform] = Sum_form_cond1 Sum_form_cond2 -lemmas Sum_comps [comp] = Sum_comp +lemmas Sum_comp [comp] +lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2 +lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_comp Sum_elim section \Empty type\ @@ -74,7 +76,7 @@ where and Empty_elim: "\C: \ \ U(i); z: \\ \ ind\<^sub>\(z): C(z)" -lemmas Empty_rules [intro] = Empty_form Empty_elim +lemmas Empty_routine [intro] = Empty_form Empty_elim end diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy index cc0adf5..d5f05dd 100644 --- a/ex/HoTT book/Ch1.thy +++ b/ex/HoTT book/Ch1.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/HoTT book/Ch1.thy Author: Josh Chen - Date: Aug 2018 A formalization of some content of Chapter 1 of the Homotopy Type Theory book. *) @@ -41,4 +40,4 @@ proof (rule Sum_elim[where ?p=p]) qed (derive lems: assms) -end \ No newline at end of file +end diff --git a/ex/Methods.thy b/ex/Methods.thy index 871964f..415fbc3 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/Methods.thy Author: Josh Chen - Date: Aug 2018 HoTT method usage examples *) @@ -74,4 +73,4 @@ proof compute qed fact -end \ No newline at end of file +end diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index e5a8ecf..cff9374 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/Synthesis.thy Author: Josh Chen - Date: Aug 2018 Examples of synthesis. *) @@ -33,8 +32,8 @@ text " schematic_goal "?p`0 \ 0" and "\n. n: \ \ (?p`(succ n)) \ n" apply compute prefer 4 apply compute -prefer 3 apply (rule Nat_rules) -apply (rule Nat_rules | assumption)+ +prefer 3 apply compute +apply (rule Nat_routine Nat_elim | assumption)+ done text " @@ -52,7 +51,7 @@ proof (simple lems: pred_type) proof compute show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by simple show "ind\<^sub>\ (\a b. a) 0 0 \ 0" - proof (rule Nat_comps) + proof compute show "\: U(O)" .. qed simple qed rule diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy index 4fcffad..9690013 100644 --- a/tests/Subgoal.thy +++ b/tests/Subgoal.thy @@ -13,21 +13,16 @@ lemma rpathcomp_type: shows "rpathcomp: \x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" unfolding rpathcomp_def apply standard -prefer 2 subgoal premises 1 for x \ \\subgoal\ is the proof script version of \fix-assume-show\.\ apply standard - prefer 2 subgoal premises 2 for y apply standard - prefer 2 subgoal premises 3 for p apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) \ \specifying \?A=A\ is crucial here to prevent the next \subgoal\ from binding a schematic ?A which should be instantiated to \A\.\ - prefer 2 + prefer 4 apply standard - prefer 2 apply (rule Prod_intro) - prefer 2 subgoal premises 4 for u z q apply (rule Equal_elim[where ?x=u and ?y=z]) apply (simple lems: assms 4) @@ -58,11 +53,8 @@ text " " apply (rule Prod_intro) -prefer 2 apply (rule Prod_intro) - prefer 2 apply (rule Prod_intro) - prefer 2 subgoal 123 for x y p apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) oops diff --git a/tests/Test.thy b/tests/Test.thy index 433039c..c0dc0dd 100644 --- a/tests/Test.thy +++ b/tests/Test.thy @@ -6,8 +6,8 @@ This is an old "test suite" from early implementations of the theory. It is not always guaranteed to be up to date, or reflect most recent versions of the theory. *) -theory HoTT_Test - imports HoTT +theory Test + imports "../HoTT" begin @@ -31,14 +31,14 @@ text " Declaring \Prod_intro\ with the \intro\ attribute (in HoTT.thy) enables \standard\ to prove the following. " -proposition assumes "A : U(i)" shows "\<^bold>\x. x: A \ A" using assms .. +proposition assumes "A : U(i)" shows "\<^bold>\x. x: A \ A" by (simple lems: assms) proposition assumes "A : U(i)" and "A \ B" shows "\<^bold>\x. x : B \ A" proof - - have "A\A \ B\A" using assms by simp - moreover have "\<^bold>\x. x : A \ A" using assms(1) .. + have "A \ A \ B \ A" using assms by simp + moreover have "\<^bold>\x. x : A \ A" by (simple lems: assms) ultimately show "\<^bold>\x. x : B \ A" by simp qed @@ -102,7 +102,7 @@ lemma curried_type_judgment: text " - Polymorphic identity function. Trivial due to lambda expression polymorphism. + Polymorphic identity function is now trivial due to lambda expression polymorphism. (Was more involved in previous monomorphic incarnations.) " -- cgit v1.2.3