diff options
Diffstat (limited to 'ex')
| -rw-r--r-- | ex/Book/Ch1.thy | 50 | ||||
| -rw-r--r-- | ex/Methods.thy | 49 | ||||
| -rw-r--r-- | ex/Synthesis.thy | 58 |
3 files changed, 0 insertions, 157 deletions
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 \<open>HoTT Book, Chapter 1\<close> - -section \<open>1.6 Dependent pair types (\<Sum>-types)\<close> - -paragraph \<open>Propositional uniqueness principle.\<close> - -schematic_goal - assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" - shows "?a: p =[\<Sum>x:A. B x] <fst p, snd p>" - -text \<open>Proof by induction on @{term "p: \<Sum>x:A. B x"}:\<close> - -proof (rule Sum_elim[where ?p=p]) - text \<open>We prove the base case.\<close> - fix x y assume asm: "x: A" "y: B x" show "refl <x,y>: <x,y> =[\<Sum>x:A. B x] <fst <x,y>, snd <x,y>>" - proof compute - show "x: A" and "y: B x" by (fact asm)+ \<comment> \<open>Hint the correct types.\<close> - - text \<open>And now @{method derive} takes care of the rest. -\<close> - qed (derive lems: assms asm) -qed (derive lems: assms) - - -section \<open>Exercises\<close> - -paragraph \<open>Exercise 1.13\<close> - -abbreviation "not" ("\<not>_") where "\<not>A \<equiv> A \<rightarrow> \<zero>" - -text "This proof requires the use of universe cumulativity." - -proposition assumes "A: U i" shows "\<^bold>\<lambda>f. f`(inr(\<^bold>\<lambda>a. f`(inl a))): \<not>(\<not>(A + \<not>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 \<longrightarrow> U(i)" "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" - shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w: U(i)" -by (routine add: assms) - -\<comment> \<open>Correctly determines the type of the pair.\<close> -schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> <a, b> : ?A" -by routine - -\<comment> \<open>Finds pair (too easy).\<close> -schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B" -apply (rule intros) -apply assumption+ -done - -\<comment> \<open>Function application. We still often have to explicitly specify types.\<close> -lemma "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>" -proof compute - show "\<And>x. x: A \<Longrightarrow> <x,0>: A \<times> \<nat>" by routine -qed - -text \<open> -The proof below takes a little more work than one might expect; it would be nice to have a one-line method or proof. -\<close> - -lemma "\<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>" -proof (compute, routine) - show "\<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>y. <a,y>)`b \<equiv> <a,b>" - proof compute - show "\<And>b. \<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>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 \<open>Synthesis of the predecessor function\<close> - -text \<open> -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. -\<close> - -text \<open>First we show that the property we want is well-defined.\<close> - -lemma pred_welltyped: "\<Sum>pred: \<nat>\<rightarrow>\<nat>. (pred`0 =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n): U O" -by routine - -text \<open> -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>\<nat> 0"} and @{term "\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n"}. -What if we require *definitional* instead of just propositional equality? -\<close> - -schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n" -apply compute -prefer 4 apply compute -apply (rule Nat_routine | compute)+ -oops -\<comment> \<open>Something in the original proof broke when I revamped the theory. The completion of this derivation is left as an exercise to the reader.\<close> - -text \<open> -The above proof finds a candidate, namely @{term "\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n"}. -We prove this has the required type and properties. -\<close> - -definition pred :: t where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n" - -lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" -unfolding pred_def by routine - -lemma pred_props: "<refl 0, \<^bold>\<lambda>n. refl n>: (pred`0 =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n)" -unfolding pred_def by derive - -theorem "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" -by (derive lems: pred_type pred_props) - - -end |