From 515872533295e8464799467303fff923b52a2c01 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 15 Sep 2018 20:51:39 +0200 Subject: begin reorganizing --- tests/Test.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests/Test.thy') diff --git a/tests/Test.thy b/tests/Test.thy index b0eb87a..de65dbd 100644 --- a/tests/Test.thy +++ b/tests/Test.thy @@ -23,7 +23,7 @@ declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit \ \Turn on trace for unification and the simplifier, for debugging.\ -section \\-type\ +section \\-type\ subsection \Typing functions\ -- cgit v1.2.3 From 6857e783fa5cb91f058be322a18fb9ea583f2aad Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 18 Sep 2018 11:38:54 +0200 Subject: Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0! --- tests/Test.thy | 103 ++++++++++++++++++++++++++------------------------------- 1 file changed, 46 insertions(+), 57 deletions(-) (limited to 'tests/Test.thy') diff --git a/tests/Test.thy b/tests/Test.thy index de65dbd..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 \A\ is a well-formed type, when writing things like \x : A\ and \A : U\. - - Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair? -" +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: +\<^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? +\ declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]] - \ \Turn on trace for unification and the simplifier, for debugging.\ +\ \Turn on trace for unification and the Simplifier, for debugging.\ section \\-type\ subsection \Typing functions\ -text " - Declaring \Prod_intro\ with the \intro\ attribute (in HoTT.thy) enables \standard\ to prove the following. -" +text \Declaring @{thm Prod_intro} with the @{attribute intro} attribute enables @{method rule} to prove the following.\ -proposition assumes "A : U(i)" shows "\<^bold>\x. x: A \ A" by (routine lems: assms) +proposition assumes "A : U(i)" shows "\<^bold>\x. x: A \ A" +by (routine add: assms) proposition assumes "A : U(i)" and "A \ B" shows "\<^bold>\x. x : B \ A" proof - have "A \ A \ B \ A" using assms by simp - moreover have "\<^bold>\x. x : A \ A" by (routine lems: assms) + moreover have "\<^bold>\x. x : A \ A" by (routine add: assms) ultimately show "\<^bold>\x. x : B \ A" by simp qed proposition assumes "A : U(i)" and "B : U(i)" shows "\<^bold>\x y. x : A \ B \ A" -by (routine lems: assms) - +by (routine add: assms) subsection \Function application\ -proposition assumes "a : A" shows "(\<^bold>\x. x)`a \ a" by (derive lems: assms) - -text "Currying:" +proposition assumes "a : A" shows "(\<^bold>\x. x)`a \ a" +by (derive lems: assms) lemma assumes "a : A" and "\x. x: A \ B(x): U(i)" shows "(\<^bold>\x y. y)`a \ \<^bold>\y. y" -proof compute - show "\x. x : A \ \<^bold>\y. y : B(x) \ B(x)" by (routine lems: assms) -qed fact +by (derive lems: assms) -lemma "\A: U(i); B: U(i); a : A; b : B\ \ (\<^bold>\x y. y)`a`b \ b" by derive +lemma "\A: U(i); B: U(i); a : A; b : B\ \ (\<^bold>\x y. y)`a`b \ b" +by derive -lemma "\A: U(i); a : A \ \ (\<^bold>\x y. f x y)`a \ \<^bold>\y. f a y" -proof compute - show "\x. \A: U(i); x: A\ \ \<^bold>\y. f x y: \y:B(x). C x y" - proof - oops +lemma "\A: U(i); a : A\ \ (\<^bold>\x y. f x y)`a \ \<^bold>\y. f a y" +proof derive +oops \ \Missing some premises.\ lemma "\a : A; b : B(a); c : C(a)(b)\ \ (\<^bold>\x. \<^bold>\y. \<^bold>\z. f x y z)`a`b`c \ f a b c" - oops +proof derive +oops subsection \Currying functions\ proposition curried_function_formation: - fixes A B C - assumes - "A : U(i)" and - "B: A \ U(i)" and - "\x. C(x): B(x) \ U(i)" + assumes "A : U(i)" and "B: A \ U(i)" and "\x. C(x): B(x) \ U(i)" shows "\x:A. \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 \ U(i)" and + "A: U(i)" and "B: A \ U(i)" and "\x y. y: B(x) \ C(x)(y): U(i)" and "\x y z. z : C(x)(y) \ D(x)(y)(z): U(i)" shows "\x:A. \y:B(x). \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 \ U(i)" "\x y. \x : A; y : B(x)\ \ f x y : C x y" + assumes "A: U(i)" and "B: A \ U(i)" and "\x y. \x : A; y : B(x)\ \ f x y : C x y" shows "\<^bold>\x y. f x y : \x:A. \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 \ +Polymorphic identity function is now trivial due to lambda expression polymorphism. +It was more involved in previous monomorphic incarnations. +\ -definition Id :: "Term" where "Id \ \<^bold>\x. x" - -lemma "\x: A\ \ Id`x \ x" -unfolding Id_def by (compute, routine) +lemma "x: A \ id`x \ x" +by derive section \Natural numbers\ -text "Automatic proof methods recognize natural numbers." +text \Automatic proof methods recognize natural numbers.\ + +proposition "succ(succ(succ 0)): \" by routine -proposition "succ(succ(succ 0)): Nat" by routine end -- cgit v1.2.3