From 9723fc3ffc55b22a2a8ec09cbba80f14c40d7991 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 11 Jul 2018 19:37:07 +0200 Subject: Universes implemented. Type rules modified accordingly. No more automatic derivation of "A:U" from "a:A". --- Equal.thy | 16 ++++++++-------- EqualProps.thy | 13 ++++++++----- HoTT_Base.thy | 35 ++++++++++++----------------------- HoTT_Methods.thy | 11 +++++------ Prod.thy | 8 ++++---- Proj.thy | 26 ++++++++++++++++++-------- Sum.thy | 24 ++++++++---------------- 7 files changed, 63 insertions(+), 70 deletions(-) diff --git a/Equal.thy b/Equal.thy index 18a4207..8c5cf29 100644 --- a/Equal.thy +++ b/Equal.thy @@ -29,26 +29,26 @@ translations section \Type rules\ axiomatization where - Equal_form: "\A a b. \a : A; b : A\ \ a =\<^sub>A b : U" + Equal_form: "\i A a b. \A : U(i); a : A; b : A\ \ a =\<^sub>A b : U(i)" and - Equal_form_cond1: "\A a b. a =\<^sub>A b : U \ A : U" + Equal_form_cond1: "\i A a b. a =\<^sub>A b : U(i) \ A : U(i)" and - Equal_form_cond2: "\A a b. a =\<^sub>A b : U \ a : A" + Equal_form_cond2: "\i A a b. a =\<^sub>A b : U(i) \ a : A" and - Equal_form_cond3: "\A a b. a =\<^sub>A b : U \ b : A" + Equal_form_cond3: "\i A a b. a =\<^sub>A b : U(i) \ b : A" and Equal_intro: "\A a. a : A \ refl(a) : a =\<^sub>A a" and - Equal_elim: "\A C f a b p. \ - \x y.\x : A; y : A\ \ C x y: x =\<^sub>A y \ U; + Equal_elim: "\i A C f a b p. \ + \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; b : A; p : a =\<^sub>A b \ \ indEqual[A] C f a b p : C a b p" and - Equal_comp: "\A C f a. \ - \x y.\x : A; y : A\ \ C x y: x =\<^sub>A y \ U; + Equal_comp: "\i A C f a. \ + \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 \ \ indEqual[A] C f a a refl(a) \ f a" diff --git a/EqualProps.thy b/EqualProps.thy index 43b4eb5..17c7fa6 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -19,14 +19,15 @@ 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" -lemma inv_type: assumes "x : A" and "y : A" shows "inv[A,x,y] : x =\<^sub>A y \ y =\<^sub>A x" +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) -corollary assumes "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x" +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 : A" shows "inv[A,a,a]`refl(a) \ refl(a)" +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) @@ -48,11 +49,13 @@ abbreviation compose :: "[Term, Term, Term, Term] \ Term" ("(1compo lemma compose_type: -assumes "x : A" and "y : A" and "z : A" shows "compose[A,x,y,z] : x =\<^sub>A y \ y =\<^sub>A z \ x =\<^sub>A z" + assumes "A : U(i)" and "x : A" and "y : A" and "z : A" + shows "compose[A,x,y,z] : x =\<^sub>A y \ y =\<^sub>A z \ x =\<^sub>A z" unfolding rcompose_def by (derive lems: assms) -lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" +lemma compose_comp: + assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" unfolding rcompose_def by (simplify lems: assms) diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 610e5d8..703f1aa 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -30,21 +30,12 @@ named_theorems comp section \Judgments\ -text "Formalize the basic judgments. +text "Formalize the context and typing judgments \a : A\. -For judgmental equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it. - -The judgment \is_a_type A\ expresses the statement ``A is an inhabitant of some universe type'', i.e. ``A is a type''." +For judgmental equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it." consts - is_of_type :: "[Term, Term] \ prop" ("(1_ : _)" [0, 1000] 1000) - is_a_type :: "Term \ prop" ("(1_ : U)" [0] 1000) - - -text "The following fact is used to make explicit the assumption of well-formed contexts." - -axiomatization where - inhabited_implies_type [intro, elim, wellform]: "\a A. a : A \ A : U" + is_of_type :: "[Term, Term] \ prop" ("(1_ : _)" [0, 0] 1000) section \Universes\ @@ -62,31 +53,29 @@ where and Numeral_lt_trans: "\m n. m <- n \ S m <- S n" -\ \This lets \standard\ prove ordering statements on Numerals.\ -lemmas Numeral_lt_rules [intro] = Numeral_lt_min Numeral_lt_trans +lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans + \ \Lets \standard\ automatically solve inequalities.\ text "Universe types:" axiomatization - U :: "Numeral \ Term" ("U_") + U :: "Numeral \ Term" ("U _") where Universe_hierarchy: "\i j. i <- j \ U(i) : U(j)" and - Universe_cumulative: "\a i j. \a : U(i); i <- j\ \ a : U(j)" - -lemmas Universe_rules [intro] = Universe_hierarchy Universe_cumulative + Universe_cumulative: "\A i j. \A : U(i); i <- j\ \ A : U(j)" section \Type families\ -text "A (one-variable) type family is a meta lambda term \P :: Term \ Term\ that further satisfies the following property." +text "We define the following abbreviation constraining the output type of a meta lambda expression when given input of certain type." -type_synonym Typefam = "Term \ Term" +abbreviation (input) constrained :: "[Term \ Term, Term, Term] \ prop" ("_: _ \ _") + where "f: A \ B \ (\x. x : A \ f x : B)" -abbreviation (input) is_type_family :: "[Typefam, Term] \ prop" ("(3_:/ _ \ U)") - where "P: A \ U \ (\x. x : A \ P x : U)" +text "The above is used to define type families, which are just constrained meta-lambdas \P: A \ B\ where \A\ and \B\ are elements of some universe type." -\ \There is an obvious generalization to multivariate type families, but implementing such an abbreviation would probably involve writing ML code, and is for the moment not really crucial.\ +type_synonym Typefam = "Term \ Term" end \ No newline at end of file diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 9a101e5..c314ed4 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -32,7 +32,7 @@ text "Prove type judgments \A : U\ and inhabitation judgments \Wellformedness checker\ @@ -62,13 +62,12 @@ method derive uses lems unfolds = ( subsection \Simplification\ -text "The methods \rsimplify\ and \simplify\ attempt to solve definitional equations by simplifying lambda applications. +text "The methods \rsimplify\ and \simplify\ search for lambda applications to simplify and are suitable for solving definitional equalities, as well as harder proofs where \derive\ fails. -\simplify\ is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules. -In this case use \rsimplify\ instead. +It is however not true that these methods are strictly stronger; if they fail to find a suitable substitution they will fail where \derive\ may succeed. -Since these methods use \derive\, it is often (but not always) the case that theorems provable with \derive\ are also provable with them. -(Whether this is the case depends on whether the call to \subst (0) comp\ fails.)" +\simplify\ is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules. +In this case use \rsimplify\ instead." method rsimplify uses lems = (subst (0) comp, derive lems: lems)+ \ \\subst\ performs an equational rewrite according to some computation rule declared as [comp], after which \derive\ attempts to solve any new assumptions that arise.\ diff --git a/Prod.thy b/Prod.thy index bf4e4e9..445ddd8 100644 --- a/Prod.thy +++ b/Prod.thy @@ -37,13 +37,13 @@ translations section \Type rules\ axiomatization where - Prod_form: "\A B. \A : U; B: A \ U\ \ \x:A. B x : U" + Prod_form: "\i A B. \A : U(i); B: A \ U(i)\ \ \x:A. B x : U(i)" and - Prod_form_cond1: "\A B. (\x:A. B x : U) \ A : U" + Prod_form_cond1: "\i A B. (\x:A. B x : U(i)) \ A : U(i)" and - Prod_form_cond2: "\A B. (\x:A. B x : U) \ B: A \ U" + Prod_form_cond2: "\i A B. (\x:A. B x : U(i)) \ B: A \ U(i)" and - Prod_intro: "\A B b. \A : U; \x. x : A \ b x : B x\ \ \<^bold>\x:A. b x : \x:A. B x" + Prod_intro: "\i A B b. (\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" and diff --git a/Proj.thy b/Proj.thy index 31deaf9..f878469 100644 --- a/Proj.thy +++ b/Proj.thy @@ -47,12 +47,14 @@ 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" +lemma fst_dep_type: assumes "\x:A. B x : U(i)" and "p : \x:A. B x" shows "fst[A,B]`p : A" unfolding fst_dep_def by (derive lems: assms) -lemma fst_dep_comp: assumes "B: A \ U" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \ a" +lemma fst_dep_comp: + assumes "A : U(i)" and "B: A \ U(i)" and "a : A" and "b : B a" + shows "fst[A,B]`(a,b) \ a" unfolding fst_dep_def by (simplify lems: assms) @@ -82,7 +84,9 @@ qed \ -lemma snd_dep_type: assumes "p : \x:A. B x" shows "snd[A,B]`p : B (fst[A,B]`p)" +lemma snd_dep_type: + assumes "\x:A. B x : U(i)" and "p : \x:A. B x" + shows "snd[A,B]`p : B (fst[A,B]`p)" unfolding fst_dep_def snd_dep_def by (simplify lems: assms) @@ -97,7 +101,9 @@ qed (assumption | rule assms)+ \ -lemma snd_dep_comp: assumes "B: A \ U" and "a : A" and "b : B a" shows "snd[A,B]`(a,b) \ b" +lemma snd_dep_comp: + assumes "A : U(i)" and "B: A \ U(i)" and "a : A" and "b : B a" + shows "snd[A,B]`(a,b) \ b" unfolding snd_dep_def fst_dep_def by (simplify lems: assms) @@ -126,12 +132,14 @@ qed text "Nondependent projections:" -lemma fst_nondep_type: assumes "p : A \ B" shows "fst[A,B]`p : A" +lemma fst_nondep_type: assumes "A \ B : U(i)" and "p : A \ B" shows "fst[A,B]`p : A" unfolding fst_nondep_def by (derive lems: assms) -lemma fst_nondep_comp: assumes "a : A" and "b : B" shows "fst[A,B]`(a,b) \ a" +lemma fst_nondep_comp: + assumes "A : U(i)" and "B : U(i)" and "a : A" and "b : B" + shows "fst[A,B]`(a,b) \ a" unfolding fst_nondep_def by (simplify lems: assms) @@ -148,7 +156,7 @@ qed \ -lemma snd_nondep_type: assumes "p : A \ B" shows "snd[A,B]`p : B" +lemma snd_nondep_type: assumes "A \ B : U(i)" and "p : A \ B" shows "snd[A,B]`p : B" unfolding snd_nondep_def by (derive lems: assms) @@ -163,7 +171,9 @@ qed (rule assms) \ -lemma snd_nondep_comp: assumes "a : A" and "b : B" shows "snd[A,B]`(a,b) \ b" +lemma snd_nondep_comp: + assumes "A : U(i)" and "B : U(i)" and "a : A" and "b : B" + shows "snd[A,B]`(a,b) \ b" unfolding snd_nondep_def by (simplify lems: assms) diff --git a/Sum.thy b/Sum.thy index 46bb022..b608e75 100644 --- a/Sum.thy +++ b/Sum.thy @@ -30,22 +30,22 @@ translations section \Type rules\ axiomatization where - Sum_form: "\A B. \A : U; B: A \ U\ \ \x:A. B x : U" + Sum_form: "\i A B. \A : U(i); B: A \ U(i)\ \ \x:A. B x : U(i)" and - Sum_form_cond1: "\A B. (\x:A. B x : U) \ A : U" + Sum_form_cond1: "\i A B. (\x:A. B x : U(i)) \ A : U(i)" and - Sum_form_cond2: "\A B. (\x:A. B x : U) \ B: A \ U" + Sum_form_cond2: "\i A B. (\x:A. B x : U(i)) \ B: A \ U(i)" and - Sum_intro: "\A B a b. \B: A \ U; a : A; b : B a\ \ (a,b) : \x:A. B x" + Sum_intro: "\i A B a b. \B: A \ U(i); a : A; b : B a\ \ (a,b) : \x:A. B x" and - Sum_elim: "\A B C f p. \ - C: \x:A. B x \ U; + Sum_elim: "\i A B C f p. \ + C: \x:A. B x \ U(i); \x y. \x : A; y : B x\ \ f x y : C (x,y); p : \x:A. B x \ \ indSum[A,B] C f p : C p" and - Sum_comp: "\A B C f a b. \ - C: \x:A. B x \ U; + Sum_comp: "\i A B C f a b. \ + C: \x:A. B x \ U(i); \x y. \x : A; y : B x\ \ f x y : C (x,y); a : A; b : B a @@ -59,13 +59,5 @@ text "Nondependent pair." abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) where "A \ B \ \_:A. B" -text "The nondependent pair needs its own separate introduction rule." - -lemma Pair_intro [intro]: "\A B a b. \a : A; b : B\ \ (a,b) : A \ B" -proof - fix b B assume "b : B" - then show "B : U" .. -qed - end \ No newline at end of file -- cgit v1.2.3