diff options
author | Josh Chen | 2018-09-18 11:39:40 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-18 11:39:40 +0200 |
commit | a9588dfbd929fbc1b53a5c9b4f41fc5eb4ed4e46 (patch) | |
tree | ef21f4328214618f98ee465e92fb3308dfb786da /ex/Methods.thy | |
parent | a2bb39ee8002eccc04b0cdaa82143840e6ec2565 (diff) | |
parent | 6857e783fa5cb91f058be322a18fb9ea583f2aad (diff) |
Merge branch 'develop', ready for release 0.1.0
Diffstat (limited to '')
-rw-r--r-- | ex/Methods.thy | 73 |
1 files changed, 23 insertions, 50 deletions
diff --git a/ex/Methods.thy b/ex/Methods.thy index c78af14..09975b0 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -1,76 +1,49 @@ -(* Title: HoTT/ex/Methods.thy - Author: Josh Chen +(* +Title: ex/Methods.thy +Author: Joshua Chen +Date: 2018 -HoTT method usage examples +Basic HoTT method usage examples. *) theory Methods - imports "../HoTT" -begin +imports "../HoTT" +begin -text "Wellformedness results, metatheorems written into the object theory using the wellformedness rules." lemma assumes "A : U(i)" "B: A \<longrightarrow> U(i)" "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" - shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U(i)" -by (routine lems: assms) - - -lemma - assumes "\<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z: U(i)" - shows - "A : U(i)" and - "B: A \<longrightarrow> U(i)" and - "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and - "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)" -proof - - show - "A : U(i)" and - "B: A \<longrightarrow> U(i)" and - "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" and - "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<longrightarrow> U(i)" - by (derive lems: assms) -qed - - -text "Typechecking and constructing inhabitants:" + shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w: U(i)" +by (routine add: assms) -\<comment> \<open>Correctly determines the type of the pair\<close> +\<comment> \<open>Correctly determines the type of the pair.\<close> schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> <a, b> : ?A" by routine \<comment> \<open>Finds pair (too easy).\<close> schematic_goal "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B" -apply (rule Sum_intro) +apply (rule intros) apply assumption+ done - -text " - Function application. - The proof methods are not yet automated as well as I would like; we still often have to explicitly specify types. -" - -lemma - assumes "A: U(i)" "a: A" - shows "(\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>" +\<comment> \<open>Function application. We still often have to explicitly specify types.\<close> +lemma "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>" proof compute show "\<And>x. x: A \<Longrightarrow> <x,0>: A \<times> \<nat>" by routine -qed (routine lems: assms) - +qed -lemma - assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "a: A" "b: B(a)" - shows "(\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>" -proof compute - show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>y. <x,y>: \<Prod>y:B(x). \<Sum>x:A. B(x)" by (routine lems: assms) +text \<open> +The proof below takes a little more work than one might expect; it would be nice to have a one-line method or proof. +\<close> - show "(\<^bold>\<lambda>b. <a,b>)`b \<equiv> <a, b>" +lemma "\<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>" +proof (compute, routine) + show "\<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>y. <a,y>)`b \<equiv> <a,b>" proof compute - show "\<And>b. b: B(a) \<Longrightarrow> <a, b>: \<Sum>x:A. B(x)" by (routine lems: assms) - qed fact -qed fact + show "\<And>b. \<lbrakk>A: U i; B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x" by routine + qed +qed end |