diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/Subgoal.thy | 63 | ||||
| -rw-r--r-- | tests/Test.thy | 105 |
2 files changed, 47 insertions, 121 deletions
diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy deleted file mode 100644 index 82d7e5d..0000000 --- a/tests/Subgoal.thy +++ /dev/null @@ -1,63 +0,0 @@ -theory Subgoal - imports "../HoTT" -begin - - -text " - Proof of \<open>rpathcomp_type\<close> (see EqualProps.thy) in apply-style. - Subgoaling can be used to fix variables and apply the elimination rules. -" - -lemma rpathcomp_type: - assumes "A: U(i)" - shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" -unfolding rpathcomp_def -apply standard - subgoal premises 1 for x \<comment> \<open>\<open>subgoal\<close> is the proof script version of \<open>fix-assume-show\<close>.\<close> - apply standard - subgoal premises 2 for y - apply standard - subgoal premises 3 for p - apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) - \<comment> \<open>specifying \<open>?A=A\<close> is crucial here to prevent the next \<open>subgoal\<close> from binding a schematic ?A which should be instantiated to \<open>A\<close>.\<close> - prefer 4 - apply standard - apply (rule Prod_intro) - subgoal premises 4 for u z q - apply (rule Equal_elim[where ?x=u and ?y=z]) - apply (routine lems: assms 4) - done - apply (routine lems: assms 1 2 3) - done - apply (routine lems: assms 1 2) - done - apply fact - done -apply fact -done - - -text " - \<open>subgoal\<close> converts schematic variables to fixed free variables, making it unsuitable for use in \<open>schematic_goal\<close> proofs. - This is the same thing as being unable to start a ``sub schematic-goal'' inside an ongoing proof. - - This is a problem for syntheses which need to use induction (elimination rules), as these often have to be applied to fixed variables, while keeping any schematic variables intact. -" - -schematic_goal rpathcomp_synthesis: - assumes "A: U(i)" - shows "?a: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" - -text " - Try (and fail) to synthesize the constant for path composition, following the proof of \<open>rpathcomp_type\<close> below. -" - -apply (rule intros) - apply (rule intros) - apply (rule intros) - subgoal 123 for x y p - apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A]) - oops - - -end diff --git a/tests/Test.thy b/tests/Test.thy index b0eb87a..6f9f996 100644 --- a/tests/Test.thy +++ b/tests/Test.thy @@ -1,121 +1,110 @@ -(* Title: HoTT/tests/Test.thy - Author: Josh Chen - Date: Aug 2018 +(* +Title: tests/Test.thy +Author: Joshua Chen +Date: 2018 -This is an old "test suite" from early implementations of the theory. -It is not always guaranteed to be up to date, or reflect most recent versions of the theory. +This is an old test suite from early implementations. +It is not always guaranteed to be up to date or to reflect most recent versions of the theory. *) theory Test - imports "../HoTT" +imports "../HoTT" + begin -text " - A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified. - - Things that *should* be automated: - - Checking that \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>. - - Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair? -" +text \<open> +A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified. + +Things that *should* be automated: +\<^item> Checking that @{term A} is a well-formed type, when writing things like @{prop "x: A"} and @{prop "A: U i"}. +\<^item> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair? +\<close> declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]] - \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close> +\<comment> \<open>Turn on trace for unification and the Simplifier, for debugging.\<close> -section \<open>\<Pi>-type\<close> +section \<open>\<Prod>-type\<close> subsection \<open>Typing functions\<close> -text " - Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following. -" +text \<open>Declaring @{thm Prod_intro} with the @{attribute intro} attribute enables @{method rule} to prove the following.\<close> -proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" by (routine lems: assms) +proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" +by (routine add: assms) proposition assumes "A : U(i)" and "A \<equiv> B" shows "\<^bold>\<lambda>x. x : B \<rightarrow> A" proof - have "A \<rightarrow> A \<equiv> B \<rightarrow> A" using assms by simp - moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (routine lems: assms) + moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (routine add: assms) ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp qed proposition assumes "A : U(i)" and "B : U(i)" shows "\<^bold>\<lambda>x y. x : A \<rightarrow> B \<rightarrow> A" -by (routine lems: assms) - +by (routine add: assms) subsection \<open>Function application\<close> -proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (derive lems: assms) - -text "Currying:" +proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" +by (derive lems: assms) lemma assumes "a : A" and "\<And>x. x: A \<Longrightarrow> B(x): U(i)" shows "(\<^bold>\<lambda>x y. y)`a \<equiv> \<^bold>\<lambda>y. y" -proof compute - show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. y : B(x) \<rightarrow> B(x)" by (routine lems: assms) -qed fact +by (derive lems: assms) -lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b" by derive +lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b" +by derive -lemma "\<lbrakk>A: U(i); a : A \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y" -proof compute - show "\<And>x. \<lbrakk>A: U(i); x: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>y. f x y: \<Prod>y:B(x). C x y" - proof - oops +lemma "\<lbrakk>A: U(i); a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y" +proof derive +oops \<comment> \<open>Missing some premises.\<close> lemma "\<lbrakk>a : A; b : B(a); c : C(a)(b)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. \<^bold>\<lambda>y. \<^bold>\<lambda>z. f x y z)`a`b`c \<equiv> f a b c" - oops +proof derive +oops subsection \<open>Currying functions\<close> proposition curried_function_formation: - fixes A B C - assumes - "A : U(i)" and - "B: A \<longrightarrow> U(i)" and - "\<And>x. C(x): B(x) \<longrightarrow> U(i)" + assumes "A : U(i)" and "B: A \<longrightarrow> U(i)" and "\<And>x. C(x): B(x) \<longrightarrow> U(i)" shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U(i)" - by (routine lems: assms) - +by (routine add: assms) proposition higher_order_currying_formation: assumes - "A: U(i)" and - "B: A \<longrightarrow> U(i)" and + "A: U(i)" and "B: A \<longrightarrow> U(i)" and "\<And>x y. y: B(x) \<Longrightarrow> C(x)(y): U(i)" and "\<And>x y z. z : C(x)(y) \<Longrightarrow> D(x)(y)(z): U(i)" shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z): U(i)" - by (routine lems: assms) - +by (routine add: assms) lemma curried_type_judgment: - assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "\<And>x y. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y" + assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "\<And>x y. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y" shows "\<^bold>\<lambda>x y. f x y : \<Prod>x:A. \<Prod>y:B(x). C x y" - by (routine lems: assms) +by (routine add: assms) -text " - Polymorphic identity function is now trivial due to lambda expression polymorphism. - (Was more involved in previous monomorphic incarnations.) -" +text \<open> +Polymorphic identity function is now trivial due to lambda expression polymorphism. +It was more involved in previous monomorphic incarnations. +\<close> -definition Id :: "Term" where "Id \<equiv> \<^bold>\<lambda>x. x" - -lemma "\<lbrakk>x: A\<rbrakk> \<Longrightarrow> Id`x \<equiv> x" -unfolding Id_def by (compute, routine) +lemma "x: A \<Longrightarrow> id`x \<equiv> x" +by derive section \<open>Natural numbers\<close> -text "Automatic proof methods recognize natural numbers." +text \<open>Automatic proof methods recognize natural numbers.\<close> + +proposition "succ(succ(succ 0)): \<nat>" by routine -proposition "succ(succ(succ 0)): Nat" by routine end |