diff options
author | Josh Chen | 2018-05-10 19:13:05 +0200 |
---|---|---|
committer | Josh Chen | 2018-05-10 19:13:05 +0200 |
commit | 5b217a7eb36906eabdcb6ec626a2d02e0f94c308 (patch) | |
tree | af22f3e27f96d533370fa368f7c742c165dee3d9 /test.thy | |
parent | 502e5d2526e59c9b5d98fbbaef93b5fbc0c3011d (diff) |
Decided to go with no explicit type declarations in object-lambda expressions. Everything in the proof stuff is working at the moment.
Diffstat (limited to 'test.thy')
-rw-r--r-- | test.thy | 29 |
1 files changed, 18 insertions, 11 deletions
@@ -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 |