diff options
| -rw-r--r-- | HoTT.thy | 39 | ||||
| -rw-r--r-- | test.thy | 29 |
2 files changed, 43 insertions, 25 deletions
@@ -3,32 +3,42 @@ imports Pure begin section \<open>Setup\<close> - -(* ML files, routines and setup should probably go here *) +text \<open> +For ML files, routines and setup. +\<close> section \<open>Basic definitions\<close> - text \<open> A single meta-level type \<open>Term\<close> 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. -\<close> -(* Actually unsure if a single meta-type suffices... *) +\<close> (* Actually unsure if a single meta-type suffices... *) typedecl Term subsection \<open>Judgements\<close> - consts is_a_type :: "Term \<Rightarrow> prop" ("(_ : U)") (* Add precedences when I figure them out! *) is_of_type :: "Term \<Rightarrow> Term \<Rightarrow> prop" ("(_ : _)") subsection \<open>Basic axioms\<close> +subsubsection \<open>Definitional equality\<close> +text\<open> +We take the meta-equality \<equiv>, 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. -axiomatization -where - inhabited_implies_type: "\<And>x A. x : A \<Longrightarrow> A : U" and - equal_types: "\<And>A B x. A \<equiv> B \<Longrightarrow> x : A \<Longrightarrow> x : B" +Note that the Pure framework already provides axioms and results for the various properties of \<equiv>, +which we make use of and extend where necessary. +\<close> + + +theorem DefEq_symmetry: "\<And>A B. A \<equiv> B \<Longrightarrow> B \<equiv> A" + by (rule Pure.symmetric) + +subsubsection \<open>Type-related properties\<close> + +axiomatization where + equal_types: "\<And>A B x. \<lbrakk>A \<equiv> B; x : A\<rbrakk> \<Longrightarrow> x : B" and + inhabited_implies_type: "\<And>x A. x : A \<Longrightarrow> A : U" subsection \<open>Basic types\<close> @@ -41,7 +51,8 @@ Same for the nondependent product below. axiomatization Function :: "Term \<Rightarrow> Term \<Rightarrow> Term" (infixr "\<rightarrow>" 10) and - lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" (binder "\<^bold>\<lambda>" 10) and (* precedence! *) + lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" (binder "\<^bold>\<lambda>" 10) and + (* Is bold lambda already used by something else? Proof transformers in Pure maybe?... *) appl :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(_`_)") where Function_form: "\<And>A B. \<lbrakk>A : U; B : U\<rbrakk> \<Longrightarrow> A\<rightarrow>B : U" and @@ -62,8 +73,8 @@ where Product_comp: "\<And>A B C g a b. \<lbrakk>C : U; g : A\<rightarrow>B\<rightarrow>C; a : A; b : B\<rbrakk> \<Longrightarrow> rec_Product(A,B,C,g)`(a,b) \<equiv> (g`a)`b" \<comment> \<open>Projection onto first component\<close> -definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1'(_,_'))") where - "proj1(A,B) \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x. \<^bold>\<lambda>y. x)" +definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1\<langle>_,_\<rangle>)") where + "proj1\<langle>A,B\<rangle> \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x. \<^bold>\<lambda>y. x)" subsubsection \<open>Empty type\<close> @@ -2,12 +2,19 @@ theory test imports HoTT begin +text \<open>Check trivial stuff:\<close> lemma "Null : U" by (rule Null_form) +text \<open> +Do functions behave like we expect them to? +(Or, is my implementation at least somewhat correct?... +\<close> + lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A" proof - - have "\<And>x. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types) + have "A \<equiv> B \<Longrightarrow> B \<equiv> A" by (rule DefEq_symmetry) + then have "\<And>x. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types) thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A" by (rule Function_intro) qed @@ -17,19 +24,19 @@ proof - thus "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A" by (rule Function_intro) qed -(* The previous proofs are nice, BUT I want to be able to do something like the following: -lemma "x : A \<Longrightarrow> \<^bold>\<lambda>x. x : B\<rightarrow>B" <Fail> -i.e. I want to be able to associate a type to variables, and have the type remembered by any -binding I define later. - -Do I need to give up using the \<open>binder\<close> syntax in order to do this? -*) - +text \<open>Here's a dumb proof that 2 is a natural number:\<close> lemma "succ(succ 0) : Nat" proof - - have "(succ 0) : Nat" by (rule Nat_intro2) - from this have "succ(succ 0) : Nat" by (rule Nat_intro2) + 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 \<open> +We can of course iterate the above for as many applications of \<open>succ\<close> 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. +\<close> end
\ No newline at end of file |