diff options
Diffstat (limited to '')
| -rw-r--r-- | EqualProps.thy | 25 | ||||
| -rw-r--r-- | HoTT.thy | 2 | ||||
| -rw-r--r-- | HoTT_Base.thy | 25 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 10 | ||||
| -rw-r--r-- | Proj.thy | 41 | ||||
| -rw-r--r-- | 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] \<Rightarrow> Term" ("(1inv[_,/ _,/ _])") where "inv[A,x,y] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>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 \<rightarrow> y =\<^sub>A x" unfolding inv_def by (derive lems: assms) - -lemma inv_comp: - assumes "a : A" - shows "inv[A,a,a]`refl(a) \<equiv> 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) \<equiv> refl(a)" unfolding inv_def by (simplify lems: assms) @@ -43,27 +41,24 @@ definition rcompose :: "Term \<Rightarrow> Term" ("(1rcompose[_])") x y p" -text "``Natural'' composition function abbreviation, effectively equivalent to a function of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>." +text "``Natural'' composition function, of type \<open>\<Prod>x,y,z:A. x =\<^sub>A y \<rightarrow> y =\<^sub>A z \<rightarrow> x =\<^sub>A z\<close>." abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term" ("(1compose[_,/ _,/ _,/ _])") where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:(x =\<^sub>A y). \<^bold>\<lambda>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 \<rightarrow> y =\<^sub>A z \<rightarrow> 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) \<equiv> refl(a)" +lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> 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 @@ -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 \<open>Setup\<close> +section \<open>Named theorems\<close> 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 \<open>Metalogical definitions\<close> +section \<open>Foundational definitions\<close> text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms. We do not implement universes, and simply use \<open>a : U\<close> as a convenient shorthand to mean ``\<open>a\<close> is a type''." @@ -29,6 +29,27 @@ We do not implement universes, and simply use \<open>a : U\<close> as a convenie typedecl Term +section \<open>Universes\<close> + +ML \<open> +(* 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 +\<close> + +(* +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 \<open>Judgments\<close> text "We formalize the judgments \<open>a : A\<close> and \<open>A : U\<close> 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 \<open>simple\<close>, \<open>wellformed\<close>, \<open>derive\<close>, and \<open>simplify\<close> should together should suffice to automatically prove most HoTT theorems. -We also provide a method -" - - section \<open>Setup\<close> text "Import the \<open>subst\<close> method, used by \<open>simplify\<close>." @@ -67,9 +62,10 @@ method derive uses lems unfolds = ( subsection \<open>Simplification\<close> -text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> simplify lambda applications and attempt to solve definitional equations. +text "The methods \<open>rsimplify\<close> and \<open>simplify\<close> attempt to solve definitional equations by simplifying lambda applications. -\<open>rsimplify\<close> can also be used to search for lambda expressions inhabiting given types. +\<open>simplify\<close> is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules. +In this case use \<open>rsimplify\<close> instead. Since these methods use \<open>derive\<close>, it is often (but not always) the case that theorems provable with \<open>derive\<close> are also provable with them. (Whether this is the case depends on whether the call to \<open>subst (0) comp\<close> fails.)" @@ -47,16 +47,12 @@ section \<open>Properties\<close> text "Typing judgments and computation rules for the dependent and non-dependent projection functions." -lemma fst_dep_type: - assumes "p : \<Sum>x:A. B x" - shows "fst[A,B]`p : A" +lemma fst_dep_type: assumes "p : \<Sum>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 \<rightarrow> U" and "a : A" and "b : B a" - shows "fst[A,B]`(a,b) \<equiv> a" +lemma fst_dep_comp: assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def by (simplify lems: assms) @@ -86,9 +82,7 @@ qed \<close> -lemma snd_dep_type: - assumes "p : \<Sum>x:A. B x" - shows "snd[A,B]`p : B (fst[A,B]`p)" +lemma snd_dep_type: assumes "p : \<Sum>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)+ \<close> -lemma snd_dep_comp: - assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" - shows "snd[A,B]`(a,b) \<equiv> b" +lemma snd_dep_comp: assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def fst_dep_def by (simplify lems: assms) @@ -132,18 +124,14 @@ qed \<close> -text "For non-dependent projection functions:" +text "Nondependent projections:" -lemma fst_nondep_type: - assumes "p : A \<times> B" - shows "fst[A,B]`p : A" +lemma fst_nondep_type: assumes "p : A \<times> 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) \<equiv> a" +lemma fst_nondep_comp: assumes "a : A" and "b : B" shows "fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by (simplify lems: assms) @@ -160,9 +148,7 @@ qed \<close> -lemma snd_nondep_type: - assumes "p : A \<times> B" - shows "snd[A,B]`p : B" +lemma snd_nondep_type: assumes "p : A \<times> B" shows "snd[A,B]`p : B" unfolding snd_nondep_def by (derive lems: assms) @@ -177,9 +163,7 @@ qed (rule assms) \<close> -lemma snd_nondep_comp: - assumes "a : A" and "b : B" - shows "snd[A,B]`(a,b) \<equiv> b" +lemma snd_nondep_comp: assumes "a : A" and "b : B" shows "snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by (simplify lems: assms) @@ -196,4 +180,11 @@ qed \<close> +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 "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A" by simple +schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : ?A" + by derive (* Simplification *) @@ -17,45 +20,73 @@ assume asm: "c : A" "d : B" -have "f`a`b`c \<equiv> d" by (simp add: asm | rule comp | derive lems: asm)+ +have "f`a`b`c \<equiv> d" by (simplify lems: asm) end lemma "a : A \<Longrightarrow> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)" - by verify_simp + by simplify lemma "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" - by verify_simp + by simplify + +schematic_goal "\<lbrakk>a : A; \<And>x. x : A \<Longrightarrow> b x : X\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> ?x" + by rsimplify lemma assumes "a : A" and "\<And>x. x : A \<Longrightarrow> b x : B x" shows "(\<^bold>\<lambda>x:A. b x)`a \<equiv> b a" - by (verify_simp lems: assms) + by (simplify lems: assms) -lemma "\<lbrakk>a : A; b : B a; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" -oops +lemma "\<lbrakk>a : A; b : B a; B: A \<rightarrow> U; \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y\<rbrakk> + \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" + by (simplify) lemma assumes "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a \<equiv> \<^bold>\<lambda>y:B a. c a y" "(\<^bold>\<lambda>y:B a. c a y)`b \<equiv> c a b" shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" -apply (simp add: assms) -done - -lemmas lems = - Prod_comp[where ?A = "B a" and ?b = "\<lambda>b. c a b" and ?a = b] - Prod_comp[where ?A = A and ?b = "\<lambda>x. \<^bold>\<lambda>y:B x. c x y" and ?a = a] +by (simplify lems: assms) lemma - assumes - "a : A" - "b : B a" - "B: A \<rightarrow> U" - "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y" - shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" -apply (verify_simp lems: assms) +assumes + "a : A" + "b : B a" + "B: A \<rightarrow> U" + "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> c x y : D x y" +shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. c x y)`a`b \<equiv> c a b" +by (simplify lems: assms) +lemma +assumes + "a : A" + "b : B a" + "c : C a b" + "B: A \<rightarrow> U" + "\<And>x. x : A\<Longrightarrow> C x: B x \<rightarrow> U" + "\<And>x y z. \<lbrakk>x : A; y : B x; z : C x y\<rbrakk> \<Longrightarrow> d x y z : D x y z" +shows "(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B x. \<^bold>\<lambda>z:C x y. d x y z)`a`b`c \<equiv> 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 "\<lbrakk>A : U; x : A; y : A\<rbrakk> \<Longrightarrow> ?x : x =\<^sub>A y \<rightarrow> 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 |