diff options
| -rw-r--r-- | Eq.thy | 216 | ||||
| -rw-r--r-- | Equality.thy | 201 | ||||
| -rw-r--r-- | HoTT_Base.thy | 11 | ||||
| -rw-r--r-- | HoTT_Typing.thy | 169 | ||||
| -rw-r--r-- | Prod.thy | 34 | ||||
| -rw-r--r-- | util.ML | 124 |
6 files changed, 178 insertions, 577 deletions
@@ -2,6 +2,8 @@ Isabelle/HoTT: Equality Feb 2019 +Intensional equality, path induction, and proofs of various results. + ********) theory Eq @@ -57,6 +59,13 @@ method path_ind' for a b p :: t = syntax "_induct_over" :: "[idt, idt, idt, t] \<Rightarrow> [t, t, t] \<Rightarrow> t" ("(2{_, _, _}/ _)" 0) translations "{x, y, p} C" \<rightharpoonup> "\<lambda>x y p. C" +text \<open> +Use "@{method path_ind} @{term "{x, y, p} C x y p"}" to perform path induction for the given type family over the variables @{term x}, @{term y}, and @{term p}, +and "@{method path_ind'} @{term a} @{term b} @{term p}" to let Isabelle try and infer the shape of the type family itself (this doesn't always work!). + +Note that @{term "{x, y, p} C x y p"} is just syntactic sugar for @{term "\<lambda>x y p. C x y p"}. +\<close> + section \<open>Properties of equality\<close> @@ -91,6 +100,7 @@ declare inv_type [intro] inv_comp [comp] + subsection \<open>Transitivity (path composition)\<close> schematic_goal transitivity: @@ -105,15 +115,13 @@ definition pathcomp :: "[t, t, t, t, t, t] \<Rightarrow> t" where "pathcomp A x y z p q \<equiv> (indEq (\<lambda>x y _. \<Prod>z: A. y =[A] z \<rightarrow> x =[A] z) - (\<lambda>x. \<lambda>(z: A). \<lambda>(q: x =[A] z). indEq (\<lambda>x z _. x =[A] z) (\<lambda>x. refl x) x z q) + (\<lambda>x. \<lambda>z: A. \<lambda>q: x =[A] z. indEq (\<lambda>x z _. x =[A] z) (\<lambda>x. refl x) x z q) x y p)`z`q" - syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "*" 110) -text \<open>Pretty-printing switch for path composition:\<close> - ML \<open>val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\<close> +\<comment> \<open>Pretty-printing switch for path composition\<close> print_translation \<open> let fun pathcomp_tr' ctxt [A, x, y, z, p, q] = @@ -126,80 +134,80 @@ end \<close> lemma pathcomp_type: - assumes "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z" + assumes [intro]: "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z" shows "pathcomp A x y z p q: x =[A] z" -unfolding pathcomp_def by (derive lems: transitivity assms) +unfolding pathcomp_def by (derive lems: transitivity) -lemma pathcomp_cmp: - assumes "A: U i" and "a: A" +lemma pathcomp_comp: + assumes [intro]: "A: U i" "a: A" shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a" -unfolding pathcomp_def by (derive lems: transitivity assms) +unfolding pathcomp_def by (derive lems: transitivity) -lemmas pathcomp_type [intro] -lemmas pathcomp_comp [comp] = pathcomp_cmp +declare + pathcomp_type [intro] + pathcomp_comp [comp] section \<open>Higher groupoid structure of types\<close> schematic_goal pathcomp_idr: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A x y y p (refl y) =[x =[A] y] p" + assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?prf: pathcomp A x y y p (refl y) =[x =[A] y] p" proof (path_ind' x y p) show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) + by derive +qed routine schematic_goal pathcomp_idl: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A x x y (refl x) p =[x =[A] y] p" + assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?prf: pathcomp A x x y (refl x) p =[x =[A] y] p" proof (path_ind' x y p) show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) + by derive +qed routine schematic_goal pathcomp_invr: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)" + assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?prf: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)" proof (path_ind' x y p) show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (inv A x x (refl x)) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) + by derive +qed routine schematic_goal pathcomp_invl: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)" + assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?prf: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)" proof (path_ind' x y p) show "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (inv A x x (refl x)) (refl x) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) + by derive +qed routine schematic_goal inv_involutive: - assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?a: inv A y x (inv A x y p) =[x =[A] y] p" + assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?prf: inv A y x (inv A x y p) =[x =[A] y] p" proof (path_ind' x y p) show "\<And>x. x: A \<Longrightarrow> refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)" - by (derive lems: assms) -qed (routine add: assms) + by derive +qed routine text \<open> We use the proof of associativity of path composition to demonstrate the process of deriving proof terms. The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the correct form of the proof term in the first place. -However, using proof scripts the derivation becomes quite easy; we simply give the correct form of the statements to induct over, and prove the simple subgoals returned by the prover. +However, using proof scripts the derivation becomes quite easy: we simply give the correct form of the statements to induct over, and prove the simple subgoals returned by the prover. The proof is sensitive to the order of the quantifiers in the product. In particular, changing the order causes unification to fail in the path inductions. It seems to be good practice to order the variables in the order over which we will path-induct. \<close> -declare[[pretty_pathcomp=false]] schematic_goal pathcomp_assoc: - assumes "A: U i" + assumes [intro]: "A: U i" shows - "?a: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y. \<Prod>z: A. \<Prod>q: y =[A] z. \<Prod>w: A. \<Prod>r: z =[A] w. + "?prf: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y. \<Prod>z: A. \<Prod>q: y =[A] z. \<Prod>w: A. \<Prod>r: z =[A] w. pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w] pathcomp A x z w (pathcomp A x y z p q) r" @@ -225,26 +233,40 @@ proof - "\<And>x. x: A \<Longrightarrow> refl(refl x): pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)) =[x =[A] x] pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x)" - by (derive lems: assms) -qed (derive lems: assms) + by derive +qed routine (* Todo, if possible: Implement a custom version of schematic_goal/theorem that exports the derived proof term. *) -section \<open>Functoriality of functions on types\<close> +section \<open>Functoriality of functions on types under equality\<close> schematic_goal transfer: - assumes + assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" "x: A" "y: A" "p: x =[A] y" - shows "?a: f`x =[B] f`y" -by (path_ind' x y p, rule Eq_intro, routine add: assms) + shows "?prf: f`x =[B] f`y" +by (path_ind' x y p, rule Eq_routine, routine) definition ap :: "[t, t, t, t, t] \<Rightarrow> t" where "ap B f x y p \<equiv> indEq ({x, y, _} f`x =[B] f`y) (\<lambda>x. refl (f`x)) x y p" +syntax "_ap" :: "[t, t] \<Rightarrow> t" ("(_{_})" [1000, 0] 1000) + +ML \<open>val pretty_ap = Attrib.setup_config_bool @{binding "pretty_ap"} (K true)\<close> + +print_translation \<open> +let fun ap_tr' ctxt [B, f, x, y, p] = + if Config.get ctxt pretty_ap + then Syntax.const @{syntax_const "_ap"} $ f $ p + else @{const ap} $ B $ f $ x $ y $ p +in + [(@{const_syntax ap}, ap_tr')] +end +\<close> + lemma ap_type: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" @@ -252,22 +274,22 @@ lemma ap_type: shows "ap B f x y p: f`x =[B] f`y" unfolding ap_def using assms by (rule transfer) -lemma ap_cmp: - assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "x: A" +lemma ap_comp: + assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" "x: A" shows "ap B f x x (refl x) \<equiv> refl (f`x)" -unfolding ap_def by (derive lems: assms) +unfolding ap_def by derive -lemmas ap_type [intro] -lemmas ap_comp [comp] = ap_cmp +declare + ap_type [intro] + ap_comp [comp] -schematic_goal ap_func1: - assumes "A: U i" "B: U i" "f: A \<rightarrow> B" +schematic_goal ap_func_pathcomp: + assumes [intro]: "A: U i" "B: U i" "f: A \<rightarrow> B" shows - "?a: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y. \<Prod>z: A. \<Prod>q: y =[A] z. + "?prf: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y. \<Prod>z: A. \<Prod>q: y =[A] z. ap B f x z (pathcomp A x y z p q) =[f`x =[B] f`z] pathcomp B (f`x) (f`y) (f`z) (ap B f x y p) (ap B f y z q)" - apply (quantify 3) apply (path_ind "{x, y, p} \<Prod>z: A. \<Prod>q: y =[A] z. @@ -277,12 +299,100 @@ apply (quantify 2) apply (path_ind "{x, z, q} ap B f x z (pathcomp A x x z (refl x) q) =[f`x =[B] f`z] pathcomp B (f`x) (f`x) (f`z) (ap B f x x (refl x)) (ap B f x z q)") - proof - show "\<And>x. x: A \<Longrightarrow> refl(refl(f`x)): ap B f x x (pathcomp A x x x (refl x) (refl x)) =[f`x =[B] f`x] pathcomp B (f`x) (f`x) (f`x) (ap B f x x (refl x)) (ap B f x x (refl x))" - by (derive lems: assms) -qed (derive lems: assms) + by derive +qed derive + + +schematic_goal ap_func_compose: + assumes [intro]: + "A: U i" "B: U i" "C: U i" + "f: A \<rightarrow> B" "g: B \<rightarrow> C" + shows + "?prf: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y. + ap C g (f`x) (f`y) (ap B f x y p) =[g`(f`x) =[C] g`(f`y)] + ap C (compose A g f) x y p" +apply (quantify 3) +apply (path_ind "{x, y, p} + ap C g (f`x) (f`y) (ap B f x y p) =[g`(f`x) =[C] g`(f`y)] + ap C (compose A g f) x y p") +proof - + show "\<And>x. x: A \<Longrightarrow> refl(refl (g`(f`x))) : + ap C g (f`x) (f`x) (ap B f x x (refl x)) =[g`(f`x) =[C] g`(f`x)] + ap C (compose A g f) x x (refl x)" + unfolding compose_def by derive + + fix x y p assume [intro]: "x: A" "y: A" "p: x =[A] y" + show "ap C g (f`x) (f`y) (ap B f x y p) =[g`(f`x) =[C] g`(f`y)] ap C (compose A g f) x y p: U i" + proof + have + "(\<lambda>x: A. g`(f`x))`x =[C] (\<lambda>x: A. g`(f`x))`y \<equiv> g`(f`x) =[C] g`(f`y)" by derive + moreover have + "ap C (compose A g f) x y p : (\<lambda>x: A. g`(f`x))`x =[C] (\<lambda>x: A. g`(f`x))`y" + unfolding compose_def by derive + ultimately show + "ap C (compose A g f) x y p : g`(f`x) =[C] g`(f`y)" by simp + qed derive +qed routine + + +schematic_goal ap_func_inv: + assumes [intro]: + "A: U i" "B: U i" "f: A \<rightarrow> B" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: ap B f y x (inv A x y p) =[f`y =[B] f`x] inv B (f`x) (f`y) (ap B f x y p)" +proof (path_ind' x y p) + show "\<And>x. x: A \<Longrightarrow> refl(refl(f`x)): + ap B f x x (inv A x x (refl x)) =[f`x =[B] f`x] inv B (f`x) (f`x) (ap B f x x (refl x))" + by derive +qed routine + +schematic_goal ap_func_id: + assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?prf: ap A (id A) x y p =[x =[A] y] p" +proof (path_ind' x y p) + fix x assume [intro]: "x: A" + show "refl(refl x): ap A (id A) x x (refl x) =[x =[A] x] refl x" by derive + + fix y p assume [intro]: "y: A" "p: x =[A] y" + have "ap A (id A) x y p: (id A)`x =[A] (id A)`y" by derive + moreover have "(id A)`x =[A] (id A)`y \<equiv> x =[A] y" by derive + ultimately have [intro]: "ap A (id A) x y p: x =[A] y" by simp + + show "ap A (id A) x y p =[x =[A] y] p: U i" by derive +qed + + +section \<open>Transport\<close> + +schematic_goal transport: + assumes [intro]: + "A: U i" "P: A \<leadsto> U i" + "x: A" "y: A" "p: x =[A] y" + shows "?prf: P x \<rightarrow> P y" +proof (path_ind' x y p) + show "\<And>x. x: A \<Longrightarrow> id (P x): P x \<rightarrow> P x" by derive +qed routine + +definition transport :: "[t \<Rightarrow> t, t, t, t] \<Rightarrow> t" +where "transport P x y p \<equiv> indEq (\<lambda>a b _. P a \<rightarrow> P b) (\<lambda>x. id (P x)) x y p" + +lemma transport_type: + assumes "A: U i" "P: A \<leadsto> U i" "x: A" "y: A" "p: x =[A] y" + shows "transport P x y p: P x \<rightarrow> P y" +unfolding transport_def using assms by (rule transport) + +lemma transport_comp: + assumes [intro]: "A: U i" "P: A \<leadsto> U i" "a: A" + shows "transport P a a (refl a) \<equiv> id (P a)" +unfolding transport_def by derive + +declare + transport_type [intro] + transport_comp [comp] + end diff --git a/Equality.thy b/Equality.thy deleted file mode 100644 index 851c569..0000000 --- a/Equality.thy +++ /dev/null @@ -1,201 +0,0 @@ -(* -Title: Equality.thy -Author: Joshua Chen -Date: 2018 - -Properties of equality -*) - -theory Equality -imports HoTT_Methods Equal Prod - -begin - - -section \<open>Symmetry of equality/Path inverse\<close> - -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 - -lemma inv_comp: "\<lbrakk>A: U i; a: A\<rbrakk> \<Longrightarrow> (refl a)\<inverse> \<equiv> refl a" -unfolding inv_def by compute routine - -declare - inv_type [intro] - inv_comp [comp] - - -section \<open>Transitivity of equality/Path composition\<close> - -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> - -definition pathcomp :: t where "pathcomp \<equiv> \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. (refl x)) q) p" - -syntax "_pathcomp" :: "[t, t] \<Rightarrow> t" (infixl "\<bullet>" 110) -translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q" - -lemma pathcomp_type: - assumes "A: U i" "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) - -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) - -lemma pathcomp_comp: - assumes "A: U i" and "a: A" - shows "(refl a) \<bullet> (refl a) \<equiv> refl a" -unfolding pathcomp_def by (derive lems: assms) - -declare - pathcomp_type [intro] - pathcomp_trans [intro] - pathcomp_comp [comp] - - -section \<open>Higher groupoid structure of types\<close> - -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) -qed (routine add: assms) - -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) -qed (routine add: assms) - -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) -qed (routine add: assms) - -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) -qed (routine add: assms) - -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) -qed (routine add: assms) - -text \<open>All of the propositions above have the same proof term, which we abbreviate here.\<close> -abbreviation \<iota> :: "t \<Rightarrow> t" where "\<iota> p \<equiv> ind\<^sub>= (\<lambda>x. refl (refl x)) p" - -text \<open>The next proof has a triply-nested path induction.\<close> - -lemma pathcomp_assoc: - assumes "A: U i" "x: A" "y: A" "z: A" "w: A" - shows "\<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>r. \<iota> r) q) p: - \<Prod>p: x =\<^sub>A y. \<Prod>q: y =\<^sub>A z. \<Prod>r: z =\<^sub>A w. p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] (p \<bullet> q) \<bullet> r" -proof - show "\<And>p. p: x =\<^sub>A y \<Longrightarrow> ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>r. \<iota> r) q) p: - \<Prod>q: y =\<^sub>A z. \<Prod>r: z =\<^sub>A w. p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] p \<bullet> q \<bullet> r" - proof (elim Equal_elim) - fix x assume 1: "x: A" - show "\<^bold>\<lambda>q. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>r. \<iota> r) q: - \<Prod>q: x =\<^sub>A z. \<Prod>r: z =\<^sub>A w. refl x \<bullet> (q \<bullet> r) =[x =\<^sub>A w] refl x \<bullet> q \<bullet> r" - proof - show "\<And>q. q: x =\<^sub>A z \<Longrightarrow> ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>r. \<iota> r) q: - \<Prod>r: z =\<^sub>A w. refl x \<bullet> (q \<bullet> r) =[x =\<^sub>A w] refl x \<bullet> q \<bullet> r" - proof (elim Equal_elim) - fix x assume *: "x: A" - show "\<^bold>\<lambda>r. \<iota> r: \<Prod>r: x =\<^sub>A w. refl x \<bullet> (refl x \<bullet> r) =[x =\<^sub>A w] refl x \<bullet> refl x \<bullet> r" - proof - show "\<And>r. r: x =[A] w \<Longrightarrow> \<iota> r: refl x \<bullet> (refl x \<bullet> r) =[x =[A] w] refl x \<bullet> refl x \<bullet> r" - by (elim Equal_elim, derive lems: * assms) - qed (routine add: * assms) - qed (routine add: 1 assms) - qed (routine add: 1 assms) - - text \<open> - In the following part @{method derive} fails to obtain the correct subgoals, so we have to prove the statement manually. - \<close> - fix y p assume 2: "y: A" "p: x =\<^sub>A y" - show "\<Prod>q: y =\<^sub>A z. \<Prod>r: z =\<^sub>A w. p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] p \<bullet> q \<bullet> r: U i" - proof (routine add: assms) - fix q assume 3: "q: y =\<^sub>A z" - show "\<Prod>r: z =\<^sub>A w. p \<bullet> (q \<bullet> r) =[x =\<^sub>A w] p \<bullet> q \<bullet> r: U i" - proof (routine add: assms) - show "\<And>r. r: z =[A] w \<Longrightarrow> p \<bullet> (q \<bullet> r): x =[A] w" and "\<And>r. r: z =[A] w \<Longrightarrow> p \<bullet> q \<bullet> r: x =[A] w" - by (routine add: 1 2 3 assms) - qed (routine add: 1 assms) - qed fact+ - qed fact+ -qed (routine add: assms) - - -section \<open>Functoriality of functions on types\<close> - -schematic_goal transfer_lemma: - assumes - "f: A \<rightarrow> B" "A: U i" "B: U i" - "p: x =\<^sub>A y" "x: A" "y: A" - shows "?a: (f`x =\<^sub>B f`y)" -proof (rule Equal_elim[where ?C="\<lambda>x y _. f`x =\<^sub>B f`y"]) - show "\<And>x. x: A \<Longrightarrow> refl (f`x): f`x =\<^sub>B f`x" by (routine add: assms) -qed (routine add: assms) - -definition ap :: "t \<Rightarrow> t" ("(ap\<^sub>_)") where "ap f \<equiv> \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>x. refl (f`x)) p" - -syntax "_ap_ascii" :: "t \<Rightarrow> t" ("(ap[_])") -translations "ap[f]" \<rightleftharpoons> "CONST ap f" - -corollary ap_type: - assumes "f: A \<rightarrow> B" "A: U i" "B: U i" - shows "\<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> ap f: x =\<^sub>A y \<rightarrow> f`x =\<^sub>B f`y" -unfolding ap_def by (derive lems: assms transfer_lemma) - -schematic_goal functions_are_functorial: - assumes - "f: A \<rightarrow> B" "g: B \<rightarrow> C" - "A: U i" "B: U i" "C: U i" - "x: A" "y: A" "z: A" - "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows - 1: "?a: ap\<^sub>f`(p \<bullet> q) =[?A] ap\<^sub>f`p \<bullet> ap\<^sub>f`q" and - 2: "?b: ap\<^sub>f`(p\<inverse>) =[?B] (ap\<^sub>f`p)\<inverse>" and - 3: "?c: ap\<^sub>g`(ap\<^sub>f`p) =[?C] ap[g \<circ> f]`p" and - 4: "?d: ap[id]`p =[?D] p" -oops - - -section \<open>Transport\<close> - -definition transport :: "t \<Rightarrow> t" where "transport p \<equiv> ind\<^sub>= (\<lambda>_. (\<^bold>\<lambda>x. x)) p" - -text \<open>Note that @{term transport} is a polymorphic function in our formulation.\<close> - -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 - -corollary transport_elim: "\<lbrakk>x: P a; P: A \<longrightarrow> U i; p: a =\<^sub>A b; a: A; b: A; A: U i\<rbrakk> \<Longrightarrow> (transport p)`x: P b" -by (routine add: transport_type) - -lemma transport_comp: "\<lbrakk>A: U i; x: A\<rbrakk> \<Longrightarrow> transport (refl x) \<equiv> id" -unfolding transport_def by derive - - -end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 1dcf61c..34474d1 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -11,11 +11,20 @@ This file completes the basic logical and functional setup of the HoTT logic. It ********) theory HoTT_Base -imports HoTT_Typing +imports Pure begin +section \<open>Basic setup\<close> + +declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close> + +typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close> + +judgment has_type :: "[t, t] \<Rightarrow> prop" ("(2_ :/ _)") + + section \<open>Universes\<close> typedecl ord \<comment> \<open>Type of meta-numerals\<close> diff --git a/HoTT_Typing.thy b/HoTT_Typing.thy deleted file mode 100644 index ec7456e..0000000 --- a/HoTT_Typing.thy +++ /dev/null @@ -1,169 +0,0 @@ -(******** -Isabelle/HoTT: Core typing judgment form and associated automation -Feb 2019 - -This file is the starting point of the definition of Isabelle/HoTT. -It declares the fundamental typing judgment form and sets up various -ML functionality to automate type inference. - -********) - -theory HoTT_Typing -imports Pure -keywords "assume_type" "assume_types" :: thy_decl - -begin - - -section \<open>Initial settings\<close> - -declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close> - -ML \<open>val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\<close> - \<comment> \<open>Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\<close> - - -section \<open>Terms and typing\<close> - -typedecl t \<comment> \<open>Type of object-logic terms (which includes the types)\<close> - -judgment has_type :: "[t, t] \<Rightarrow> prop" ("(3_ :/ _)") - - -section \<open>Typing functionality\<close> - -ML_file "util.ML" - -ML \<open> -signature TYPING = -sig - type jmt = term - val is_typing_jmt: term -> bool - val term_of_jmt: jmt -> term - val type_of_jmt: jmt -> term - - val typing_this: Proof.context -> jmt list - val typing_assms: Proof.context -> jmt list - val typing_all: Proof.context -> jmt list - - val get_typing_in: term -> jmt list -> term option - - val get_local_typing: Proof.context -> term -> term option - - val put_theory_typing: term -> theory -> theory - val get_theory_typing: theory -> term -> term option - - val get_typing: Proof.context -> term -> term option -end - -structure Typing: TYPING = -struct - -type jmt = term - -(* Determine if a term is a typing judgment *) -fun is_typing_jmt (@{const has_type} $ _ $ _) = true - | is_typing_jmt _ = false - -(* Functions to extract a and A from propositions "a: A" *) -fun term_of_jmt (@{const has_type} $ t $ _) = t - | term_of_jmt _ = Exn.error "Not a typing judgment" - -fun type_of_jmt (@{const has_type} $ _ $ T) = T - | type_of_jmt _ = Exn.error "Not a typing judgment" - -(* Get typing assumptions in "this" *) -fun typing_this ctxt = Util.get_this ctxt |> map Thm.prop_of |> filter is_typing_jmt - -(* Get the typing assumptions in the current proof context *) -val typing_assms = Util.get_assms #> map Thm.prop_of #> filter is_typing_jmt - -(* Search the context and return all visible typing judgments *) -fun typing_all ctxt = - Util.get_all_thms ctxt |> map (Thm.prop_of o snd) |> filter is_typing_jmt - -(* Search for a term typing in a list of judgments, and return the type if found. - -- - The use of aconv_untyped as opposed to aconv is crucial here: - meta-level type inference is performed *after* syntax translation, which means that - the translation functions see an unannotated term "f" (in contrast to one annotated - e.g. "f::t") as having a blank type field. - Using aconv would result in no match ever being found for f, because any judgment - involving f records it together with its (non-blank) type field, e.g. - "Free ("f", "_")" - seen by the translation function, vs. - "Free ("f", "t")" - recorded in the typing judgment. -*) -fun get_typing_in tm jmts = - let val find_type = - fn jmt => if Term.aconv_untyped (tm, term_of_jmt jmt) then SOME (type_of_jmt jmt) else NONE - in get_first find_type jmts end - -(* Search for typing in the local proof context (no global data). - We search the facts bound to "this" before searching the assumptions. - -- - A previous version of this function passed the argument - (typing_this ctxt @ typing_assms ctxt) - to get_typing_in. - -- - This version only evaluates successive lists if the search on the previous list was unsuccessful. -*) -fun get_local_typing ctxt tm = - case get_typing_in tm (typing_this ctxt) of - NONE => get_typing_in tm (typing_assms ctxt) - | res => res - -(* Dedicated theory data for proven typing judgments *) -structure Theory_Typings = Theory_Data -( - type T = term Symtab.table - val empty = Symtab.empty - val extend = I - val merge = Symtab.join (fn key => fn (x, y) => y) -) -(* Accessor for the above data *) -fun get_theory_typing thy tm = - Symtab.lookup (Theory_Typings.get thy) (Util.string_of_term tm) - -fun put_theory_typing jmt = - case jmt of - Const("HoTT_Base.has_type", _) $ term $ typing => - Theory_Typings.map (Symtab.update (Util.string_of_term term, typing)) - | _ => Exn.error "Not a typing judgment" - -(* Get the typing of a term *) -fun get_typing ctxt tm = - case get_local_typing ctxt tm of - NONE => get_theory_typing (Proof_Context.theory_of ctxt) tm - | res => res - -end -\<close> - -ML \<open> -val _ = - let - fun store_typing ctxt = Typing.put_theory_typing o (Syntax.read_prop ctxt) - in - Outer_Syntax.local_theory - @{command_keyword "assume_type"} - "Declare typing assumptions" - (Parse.prop >> - (fn prop => fn lthy => Local_Theory.background_theory (store_typing lthy prop) lthy)) - end - -val _ = - let - val parser = Parse.and_list (Parse.prop) - fun store_typings ctxt = fold (Typing.put_theory_typing o (Syntax.read_prop ctxt)) - in - Outer_Syntax.local_theory - @{command_keyword "assume_types"} - "Declare typing assumptions" - (parser >> - (fn props => fn lthy => Local_Theory.background_theory (store_typings lthy props) lthy)) - end -\<close> - -end @@ -15,7 +15,7 @@ section \<open>Basic type definitions\<close> axiomatization Prod :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and lam :: "[t, t \<Rightarrow> t] \<Rightarrow> t" and - app :: "[t, t] \<Rightarrow> t" ("(2_/ ` _)" [120, 121] 120) + app :: "[t, t] \<Rightarrow> t" ("(2_`_)" [120, 121] 120) \<comment> \<open>Application should bind tighter than abstraction.\<close> syntax @@ -75,33 +75,7 @@ section \<open>Function composition\<close> definition compose :: "[t, t, t] \<Rightarrow> t" where "compose A g f \<equiv> \<lambda>x: A. g`(f`x)" -declare compose_def [comp] - syntax "_compose" :: "[t, t] \<Rightarrow> t" (infixr "o" 110) -(* -parse_translation \<open> -let fun compose_tr ctxt [g, f] = - let - val [g, f] = [g, f] |> map (Util.prep_term ctxt) - val dom = - case f of - Const ("Prod.lam", _) $ T $ _ => T - | Const ("Prod.compose", _) $ T $ _ $ _ => T - | _ => - case Typing.get_typing ctxt f of - SOME (Const ("Prod.Prod", _) $ T $ _) => T - | SOME t => - Exn.error ("Can't compose with a non-function " ^ Syntax.string_of_term ctxt f) - | NONE => - Exn.error "Cannot infer domain of composition; please state this explicitly" - in - @{const compose} $ dom $ g $ f - end -in - [("_compose", compose_tr)] -end -\<close> -*) text \<open>Pretty-printing switch for composition; hides domain type information.\<close> @@ -120,12 +94,14 @@ end lemma compose_assoc: assumes "A: U i" and "f: A \<rightarrow> B" and "g: B \<rightarrow> C" and "h: \<Prod>x: C. D x" shows "compose A (compose B h g) f \<equiv> compose A h (compose A g f)" -by (derive lems: assms cong) +unfolding compose_def by (derive lems: assms cong) 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 "compose A (\<lambda>x: B. c x) (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)" -by (derive lems: assms cong) +unfolding compose_def by (derive lems: assms cong) + +declare compose_comp [comp] abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x" diff --git a/util.ML b/util.ML deleted file mode 100644 index f7aab9a..0000000 --- a/util.ML +++ /dev/null @@ -1,124 +0,0 @@ -(******** -Isabelle/HoTT: util.ML -Feb 2019 - -Libary of various helper functions. - -********) - -signature UTIL = -sig - (* Lexical functions *) - val unmark: string -> string - - (* Functions on ML terms and types *) - val prep_term: Proof.context -> term -> term - val string_of_typ: typ -> string - val string_of_term: term -> string - - (* General functions *) - val get_all_thms: Proof.context -> (string * thm) list - val find_thm: Proof.context -> string -> (string * thm) list - - (* Get specific theorems *) - val get_this: Proof.context -> thm list - val get_assms: Proof.context -> thm list -end - -structure Util: UTIL = -struct - -(* Unmark a name string identifier *) -fun unmark s = - Lexicon.unmark_class s - handle Fail "unprefix" => - Lexicon.unmark_type s - handle Fail "unprefix" => - Lexicon.unmark_const s - handle Fail "unprefix" => - Lexicon.unmark_fixed s - handle Fail "unprefix" => - s - -(* Prepare a Pure pre-term, converting it to a (unchecked) term *) -fun prep_term ctxt ptm = - let val ptm = Term_Position.strip_positions ptm - in - (case ptm of - Const ("_constrain", _) $ Free (t, _) $ - (Const ("\<^type>fun", _) $ Const(typ1, _) $ Const (typ2, _)) => - let - val typ1 = Lexicon.unmark_type typ1 - val typ2 = Lexicon.unmark_type typ2 - val typ = typ1 ^ "\<Rightarrow>" ^ typ2 |> Syntax.read_typ ctxt - in Free (t, typ) end - | Const ("_constrain", _) $ t $ Const (typ, _) => - let - val T = Syntax.read_typ ctxt (Lexicon.unmark_type typ) - in - case t of - Free (s, _) => Free (s, T) - | Const (s, _) => Const (Lexicon.unmark_const s, T) - | _ => Exn.error "Unimplemented term constraint handler" - end - | ptm1 $ ptm2 => - (prep_term ctxt ptm1) $ (prep_term ctxt ptm2) - | Abs (t, T, ptm') => - Abs (t, T, prep_term ctxt ptm') - | Const (t, T) => Const (unmark t, T) - | t => t) - end - -fun string_of_typ typ = - case typ of - Type (name, typs) => "Type (" ^ name ^ Library.commas (map string_of_typ typs) ^")" - | TFree (name, sort) => "TFree (" ^ name ^ Library.commas sort ^ ")" - | TVar ((name, idx), sort) => - "TVar ((" ^ name ^ ", " ^ string_of_int idx ^ "), " ^ Library.commas sort ^ ")" - -fun string_of_term tm = - case tm of - Const (name, typ) => "Const (" ^ name ^ ", " ^ string_of_typ typ ^ ")" - | Free (name, typ) => "Free (" ^ name ^ ", " ^ string_of_typ typ ^ ")" - | Var ((name, idx), typ) => - "Var ((" ^ name ^ ", " ^ string_of_int idx ^ "), " ^ string_of_typ typ ^ ")" - | Bound idx => "Bound " ^ string_of_int idx ^ ")" - | Abs (_, typ, body) => "Abs (_, " ^ string_of_typ typ ^ ", " ^ string_of_term body ^ ")" - | t1 $ t2 => "(" ^ string_of_term t1 ^ ") $ (" ^ string_of_term t2 ^ ")" - -fun name_and_thm (fact, thm) = - ((case fact of - Facts.Named ((name, _), _) => name - | Facts.Fact name => name), - thm) - -(* Return all visible theorems *) -fun get_all_thms ctxt = - let val (_, ref_thms) = Find_Theorems.find_theorems ctxt NONE NONE true [] - in ref_thms |> (map name_and_thm) - end - -(* Search all visible theorems (including local assumptions) containing a given name *) -fun find_thm ctxt name = - let val (_, ref_thms) = - Find_Theorems.find_theorems ctxt NONE NONE true [(true, Find_Theorems.Name name)] - in - ref_thms |> (map name_and_thm) - end - -(* Get the fact corresponding to the Isar term "this" in the current proof scope *) -fun get_this ctxt = - Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN) - |> Proof_Context.lookup_fact ctxt |> the |> #thms - handle Option.Option => ( - if (Config.get ctxt trace) then warning "\"this\" undefined in the context" else (); - [] - ) - -(* Get all visible assumptions in the current proof scope. - This includes the facts introduced in the statement of the goal using "assumes", - as well as all facts introduced using "assume" that are visible in the current block. - *) -val get_assms = Assumption.all_prems_of - -end |