From bd6fd85d8c102f006c89ec471f7f8cc701a0dd4d Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 14 May 2018 10:42:22 +0200 Subject: Added precedences. Need to figure out how to organize metatypes. --- HoTT.thy | 25 ++++++++++++------------- HoTT_Test.thy | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ test.thy | 42 ------------------------------------------ 3 files changed, 70 insertions(+), 55 deletions(-) create mode 100644 HoTT_Test.thy delete mode 100644 test.thy diff --git a/HoTT.thy b/HoTT.thy index 3e5ba71..682319d 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -17,8 +17,8 @@ typedecl Term subsection \Judgements\ consts - is_a_type :: "Term \ prop" ("(_ : U)") (* Add precedences when I figure them out! *) - is_of_type :: "Term \ Term \ prop" ("(_ : _)") + is_a_type :: "Term \ prop" ("(_ : U)" [0] 1000) + is_of_type :: "Term \ Term \ prop" ("(3_ :/ _)" [0, 0] 1000) subsection \Basic axioms\ subsubsection \Definitional equality\ @@ -30,15 +30,12 @@ Note that the Pure framework already provides axioms and results for the various which we make use of and extend where necessary. \ - -theorem DefEq_symmetry: "\A B. A \ B \ B \ A" - by (rule Pure.symmetric) - subsubsection \Type-related properties\ axiomatization where - equal_types: "\A B x. \A \ B; x : A\ \ x : B" and - inhabited_implies_type: "\x A. x : A \ A : U" + 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" subsection \Basic types\ @@ -47,16 +44,18 @@ 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. + +Note that the syntax \<^bold>\ (bold lambda) clashes with the proof term syntax! +(See \
2.5.2, The Isabelle/Isar Implementation.) *) axiomatization Function :: "Term \ Term \ Term" (infixr "\" 10) and - lambda :: "(Term \ Term) \ Term" (binder "\<^bold>\" 10) and - (* Is bold lambda already used by something else? Proof transformers in Pure maybe?... *) - appl :: "Term \ Term \ Term" ("(_`_)") + lambda :: "Term \ Term \ Term \ Term" ("(3\<^bold>\_:_./ _)" [1000, 0, 0] 10) and + appl :: "Term \ Term \ Term" ("(3_`/_)" [10, 10] 10) where - Function_form: "\A B. \A : U; B : U\ \ A\B : U" and - Function_intro: "\A B b. (\x. x : A \ b(x) : B) \ \<^bold>\x. b(x) : A\B" and + 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 *) diff --git a/HoTT_Test.thy b/HoTT_Test.thy new file mode 100644 index 0000000..b37ac76 --- /dev/null +++ b/HoTT_Test.thy @@ -0,0 +1,58 @@ +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/test.thy b/test.thy deleted file mode 100644 index d22e710..0000000 --- a/test.thy +++ /dev/null @@ -1,42 +0,0 @@ -theory test -imports HoTT -begin - -text \Check trivial stuff:\ -lemma "Null : U" - by (rule Null_form) - -text \ -Do functions behave like we expect them to? -(Or, is my implementation at least somewhat correct?... -\ - -lemma "A \ B \ (\<^bold>\x. x) : B\A" -proof - - have "A \ B \ B \ A" by (rule DefEq_symmetry) - then have "\x. A \ B \ x : B \ x : A" by (rule equal_types) - thus "A \ B \ (\<^bold>\x. 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 -- cgit v1.2.3