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 | |
| parent | a2bb39ee8002eccc04b0cdaa82143840e6ec2565 (diff) | |
| parent | 6857e783fa5cb91f058be322a18fb9ea583f2aad (diff) | |
Merge branch 'develop', ready for release 0.1.0
| -rw-r--r-- | Coprod.thy | 67 | ||||
| -rw-r--r-- | Empty.thy | 25 | ||||
| -rw-r--r-- | Equal.thy | 58 | ||||
| -rw-r--r-- | EqualProps.thy | 361 | ||||
| -rw-r--r-- | HoTT.thy | 18 | ||||
| -rw-r--r-- | HoTT_Base.thy | 111 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 79 | ||||
| -rw-r--r-- | Nat.thy | 63 | ||||
| -rw-r--r-- | Prod.thy | 106 | ||||
| -rw-r--r-- | ProdProps.thy | 57 | ||||
| -rw-r--r-- | Proj.thy | 59 | ||||
| -rw-r--r-- | Sum.thy | 62 | ||||
| -rw-r--r-- | Unit.thy | 33 | ||||
| -rw-r--r-- | Univalence.thy | 195 | ||||
| -rw-r--r-- | ex/HoTT book/Ch1.thy | 47 | ||||
| -rw-r--r-- | ex/Methods.thy | 73 | ||||
| -rw-r--r-- | ex/Synthesis.thy | 94 | ||||
| -rw-r--r-- | tests/Subgoal.thy | 63 | ||||
| -rw-r--r-- | tests/Test.thy | 105 |
19 files changed, 588 insertions, 1088 deletions
@@ -1,65 +1,50 @@ -(* Title: HoTT/Coprod.thy - Author: Josh Chen +(* +Title: Coprod.thy +Author: Joshua Chen +Date: 2018 Coproduct type *) theory Coprod - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and type rules\<close> axiomatization - Coprod :: "[Term, Term] \<Rightarrow> Term" (infixr "+" 50) and - inl :: "Term \<Rightarrow> Term" and - inr :: "Term \<Rightarrow> Term" and - indCoprod :: "[Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>+)") + Coprod :: "[t, t] \<Rightarrow> t" (infixr "+" 50) and + inl :: "t \<Rightarrow> t" and + inr :: "t \<Rightarrow> t" and + indCoprod :: "[t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>+)") where - Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" -and - Coprod_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl a: A + B" -and - Coprod_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr b: A + B" -and + Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and + + Coprod_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl a: A + B" and + + Coprod_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr b: A + B" and + Coprod_elim: "\<lbrakk> + u: A + B; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y); - u: A + B - \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u" -and + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda> x. c x) (\<lambda>y. d y) u: C u" and + Coprod_comp_inl: "\<lbrakk> + a: A; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y); - a: A - \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inl a) \<equiv> c a" -and + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inl a) \<equiv> c a" and + Coprod_comp_inr: "\<lbrakk> + b: B; C: A + B \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> c x: C (inl x); - \<And>y. y: B \<Longrightarrow> d y: C (inr y); - b: B - \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b" - - -text "Admissible formation inference rules:" - -axiomatization where - Coprod_wellform1: "A + B: U i \<Longrightarrow> A: U i" -and - Coprod_wellform2: "A + B: U i \<Longrightarrow> B: U i" - - -text "Rule attribute declarations:" - -lemmas Coprod_intro = Coprod_intro_inl Coprod_intro_inr + \<And>y. y: B \<Longrightarrow> d y: C (inr y) \<rbrakk> \<Longrightarrow> ind\<^sub>+ (\<lambda>x. c x) (\<lambda>y. d y) (inr b) \<equiv> d b" +lemmas Coprod_form [form] +lemmas Coprod_routine [intro] = Coprod_form Coprod_intro_inl Coprod_intro_inr Coprod_elim lemmas Coprod_comp [comp] = Coprod_comp_inl Coprod_comp_inr -lemmas Coprod_wellform [wellform] = Coprod_wellform1 Coprod_wellform2 -lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_elim end @@ -1,29 +1,26 @@ -(* Title: HoTT/Empty.thy - Author: Josh Chen +(* +Title: Empty.thy +Author: Joshua Chen +Date: 2018 Empty type *) theory Empty - imports HoTT_Base -begin - +imports HoTT_Base -section \<open>Constants and type rules\<close> +begin -section \<open>Empty type\<close> axiomatization - Empty :: Term ("\<zero>") and - indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)") + Empty :: t ("\<zero>") and + indEmpty :: "t \<Rightarrow> t" ("(1ind\<^sub>\<zero>)") where - Empty_form: "\<zero>: U O" -and - Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U i; z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> z: C z" - + Empty_form: "\<zero>: U O" and -text "Rule attribute declarations:" + Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a" +lemmas Empty_form [form] lemmas Empty_routine [intro] = Empty_form Empty_elim @@ -1,66 +1,52 @@ -(* Title: HoTT/Equal.thy - Author: Josh Chen +(* +Title: Equal.thy +Author: Joshua Chen +Date: 2018 Equality type *) theory Equal - imports HoTT_Base +imports HoTT_Base + begin -section \<open>Constants and syntax\<close> +section \<open>Basic definitions\<close> axiomatization - Equal :: "[Term, Term, Term] \<Rightarrow> Term" and - refl :: "Term \<Rightarrow> Term" and - indEqual :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>=)") + Equal :: "[t, t, t] \<Rightarrow> t" and + refl :: "t \<Rightarrow> t" and + indEqual :: "[t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>=)") syntax - "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) - "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =[_]/ _)" [101, 0, 101] 100) + "_equal" :: "[t, t, t] \<Rightarrow> t" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) + "_equal_ascii" :: "[t, t, t] \<Rightarrow> t" ("(3_ =[_]/ _)" [101, 0, 101] 100) + translations "a =[A] b" \<rightleftharpoons> "CONST Equal A a b" "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b" +axiomatization where + Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U i" and -section \<open>Type rules\<close> + Equal_intro: "a : A \<Longrightarrow> (refl a): a =\<^sub>A a" and -axiomatization where - Equal_form: "\<lbrakk>A: U i; a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U i" -and - Equal_intro: "a : A \<Longrightarrow> (refl a): a =\<^sub>A a" -and Equal_elim: "\<lbrakk> + p: x =\<^sub>A y; x: A; y: A; - p: x =\<^sub>A y; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i - \<rbrakk> \<Longrightarrow> ind\<^sub>= f p : C x y p" -and + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) p : C x y p" and + Equal_comp: "\<lbrakk> a: A; \<And>x. x: A \<Longrightarrow> f x: C x x (refl x); - \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i - \<rbrakk> \<Longrightarrow> ind\<^sub>= f (refl a) \<equiv> f a" - + \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U i \<rbrakk> \<Longrightarrow> ind\<^sub>= (\<lambda>x. f x) (refl a) \<equiv> f a" -text "Admissible inference rules for equality type formation:" - -axiomatization where - Equal_wellform1: "a =\<^sub>A b: U i \<Longrightarrow> A: U i" -and - Equal_wellform2: "a =\<^sub>A b: U i \<Longrightarrow> a: A" -and - Equal_wellform3: "a =\<^sub>A b: U i \<Longrightarrow> b: A" - - -text "Rule attribute declarations:" - -lemmas Equal_comp [comp] -lemmas Equal_wellform [wellform] = Equal_wellform1 Equal_wellform2 Equal_wellform3 +lemmas Equal_form [form] lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim +lemmas Equal_comp [comp] end diff --git a/EqualProps.thy b/EqualProps.thy index 5db8487..abb2623 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -1,298 +1,137 @@ -(* Title: HoTT/EqualProps.thy - Author: Josh Chen +(* +Title: EqualProps.thy +Author: Joshua Chen +Date: 2018 Properties of equality *) theory EqualProps - imports - HoTT_Methods - Equal - Prod -begin - - -section \<open>Symmetry / Path inverse\<close> - -definition inv :: "Term \<Rightarrow> Term" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. (refl x)) p" - -text " - In the proof below we begin by using path induction on \<open>p\<close> with the application of \<open>rule Equal_elim\<close>, telling Isabelle the specific substitutions to use. - The proof is finished with a standard application of the relevant type rules. -" - -lemma inv_type: - assumes "A : U i" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\<inverse>: y =\<^sub>A x" -unfolding inv_def -by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms) - \<comment> \<open>The type doesn't depend on \<open>p\<close> so we don't need to specify \<open>?p\<close> in the \<open>where\<close> clause above.\<close> - -text " - The next proof requires explicitly telling Isabelle what to substitute on the RHS of the typing judgment after the initial application of the type rules. - (If viewing this inside Isabelle, place the cursor after the \<open>proof\<close> statement and observe the second subgoal.) -" - -lemma inv_comp: - assumes "A : U i " and "a : A" shows "(refl a)\<inverse> \<equiv> refl a" -unfolding inv_def -proof compute - show "\<And>x. x: A \<Longrightarrow> refl x: x =\<^sub>A x" .. -qed (routine lems: assms) - - -section \<open>Transitivity / Path composition\<close> - -text " - Raw composition function, of type \<open>\<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)\<close> polymorphic over the type \<open>A\<close>. -" - -definition rpathcomp :: Term where "rpathcomp \<equiv> \<^bold>\<lambda>_ _ p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>_ q. ind\<^sub>= (\<lambda>x. (refl x)) q) p" - -text " - More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: -" - -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 -proof - fix x assume 1: "x: A" - show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" - proof - fix y assume 2: "y: A" - show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" - proof - fix p assume 3: "p: x =\<^sub>A y" - show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z" - proof (rule Equal_elim[where ?x=x and ?y=y]) - show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix u z q assume asm: "u: A" "z: A" "q: u =\<^sub>A z" - show "ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) - qed (routine lems: assms) - qed (rule assms) - qed (routine lems: assms 1 2 3) - qed (routine lems: assms 1 2) - qed (rule assms) -qed fact - -corollary - assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z" - by (routine lems: assms rpathcomp_type) - -text " - The following proof is very long, chiefly because for every application of \<open>`\<close> we have to show the wellformedness of the type family appearing in the equality computation rule. -" - -lemma rpathcomp_comp: - assumes "A: U i" and "a: A" - shows "rpathcomp`a`a`(refl a)`a`(refl a) \<equiv> refl a" -unfolding rpathcomp_def -proof compute - fix x assume 1: "x: A" - show "\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" - proof - fix y assume 2: "y: A" - show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)" - proof - fix p assume 3: "p: x =\<^sub>A y" - show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z" - proof (rule Equal_elim[where ?x=x and ?y=y]) - show "\<And>u. u: A \<Longrightarrow> \<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>u z. \<lbrakk>u: A; z: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix u z assume asm: "u: A" "z: A" - show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) - qed (routine lems: assms) - qed (rule assms) - qed (routine lems: assms 1 2 3) - qed (routine lems: assms 1 2) - qed (rule assms) - - next show "(\<^bold>\<lambda>y p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p)`a`(refl a)`a`(refl a) \<equiv> refl a" - proof compute - fix y assume 1: "y: A" - show "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: a =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z)" - proof - fix p assume 2: "p: a =\<^sub>A y" - show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. y =\<^sub>A z \<rightarrow> a =\<^sub>A z" - proof (rule Equal_elim[where ?x=a and ?y=y]) - fix u assume 3: "u: A" - show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix z assume 4: "z: A" - show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 3 4) - qed (routine lems: assms 3 4) - qed fact - qed (routine lems: assms 1 2) - qed (routine lems: assms 1) - - next show "(\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z. \<^bold>\<lambda>q. ind\<^sub>= refl q) p)`(refl a)`a`(refl a) \<equiv> refl a" - proof compute - fix p assume 1: "p: a =\<^sub>A a" - show "ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q) p: \<Prod>z:A. a =\<^sub>A z \<rightarrow> a =\<^sub>A z" - proof (rule Equal_elim[where ?x=a and ?y=a]) - fix u assume 2: "u: A" - show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix z assume 3: "z: A" - show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3) - qed (routine lems: assms 2 3) - qed fact - qed (routine lems: assms 1) - - next show "(ind\<^sub>=(\<lambda>_. \<^bold>\<lambda>z q. ind\<^sub>= refl q)(refl a))`a`(refl a) \<equiv> refl a" - proof compute - fix u assume 1: "u: A" - show "\<^bold>\<lambda>z q. ind\<^sub>= refl q: \<Prod>z:A. u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - fix z assume 2: "z: A" - show "\<^bold>\<lambda>q. ind\<^sub>= refl q: u =\<^sub>A z \<rightarrow> u =\<^sub>A z" - proof - show "\<And>q. q: u =\<^sub>A z \<Longrightarrow> ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2) - qed (routine lems: assms 1 2) - qed fact - - next show "(\<^bold>\<lambda>z q. ind\<^sub>= refl q)`a`(refl a) \<equiv> refl a" - proof compute - fix a assume 1: "a: A" - show "\<^bold>\<lambda>q. ind\<^sub>= refl q: a =\<^sub>A a \<rightarrow> a =\<^sub>A a" - proof - show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl q: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1) - qed (routine lems: assms 1) - - next show "(\<^bold>\<lambda>q. ind\<^sub>= refl q)`(refl a) \<equiv> refl a" - proof compute - show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= refl p: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms) - show "ind\<^sub>= refl (refl a) \<equiv> refl a" - proof compute - show "\<And>x. x: A \<Longrightarrow> refl(x): x =\<^sub>A x" .. - qed (routine lems: assms) - qed (routine lems: assms) - qed fact - qed (routine lems: assms) - qed (routine lems: assms) - qed fact -qed fact - - -text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." - -axiomatization pathcomp :: "[Term, Term] \<Rightarrow> Term" (infixl "\<bullet>" 120) where - pathcomp_def: "\<lbrakk> - A: U i; - x: A; y: A; z: A; - p: x =\<^sub>A y; q: y =\<^sub>A z - \<rbrakk> \<Longrightarrow> p \<bullet> q \<equiv> rpathcomp`x`y`p`z`q" +imports HoTT_Methods Equal Prod +begin -lemma pathcomp_type: - assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "p \<bullet> q: x =\<^sub>A z" - -proof (subst pathcomp_def) - show "A: U i" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" by fact+ -qed (routine lems: assms rpathcomp_type) +section \<open>Symmetry of equality/Path inverse\<close> -lemma pathcomp_comp: - assumes "A : U i" and "a : A" shows "(refl a) \<bullet> (refl a) \<equiv> refl a" -by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) +definition inv :: "t \<Rightarrow> t" ("_\<inverse>" [1000] 1000) where "p\<inverse> \<equiv> ind\<^sub>= (\<lambda>x. refl x) p" +lemma inv_type: "\<lbrakk>A: U i; x: A; y: A; p: x =\<^sub>A y\<rbrakk> \<Longrightarrow> p\<inverse>: y =\<^sub>A x" +unfolding inv_def by (elim Equal_elim) routine -lemmas EqualProps_type [intro] = inv_type pathcomp_type -lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp +lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (refl a)\<inverse> \<equiv> refl a" +unfolding inv_def by compute routine -section \<open>Higher groupoid structure of types\<close> +section \<open>Transitivity of equality/Path composition\<close> -lemma - assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" - shows - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] p \<bullet> (refl y)" and - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =\<^sub>A y] (refl x) \<bullet> p" +text \<open> +Composition function, of type @{term "x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)"} polymorphic over @{term A}, @{term x}, @{term y}, and @{term z}. +\<close> -proof - - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] p \<bullet> (refl y)" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ +definition pathcomp :: t where "pathcomp \<equiv> \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. (refl x)) q) p" - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p =[x =[A] y] (refl x) \<bullet> p" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ -qed +syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 120) +translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q" +lemma pathcomp_type: + assumes "A: U i" and "x: A" "y: A" "z: A" + shows "pathcomp: x =\<^sub>A y \<rightarrow> (y =\<^sub>A z) \<rightarrow> (x =\<^sub>A z)" +unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms) -lemma - assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" - shows - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)" and - "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)" +corollary pathcomp_trans: + assumes "A: U i" and "x: A" "y: A" "z: A" and "p: x =\<^sub>A y" "q: y =\<^sub>A z" + shows "p \<bullet> q: x =\<^sub>A z" +by (routine add: assms pathcomp_type) -proof - - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse> \<bullet> p =[y =\<^sub>A y] (refl y)" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ +lemma pathcomp_comp: + assumes "A: U i" and "a: A" + shows "(refl a) \<bullet> (refl a) \<equiv> refl a" +unfolding pathcomp_def proof compute + show "(ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) (refl a))`(refl a) \<equiv> refl a" + proof compute + show "\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q): a =\<^sub>A a \<rightarrow> a =\<^sub>A a" + by (routine add: assms) - show "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p \<bullet> p\<inverse> =[x =\<^sub>A x] (refl x)" - by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms)+ -qed + show "(\<^bold>\<lambda>q. (ind\<^sub>= (\<lambda>x. refl x) q))`(refl a) \<equiv> refl a" + proof compute + show "\<And>q. q: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>x. refl x) q: a =\<^sub>A a" by (routine add: assms) + qed (derive lems: assms) + qed (routine add: assms) + show "\<And>p. p: a =\<^sub>A a \<Longrightarrow> ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. refl x) q) p: a =\<^sub>A a \<rightarrow> a =\<^sub>A a" + by (routine add: assms) +qed (routine add: assms) -lemma - assumes "A: U i" "x: A" "y: A" "p: x =\<^sub>A y" - shows "ind\<^sub>= (\<lambda>u. refl (refl u)) p: p\<inverse>\<inverse> =[x =\<^sub>A y] p" -by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (derive lems: assms) -text "Next we construct a proof term of associativity of path composition." +section \<open>Higher groupoid structure of types\<close> -schematic_goal +schematic_goal pathcomp_right_id: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: p \<bullet> (refl y) =[x =\<^sub>A y] p" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) \<comment> \<open>@{method elim} does not seem to work with schematic goals.\<close> + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)" + by (derive lems: assms pathcomp_comp) +qed (routine add: assms pathcomp_type) + +schematic_goal pathcomp_left_id: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: (refl x) \<bullet> p =[x =\<^sub>A y] p" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x) =[x =\<^sub>A x] (refl x)" + by (derive lems: assms pathcomp_comp) +qed (routine add: assms pathcomp_type) + +schematic_goal pathcomp_left_inv: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: (p\<inverse> \<bullet> p) =[y =\<^sub>A y] refl(y)" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse> \<bullet> (refl x) =[x =\<^sub>A x] (refl x)" + by (derive lems: assms inv_comp pathcomp_comp) +qed (routine add: assms inv_type pathcomp_type) + +schematic_goal pathcomp_right_inv: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: (p \<bullet> p\<inverse>) =[x =\<^sub>A x] refl(x)" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x) \<bullet> (refl x)\<inverse> =[x =\<^sub>A x] (refl x)" + by (derive lems: assms inv_comp pathcomp_comp) +qed (routine add: assms inv_type pathcomp_type) + +schematic_goal inv_involutive: + assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" + shows "?a: p\<inverse>\<inverse> =[x =\<^sub>A y] p" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + show "\<And>x. x: A \<Longrightarrow> refl(refl x): (refl x)\<inverse>\<inverse> =[x =\<^sub>A x] (refl x)" + by (derive lems: assms inv_comp) +qed (routine add: assms inv_type) + +schematic_goal pathcomp_assoc: assumes - "A: U i" + "A: U(i)" "x: A" "y: A" "z: A" "w: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" shows - "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A z] (p \<bullet> q) \<bullet> r" - -apply (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) -apply (rule assms)+ -\<comment> \<open>Continue by substituting \<open>refl x \<bullet> q = q\<close> etc.\<close> -sorry + "?a: p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] (p \<bullet> q) \<bullet> r" +proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) + fix x assume "x: A" + show "refl (q \<bullet> r): (refl x) \<bullet> (q \<bullet> r) =[x =\<^sub>A w] ((refl x) \<bullet> q) \<bullet> r" + \<comment> \<open>This requires substitution of *propositional* equality. \<close> + sorry + oops section \<open>Transport\<close> -definition transport :: "Term \<Rightarrow> Term" where - "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p" +definition transport :: "t \<Rightarrow> t" where "transport p \<equiv> ind\<^sub>= (\<lambda>_. (\<^bold>\<lambda>x. x)) p" -text "Note that \<open>transport\<close> is a polymorphic function in our formulation." +text \<open>Note that @{term transport} is a polymorphic function in our formulation.\<close> -lemma transport_type: - assumes - "A: U i" "P: A \<longrightarrow> U i" - "x: A" "y: A" - "p: x =\<^sub>A y" - shows "transport p: P x \<rightarrow> P y" -unfolding transport_def -by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (routine lems: assms) - -lemma transport_comp: - assumes "A: U i" and "x: A" - shows "transport (refl x) \<equiv> id" -unfolding transport_def by (derive lems: assms) +lemma transport_type: "\<lbrakk>p: x =\<^sub>A y; x: A; y: A; A: U i; P: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> transport p: P x \<rightarrow> P y" +unfolding transport_def by (elim Equal_elim) routine + +lemma transport_comp: "\<lbrakk>A: U i; x: A\<rbrakk> \<Longrightarrow> transport (refl x) \<equiv> id" +unfolding transport_def by derive end @@ -1,12 +1,13 @@ -(* Title: HoTT/HoTT.thy - Author: Josh Chen +(* +Title: HoTT.thy +Author: Joshua Chen +Date: 2018 Homotopy type theory *) theory HoTT imports - (* Basic theories *) HoTT_Base HoTT_Methods @@ -22,18 +23,21 @@ Unit (* Derived definitions and properties *) EqualProps -ProdProps Proj begin -lemmas forms = - Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form + +text \<open>Rule bundles:\<close> + lemmas intros = - Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro + Nat_intro_0 Nat_intro_succ Prod_intro Sum_intro Equal_intro Coprod_intro_inl Coprod_intro_inr Unit_intro + lemmas elims = Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim + lemmas routines = Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine + end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 916f6aa..2ad0ac5 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,97 +1,82 @@ -(* Title: HoTT/HoTT_Base.thy - Author: Josh Chen +(* +Title: HoTT_Base.thy +Author: Joshua Chen +Date: 2018 -Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell. +Basic setup of a homotopy type theory object logic with a cumulative Russell-style universe hierarchy. *) theory HoTT_Base - imports Pure -begin - +imports Pure -section \<open>Foundational definitions\<close> +begin -text "Meta syntactic type for object-logic types and terms." -typedecl Term +section \<open>Basic setup\<close> +typedecl t \<comment> \<open>Type of object types and terms\<close> +typedecl ord \<comment> \<open>Type of meta-level numerals\<close> -text " - Formalize the typing judgment \<open>a: A\<close>. - For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it. -" +axiomatization + O :: ord and + Suc :: "ord \<Rightarrow> ord" and + lt :: "[ord, ord] \<Rightarrow> prop" (infix "<" 999) and + leq :: "[ord, ord] \<Rightarrow> prop" (infix "\<le>" 999) +where + lt_Suc [intro]: "n < (Suc n)" and + lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and + leq_min [intro]: "O \<le> n" -judgment has_type :: "[Term, Term] \<Rightarrow> prop" ("(3_:/ _)" [0, 0] 1000) +section \<open>Judgment\<close> -section \<open>Universe hierarchy\<close> +judgment hastype :: "[t, t] \<Rightarrow> prop" ("(3_:/ _)") -text "Finite meta-ordinals to index the universes." -typedecl Ord +section \<open>Universes\<close> axiomatization - O :: Ord and - S :: "Ord \<Rightarrow> Ord" ("S _" [0] 1000) and - lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<" 999) and - leq :: "[Ord, Ord] \<Rightarrow> prop" (infix "\<le>" 999) + U :: "ord \<Rightarrow> t" where - lt_min: "\<And>n. O < S n" -and - lt_monotone1: "\<And>n. n < S n" -and - lt_monotone2: "\<And>m n. m < n \<Longrightarrow> S m < S n" -and - leq_min: "\<And>n. O \<le> n" -and - leq_monotone1: "\<And>n. n \<le> S n" -and - leq_monotone2: "\<And>m n. m \<le> n \<Longrightarrow> S m \<le> S n" - -lemmas Ord_rules [intro] = lt_min lt_monotone1 lt_monotone2 leq_min leq_monotone1 leq_monotone2 - \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close> - -text "Define the universe types." + U_hierarchy: "i < j \<Longrightarrow> U i: U j" and + U_cumulative: "\<lbrakk>A: U i; i < j\<rbrakk> \<Longrightarrow> A: U j" and + U_cumulative': "\<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j" -axiomatization - U :: "Ord \<Rightarrow> Term" -where - U_hierarchy: "\<And>i j. i < j \<Longrightarrow> U i: U j" -and - U_cumulative: "\<And>A i j. \<lbrakk>A: U i; i \<le> j\<rbrakk> \<Longrightarrow> A: U j" +text \<open> +Using method @{method rule} with @{thm U_cumulative} is unsafe, if applied blindly it will typically lead to non-termination. +One should instead use @{method elim}, or instantiate @{thm U_cumulative} suitably. -text " - The rule \<open>U_cumulative\<close> is very unsafe: if used as-is it will usually lead to an infinite rewrite loop! - To avoid this, it should be instantiated before being applied. -" +@{thm U_cumulative'} is an alternative rule used by the method \<open>lift\<close> in @{file HoTT_Methods.thy}. +\<close> section \<open>Type families\<close> -text " - The following abbreviation constrains the output type of a meta lambda expression when given input of certain type. -" - -abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop" ("(1_: _ \<longrightarrow> _)") +abbreviation (input) constrained :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop" ("(1_:/ _ \<longrightarrow> _)") where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x: B)" -text " - The above is used to define type families, which are constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are small types. -" +text \<open> +The abbreviation @{abbrev constrained} is used to define type families, which are constrained expressions @{term "P: A \<longrightarrow> B"}, where @{term "A::t"} and @{term "B::t"} are small types. +\<close> -type_synonym Typefam = "Term \<Rightarrow> Term" +type_synonym tf = "t \<Rightarrow> t" \<comment> \<open>Type of type families\<close> section \<open>Named theorems\<close> -text " - Named theorems to be used by proof methods later (see HoTT_Methods.thy). - - \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are usually passed to invocations of the method \<open>subst\<close> to perform equational rewriting. -" - -named_theorems wellform named_theorems comp +named_theorems form + +text \<open> +Declare named theorems to be used by proof methods defined in @{file HoTT_Methods.thy}. + +@{attribute comp} declares computation rules, which are used by the \<open>compute\<close> method, and may also be passed to invocations of the method \<open>subst\<close> to perform equational rewriting. + +@{attribute form} declares type formation rules. +These are mainly used by the \<open>cumulativity\<close> method, which lifts types into higher universes. +\<close> + +(* Todo: Set up the Simplifier! *) end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 32e412b..f0cee6c 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -1,46 +1,47 @@ -(* Title: HoTT/HoTT_Methods.thy - Author: Josh Chen +(* +Title: HoTT_Methods.thy +Author: Joshua Chen +Date: 2018 -Method setup for the HoTT library. Relies heavily on Eisbach. +Method setup for the HoTT logic. *) theory HoTT_Methods - imports - "HOL-Eisbach.Eisbach" - "HOL-Eisbach.Eisbach_Tools" - HoTT_Base +imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" + begin -section \<open>Deriving typing judgments\<close> +section \<open>Handling universes\<close> -text " - \<open>routine\<close> proves routine type judgments \<open>a : A\<close> using the rules declared [intro] in the respective theory files, as well as additional provided lemmas. -" +method provelt = (rule lt_Suc | (rule lt_trans, (rule lt_Suc)+)+) -method routine uses lems = (assumption | rule lems | standard)+ +method hierarchy = (rule U_hierarchy, provelt) -text " - \<open>wellformed'\<close> finds a proof of any valid typing judgment derivable from the judgment passed as \<open>jdmt\<close>. - If no judgment is passed, it will try to resolve with the theorems declared \<open>wellform\<close>. - \<open>wellform\<close> is like \<open>wellformed'\<close> but takes multiple judgments. +method cumulativity declares form = ( + ((elim U_cumulative' | (rule U_cumulative', rule form)), rule leq_min) | + ((elim U_cumulative | (rule U_cumulative, rule form)), provelt) +) - The named theorem \<open>wellform\<close> is declared in HoTT_Base.thy. -" +text \<open> +Methods @{method provelt}, @{method hierarchy}, and @{method cumulativity} prove statements of the form +\<^item> \<open>n < (Suc (... (Suc n) ...))\<close>, +\<^item> \<open>U i: U (Suc (... (Suc i) ...))\<close>, and +\<^item> @{prop "A: U i \<Longrightarrow> A: U j"}, where @{prop "i \<le> j"} +respectively. +\<close> -method wellformed' uses jdmt declares wellform = - match wellform in rl: "PROP ?P" \<Rightarrow> \<open>( - catch \<open>rule rl[OF jdmt]\<close> \<open>fail\<close> | - catch \<open>wellformed' jdmt: rl[OF jdmt]\<close> \<open>fail\<close> - )\<close> -method wellformed uses lems = - match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed' jdmt: lem\<close> +section \<open>Deriving typing judgments\<close> +method routine uses add = (assumption | rule add | rule)+ -section \<open>Substitution and simplification\<close> +text \<open> +The method @{method routine} proves type judgments @{prop "a : A"} using the rules declared @{attribute intro} in the respective theory files, as well as additional provided lemmas passed using the modifier \<open>add\<close>. +\<close> -text "Import the \<open>subst\<close> method, used for substituting definitional equalities." + +section \<open>Substitution and simplification\<close> ML_file "~~/src/Tools/misc_legacy.ML" ML_file "~~/src/Tools/IsaPlanner/isand.ML" @@ -48,24 +49,32 @@ ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" ML_file "~~/src/Tools/IsaPlanner/zipper.ML" ML_file "~~/src/Tools/eqsubst.ML" -text "Perform basic single-step computations:" +\<comment> \<open>Import the @{method subst} method, used for substituting definitional equalities.\<close> + +method compute declares comp = (subst comp) -method compute uses lems = (subst lems comp | rule lems comp) +text \<open> +Method @{method compute} performs single-step simplifications, using any rules declared @{attribute comp} in the context. +Premises of the rule(s) applied are added as new subgoals. +\<close> section \<open>Derivation search\<close> -text " Combine \<open>routine\<close>, \<open>wellformed\<close>, and \<open>compute\<close> to search for derivations of judgments." +text \<open> +Combine @{method routine} and @{method compute} to search for derivations of judgments. +Also handle universes using @{method hierarchy} and @{method cumulativity}. +\<close> -method derive uses lems = (routine lems: lems | compute lems: lems | wellformed lems: lems)+ +method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ section \<open>Induction\<close> -text " - Placeholder section for the automation of induction, i.e. using the elimination rules. - At the moment one must directly apply them with \<open>rule X_elim\<close>. -" +text \<open> +Placeholder section for the automation of induction, i.e. using the elimination rules. +At the moment one must directly apply them with \<open>rule X_elim\<close>. +\<close> end @@ -1,54 +1,49 @@ -(* Title: HoTT/Nat.thy - Author: Josh Chen +(* +Title: Nat.thy +Author: Joshua Chen +Date: 2018 Natural numbers *) theory Nat - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and type rules\<close> axiomatization - Nat :: Term ("\<nat>") and - zero :: Term ("0") and - succ :: "Term \<Rightarrow> Term" and - indNat :: "[[Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<nat>)") + Nat :: t ("\<nat>") and + zero :: t ("0") and + succ :: "t \<Rightarrow> t" and + indNat :: "[[t, t] \<Rightarrow> t, t, t] \<Rightarrow> t" ("(1ind\<^sub>\<nat>)") where - Nat_form: "\<nat>: U O" -and - Nat_intro_0: "0: \<nat>" -and - Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" -and + Nat_form: "\<nat>: U O" and + + Nat_intro_0: "0: \<nat>" and + + Nat_intro_succ: "n: \<nat> \<Longrightarrow> succ n: \<nat>" and + Nat_elim: "\<lbrakk> - C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n); a: C 0; - n: \<nat> - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a n: C n" -and + n: \<nat>; + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a n: C n" and + Nat_comp_0: "\<lbrakk> + a: C 0; C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n); - a: C 0 - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a 0 \<equiv> a" -and + \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a 0 \<equiv> a" and + Nat_comp_succ: "\<lbrakk> - C: \<nat> \<longrightarrow> U i; - \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n); a: C 0; - n: \<nat> - \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> f a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)" - - -text "Rule attribute declarations:" + n: \<nat>; + C: \<nat> \<longrightarrow> U i; + \<And>n c. \<lbrakk>n: \<nat>; c: C n\<rbrakk> \<Longrightarrow> f n c: C (succ n) \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>n c. f n c) a (succ n) \<equiv> f n (ind\<^sub>\<nat> f a n)" -lemmas Nat_intro = Nat_intro_0 Nat_intro_succ -lemmas Nat_comp [comp] = Nat_comp_0 Nat_comp_succ -lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_elim +lemmas Nat_form [form] +lemmas Nat_routine [intro] = Nat_form Nat_intro_0 Nat_intro_succ Nat_elim +lemmas Nat_comps [comp] = Nat_comp_0 Nat_comp_succ end @@ -1,89 +1,91 @@ -(* Title: HoTT/Prod.thy - Author: Josh Chen +(* +Title: Prod.thy +Author: Joshua Chen +Date: 2018 -Dependent product (function) type +Dependent product type *) theory Prod - imports HoTT_Base +imports HoTT_Base HoTT_Methods + begin -section \<open>Constants and syntax\<close> +section \<open>Basic definitions\<close> axiomatization - Prod :: "[Term, Typefam] \<Rightarrow> Term" and - lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" (binder "\<^bold>\<lambda>" 30) and - appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60) - \<comment> \<open>Application binds tighter than abstraction.\<close> + Prod :: "[t, tf] \<Rightarrow> t" and + lambda :: "(t \<Rightarrow> t) \<Rightarrow> t" (binder "\<^bold>\<lambda>" 30) and + appl :: "[t, t] \<Rightarrow> t" ("(1_`/_)" [105, 106] 105) \<comment> \<open>Application binds tighter than abstraction.\<close> syntax - "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 30) - "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3PROD _:_./ _)" 30) + "_prod" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Prod>_:_./ _)" 30) + "_prod_ascii" :: "[idt, t, t] \<Rightarrow> t" ("(3II _:_./ _)" 30) -text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>." +text \<open>The translations below bind the variable @{term x} in the expressions @{term B} and @{term b}.\<close> translations "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)" - "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)" + "II x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)" -text "Nondependent functions are a special case." +text \<open>Non-dependent functions are a special case.\<close> -abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40) +abbreviation Fun :: "[t, t] \<Rightarrow> t" (infixr "\<rightarrow>" 40) where "A \<rightarrow> B \<equiv> \<Prod>_: A. B" +axiomatization where +\<comment> \<open>Type rules\<close> -section \<open>Type rules\<close> + Prod_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x: U i" and -axiomatization where - Prod_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x: U i" -and - Prod_intro: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; A: U i\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b x: \<Prod>x:A. B x" -and - Prod_elim: "\<lbrakk>f: \<Prod>x:A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" -and - Prod_appl: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; a: A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a" -and - Prod_uniq: "f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x. (f`x) \<equiv> f" -and - Prod_eq: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b x \<equiv> \<^bold>\<lambda>x. c x" - -text " - The Pure rules for \<open>\<equiv>\<close> only let us judge strict syntactic equality of object lambda expressions; Prod_eq is the actual definitional equality rule. - - Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation). -" - -text " - In addition to the usual type rules, it is a meta-theorem that whenever \<open>\<Prod>x:A. B x: U i\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A: U i\<close> and \<open>B: A \<longrightarrow> U i\<close>. - - That is to say, the following inference rules are admissible, and it simplifies proofs greatly to axiomatize them directly. -" + Prod_intro: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x: B x; A: U i\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b x: \<Prod>x:A. B x" and -axiomatization where - Prod_wellform1: "(\<Prod>x:A. B x: U i) \<Longrightarrow> A: U i" -and - Prod_wellform2: "(\<Prod>x:A. B x: U i) \<Longrightarrow> B: A \<longrightarrow> U i" + Prod_elim: "\<lbrakk>f: \<Prod>x:A. B x; a: A\<rbrakk> \<Longrightarrow> f`a: B a" and + + Prod_comp: "\<lbrakk>a: A; \<And>x. x: A \<Longrightarrow> b x: B x\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b x)`a \<equiv> b a" and + Prod_uniq: "f: \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x. f`x \<equiv> f" and -text "Rule attribute declarations---set up various methods to use the type rules." +\<comment> \<open>Congruence rules\<close> -lemmas Prod_comp [comp] = Prod_appl Prod_uniq -lemmas Prod_wellform [wellform] = Prod_wellform1 Prod_wellform2 + Prod_form_eq: "\<lbrakk>A: U i; B: A \<longrightarrow> U i; C: A \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x \<equiv> \<Prod>x:A. C x" and + + Prod_intro_eq: "\<lbrakk>\<And>x. x: A \<Longrightarrow> b x \<equiv> c x; A: U i\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b x \<equiv> \<^bold>\<lambda>x. c x" + +text \<open> +The Pure rules for \<open>\<equiv>\<close> only let us judge strict syntactic equality of object lambda expressions. +The actual definitional equality rule is @{thm Prod_intro_eq}. +Note that this is a separate rule from function extensionality. + +Note that the bold lambda symbol \<open>\<^bold>\<lambda>\<close> used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation). +\<close> + +lemmas Prod_form [form] lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim +lemmas Prod_comps [comp] = Prod_comp Prod_uniq -section \<open>Function composition\<close> +section \<open>Additional definitions\<close> -definition compose :: "[Term, Term] \<Rightarrow> Term" (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)" +definition compose :: "[t, t] \<Rightarrow> t" (infixr "o" 110) where "g o f \<equiv> \<^bold>\<lambda>x. g`(f`x)" -syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 110) +syntax "_compose" :: "[t, t] \<Rightarrow> t" (infixr "\<circ>" 110) translations "g \<circ> f" \<rightleftharpoons> "g o f" +declare compose_def [comp] + +lemma compose_assoc: + assumes "A: U i" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D x" + shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)" +by (derive lems: assms Prod_intro_eq) -section \<open>Polymorphic identity function\<close> +lemma compose_comp: + assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x" + shows "(\<^bold>\<lambda>x. c x) \<circ> (\<^bold>\<lambda>x. b x) \<equiv> \<^bold>\<lambda>x. c (b x)" +by (derive lems: assms Prod_intro_eq) -abbreviation id :: Term where "id \<equiv> \<^bold>\<lambda>x. x" +abbreviation id :: t where "id \<equiv> \<^bold>\<lambda>x. x" \<comment> \<open>Polymorphic identity function\<close> end diff --git a/ProdProps.thy b/ProdProps.thy deleted file mode 100644 index a68f79b..0000000 --- a/ProdProps.thy +++ /dev/null @@ -1,57 +0,0 @@ -(* Title: HoTT/ProdProps.thy - Author: Josh Chen - -Properties of the dependent product -*) - -theory ProdProps - imports - HoTT_Methods - Prod -begin - - -section \<open>Composition\<close> - -text " - The proof of associativity needs some guidance; it involves telling Isabelle to use the correct rule for \<Prod>-type definitional equality, and the correct substitutions in the subgoals thereafter. -" - -lemma compose_assoc: - assumes "A: U i" and "f: A \<rightarrow> B" "g: B \<rightarrow> C" "h: \<Prod>x:C. D x" - shows "(h \<circ> g) \<circ> f \<equiv> h \<circ> (g \<circ> f)" -proof (subst (0 1 2 3) compose_def) - show "\<^bold>\<lambda>x. (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> \<^bold>\<lambda>x. h`((\<^bold>\<lambda>y. g`(f`y))`x)" - proof (subst Prod_eq) - \<comment> \<open>Todo: set the Simplifier (or other simplification methods) up to use \<open>Prod_eq\<close>!\<close> - - show "\<And>x. x: A \<Longrightarrow> (\<^bold>\<lambda>y. h`(g`y))`(f`x) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)" - proof compute - show "\<And>x. x: A \<Longrightarrow> h`(g`(f`x)) \<equiv> h`((\<^bold>\<lambda>y. g`(f`y))`x)" - proof compute - show "\<And>x. x: A \<Longrightarrow> g`(f`x): C" by (routine lems: assms) - qed - show "\<And>x. x: B \<Longrightarrow> h`(g`x): D (g`x)" by (routine lems: assms) - qed (routine lems: assms) - qed fact -qed - - -lemma compose_comp: - assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x" - shows "(\<^bold>\<lambda>x. c x) \<circ> (\<^bold>\<lambda>x. b x) \<equiv> \<^bold>\<lambda>x. c (b x)" -proof (subst compose_def, subst Prod_eq) - show "\<And>a. a: A \<Longrightarrow> (\<^bold>\<lambda>x. c x)`((\<^bold>\<lambda>x. b x)`a) \<equiv> (\<^bold>\<lambda>x. c (b x))`a" - proof compute - show "\<And>a. a: A \<Longrightarrow> c ((\<^bold>\<lambda>x. b x)`a) \<equiv> (\<^bold>\<lambda>x. c (b x))`a" - by (derive lems: assms) - qed (routine lems: assms) -qed (derive lems: assms) - - -text "Set up the \<open>compute\<close> method to automatically simplify function compositions." - -lemmas compose_comp [comp] - - -end @@ -1,62 +1,43 @@ -(* Title: HoTT/Proj.thy - Author: Josh Chen +(* +Title: Proj.thy +Author: Joshua Chen +Date: 2018 Projection functions \<open>fst\<close> and \<open>snd\<close> for the dependent sum type. *) theory Proj - imports - HoTT_Methods - Prod - Sum -begin +imports HoTT_Methods Prod Sum +begin -definition fst :: "Term \<Rightarrow> Term" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p" -definition snd :: "Term \<Rightarrow> Term" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p" -text "Typing judgments and computation rules for the dependent and non-dependent projection functions." +definition fst :: "t \<Rightarrow> t" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p" +definition snd :: "t \<Rightarrow> t" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p" lemma fst_type: - assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "fst p: A" + assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "fst p: A" unfolding fst_def by (derive lems: assms) lemma fst_comp: assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "fst <a,b> \<equiv> a" -unfolding fst_def -proof compute - show "a: A" and "b: B a" by fact+ -qed (routine lems: assms)+ +unfolding fst_def by compute (derive lems: assms) lemma snd_type: - assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)" -unfolding snd_def -proof - show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> B (fst p): U i" by (derive lems: assms fst_type) - - fix x y - assume asm: "x: A" "y: B x" - show "y: B (fst <x,y>)" - proof (subst fst_comp) - show "A: U i" by (wellformed lems: assms(1)) - show "\<And>x. x: A \<Longrightarrow> B x: U i" by (wellformed lems: assms(1)) - qed fact+ -qed fact + assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)" +unfolding snd_def proof (derive lems: assms) + show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> fst p: A" using assms(1-2) by (rule fst_type) + + fix x y assume asm: "x: A" "y: B x" + show "y: B (fst <x,y>)" by (derive lems: asm assms fst_comp) +qed lemma snd_comp: assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "snd <a,b> \<equiv> b" -unfolding snd_def -proof compute - show "\<And>x y. y: B x \<Longrightarrow> y: B x" . - show "a: A" by fact - show "b: B a" by fact -qed (routine lems: assms) - - -text "Rule attribute declarations:" +unfolding snd_def by (derive lems: assms) -lemmas Proj_type [intro] = fst_type snd_type -lemmas Proj_comp [comp] = fst_comp snd_comp +lemmas Proj_types [intro] = fst_type snd_type +lemmas Proj_comps [comp] = fst_comp snd_comp end @@ -1,69 +1,59 @@ -(* Title: HoTT/Sum.thy - Author: Josh Chen +(* +Title: Sum.thy +Author: Joshua Chen +Date: 2018 Dependent sum type *) theory Sum - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and syntax\<close> axiomatization - Sum :: "[Term, Typefam] \<Rightarrow> Term" and - pair :: "[Term, Term] \<Rightarrow> Term" ("(1<_,/ _>)") and - indSum :: "[[Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<Sum>)") + Sum :: "[t, tf] \<Rightarrow> t" and + pair :: "[t, t] \<Rightarrow> t" ("(1<_,/ _>)") and + indSum :: "[[t, t] \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>\<Sum>)") syntax - "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20) - "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3SUM _:_./ _)" 20) + "_sum" :: "[idt, t, t] \<Rightarrow> t" ("(3\<Sum>_:_./ _)" 20) + "_sum_ascii" :: "[idt, t, t] \<Rightarrow> t" ("(3SUM _:_./ _)" 20) translations "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)" -text "Nondependent pair." - -abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) +abbreviation Pair :: "[t, t] \<Rightarrow> t" (infixr "\<times>" 50) where "A \<times> B \<equiv> \<Sum>_:A. B" +axiomatization where +\<comment> \<open>Type rules\<close> -section \<open>Type rules\<close> + Sum_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x: U i" and + + Sum_intro: "\<lbrakk>B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x" and -axiomatization where - Sum_form: "\<lbrakk>A: U i; B: A \<longrightarrow> U i\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x: U i" -and - Sum_intro: "\<lbrakk>B: A \<longrightarrow> U i; a: A; b: B a\<rbrakk> \<Longrightarrow> <a,b>: \<Sum>x:A. B x" -and Sum_elim: "\<lbrakk> p: \<Sum>x:A. B x; - \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y>; - C: \<Sum>x:A. B x \<longrightarrow> U i - \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f p: C p" (* What does writing \<lambda>x y. f(x, y) change? *) -and + C: \<Sum>x:A. B x \<longrightarrow> U i; + \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) p: C p" and + Sum_comp: "\<lbrakk> a: A; b: B a; - \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y>; B: A \<longrightarrow> U i; - C: \<Sum>x:A. B x \<longrightarrow> U i - \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> f <a,b> \<equiv> f a b" - -text "Admissible inference rules for sum formation:" - -axiomatization where - Sum_wellform1: "(\<Sum>x:A. B x: U i) \<Longrightarrow> A: U i" -and - Sum_wellform2: "(\<Sum>x:A. B x: U i) \<Longrightarrow> B: A \<longrightarrow> U i" + C: \<Sum>x:A. B x \<longrightarrow> U i; + \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f x y: C <x,y> \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum> (\<lambda>x y. f x y) <a,b> \<equiv> f a b" and +\<comment> \<open>Congruence rules\<close> -text "Rule attribute declarations:" + Sum_form_eq: "\<lbrakk>A: U i; B: A \<longrightarrow> U i; C: A \<longrightarrow> U i; \<And>x. x: A \<Longrightarrow> B x \<equiv> C x\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x \<equiv> \<Sum>x:A. C x" -lemmas Sum_comp [comp] -lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2 +lemmas Sum_form [form] lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim +lemmas Sum_comp [comp] end @@ -1,33 +1,32 @@ -(* Title: HoTT/Unit.thy - Author: Josh Chen +(* +Title: Unit.thy +Author: Joshua Chen +Date: 2018 Unit type *) theory Unit - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and type rules\<close> axiomatization - Unit :: Term ("\<one>") and - pt :: Term ("\<star>") and - indUnit :: "[Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<one>)") + Unit :: t ("\<one>") and + pt :: t ("\<star>") and + indUnit :: "[t, t] \<Rightarrow> t" ("(1ind\<^sub>\<one>)") where - Unit_form: "\<one>: U O" -and - Unit_intro: "\<star>: \<one>" -and - Unit_elim: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>; a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" -and - Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c" + Unit_form: "\<one>: U O" and + Unit_intro: "\<star>: \<one>" and -text "Rule attribute declarations:" + Unit_elim: "\<lbrakk>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and -lemmas Unit_comp [comp] + Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c" + +lemmas Unit_form [form] lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim +lemmas Unit_comp [comp] end diff --git a/Univalence.thy b/Univalence.thy index b7f4400..3c9b520 100644 --- a/Univalence.thy +++ b/Univalence.thy @@ -1,177 +1,88 @@ -(* Title: HoTT/Univalence.thy - Author: Josh Chen +(* +Title: Univalence.thy +Author: Joshua Chen +Date: 2018 Definitions of homotopy, equivalence and the univalence axiom. *) theory Univalence - imports - HoTT_Methods - EqualProps - ProdProps - Sum +imports HoTT_Methods EqualProps Prod Sum + begin section \<open>Homotopy and equivalence\<close> -text "We define polymorphic constants implementing the definitions of homotopy and equivalence." - -axiomatization homotopic :: "[Term, Term] \<Rightarrow> Term" (infix "~" 100) where - homotopic_def: "\<lbrakk> - f: \<Prod>x:A. B x; - g: \<Prod>x:A. B x - \<rbrakk> \<Longrightarrow> f ~ g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)" - -axiomatization isequiv :: "Term \<Rightarrow> Term" where - isequiv_def: "f: A \<rightarrow> B \<Longrightarrow> isequiv f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~ id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~ id)" - -definition equivalence :: "[Term, Term] \<Rightarrow> Term" (infix "\<simeq>" 100) - where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv f" +definition homotopic :: "[t, tf, t, t] \<Rightarrow> t" where "homotopic A B f g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)" +syntax "_homotopic" :: "[t, idt, t, t, t] \<Rightarrow> t" ("(1_ ~[_:_. _]/ _)" [101, 0, 0, 0, 101] 100) +translations "f ~[x:A. B] g" \<rightleftharpoons> "CONST homotopic A (\<lambda>x. B) f g" -text "The identity function is an equivalence:" - -lemma isequiv_id: - assumes "A: U i" and "id: A \<rightarrow> A" - shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id" -proof (derive lems: assms isequiv_def homotopic_def) - fix g assume asm: "g: A \<rightarrow> A" - show "id \<circ> g: A \<rightarrow> A" - unfolding compose_def by (routine lems: asm assms) - - show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" - unfolding compose_def by (routine lems: asm assms) - next - - show "<\<^bold>\<lambda>x. x, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~ id" - unfolding compose_def by (derive lems: assms homotopic_def) +declare homotopic_def [comp] - show "<\<^bold>\<lambda>x. x, lambda refl>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~ id" - unfolding compose_def by (derive lems: assms homotopic_def) -qed (rule assms) +definition isequiv :: "[t, t, t] \<Rightarrow> t" ("(3isequiv[_, _]/ _)") where + "isequiv[A, B] f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~[x:A. A] id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~[x:B. B] id)" +text \<open> +The meanings of the syntax defined above are: +\<^item> @{term "f ~[x:A. B x] g"} expresses that @{term f} and @{term g} are homotopic functions of type @{term "\<Prod>x:A. B x"}. +\<^item> @{term "isequiv[A, B] f"} expresses that the non-dependent function @{term f} of type @{term "A \<rightarrow> B"} is an equivalence. +\<close> -text "We use the following lemma in a few proofs:" +definition equivalence :: "[t, t] \<Rightarrow> t" (infix "\<simeq>" 100) + where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv[A, B] f" -lemma isequiv_type: - assumes "A: U i" and "B: U i" and "f: A \<rightarrow> B" - shows "isequiv f: U i" - by (derive lems: assms isequiv_def homotopic_def compose_def) - - -text "The equivalence relation \<open>\<simeq>\<close> is symmetric:" +lemma id_isequiv: + assumes "A: U i" "id: A \<rightarrow> A" + shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[A, A] id" +unfolding isequiv_def proof (routine add: assms) + show "\<And>g. g: A \<rightarrow> A \<Longrightarrow> id \<circ> g ~[x:A. A] id: U i" by (derive lems: assms) + show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~[x:A. A] id" by (derive lems: assms) + show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~[x:A. A] id" by (derive lems: assms) +qed -lemma equiv_sym: +lemma equivalence_symm: assumes "A: U i" and "id: A \<rightarrow> A" shows "<id, <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>>: A \<simeq> A" unfolding equivalence_def proof - show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id" using assms by (rule isequiv_id) - - fix f assume "f: A \<rightarrow> A" - with assms(1) assms(1) show "isequiv f: U i" by (rule isequiv_type) -qed (rule assms) + show "\<And>f. f: A \<rightarrow> A \<Longrightarrow> isequiv[A, A] f: U i" by (derive lems: assms isequiv_def) + show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[A, A] id" using assms by (rule id_isequiv) +qed fact -section \<open>idtoeqv and the univalence axiom\<close> +section \<open>idtoeqv\<close> -definition idtoeqv :: Term - where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>" +definition idtoeqv :: t where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>_. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>" - -text "We prove that equal types are equivalent. The proof is long and uses universes." +text \<open>We prove that equal types are equivalent. The proof involves universe types.\<close> theorem assumes "A: U i" and "B: U i" shows "idtoeqv: (A =[U i] B) \<rightarrow> A \<simeq> B" -unfolding idtoeqv_def equivalence_def -proof - fix p assume "p: A =[U i] B" - show "<transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>: \<Sum>f: A \<rightarrow> B. isequiv f" - proof - { fix f assume "f: A \<rightarrow> B" - with assms show "isequiv f: U i" by (rule isequiv_type) - } - - show "transport p: A \<rightarrow> B" - proof (rule transport_type[where ?P="\<lambda>x. x" and ?A="U i" and ?i="S i"]) - show "\<And>x. x: U i \<Longrightarrow> x: U S i" by (elim U_cumulative) standard - show "U i: U S i" by (rule U_hierarchy) standard - qed fact+ +unfolding idtoeqv_def equivalence_def proof (routine add: assms) + show *: "\<And>f. f: A \<rightarrow> B \<Longrightarrow> isequiv[A, B] f: U i" + unfolding isequiv_def by (derive lems: assms) + + show "\<And>p. p: A =[U i] B \<Longrightarrow> transport p: A \<rightarrow> B" + by (derive lems: assms transport_type[where ?i="Suc i"]) + \<comment> \<open>Instantiate @{thm transport_type} with a suitable universe level here...\<close> + + show "\<And>p. p: A =[U i] B \<Longrightarrow> ind\<^sub>= (\<lambda>_. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv[A, B] (transport p)" + proof (elim Equal_elim) + show "\<And>T. T: U i \<Longrightarrow> <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv[T, T] (transport (refl T))" + by (derive lems: transport_comp[where ?i="Suc i" and ?A="U i"] id_isequiv) + \<comment> \<open>...and also here.\<close> - show "ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv (transport p)" - proof (rule Equal_elim[where ?C="\<lambda>_ _ p. isequiv (transport p)"]) - fix A assume asm: "A: U i" - show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv (transport (refl A))" - proof (derive lems: isequiv_def) - show "transport (refl A): A \<rightarrow> A" - unfolding transport_def - by (compute lems: Equal_comp[where ?A="U i" and ?C="\<lambda>_ _ _. A \<rightarrow> A"]) (derive lems: asm) - - show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: - (\<Sum>g:A \<rightarrow> A. g \<circ> (transport (refl A)) ~ id) \<times> - (\<Sum>g:A \<rightarrow> A. (transport (refl A)) \<circ> g ~ id)" - proof (subst (1 2) transport_comp) - show "U i: U S i" by (rule U_hierarchy) standard - show "U i: U S i" by (rule U_hierarchy) standard - - show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: - (\<Sum>g:A \<rightarrow> A. g \<circ> id ~ id) \<times> (\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id)" - proof - show "\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id: U i" - proof (derive lems: asm homotopic_def) - fix g assume asm': "g: A \<rightarrow> A" - show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def) - show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *) - qed (routine lems: asm) - - show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. id \<circ> g ~ id" - proof - fix g assume asm': "g: A \<rightarrow> A" - show "id \<circ> g ~ id: U i" - proof (derive lems: homotopic_def) - show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def) - show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *) - qed (routine lems: asm) - next - show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id" - proof compute - show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm) - qed (rule asm) - qed (routine lems: asm) - - show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. g \<circ> id ~ id" - proof - fix g assume asm': "g: A \<rightarrow> A" - show "g \<circ> id ~ id: U i" by (derive lems: asm asm' homotopic_def compose_def) - next - show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id" - proof compute - show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm) - qed (rule asm) - qed (routine lems: asm) - qed - qed fact+ - qed - next - - fix A' B' p' assume asm: "A': U i" "B': U i" "p': A' =[U i] B'" - show "isequiv (transport p'): U i" - proof (rule isequiv_type) - show "transport p': A' \<rightarrow> B'" by (derive lems: asm transport_def) - qed fact+ - qed fact+ - qed - next - - show "A =[U i] B: U (S i)" by (derive lems: assms | rule U_hierarchy)+ -qed + show "\<And>A B p. \<lbrakk>A: U i; B: U i; p: A =[U i] B\<rbrakk> \<Longrightarrow> isequiv[A, B] (transport p): U i" + unfolding isequiv_def by (derive lems: assms transport_type) + qed fact+ +qed (derive lems: assms) -text "The univalence axiom." +section \<open>The univalence axiom\<close> -axiomatization univalence :: Term where - UA: "univalence: isequiv idtoeqv" +axiomatization univalence :: "[t, t] \<Rightarrow> t" where UA: "univalence A B: isequiv[A, B] idtoeqv" end diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy index a577fca..263f43d 100644 --- a/ex/HoTT book/Ch1.thy +++ b/ex/HoTT book/Ch1.thy @@ -1,55 +1,50 @@ -(* Title: HoTT/ex/HoTT book/Ch1.thy - Author: Josh Chen +(* +Title: ex/HoTT book/Ch1.thy +Author: Josh Chen +Date: 2018 A formalization of some content of Chapter 1 of the Homotopy Type Theory book. *) theory Ch1 - imports "../../HoTT" +imports "../../HoTT" + begin chapter \<open>HoTT Book, Chapter 1\<close> -section \<open>1.6 Dependent pair types (\<Sigma>-types)\<close> +section \<open>1.6 Dependent pair types (\<Sum>-types)\<close> -text "Propositional uniqueness principle:" +paragraph \<open>Propositional uniqueness principle.\<close> schematic_goal - assumes "(\<Sum>x:A. B(x)): U(i)" and "p: \<Sum>x:A. B(x)" - shows "?a: p =[\<Sum>x:A. B(x)] <fst p, snd p>" + assumes "A: U i" and "B: A \<longrightarrow> U i" and "p: \<Sum>x:A. B x" + shows "?a: p =[\<Sum>x:A. B x] <fst p, snd p>" -text "Proof by induction on \<open>p: \<Sum>x:A. B(x)\<close>:" +text \<open>Proof by induction on @{term "p: \<Sum>x:A. B x"}:\<close> proof (rule Sum_elim[where ?p=p]) - text "We just need to prove the base case; the rest will be taken care of automatically." - - fix x y assume asm: "x: A" "y: B(x)" show - "refl(<x,y>): <x,y> =[\<Sum>x:A. B(x)] <fst <x,y>, snd <x,y>>" - proof (subst (0 1) comp) - text " - The computation rules for \<open>fst\<close> and \<open>snd\<close> require that \<open>x\<close> and \<open>y\<close> have appropriate types. - The automatic proof methods have trouble picking the appropriate types, so we state them explicitly, - " - show "x: A" and "y: B(x)" by (fact asm)+ - - text "...twice, once each for the substitutions of \<open>fst\<close> and \<open>snd\<close>." - show "x: A" and "y: B(x)" by (fact asm)+ + text \<open>We prove the base case.\<close> + fix x y assume asm: "x: A" "y: B x" show "refl <x,y>: <x,y> =[\<Sum>x:A. B x] <fst <x,y>, snd <x,y>>" + proof compute + show "x: A" and "y: B x" by (fact asm)+ \<comment> \<open>Hint the correct types.\<close> + text \<open>And now @{method derive} takes care of the rest. +\<close> qed (derive lems: assms asm) - qed (derive lems: assms) section \<open>Exercises\<close> -text "Exercise 1.13" +paragraph \<open>Exercise 1.13\<close> -abbreviation "not" ("\<not>'(_')") where "\<not>(A) \<equiv> A \<rightarrow> \<zero>" +abbreviation "not" ("\<not>_") where "\<not>A \<equiv> A \<rightarrow> \<zero>" text "This proof requires the use of universe cumulativity." -proposition assumes "A: U(i)" shows "\<^bold>\<lambda>f. f`(inr(\<^bold>\<lambda>a. f`inl(a))): \<not>(\<not>(A + \<not>(A)))" -by (derive lems: assms U_cumulative[where ?A=\<zero> and ?i=O and ?j=i]) +proposition assumes "A: U i" shows "\<^bold>\<lambda>f. f`(inr(\<^bold>\<lambda>a. f`(inl a))): \<not>(\<not>(A + \<not>A))" +by (derive lems: assms) end 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 diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index a5e77ec..3ee973c 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -1,78 +1,58 @@ -(* Title: HoTT/ex/Synthesis.thy - Author: Josh Chen +(* +Title: ex/Synthesis.thy +Author: Joshua Chen +Date: 2018 -Examples of synthesis. +Examples of synthesis *) theory Synthesis - imports "../HoTT" +imports "../HoTT" + begin section \<open>Synthesis of the predecessor function\<close> -text " - In this example we construct, with the help of Isabelle, a predecessor function for the natural numbers. - - This is also done in \<open>CTT.thy\<close>; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely. -" +text \<open> +In this example we construct a predecessor function for the natural numbers. +This is also done in @{file "~~/src/CTT/ex/Synthesis.thy"}, there the work is much easier as the equality type is extensional. +\<close> -text "First we show that the property we want is well-defined." +text \<open>First we show that the property we want is well-defined.\<close> -lemma pred_welltyped: "\<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n): U(O)" +lemma pred_welltyped: "\<Sum>pred: \<nat>\<rightarrow>\<nat>. (pred`0 =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n): U O" by routine -text " - Now we look for an inhabitant of this type. - Observe that we're looking for a lambda term \<open>pred\<close> satisfying \<open>(pred`0) =\<^sub>\<nat> 0\<close> and \<open>\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n\<close>. - What if we require **definitional** equality instead of just propositional equality? -" +text \<open> +Now we look for an inhabitant of this type. +Observe that we're looking for a lambda term @{term pred} satisfying @{term "pred`0 =\<^sub>\<nat> 0"} and @{term "\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n"}. +What if we require *definitional* instead of just propositional equality? +\<close> schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n" apply compute prefer 4 apply compute -prefer 3 apply compute -apply (rule Nat_routine Nat_elim | compute | assumption)+ -done - -text " - The above proof finds a candidate, namely \<open>\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n\<close>. - We prove this has the required type and properties. -" - -definition pred :: Term where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n" - -lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" unfolding pred_def by routine - -lemma pred_props: "<refl(0), \<^bold>\<lambda>n. refl(n)>: ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" -proof (routine lems: pred_type) - have *: "pred`0 \<equiv> 0" unfolding pred_def - proof compute - show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine - show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0" - proof compute - show "\<nat>: U(O)" .. - qed routine - qed rule - then show "refl(0): (pred`0) =\<^sub>\<nat> 0" by (subst *) routine - - show "\<^bold>\<lambda>n. refl(n): \<Prod>n:\<nat>. (pred`(succ(n))) =\<^sub>\<nat> n" - unfolding pred_def proof - show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ((\<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n)`succ(n)) =\<^sub>\<nat> n" - proof compute - show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by routine - show "\<And>n. n: \<nat> \<Longrightarrow> refl(n): ind\<^sub>\<nat> (\<lambda>a b. a) 0 (succ n) =\<^sub>\<nat> n" - proof compute - show "\<nat>: U(O)" .. - qed routine - qed rule - qed rule -qed - -theorem - "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" -by (routine lems: pred_welltyped pred_type pred_props) +apply (rule Nat_routine | compute)+ +oops +\<comment> \<open>Something in the original proof broke when I revamped the theory. The completion of this derivation is left as an exercise to the reader.\<close> + +text \<open> +The above proof finds a candidate, namely @{term "\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n"}. +We prove this has the required type and properties. +\<close> + +definition pred :: t where "pred \<equiv> \<^bold>\<lambda>n. ind\<^sub>\<nat> (\<lambda>a b. a) 0 n" + +lemma pred_type: "pred: \<nat> \<rightarrow> \<nat>" +unfolding pred_def by routine + +lemma pred_props: "<refl 0, \<^bold>\<lambda>n. refl n>: (pred`0 =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. pred`(succ n) =\<^sub>\<nat> n)" +unfolding pred_def by derive + +theorem "<pred, <refl(0), \<^bold>\<lambda>n. refl(n)>>: \<Sum>pred:\<nat>\<rightarrow>\<nat> . ((pred`0) =\<^sub>\<nat> 0) \<times> (\<Prod>n:\<nat>. (pred`(succ n)) =\<^sub>\<nat> n)" +by (derive lems: pred_type pred_props) end 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 |