From 4bab3b7f757f7cfbf86ad289b9d92b19a987043a Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 6 Aug 2018 23:56:10 +0200 Subject: Partway through changing function application syntax style. --- HoTT.thy | 4 +- HoTT_Base.thy | 21 ++++--- Nat.thy | 49 +++++++++++++++ Prod.thy | 34 +++++------ Proj.thy | 28 +++++++-- Sum.thy | 16 ++--- scratch.thy | 192 ++++++++++++++++++++++++++++------------------------------ 7 files changed, 206 insertions(+), 138 deletions(-) create mode 100644 Nat.thy diff --git a/HoTT.thy b/HoTT.thy index fa50f61..ce77ec7 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -12,9 +12,11 @@ HoTT_Base HoTT_Methods (* Types *) -Equal Prod Sum +Equal +Coprod +Nat (* Additional properties *) EqualProps diff --git a/HoTT_Base.thy b/HoTT_Base.thy index cf71813..c2bb092 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -9,6 +9,10 @@ theory HoTT_Base imports Pure begin +text "Use the syntax \f(x)\ instead of \f x\ for function application." + +setup Pure_Thy.old_appl_syntax_setup + section \Foundational definitions\ @@ -20,12 +24,12 @@ typedecl Term section \Judgments\ text " - Formalize the typing judgment \a : A\. + Formalize the typing judgment \a: A\. For judgmental/definitional equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it. " consts - has_type :: "[Term, Term] \ prop" ("(1_ : _)" [0, 0] 1000) + has_type :: "[Term, Term] \ prop" ("(1_: _)" [0, 0] 1000) section \Universe hierarchy\ @@ -39,11 +43,11 @@ axiomatization S :: "Ord \ Ord" ("S_" [0] 1000) and lt :: "[Ord, Ord] \ prop" (infix "<-" 999) where - Ord_lt_min: "\n. O <- S n" + Ord_min: "\n. O <- S(n)" and - Ord_lt_trans: "\m n. m <- n \ S m <- S n" + Ord_monotone: "\m n. m <- n \ S(m) <- S(n)" -lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_trans +lemmas Ord_rules [intro] = Ord_min Ord_monotone \ \Enables \standard\ to automatically solve inequalities.\ text "Define the universe types." @@ -51,12 +55,11 @@ text "Define the universe types." axiomatization U :: "Ord \ Term" where - U_hierarchy: "\i j. i <- j \ U(i) : U(j)" + U_hierarchy: "\i j. i <- j \ U(i): U(j)" and - U_cumulative: "\A i j. \A : U(i); i <- j\ \ A : U(j)" + 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 " @@ -64,7 +67,7 @@ text " " abbreviation (input) constrained :: "[Term \ Term, Term, Term] \ prop" ("(1_: _ \ _)") - where "f: A \ B \ (\x. x : A \ f x : B)" + where "f: A \ B \ (\x. x : A \ f(x): B)" text " The above is used to define type families, which are constrained meta-lambdas \P: A \ B\ where \A\ and \B\ are small types. diff --git a/Nat.thy b/Nat.thy new file mode 100644 index 0000000..93b7a2e --- /dev/null +++ b/Nat.thy @@ -0,0 +1,49 @@ +(* Title: HoTT/Nat.thy + Author: Josh Chen + Date: Aug 2018 + +Natural numbers. +*) + +theory Nat + imports HoTT_Base +begin + + +axiomatization + Nat :: Term ("\") and + zero :: Term ("0") and + succ :: "Term \ Term" and + indNat :: "[Typefam, [Term, Term] \ Term, Term, Term] \ Term" ("(1ind\<^sub>\)") +where + Nat_form: "\ : U(O)" +and + Nat_intro1: "0 : \" +and + Nat_intro2: "\n. n : \ \ succ n : \" +and + Nat_elim: "\i C f a n. \ + C: \ \ U(i); + \n c. \n : \; c : C n\ \ f n c : C (succ n); + a : C 0; + n : \ + \ \ ind\<^sub>\ C f a n : C n" +and + Nat_comp1: "\i C f a. \ + C: \ \ U(i); + \n c. \n : \; c : C n\ \ f n c : C (succ n); + a : C 0 + \ \ ind\<^sub>\ C f a 0 \ a" +and + Nat_comp2: "\ i C f a n. \ + C: \ \ U(i); + \n c. \n : \; c : C n\ \ f n c : C (succ n); + a : C 0; + n : \ + \ \ ind\<^sub>\ C f a (succ n) \ f n (ind\<^sub>\ C f a n)" + +lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2 +lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 + + +end \ No newline at end of file diff --git a/Prod.thy b/Prod.thy index 8fa73f3..e4e7091 100644 --- a/Prod.thy +++ b/Prod.thy @@ -15,7 +15,7 @@ section \Constants and syntax\ axiomatization Prod :: "[Term, Typefam] \ Term" and lambda :: "[Term, Term \ Term] \ Term" and - appl :: "[Term, Term] \ Term" (infixl "`" 60) + appl :: "[Term, Term] \ Term" ("(1_`_)" [61, 60] 60) \ \Application binds tighter than abstraction.\ syntax @@ -27,48 +27,48 @@ syntax text "The translations below bind the variable \x\ in the expressions \B\ and \b\." translations - "\x:A. B" \ "CONST Prod A (\x. B)" - "\<^bold>\x:A. b" \ "CONST lambda A (\x. b)" - "PROD x:A. B" \ "CONST Prod A (\x. B)" - "%%x:A. b" \ "CONST lambda A (\x. b)" + "\x:A. B" \ "CONST Prod(A, \x. B)" + "\<^bold>\x:A. b" \ "CONST lambda(A, \x. b)" + "PROD x:A. B" \ "CONST Prod(A, \x. B)" + "%%x:A. b" \ "CONST lambda(A, \x. b)" text "Nondependent functions are a special case." abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 40) - where "A \ B \ \_:A. B" + where "A \ B \ \_: A. B" section \Type rules\ axiomatization where - Prod_form: "\i A B. \A : U(i); B: A \ U(i)\ \ \x:A. B x : U(i)" + Prod_form: "\i A B. \A: U(i); B: A \ U(i)\ \ \x:A. B(x): U(i)" and - Prod_intro: "\i A B b. \A : U(i); \x. x : A \ b x : B x\ \ \<^bold>\x:A. b x : \x:A. B x" + 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)" and - Prod_elim: "\A B f a. \f : \x:A. B x; a : A\ \ f`a : B a" + Prod_elim: "\A B f a. \f: \x:A. B(x); a: A\ \ f`a: B(a)" and - Prod_comp: "\A B b a. \\x. x : A \ b x : B x; a : A\ \ (\<^bold>\x:A. b x)`a \ b a" + 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)" and - Prod_uniq: "\A B f. f : \x:A. B x \ \<^bold>\x:A. (f`x) \ f" + Prod_uniq: "\A B f. 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)\. + 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)\. That is to say, the following inference rules are admissible, and it simplifies proofs greatly to axiomatize them directly. " axiomatization where - Prod_form_cond1: "\i A B. (\x:A. B x : U(i)) \ A : U(i)" + Prod_form_cond1: "\i A B. (\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: "\i A B. (\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 +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_comps [comp] = Prod_comp Prod_uniq @@ -84,9 +84,9 @@ where and Unit_intro: "\ : \" and - Unit_elim: "\i C c a. \C: \ \ U(i); c : C \; a : \\ \ ind\<^sub>\ C c a : C a" + Unit_elim: "\i C c a. \C: \ \ U(i); c : C(\); a : \\ \ ind\<^sub>\(C, c, a) : C(a)" and - Unit_comp: "\i C c. \C: \ \ U(i); c : C \\ \ ind\<^sub>\ C c \ \ c" + Unit_comp: "\i C c. \C: \ \ U(i); c : C(\)\ \ ind\<^sub>\(C, 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 bcef939..e6ed0bb 100644 --- a/Proj.thy +++ b/Proj.thy @@ -52,6 +52,7 @@ unfolding fst_dep_def proof show "lambda (Sum A B) (ind\<^sub>\[A, B] (\_. A) (\x y. x)) : (\x:A. B x) \ A" proof + show "A : U(i)" using assms(1) .. show "Sum A B : U(i)" by (rule assms) show "\p. p : Sum A B \ ind\<^sub>\[A, B] (\_. A) (\x y. x) p : A" proof @@ -66,11 +67,11 @@ lemma fst_dep_comp: shows "fst[A,B]`(a,b) \ a" unfolding fst_dep_def proof (subst comp) + show "Sum A B : U(i)" using assms(1-2) .. show "\x. x : Sum A B \ ind\<^sub>\[A, B] (\_. A) (\x y. x) x : A" by (standard, rule assms(1), assumption+) - show "(a,b) : Sum A B" using assms(2-4) .. - show "ind\<^sub>\[A, B] (\_. A) (\x y. x) (a, b) \ a" - proof - oops + show "(a,b) : Sum A B" using assms .. + show "ind\<^sub>\[A, B] (\_. A) (\x y. x) (a, b) \ a" by (standard, (rule assms|assumption)+) +qed (rule assms) \ \ (* Old proof *) proof - @@ -101,8 +102,23 @@ qed 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) +unfolding fst_dep_def snd_dep_def +proof (subst (3) comp) + show "Sum A B : U(i)" by (rule assms) + show "\x. x : Sum A B \ ind\<^sub>\[A, B] (\_. A) (\x y. x) x : A" + proof + show "A : U(i)" using assms(1) .. + qed + show "A : U(i)" using assms(1) .. + show "p : Sum A B" by (rule assms(2)) + show "lambda + (Sum A B) + (ind\<^sub>\[A, B] (\q. B (lambda (Sum A B) (ind\<^sub>\[A, B] (\_. A) (\x y. x))`q)) (\x y. y)) + ` p : B (ind\<^sub>\[A, B] (\_. A) (\x y. x) p)" + proof (subst (2) comp) + show "Sum A B : U(i)" by (rule assms) + show " + \ \ (* Old proof *) proof (derive lems: assms unfolds: snd_dep_def) diff --git a/Sum.thy b/Sum.thy index 80f8a9c..18d4186 100644 --- a/Sum.thy +++ b/Sum.thy @@ -36,7 +36,7 @@ section \Type rules\ axiomatization where Sum_form: "\i A B. \A : U(i); B: A \ U(i)\ \ \x:A. B x : U(i)" and - Sum_intro: "\i A B a b. \B: A \ U(i); a : A; b : B a\ \ (a,b) : \x:A. B x" + 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" and Sum_elim: "\i A B C f p. \ C: \x:A. B x \ U(i); @@ -45,6 +45,8 @@ and \ \ ind\<^sub>\[A,B] C f p : C p" and Sum_comp: "\i A B C f a b. \ + A : U(i); + B: A \ U(i); C: \x:A. B x \ U(i); \x y. \x : A; y : B x\ \ f x y : C (x,y); a : A; @@ -63,17 +65,17 @@ lemmas Sum_form_conds [intro (*elim, wellform*)] = Sum_form_cond1 Sum_form_cond2 lemmas Sum_comps [comp] = Sum_comp -section \Null type\ +section \Empty type\ axiomatization - Null :: Term ("\") and - indNull :: "[Typefam, Term] \ Term" ("(1ind\<^sub>\)") + Empty :: Term ("\") and + indEmpty :: "[Typefam, Term] \ Term" ("(1ind\<^sub>\)") where - Null_form: "\ : U(O)" + Empty_form: "\ : U(O)" and - Null_elim: "\i C z. \C: \ \ U(i); z : \\ \ ind\<^sub>\ C z : C z" + Empty_elim: "\i C z. \C: \ \ U(i); z : \\ \ ind\<^sub>\ C z : C z" -lemmas Null_rules [intro] = Null_form Null_elim +lemmas Empty_rules [intro] = Empty_form Empty_elim end \ No newline at end of file diff --git a/scratch.thy b/scratch.thy index ae1bdb5..b88a8fc 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,108 +3,104 @@ theory scratch begin -(* Typechecking *) -schematic_goal "\A : U(i); B : U(i); a : A; b : B\ \ (a,b) : ?A" - by derive - -lemma "\ : U(S S S 0)" - by derive - - -(* Simplification *) - -notepad begin - -assume asm: - "f`a \ g" - "g`b \ \<^bold>\x:A. d" - "c : A" - "d : B" - -have "f`a`b`c \ d" by (simplify lems: asm) - -end - -lemma "\A : U(i); a : A\ \ indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a) \ refl(a)" - by simplify - -lemma "\a : A; \x. x : A \ b x : X\ \ (\<^bold>\x:A. b x)`a \ b a" - by simplify - -schematic_goal "\a : A; b: A \ 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 (simplify lems: assms) - -lemma "\a : A; b : B a; B: A \ U(i); \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" -by (simplify lems: assms) - -lemma -assumes - "a : A" - "b : B a" - "\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" - "\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) - -(* Polymorphic identity function *) +abbreviation pred where "pred \ \<^bold>\n:\. (ind\<^sub>\ (\n. \) (\n c. n) 0 n)" + +schematic_goal "?a : (pred`0) =\<^sub>\ 0" +apply (subst comp) +apply (rule Nat_form) +prefer 4 apply (subst comp) +apply (rule Nat_form) +apply assumption +apply (rule Nat_intro1) +apply (rule Equal_intro) +apply (rule Nat_intro1) +prefer 2 apply (rule Nat_elim) +apply (rule Nat_form) +apply assumption +apply (rule Nat_intro1) +apply assumption +apply (rule Nat_form) +done + +schematic_goal "?a : \n:\. (pred`(succ n)) =\<^sub>\ n" +apply (rule Prod_intro) +apply (rule Nat_form) +apply (subst comp) +apply (rule Nat_form) +prefer 2 apply (rule Nat_elim) +apply (rule Nat_form) +apply assumption +apply (rule Nat_intro1) +apply assumption +apply (rule Nat_form) +apply (rule Nat_intro2, assumption) +apply (rule Equal_form) +apply (rule Nat_form) +apply (rule Nat_elim) +apply (rule Nat_form) +apply assumption +apply (rule Nat_rules)+ +apply assumption+ +apply (subst comp) +apply (rule Nat_form) +prefer 2 apply (rule Nat_elim) +defer +apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+ +apply (subst Nat_comps) +apply (assumption | rule Nat_form Nat_intro1 Nat_intro2)+ +apply (rule Equal_intro) +apply assumption +apply (rule Nat_form) +done + +schematic_goal "?a : \p:\\\. \n:\. (p`(succ n)) =\<^sub>\ n" +apply (rule Sum_intro) +apply (rule Prod_form) +apply (rule Nat_form)+ +apply (rule Prod_form) +apply (rule Nat_form) +apply (rule Equal_form) +apply (rule Nat_form) +apply (rule Prod_elim) +apply assumption +apply (elim Nat_intro2) +apply assumption +prefer 2 apply (rule Prod_intro) +apply (rule Nat_form) +prefer 3 apply (rule Prod_intro) +apply (rule Nat_form)+ +prefer 3 apply (rule Nat_elim) +back +oops -definition Id :: "Numeral \ Term" where "Id n \ \<^bold>\A:U(n). \<^bold>\x:A. x" -lemma assumes "A : U 0" and "x:A" shows "(Id 0)`A`x \ x" unfolding Id_def by (simplify lems: assms) +(* Now try to derive pred directly *) +schematic_goal "?a : \pred:?A . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" +(* At some point need to perform induction *) +apply (rule Sum_intro) +defer +apply (rule Sum_form) +apply (rule Equal_form) +apply (rule Nat_form) +apply (rule Prod_elim) +defer +apply (rule Nat_intro1)+ +prefer 5 apply assumption +prefer 4 apply (rule Prod_form) +apply (rule Nat_form)+ +apply (rule Prod_form) +apply (rule Nat_form) +apply (rule Equal_form) +apply (rule Nat_form) +apply (rule Prod_elim) +apply assumption +apply (rule Nat_intro2) +apply assumption+ +(* Now begins the hard part *) +prefer 2 apply (rule Sum_rules) +prefer 2 apply (rule Prod_rules) -(* See if we can find path inverse *) -schematic_goal "\A : U(i); x : A; y : A\ \ ?x : x =\<^sub>A y \ y =\<^sub>A x" - apply (rule Prod_intro) - apply (rule Equal_elim) - back - back - back - back - back - back - back - defer - back - back - back - back - back - back - back - back - back - apply (rule Equal_form) - apply assumption+ - defer - defer - apply assumption - defer - defer - apply (rule Equal_intro) - apply assumption+ -oops end \ No newline at end of file -- cgit v1.2.3