From 9ea0e76f92383ab14859cd5857f5a3ef1acec2c0 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 23 May 2018 08:26:37 +0200 Subject: pre-system upgrade commit --- HoTT.thy | 75 +++++++++++++++++++++++++++++-------------------------- HoTT_Test.thy | 58 ------------------------------------------ HoTT_Theorems.thy | 68 +++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 108 insertions(+), 93 deletions(-) delete mode 100644 HoTT_Test.thy create mode 100644 HoTT_Theorems.thy diff --git a/HoTT.thy b/HoTT.thy index 682319d..a13b1d4 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -1,63 +1,66 @@ theory HoTT -imports Pure + imports Pure begin section \Setup\ -text \ -For ML files, routines and setup. -\ + +text "For ML files, routines and setup." section \Basic definitions\ -text \ -A single meta-level type \Term\ suffices to implement the object-level types and terms. -For now we do not implement universes, but simply follow the informal notation in the HoTT book. -\ (* Actually unsure if a single meta-type suffices... *) + +text "A single meta-level type \Term\ suffices to implement the object-level types and terms. +We do not implement universes, but simply follow the informal notation in the HoTT book." typedecl Term -subsection \Judgements\ +subsection \Judgments\ + consts is_a_type :: "Term \ prop" ("(_ : U)" [0] 1000) - is_of_type :: "Term \ Term \ prop" ("(3_ :/ _)" [0, 0] 1000) + is_of_type :: "[Term, Term] \ prop" ("(3_ :/ _)" [0, 0] 1000) subsection \Basic axioms\ + subsubsection \Definitional equality\ -text\ -We take the meta-equality \, defined by the Pure framework for any of its terms, -and use it additionally for definitional/judgmental equality of types and terms in our theory. -Note that the Pure framework already provides axioms and results for the various properties of \, -which we make use of and extend where necessary. -\ +text "We take the meta-equality \, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory. + +Note that the Pure framework already provides axioms and results for various properties of \, which we make use of and extend where necessary." subsubsection \Type-related properties\ axiomatization where - term_substitution: "\(A::Term) (x::Term) y::Term. x \ y \ A(x) \ A(y)" and - equal_types: "\(A::Term) (B::Term) x::Term. \A \ B; x : A\ \ x : B" and - inhabited_implies_type: "\(x::Term) A::Term. x : A \ A : U" + equal_types: "\(A::Term) (B::Term) (x::Term). \A \ B; x : A\ \ x : B" and + inhabited_implies_type: "\(x::Term) (A::Term). x : A \ A : U" subsection \Basic types\ -subsubsection \Nondependent function type\ -(* -Write this for now to test stuff, later I should make -this an instance of the dependent function. -Same for the nondependent product below. +subsubsection \Dependent product type\ -Note that the syntax \<^bold>\ (bold lambda) clashes with the proof term syntax! -(See \
2.5.2, The Isabelle/Isar Implementation.) -*) +consts + Prod :: "[Term, (Term \ Term)] \ Term" +syntax + "_Prod" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 10) +translations + "\x:A. B" \ "CONST Prod A (\x. B)" +(* The above syntax translation binds the x in B *) axiomatization - Function :: "Term \ Term \ Term" (infixr "\" 10) and - lambda :: "Term \ Term \ Term \ Term" ("(3\<^bold>\_:_./ _)" [1000, 0, 0] 10) and - appl :: "Term \ Term \ Term" ("(3_`/_)" [10, 10] 10) + lambda :: "(Term \ Term) \ Term" (binder "\<^bold>\" 10) and + appl :: "[Term, Term] \ Term" ("(3_`/_)" [10, 10] 60) where - Function_form: "\(A::Term) B::Term. \A : U; B : U\ \ A\B : U" and - Function_intro: "\(A::Term) (B::Term) b::Term. (\x. x : A \ b(x) : B) \ \<^bold>\x:A. b(x) : A\B" and - Function_elim: "\A B f a. \f : A\B; a : A\ \ f`a : B" - (* beta and eta reductions should go here *) + Prod_form: "\(A::Term) (B::Term \ Term). \A : U; \(x::Term). x : A \ B(x) : U\ \ \x:A. B(x) : U" and + Prod_intro: "\(A::Term) (B::Term \ Term) (b::Term \ Term). \A : U; \(x::Term). x : A \ b(x) : B(x)\ \ \<^bold>\x. b(x) : \x:A. B(x)" and + Prod_elim: "\(A::Term) (B::Term \ Term) (f::Term) (a::Term). \f : \x:A. B(x); a : A\ \ f`a : B(a)" and + Prod_comp: "\(b::Term \ Term) (a::Term). (\<^bold>\x. b(x))`a \ b(a)" and + Prod_uniq: "\(A::Term) (B::Term \ Term) (f::Term). \f : \x:A. B(x)\ \ \<^bold>\x. (f`x) \ f" + +text "Observe that the metatype \Term \ Term\ is used to represent type families, for example \Prod\ takes a type \A\ and a type family \B\ and constructs a dependent function type from them." + +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)." + +abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 30) +where "A\B \ \_:A. B" subsubsection \Nondependent product type\ @@ -72,8 +75,10 @@ where Product_comp: "\A B C g a b. \C : U; g : A\B\C; a : A; b : B\ \ rec_Product(A,B,C,g)`(a,b) \ (g`a)`b" \ \Projection onto first component\ +(* definition proj1 :: "Term \ Term \ Term" ("(proj1\_,_\)") where - "proj1\A,B\ \ rec_Product(A, B, A, \<^bold>\x. \<^bold>\y. x)" + "\A B x y. proj1\A,B\ \ rec_Product(A, B, A, \<^bold>\x:A. \<^bold>\y:B. (\x. x))" +*) subsubsection \Empty type\ diff --git a/HoTT_Test.thy b/HoTT_Test.thy deleted file mode 100644 index b37ac76..0000000 --- a/HoTT_Test.thy +++ /dev/null @@ -1,58 +0,0 @@ -theory HoTT_Test -imports HoTT -begin - -text \Check trivial stuff:\ - -lemma "Null : U" - by (rule Null_form) - -lemma "\A \ B; x : B\ \ x : A" -proof - - assume "A \ B" - then have "B \ A" by (rule Pure.symmetric) - then have "x : B \ x :A" by (rule equal_types) - oops -(* qed---figure out how to discharge assumptions *) - -text \ -Do functions behave like we expect them to? -(Or, is my implementation at least somewhat correct?... -\ - -\ {* NOTE!!! The issues with substitution here. -We need the HoTT term \b\ and the type family \B\ to indeed be a Pure \-term! -This seems to mean that I have to implement the HoTT types in more than one Pure type. -See CTT.thy for examples. -*} - -lemma "A \ B \ (\<^bold>\x:A. x) : B\A" -proof - - have "A \ B \ B \ A" by (rule Pure.symmetric) - then have "\x::Term. A \ B \ x : B \ x : A" by (rule equal_types) - thus "A \ B \ (\<^bold>\x:A. x) : B\A" by (rule Function_intro) -qed - -lemma "\<^bold>\x. \<^bold>\y. x : A\B\A" -proof - - have "\x. x : A \ \<^bold>\y. x : B \ A" by (rule Function_intro) - thus "\<^bold>\x. \<^bold>\y. x : A\B\A" by (rule Function_intro) -qed - -text \Here's a dumb proof that 2 is a natural number:\ - -lemma "succ(succ 0) : Nat" -proof - - have "0 : Nat" by (rule Nat_intro1) - from this have "(succ 0) : Nat" by (rule Nat_intro2) - thus "succ(succ 0) : Nat" by (rule Nat_intro2) -qed - -text \ -We can of course iterate the above for as many applications of \succ\ as we like. -The next thing to do is to implement some kind of induction tactic to automate such proofs. - -When we get more stuff working, I'd like to aim for formalizing the encode-decode method. -\ - -end \ No newline at end of file diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy new file mode 100644 index 0000000..bea3dfe --- /dev/null +++ b/HoTT_Theorems.thy @@ -0,0 +1,68 @@ +theory HoTT_Theorems + imports HoTT +begin + +text "A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified." + +section \Foundational stuff\ + +theorem "\A : U; A \ B\ \ B : U" by simp + +section \Functions\ + +lemma "A : U \ \<^bold>\x. x : A\A" + by (rule Prod_intro) + +text "Note that there is no provision for declaring the type of bound variables outside of the scope of a lambda expression. +Hence a statement like \x : A\ is not needed (nor possible!) in the premises of the following lemma." + +lemma "\A : U; A \ B\ \ \<^bold>\x. x : B\A" +proof - + assume + 0: "A : U" and + 1: "A \ B" + from 0 have 2: "\<^bold>\x. x : A\A" by (rule Prod_intro) + from 1 have 3: "A\A \ B\A" by simp + from 3 and 2 show "\<^bold>\x. x : B\A" by (rule equal_types) + qed + +lemma "\A : U; B : U; x : A\ \ \<^bold>\y. x : B\A" +proof - +assume + 1: "A : U" and + 2: "B : U" and + 3: "x : A" +then show "\<^bold>\y. x : B\A" +proof - +from 3 have "\<^bold>\y. x : B\A" by (rule Prod_intro) +qed +qed + +lemma "\A : U; B : U\ \ \<^bold>\x. \<^bold>\y. x : A\B\A" +proof - + fix x + assume + "A : U" and + "B : U" and + "x : A" + then have "\<^bold>\y. x : B\A" by (rule Prod_intro) + +qed + +section \Nats\ + +text "Here's a dumb proof that 2 is a natural number." + +lemma "succ(succ 0) : Nat" +proof - + have "0 : Nat" by (rule Nat_intro1) + from this have "(succ 0) : Nat" by (rule Nat_intro2) + thus "succ(succ 0) : Nat" by (rule Nat_intro2) +qed + +text "We can of course iterate the above for as many applications of \succ\ as we like. +The next thing to do is to implement induction to automate such proofs. + +When we get more stuff working, I'd like to aim for formalizing the encode-decode method to be able to prove the only naturals are 0 and those obtained from it by \succ\." + +end \ No newline at end of file -- cgit v1.2.3