From 6857e783fa5cb91f058be322a18fb9ea583f2aad Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 18 Sep 2018 11:38:54 +0200 Subject: Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0! --- ex/HoTT book/Ch1.thy | 47 ++++++++++++-------------- ex/Methods.thy | 73 +++++++++++++--------------------------- ex/Synthesis.thy | 94 +++++++++++++++++++++------------------------------- 3 files changed, 81 insertions(+), 133 deletions(-) (limited to 'ex') diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy index a577fca..263f43d 100644 --- a/ex/HoTT book/Ch1.thy +++ b/ex/HoTT book/Ch1.thy @@ -1,55 +1,50 @@ -(* Title: HoTT/ex/HoTT book/Ch1.thy - Author: Josh Chen +(* +Title: ex/HoTT book/Ch1.thy +Author: Josh Chen +Date: 2018 A formalization of some content of Chapter 1 of the Homotopy Type Theory book. *) theory Ch1 - imports "../../HoTT" +imports "../../HoTT" + begin chapter \HoTT Book, Chapter 1\ -section \1.6 Dependent pair types (\-types)\ +section \1.6 Dependent pair types (\-types)\ -text "Propositional uniqueness principle:" +paragraph \Propositional uniqueness principle.\ schematic_goal - assumes "(\x:A. B(x)): U(i)" and "p: \x:A. B(x)" - shows "?a: p =[\x:A. B(x)] " + assumes "A: U i" and "B: A \ U i" and "p: \x:A. B x" + shows "?a: p =[\x:A. B x] " -text "Proof by induction on \p: \x:A. B(x)\:" +text \Proof by induction on @{term "p: \x:A. B x"}:\ proof (rule Sum_elim[where ?p=p]) - text "We just need to prove the base case; the rest will be taken care of automatically." - - fix x y assume asm: "x: A" "y: B(x)" show - "refl(): =[\x:A. B(x)] , snd >" - proof (subst (0 1) comp) - text " - The computation rules for \fst\ and \snd\ require that \x\ and \y\ have appropriate types. - The automatic proof methods have trouble picking the appropriate types, so we state them explicitly, - " - show "x: A" and "y: B(x)" by (fact asm)+ - - text "...twice, once each for the substitutions of \fst\ and \snd\." - show "x: A" and "y: B(x)" by (fact asm)+ + text \We prove the base case.\ + fix x y assume asm: "x: A" "y: B x" show "refl : =[\x:A. B x] , snd >" + proof compute + show "x: A" and "y: B x" by (fact asm)+ \ \Hint the correct types.\ + text \And now @{method derive} takes care of the rest. +\ qed (derive lems: assms asm) - qed (derive lems: assms) section \Exercises\ -text "Exercise 1.13" +paragraph \Exercise 1.13\ -abbreviation "not" ("\'(_')") where "\(A) \ A \ \" +abbreviation "not" ("\_") where "\A \ A \ \" text "This proof requires the use of universe cumulativity." -proposition assumes "A: U(i)" shows "\<^bold>\f. f`(inr(\<^bold>\a. f`inl(a))): \(\(A + \(A)))" -by (derive lems: assms U_cumulative[where ?A=\ and ?i=O and ?j=i]) +proposition assumes "A: U i" shows "\<^bold>\f. f`(inr(\<^bold>\a. f`(inl a))): \(\(A + \A))" +by (derive lems: assms) end diff --git a/ex/Methods.thy b/ex/Methods.thy index c78af14..09975b0 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -1,76 +1,49 @@ -(* Title: HoTT/ex/Methods.thy - Author: Josh Chen +(* +Title: ex/Methods.thy +Author: Joshua Chen +Date: 2018 -HoTT method usage examples +Basic HoTT method usage examples. *) theory Methods - imports "../HoTT" -begin +imports "../HoTT" +begin -text "Wellformedness results, metatheorems written into the object theory using the wellformedness rules." lemma assumes "A : U(i)" "B: A \ U(i)" "\x. x : A \ C x: B x \ U(i)" - shows "\x:A. \y:B x. \z:C x y. \w:A. x =\<^sub>A w : U(i)" -by (routine lems: assms) - - -lemma - assumes "\x:A. \y: B x. \z: C x y. D x y z: U(i)" - shows - "A : U(i)" and - "B: A \ U(i)" and - "\x. x : A \ C x: B x \ U(i)" and - "\x y. \x : A; y : B x\ \ D x y: C x y \ U(i)" -proof - - show - "A : U(i)" and - "B: A \ U(i)" and - "\x. x : A \ C x: B x \ U(i)" and - "\x y. \x : A; y : B x\ \ D x y: C x y \ U(i)" - by (derive lems: assms) -qed - - -text "Typechecking and constructing inhabitants:" + shows "\x:A. \y:B x. \z:C x y. \w:A. x =\<^sub>A w: U(i)" +by (routine add: assms) -\ \Correctly determines the type of the pair\ +\ \Correctly determines the type of the pair.\ schematic_goal "\A: U(i); B: U(i); a : A; b : B\ \ : ?A" by routine \ \Finds pair (too easy).\ schematic_goal "\A: U(i); B: U(i); a : A; b : B\ \ ?x : A \ B" -apply (rule Sum_intro) +apply (rule intros) apply assumption+ done - -text " - Function application. - The proof methods are not yet automated as well as I would like; we still often have to explicitly specify types. -" - -lemma - assumes "A: U(i)" "a: A" - shows "(\<^bold>\x. )`a \ " +\ \Function application. We still often have to explicitly specify types.\ +lemma "\A: U i; a: A\ \ (\<^bold>\x. )`a \ " proof compute show "\x. x: A \ : A \ \" by routine -qed (routine lems: assms) - +qed -lemma - assumes "A: U(i)" "B: A \ U(i)" "a: A" "b: B(a)" - shows "(\<^bold>\x y. )`a`b \ " -proof compute - show "\x. x: A \ \<^bold>\y. : \y:B(x). \x:A. B(x)" by (routine lems: assms) +text \ +The proof below takes a little more work than one might expect; it would be nice to have a one-line method or proof. +\ - show "(\<^bold>\b. )`b \ " +lemma "\A: U i; B: A \ U i; a: A; b: B a\ \ (\<^bold>\x y. )`a`b \ " +proof (compute, routine) + show "\A: U i; B: A \ U i; a: A; b: B a\ \ (\<^bold>\y. )`b \ " proof compute - show "\b. b: B(a) \ : \x:A. B(x)" by (routine lems: assms) - qed fact -qed fact + show "\b. \A: U i; B: A \ U i; a: A; b: B a\ \ : \x:A. B x" by routine + qed +qed end diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index a5e77ec..3ee973c 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -1,78 +1,58 @@ -(* Title: HoTT/ex/Synthesis.thy - Author: Josh Chen +(* +Title: ex/Synthesis.thy +Author: Joshua Chen +Date: 2018 -Examples of synthesis. +Examples of synthesis *) theory Synthesis - imports "../HoTT" +imports "../HoTT" + begin section \Synthesis of the predecessor function\ -text " - In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers. - - This is also done in \CTT.thy\; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely. -" +text \ +In this example we construct a predecessor function for the natural numbers. +This is also done in @{file "~~/src/CTT/ex/Synthesis.thy"}, there the work is much easier as the equality type is extensional. +\ -text "First we show that the property we want is well-defined." +text \First we show that the property we want is well-defined.\ -lemma pred_welltyped: "\pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n): U(O)" +lemma pred_welltyped: "\pred: \\\. (pred`0 =\<^sub>\ 0) \ (\n:\. pred`(succ n) =\<^sub>\ n): U O" by routine -text " - Now we look for an inhabitant of this type. - Observe that we're looking for a lambda term \pred\ satisfying \(pred`0) =\<^sub>\ 0\ and \\n:\. (pred`(succ n)) =\<^sub>\ n\. - What if we require **definitional** equality instead of just propositional equality? -" +text \ +Now we look for an inhabitant of this type. +Observe that we're looking for a lambda term @{term pred} satisfying @{term "pred`0 =\<^sub>\ 0"} and @{term "\n:\. pred`(succ n) =\<^sub>\ n"}. +What if we require *definitional* instead of just propositional equality? +\ schematic_goal "?p`0 \ 0" and "\n. n: \ \ (?p`(succ n)) \ n" apply compute prefer 4 apply compute -prefer 3 apply compute -apply (rule Nat_routine Nat_elim | compute | assumption)+ -done - -text " - The above proof finds a candidate, namely \\<^bold>\n. ind\<^sub>\ (\a b. a) 0 n\. - We prove this has the required type and properties. -" - -definition pred :: Term where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) 0 n" - -lemma pred_type: "pred: \ \ \" unfolding pred_def by routine - -lemma pred_props: "\n. refl(n)>: ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -proof (routine lems: pred_type) - have *: "pred`0 \ 0" unfolding pred_def - proof compute - show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by routine - show "ind\<^sub>\ (\a b. a) 0 0 \ 0" - proof compute - show "\: U(O)" .. - qed routine - qed rule - then show "refl(0): (pred`0) =\<^sub>\ 0" by (subst *) routine - - show "\<^bold>\n. refl(n): \n:\. (pred`(succ(n))) =\<^sub>\ n" - unfolding pred_def proof - show "\n. n: \ \ refl(n): ((\<^bold>\n. ind\<^sub>\ (\a b. a) 0 n)`succ(n)) =\<^sub>\ n" - proof compute - show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by routine - show "\n. n: \ \ refl(n): ind\<^sub>\ (\a b. a) 0 (succ n) =\<^sub>\ n" - proof compute - show "\: U(O)" .. - qed routine - qed rule - qed rule -qed - -theorem - "\n. refl(n)>>: \pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -by (routine lems: pred_welltyped pred_type pred_props) +apply (rule Nat_routine | compute)+ +oops +\ \Something in the original proof broke when I revamped the theory. The completion of this derivation is left as an exercise to the reader.\ + +text \ +The above proof finds a candidate, namely @{term "\n. ind\<^sub>\ (\a b. a) 0 n"}. +We prove this has the required type and properties. +\ + +definition pred :: t where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) 0 n" + +lemma pred_type: "pred: \ \ \" +unfolding pred_def by routine + +lemma pred_props: "\n. refl n>: (pred`0 =\<^sub>\ 0) \ (\n:\. pred`(succ n) =\<^sub>\ n)" +unfolding pred_def by derive + +theorem "\n. refl(n)>>: \pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" +by (derive lems: pred_type pred_props) end -- cgit v1.2.3