aboutsummaryrefslogtreecommitdiff
path: root/ex
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--ex/HoTT book/Ch1.thy47
-rw-r--r--ex/Methods.thy73
-rw-r--r--ex/Synthesis.thy94
3 files changed, 81 insertions, 133 deletions
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 \<open>HoTT Book, Chapter 1\<close>
-section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close>
+section \<open>1.6 Dependent pair types (\<Sum>-types)\<close>
-text "Propositional uniqueness principle:"
+paragraph \<open>Propositional uniqueness principle.\<close>
schematic_goal
- assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)"
- shows "?a: p =[\<Sum>x:A. B(x)] <fst p, snd p>"
+ 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 "Proof by induction on \<open>p: \<Sum>x:A. B(x)\<close>:"
+text \<open>Proof by induction on @{term "p: \<Sum>x:A. B x"}:\<close>
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,y>): <x,y> =[\<Sum>x:A. B(x)] <fst <x,y>, snd <x,y>>"
- proof (subst (0 1) comp)
- text "
- The computation rules for \<open>fst\<close> and \<open>snd\<close> require that \<open>x\<close> and \<open>y\<close> 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 \<open>fst\<close> and \<open>snd\<close>."
- show "x: A" and "y: B(x)" by (fact asm)+
+ 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>
-text "Exercise 1.13"
+paragraph \<open>Exercise 1.13\<close>
-abbreviation "not" ("\<not>'(_')") where "\<not>(A) \<equiv> A \<rightarrow> \<zero>"
+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 U_cumulative[where ?A=\<zero> and ?i=O and ?j=i])
+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
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 \<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 lems: assms)
-
-
-lemma
- assumes "\<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z: U(i)"
- shows
- "A : U(i)" and
- "B: A \<longrightarrow> U(i)" and
- "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and
- "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)"
-proof -
- show
- "A : U(i)" and
- "B: A \<longrightarrow> U(i)" and
- "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and
- "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)"
- by (derive lems: assms)
-qed
-
-
-text "Typechecking and constructing inhabitants:"
+ 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>
+\<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 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>\<lambda>x. <x,0>)`a \<equiv> <a,0>"
+\<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 (routine lems: assms)
-
+qed
-lemma
- assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "a: A" "b: B(a)"
- shows "(\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>"
-proof compute
- show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>y. <x,y>: \<Prod>y:B(x). \<Sum>x:A. B(x)" by (routine lems: assms)
+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>
- show "(\<^bold>\<lambda>b. <a,b>)`b \<equiv> <a, b>"
+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. b: B(a) \<Longrightarrow> <a, b>: \<Sum>x:A. B(x)" by (routine lems: assms)
- qed fact
-qed fact
+ 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
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 \<open>Synthesis of the predecessor function\<close>
-text "
- In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers.
-
- This is also done in \<open>CTT.thy\<close>; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely.
-"
+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 "First we show that the property we want is well-defined."
+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)"
+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 "
- Now we look for an inhabitant of this type.
- Observe that we're looking for a lambda term \<open>pred\<close> satisfying \<open>(pred`0) =\<^sub>\<nat> 0\<close> and \<open>\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n\<close>.
- What if we require **definitional** equality instead of just propositional equality?
-"
+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
-prefer 3 apply compute
-apply (rule Nat_routine Nat_elim | compute | assumption)+
-done
-
-text "
- The above proof finds a candidate, namely \<open>\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n\<close>.
- We prove this has the required type and properties.
-"
-
-definition pred :: Term 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)"
-proof (routine lems: pred_type)
- have *: "pred`0 \<equiv> 0" unfolding pred_def
- proof compute
- show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine
- show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0"
- proof compute
- show "\<nat>: U(O)" ..
- qed routine
- qed rule
- then show "refl(0): (pred`0) =\<^sub>\<nat> 0" by (subst *) routine
-
- show "\<^bold>\<lambda>n. refl(n): \<Prod>n:\<nat>. (pred`(succ(n))) =\<^sub>\<nat> n"
- unfolding pred_def proof
- show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ((\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n)`succ(n)) =\<^sub>\<nat> n"
- proof compute
- show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine
- show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ind\<^sub>\<nat> (\<lambda>a b. a) 0 (succ n) =\<^sub>\<nat> n"
- proof compute
- show "\<nat>: U(O)" ..
- qed routine
- qed rule
- qed rule
-qed
-
-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 (routine lems: pred_welltyped pred_type pred_props)
+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