From ca8e7a2681c133abdd082cfa29d6994fa73f2d47 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 15 Aug 2018 17:17:34 +0200 Subject: Rename to distinguish function and path composition; function composition proofs, which have issues... --- EqualProps.thy | 40 +++++++++++++++---------------- HoTT_Methods.thy | 2 +- Prod.thy | 26 +++++++++++++------- ProdProps.thy | 54 ++++++++++++++++++++++++++++++++++++++++++ scratch.thy | 72 -------------------------------------------------------- 5 files changed, 93 insertions(+), 101 deletions(-) create mode 100644 ProdProps.thy diff --git a/EqualProps.thy b/EqualProps.thy index 2a13ed2..f3b355a 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -48,17 +48,17 @@ text " Raw composition function, of type \\x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)\ polymorphic over the type \A\. " -axiomatization reqcompose :: Term where - reqcompose_def: "reqcompose \ \<^bold>\x y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= (\x. refl(x)) q) p" +axiomatization rpathcomp :: Term where + rpathcomp_def: "rpathcomp \ \<^bold>\x y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= (\x. refl(x)) q) p" text " More complicated proofs---the nested path inductions require more explicit step-by-step rule applications: " -lemma reqcompose_type: +lemma rpathcomp_type: assumes "A: U(i)" - shows "reqcompose: \x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" -unfolding reqcompose_def + shows "rpathcomp: \x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" +unfolding rpathcomp_def proof fix x assume 1: "x: A" show "\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" @@ -85,17 +85,17 @@ qed fact corollary assumes "A: U(i)" "x: A" "y: A" "z: A" "p: x =\<^sub>A y" "q: y =\<^sub>A z" - shows "reqcompose`x`y`p`z`q: x =\<^sub>A z" - by (simple lems: assms reqcompose_type) + shows "rpathcomp`x`y`p`z`q: x =\<^sub>A z" + by (simple lems: assms rpathcomp_type) text " The following proof is very long, chiefly because for every application of \`\ we have to show the wellformedness of the type family appearing in the equality computation rule. " -lemma reqcompose_comp: +lemma rpathcomp_comp: assumes "A: U(i)" and "a: A" - shows "reqcompose`a`a`refl(a)`a`refl(a) \ refl(a)" -unfolding reqcompose_def + shows "rpathcomp`a`a`refl(a)`a`refl(a) \ refl(a)" +unfolding rpathcomp_def proof compute { fix x assume 1: "x: A" show "\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" @@ -197,28 +197,28 @@ qed fact text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." -axiomatization eqcompose :: "[Term, Term] \ Term" (infixl "\" 60) where - eqcompose_def: "\ +axiomatization pathcomp :: "[Term, Term] \ Term" (infixl "\" 60) where + pathcomp_def: "\ A: U(i); x: A; y: A; z: A; p: x =\<^sub>A y; q: y =\<^sub>A z - \ \ p \ q \ reqcompose`x`y`p`z`q" + \ \ p \ q \ rpathcomp`x`y`p`z`q" -lemma eqcompose_type: +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 \ q: x =\<^sub>A z" -proof (subst eqcompose_def) +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 (simple lems: assms reqcompose_type) +qed (simple lems: assms rpathcomp_type) -lemma eqcompose_comp: +lemma pathcomp_comp: assumes "A : U(i)" and "a : A" shows "refl(a) \ refl(a) \ refl(a)" -by (subst eqcompose_def) (simple lems: assms reqcompose_comp) +by (subst pathcomp_def) (simple lems: assms rpathcomp_comp) -lemmas EqualProps_rules [intro] = inv_type eqcompose_type -lemmas EqualProps_comps [comp] = inv_comp eqcompose_comp +lemmas EqualProps_rules [intro] = inv_type pathcomp_type +lemmas EqualProps_comps [comp] = inv_comp pathcomp_comp end \ No newline at end of file diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index d3aed66..c3703bf 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -62,7 +62,7 @@ ML_file "~~/src/Tools/eqsubst.ML" text "Perform basic single-step computations:" -method compute uses lems = (subst comp lems) +method compute uses lems = (subst lems comp) end \ No newline at end of file diff --git a/Prod.thy b/Prod.thy index 496bf3e..cb455ac 100644 --- a/Prod.thy +++ b/Prod.thy @@ -68,21 +68,31 @@ lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2 lemmas Prod_comps [comp] = Prod_comp Prod_uniq -subsection \Composition\ -axiomatization fncompose :: "[Term, Term] \ Term" (infixr "\" 70) where - fncompose_type: "\ +section \Function composition\ + +axiomatization compose :: "[Term, Term] \ Term" (infixr "o" 70) + +syntax "_COMPOSE" :: "[Term, Term] \ Term" (infixr "\" 70) +translations "g \ f" \ "g o f" + +axiomatization where + compose_type: "\ g: \x:B. C(x); f: A \ B; (\x:B. C(x)): U(i); A \ B: U(i) \ \ g \ f: \x:A. C(f`x)" and - fncompose_comp: "\ - A: U(i); - \x. x: A \ b(x): B; - \x. x: A \ c(x): C(x) - \ \ (\<^bold>\x. c(x)) \ (\<^bold>\x. b(x)) \ \<^bold>\x. c(b(x))" + compose_comp: "\ + g: \x:B. C(x); + f: A \ B; + (\x:B. C(x)): U(i); + A \ B: U(i) + \ \ g \ f \ \<^bold>\x. g`(f`x)" + +lemmas compose_rules [intro] = compose_type +lemmas compose_comps [comp] = compose_comp section \Unit type\ diff --git a/ProdProps.thy b/ProdProps.thy new file mode 100644 index 0000000..7c2c658 --- /dev/null +++ b/ProdProps.thy @@ -0,0 +1,54 @@ +(* Title: HoTT/ProdProps.thy + Author: Josh Chen + Date: Aug 2018 + +Properties of the dependent product. +*) + +theory ProdProps + imports + HoTT_Methods + Prod +begin + + +section \Composition\ + +text " + The following rule is admissible, but we cannot derive it only using the rules for the \-type. +" + +lemma compose_comp': "\ + A: U(i); + \x. x: A \ b(x): B; + \x. x: B \ c(x): C(x) + \ \ (\<^bold>\x. c(x)) \ (\<^bold>\x. b(x)) \ \<^bold>\x. c(b(x))" +oops + +text "However we can derive a variant with more explicit premises:" + +lemma compose_comp2: + assumes + "A: U(i)" "B: U(i)" and + "C: B \ U(i)" and + "\x. x: A \ b(x): B" and + "\x. x: B \ c(x): C(x)" + shows "(\<^bold>\x. c(x)) \ (\<^bold>\x. b(x)) \ \<^bold>\x. c(b(x))" +proof (subst (0) comp) + show "\<^bold>\x. (\<^bold>\u. c(u))`((\<^bold>\v. b(v))`x) \ \<^bold>\x. c(b(x))" + proof (subst (0) comp) + show "\<^bold>\x. c((\<^bold>\v. b(v))`x) \ \<^bold>\x. c(b(x))" + proof - + have *: "\x. x: A \ (\<^bold>\v. b(v))`x \ b(x)" by simple (rule assms) + show "\<^bold>\x. c((\<^bold>\v. b(v))`x) \ \<^bold>\x. c(b(x))" + proof (subst *) + + +text "We can show associativity of composition in general." + +lemma compose_assoc: + "(f \ g) \ h \ f \ (g \ h)" +proof + + +end \ No newline at end of file diff --git a/scratch.thy b/scratch.thy index 8800b1a..f0514c3 100644 --- a/scratch.thy +++ b/scratch.thy @@ -1,81 +1,9 @@ -(* Title: HoTT/ex/Synthesis.thy - Author: Josh Chen - Date: Aug 2018 - -Examples of inhabitant synthesis. -*) - - theory scratch imports HoTT begin -section \Synthesis of the predecessor function\ - -text " - In this example we try, with the help of Isabelle, to synthesize a predecessor function for the natural numbers. - - This -" - -text " - First we show that the property we want is well-defined: -" - -lemma pred_welltyped: "\pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n): U(O)" -by simple - -text " - Now look for an inhabitant. - Observe that we're looking for a lambda term \pred\ satisfying \(pred`0) =\<^sub>\ 0\ and \\n:\. (pred`(succ n)) =\<^sub>\ n\. - What if we require **definitional** equality instead of just propositional equality? -" - -schematic_goal "?p`0 \ 0" and "\n. n: \ \ (?p`(succ n)) \ n" -apply (subst comp, rule Nat_rules) -prefer 3 apply (subst comp, rule Nat_rules) -prefer 3 apply (rule Nat_rules) -prefer 8 apply (rule Nat_rules | assumption)+ -done - -text " - The above proof finds the candidate \\<^bold>\n. ind\<^sub>\ (\a b. a) n n\. - We prove this has the required type and properties. -" - -definition pred :: Term where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) n n" - -lemma pred_type: "pred: \ \ \" unfolding pred_def by simple - -lemma pred_props: "\n. refl(n)>: ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -proof (simple lem: pred_type) - have *: "pred`0 \ 0" unfolding pred_def - proof (subst comp) - show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple - show "ind\<^sub>\ (\a b. a) 0 0 \ 0" - proof (rule Nat_comps) - show "\: U(O)" .. - qed simple - qed rule - then show "refl(0): (pred`0) =\<^sub>\ 0" by (subst *) simple - - show "\<^bold>\n. refl(n): \n:\. (pred`(succ(n))) =\<^sub>\ n" - unfolding pred_def proof - show "\n. n: \ \ refl(n): ((\<^bold>\n. ind\<^sub>\ (\a b. a) n n)`succ(n)) =\<^sub>\ n" - proof (subst comp) - show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple - show "\n. n: \ \ refl(n): ind\<^sub>\ (\a b. a) (succ n) (succ n) =\<^sub>\ n" - proof (subst comp) - show "\: U(O)" .. - qed simple - qed rule - qed rule -qed -theorem - "\n. refl(n)>>: \pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -by (simple lem: pred_welltyped pred_type pred_props) end \ No newline at end of file -- cgit v1.2.3