From 6389f18fd17e4333aba3fcdcc9ed2810d4cb1da5 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 9 Jul 2018 11:17:50 +0200 Subject: Pre-universe implementation commit --- EqualProps.thy | 25 ++++++++------------ HoTT.thy | 2 +- HoTT_Base.thy | 25 ++++++++++++++++++-- HoTT_Methods.thy | 10 +++----- Proj.thy | 41 +++++++++++++------------------- scratch.thy | 71 ++++++++++++++++++++++++++++++++++++++++---------------- 6 files changed, 104 insertions(+), 70 deletions(-) diff --git a/EqualProps.thy b/EqualProps.thy index cb267c6..43b4eb5 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -19,16 +19,14 @@ 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 "p : x =\<^sub>A y" - shows "inv[A,x,y]`p : y =\<^sub>A x" +lemma inv_type: assumes "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) - -lemma inv_comp: - assumes "a : A" - shows "inv[A,a,a]`refl(a) \ refl(a)" +corollary assumes "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)" unfolding inv_def by (simplify lems: assms) @@ -43,27 +41,24 @@ definition rcompose :: "Term \ Term" ("(1rcompose[_])") x y p" -text "``Natural'' composition function abbreviation, effectively equivalent to a function of type \\x,y,z:A. x =\<^sub>A y \ y =\<^sub>A z \ x =\<^sub>A z\." +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" lemma compose_type: - assumes "p : x =\<^sub>A y" and "q : y =\<^sub>A z" - shows "compose[A,x,y,z]`p`q : x =\<^sub>A z" +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" 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 : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" unfolding rcompose_def by (simplify lems: assms) -lemmas Equal_simps [intro] = inv_comp compose_comp +lemmas EqualProps_rules [intro] = inv_type inv_comp compose_type compose_comp +lemmas EqualProps_comps [comp] = inv_comp compose_comp end \ No newline at end of file diff --git a/HoTT.thy b/HoTT.thy index 948dd14..fa50f61 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -21,4 +21,4 @@ EqualProps Proj begin -end +end \ No newline at end of file diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 60e5167..d119c1f 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -10,7 +10,7 @@ theory HoTT_Base begin -section \Setup\ +section \Named theorems\ text "Named theorems to be used by proof methods later (see HoTT_Methods.thy). @@ -21,7 +21,7 @@ named_theorems wellform named_theorems comp -section \Metalogical definitions\ +section \Foundational definitions\ text "A single meta-type \Term\ suffices to implement the object-logic types and terms. We do not implement universes, and simply use \a : U\ as a convenient shorthand to mean ``\a\ is a type''." @@ -29,6 +29,27 @@ We do not implement universes, and simply use \a : U\ as a convenie typedecl Term +section \Universes\ + +ML \ +(* Produces universe terms and judgments on-the-fly *) +fun Ui_type_oracle (x: int) = + let + val f = Sign.declare_const @{context} ((Binding.name ("U" ^ Int.toString x), @{typ Term}), NoSyn); + val (trm, thy) = f @{theory}; + in + Theory.setup (fn thy => #2 (f thy)); + Thm.cterm_of (Proof_Context.init_global thy) (trm) + end +\ + +(* +Sign.add_consts: (binding * typ * mixfix) list -> theory -> theory +Thm.cterm_of: Proof.context -> term -> cterm +Thm.add_oracle: binding * (’a -> cterm) -> theory -> (string * (’a -> thm)) * theory +*) + + section \Judgments\ text "We formalize the judgments \a : A\ and \A : U\ separately, in contrast to the HoTT book where the latter is considered an instance of the former. diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 1f11230..9a101e5 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -13,11 +13,6 @@ theory HoTT_Methods begin -text "The methods \simple\, \wellformed\, \derive\, and \simplify\ should together should suffice to automatically prove most HoTT theorems. -We also provide a method -" - - section \Setup\ text "Import the \subst\ method, used by \simplify\." @@ -67,9 +62,10 @@ method derive uses lems unfolds = ( subsection \Simplification\ -text "The methods \rsimplify\ and \simplify\ simplify lambda applications and attempt to solve definitional equations. +text "The methods \rsimplify\ and \simplify\ attempt to solve definitional equations by simplifying lambda applications. -\rsimplify\ can also be used to search for lambda expressions inhabiting given types. +\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. 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.)" diff --git a/Proj.thy b/Proj.thy index 805a624..31deaf9 100644 --- a/Proj.thy +++ b/Proj.thy @@ -47,16 +47,12 @@ 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 "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 "B: A \ U" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \ a" unfolding fst_dep_def by (simplify lems: assms) @@ -86,9 +82,7 @@ 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 "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) @@ -103,9 +97,7 @@ 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 "B: A \ U" 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) @@ -132,18 +124,14 @@ qed \ -text "For non-dependent projection functions:" +text "Nondependent projections:" -lemma fst_nondep_type: - assumes "p : A \ B" - shows "fst[A,B]`p : A" +lemma fst_nondep_type: assumes "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 : A" and "b : B" shows "fst[A,B]`(a,b) \ a" unfolding fst_nondep_def by (simplify lems: assms) @@ -160,9 +148,7 @@ qed \ -lemma snd_nondep_type: - assumes "p : A \ B" - shows "snd[A,B]`p : B" +lemma snd_nondep_type: assumes "p : A \ B" shows "snd[A,B]`p : B" unfolding snd_nondep_def by (derive lems: assms) @@ -177,9 +163,7 @@ 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 : A" and "b : B" shows "snd[A,B]`(a,b) \ b" unfolding snd_nondep_def by (simplify lems: assms) @@ -196,4 +180,11 @@ qed \ +lemmas Proj_rules [intro] = + fst_dep_type snd_dep_type fst_nondep_type snd_nondep_type + fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp + +lemmas Proj_comps [comp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp + + end \ No newline at end of file diff --git a/scratch.thy b/scratch.thy index 1c921bd..3f66083 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,8 +3,11 @@ theory scratch begin +term "UN" + (* Typechecking *) -schematic_goal "\a : A; b : B\ \ (a,b) : ?A" by simple +schematic_goal "\a : A; b : B\ \ (a,b) : ?A" + by derive (* Simplification *) @@ -17,45 +20,73 @@ assume asm: "c : A" "d : B" -have "f`a`b`c \ d" by (simp add: asm | rule comp | derive lems: asm)+ +have "f`a`b`c \ d" by (simplify lems: asm) end lemma "a : A \ indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a) \ refl(a)" - by verify_simp + by simplify lemma "\a : A; \x. x : A \ b x : X\ \ (\<^bold>\x:A. b x)`a \ b a" - by verify_simp + by simplify + +schematic_goal "\a : A; \x. x : A \ b x : X\ \ (\<^bold>\x:A. b x)`a \ ?x" + by rsimplify lemma assumes "a : A" and "\x. x : A \ b x : B x" shows "(\<^bold>\x:A. b x)`a \ b a" - by (verify_simp lems: assms) + by (simplify lems: assms) -lemma "\a : A; b : B a; B: A \ U\ \ (\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" -oops +lemma "\a : A; b : B a; B: A \ U; \x y. \x : A; y : B x\ \ c x y : D x y\ + \ (\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" + by (simplify) lemma assumes "(\<^bold>\x:A. \<^bold>\y:B x. c x y)`a \ \<^bold>\y:B a. c a y" "(\<^bold>\y:B a. c a y)`b \ c a b" shows "(\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" -apply (simp add: assms) -done - -lemmas lems = - Prod_comp[where ?A = "B a" and ?b = "\b. c a b" and ?a = b] - Prod_comp[where ?A = A and ?b = "\x. \<^bold>\y:B x. c x y" and ?a = a] +by (simplify lems: assms) lemma - assumes - "a : A" - "b : B a" - "B: A \ U" - "\x y. \x : A; y : B x\ \ c x y : D x y" - shows "(\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" -apply (verify_simp lems: assms) +assumes + "a : A" + "b : B a" + "B: A \ U" + "\x y. \x : A; y : B x\ \ c x y : D x y" +shows "(\<^bold>\x:A. \<^bold>\y:B x. c x y)`a`b \ c a b" +by (simplify lems: assms) +lemma +assumes + "a : A" + "b : B a" + "c : C a b" + "B: A \ U" + "\x. x : A\ C x: B x \ U" + "\x y z. \x : A; y : B x; z : C x y\ \ d x y z : D x y z" +shows "(\<^bold>\x:A. \<^bold>\y:B x. \<^bold>\z:C x y. d x y z)`a`b`c \ d a b c" +by (simplify lems: assms) + + +(* HERE IS HOW WE ATTEMPT TO DO PATH INDUCTION --- VERY GOOD CANDIDATE FOR THESIS SECTION *) + +schematic_goal "\A : U; x : A; y : A\ \ ?x : x =\<^sub>A y \ y =\<^sub>A x" + apply (rule Prod_intro) + apply (rule Equal_form) + apply assumption+ + apply (rule Equal_elim) + back + back + back + back + back + back + back + back back back back back back + +thm comp end \ No newline at end of file -- cgit v1.2.3