From c2dfffffb7586662c67e44a2d255a1a97ab0398b Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 2 Apr 2020 17:57:48 +0200 Subject: Brand-spanking new version using Spartan infrastructure --- ex/Book/Ch1.thy | 50 ------------------------------------------------ ex/Methods.thy | 49 ----------------------------------------------- ex/Synthesis.thy | 58 -------------------------------------------------------- 3 files changed, 157 deletions(-) delete mode 100644 ex/Book/Ch1.thy delete mode 100644 ex/Methods.thy delete mode 100644 ex/Synthesis.thy (limited to 'ex') diff --git a/ex/Book/Ch1.thy b/ex/Book/Ch1.thy deleted file mode 100644 index dfb1879..0000000 --- a/ex/Book/Ch1.thy +++ /dev/null @@ -1,50 +0,0 @@ -(* -Title: ex/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" - -begin - -chapter \HoTT Book, Chapter 1\ - -section \1.6 Dependent pair types (\-types)\ - -paragraph \Propositional uniqueness principle.\ - -schematic_goal - 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 @{term "p: \x:A. B x"}:\ - -proof (rule Sum_elim[where ?p=p]) - 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\ - -paragraph \Exercise 1.13\ - -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) - - -end diff --git a/ex/Methods.thy b/ex/Methods.thy deleted file mode 100644 index 09975b0..0000000 --- a/ex/Methods.thy +++ /dev/null @@ -1,49 +0,0 @@ -(* -Title: ex/Methods.thy -Author: Joshua Chen -Date: 2018 - -Basic HoTT method usage examples. -*) - -theory Methods -imports "../HoTT" - -begin - - -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 add: assms) - -\ \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 intros) -apply assumption+ -done - -\ \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 - -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. -\ - -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. \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 deleted file mode 100644 index 3ee973c..0000000 --- a/ex/Synthesis.thy +++ /dev/null @@ -1,58 +0,0 @@ -(* -Title: ex/Synthesis.thy -Author: Joshua Chen -Date: 2018 - -Examples of synthesis -*) - - -theory Synthesis -imports "../HoTT" - -begin - - -section \Synthesis of the predecessor function\ - -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.\ - -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 @{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 -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