From 8ed9cf8682c07fc47b86c2d0aaeb8b4628aeaa31 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 16 Aug 2018 16:11:42 +0200 Subject: Prod.thy now has the correct definitional equality structure rule. Definition of function composition and properties. --- Coprod.thy | 2 +- Equal.thy | 2 +- EqualProps.thy | 2 +- HoTT.thy | 2 +- HoTT_Base.thy | 2 +- HoTT_Methods.thy | 2 +- HoTT_Theorems.thy | 2 +- Nat.thy | 2 +- Prod.thy | 28 ++++++--------- ProdProps.thy | 100 +++++++++++++++++++++++++++++++++++++++++------------- Proj.thy | 2 +- Sum.thy | 2 +- ex/Synthesis.thy | 16 ++++----- 13 files changed, 105 insertions(+), 59 deletions(-) diff --git a/Coprod.thy b/Coprod.thy index 178e345..f2225f6 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -62,4 +62,4 @@ lemmas Coprod_form_conds [wellform] = Coprod_form_cond1 Coprod_form_cond2 lemmas Coprod_comps [comp] = Coprod_comp1 Coprod_comp2 -end \ No newline at end of file +end diff --git a/Equal.thy b/Equal.thy index 9fc478a..bd7dd93 100644 --- a/Equal.thy +++ b/Equal.thy @@ -65,4 +65,4 @@ lemmas Equal_comps [comp] = Equal_comp -end \ No newline at end of file +end diff --git a/EqualProps.thy b/EqualProps.thy index f3b355a..5eea920 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -221,4 +221,4 @@ lemmas EqualProps_rules [intro] = inv_type pathcomp_type lemmas EqualProps_comps [comp] = inv_comp pathcomp_comp -end \ No newline at end of file +end diff --git a/HoTT.thy b/HoTT.thy index ce77ec7..724eebc 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -23,4 +23,4 @@ EqualProps Proj begin -end \ No newline at end of file +end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 4fadd5d..647593e 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -85,4 +85,4 @@ named_theorems wellform named_theorems comp -end \ No newline at end of file +end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index c3703bf..316841d 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -65,4 +65,4 @@ text "Perform basic single-step computations:" method compute uses lems = (subst lems comp) -end \ No newline at end of file +end diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index a3a1f63..79614d3 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -203,4 +203,4 @@ The next thing to do is to implement induction to automate such proofs. When we get more stuff working, I'd like to aim for formalizing the encode-decode method to be able to prove the only naturals are 0 and those obtained from it by \succ\." *) -end \ No newline at end of file +end diff --git a/Nat.thy b/Nat.thy index 21c9b1c..b710ff2 100644 --- a/Nat.thy +++ b/Nat.thy @@ -52,4 +52,4 @@ lemmas Nat_rules [intro] = Nat_form Nat_intro Nat_elim Nat_comp1 Nat_comp2 lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 -end \ No newline at end of file +end diff --git a/Prod.thy b/Prod.thy index cb455ac..120fc59 100644 --- a/Prod.thy +++ b/Prod.thy @@ -43,11 +43,15 @@ and and Prod_elim: "\f: \x:A. B(x); a: A\ \ f`a: B(a)" and - Prod_comp: "\a: A; \x. x: A \ b(x): B(x)\ \ (\<^bold>\x. b(x))`a \ b(a)" + Prod_comp: "\\x. x: A \ b(x): B(x); a: A\ \ (\<^bold>\x. b(x))`a \ b(a)" and Prod_uniq: "f : \x:A. B(x) \ \<^bold>\x. (f`x) \ f" +and + Prod_eq: "\\x. x: A \ b(x) \ b'(x); A: U(i)\ \ \<^bold>\x. b(x) \ \<^bold>\x. b'(x)" text " + The Pure rules for \\\ only let us judge strict syntactic equality of object lambda expressions; Prod_eq is the actual definitional equality rule. + Note that the syntax \\<^bold>\\ (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \
2.5.2 of the Isabelle/Isar Implementation). " @@ -64,9 +68,9 @@ and text "Set up the standard reasoner to use the type rules:" -lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq +lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq Prod_eq lemmas Prod_wellform [wellform] = Prod_form_cond1 Prod_form_cond2 -lemmas Prod_comps [comp] = Prod_comp Prod_uniq +lemmas Prod_comps [comp] = Prod_comp Prod_uniq Prod_eq section \Function composition\ @@ -77,23 +81,13 @@ syntax "_COMPOSE" :: "[Term, Term] \ Term" (infixr "\" 70) translations "g \ f" \ "g o f" axiomatization where - compose_type: "\ - g: \x:B. C(x); + compose_def: "\ f: A \ B; - (\x:B. C(x)): U(i); - A \ B: U(i) - \ \ g \ f: \x:A. C(f`x)" -and - compose_comp: "\ g: \x:B. C(x); - f: A \ B; - (\x:B. C(x)): U(i); - A \ B: U(i) + A \ B: U(i); + (\x:B. C(x)): U(i) \ \ g \ f \ \<^bold>\x. g`(f`x)" -lemmas compose_rules [intro] = compose_type -lemmas compose_comps [comp] = compose_comp - section \Unit type\ @@ -114,4 +108,4 @@ lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp lemmas Unit_comps [comp] = Unit_comp -end \ No newline at end of file +end diff --git a/ProdProps.thy b/ProdProps.thy index 7c2c658..e48b3e6 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -15,40 +15,94 @@ begin section \Composition\ text " - The following rule is admissible, but we cannot derive it only using the rules for the \-type. + The proof of associativity is surprisingly intricate; it involves telling Isabelle to use the correct rule for \-type judgmental equality, and the correct substitutions in the subgoals thereafter, among other things. " -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))" +lemma compose_assoc: + assumes + "A \ B: U(i)" "B \ C: U(i)" and + "\x:C. D(x): U(i)" and + "f: A \ B" "g: B \ C" "h: \x:C. D(x)" + shows "(h \ g) \ f \ h \ (g \ f)" + +proof (subst (0 1 2 3) compose_def) + text "Compute the different bracketings and show they are equivalent:" + + show "\<^bold>\x. (\<^bold>\y. h`(g`y))`(f`x) \ \<^bold>\x. h`((\<^bold>\y. g`(f`y))`x)" + proof (subst Prod_eq) + show "\<^bold>\x. h`((\<^bold>\y. g`(f`y))`x) \ \<^bold>\x. h`((\<^bold>\y. g`(f`y))`x)" by simp + show "\x. x: A \ (\<^bold>\y. h`(g`y))`(f`x) \ h`((\<^bold>\y. g`(f`y))`x)" + proof compute + show "\x. x: A \ h`(g`(f`x)) \ h`((\<^bold>\y. g`(f`y))`x)" + proof compute + show "\x. x: A \ g`(f`x): C" by (simple lems: assms) + qed + show "\x. x: B \ h`(g`x): D(g`x)" by (simple lems: assms) + qed (simple lems: assms) + qed (wellformed lems: assms) + + text " + Finish off any remaining subgoals that Isabelle can't prove automatically. + These typically require the application of specific substitutions or computation rules. + " + show "g \ f: A \ C" by (subst compose_def) (derive lems: assms) + + show "h \ g: \x:B. D(g`x)" + proof (subst compose_def) + show "\<^bold>\x. h`(g`x): \x:B. D(g`x)" + proof + show "\x. x: B \ h`(g`x): D(g`x)" + proof + show "\x. x: B \ g`x: C" by (simple lems: assms) + qed (simple lems: assms) + qed (wellformed lems: assms) + qed fact+ + + show "\x:B. D (g`x): U(i)" + proof + show "\x. x: B \ D(g`x): U(i)" + proof - + have *: "D: C \ U(i)" by (wellformed lems: assms) + + fix x assume asm: "x: B" + have "g`x: C" by (simple lems: assms asm) + then show "D(g`x): U(i)" by (rule *) + qed + qed (wellformed lems: assms) + + have "A: U(i)" by (wellformed lems: assms) + moreover have "C: U(i)" by (wellformed lems: assms) + ultimately show "A \ C: U(i)" .. +qed (simple lems: assms) + + +text "The following rule is correct, but we cannot prove it using just the rules of the theory." + +lemma compose_comp': + assumes "A: 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))" oops text "However we can derive a variant with more explicit premises:" -lemma compose_comp2: +lemma compose_comp: assumes - "A: U(i)" "B: U(i)" and - "C: B \ U(i)" and + "A: U(i)" "B: U(i)" "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 *) - +proof (subst compose_def) + show "\<^bold>\x. (\<^bold>\x. c(x))`((\<^bold>\x. b(x))`x) \ \<^bold>\x. c(b(x))" + proof + show "\a. a: A \ (\<^bold>\x. c(x))`((\<^bold>\x. b(x))`a) \ c(b(a))" + proof compute + show "\a. a: A \ c((\<^bold>\x. b(x))`a) \ c(b(a))" by compute (simple lems: assms) + qed (simple lems: assms) + qed fact +qed (simple lems: assms) -text "We can show associativity of composition in general." -lemma compose_assoc: - "(f \ g) \ h \ f \ (g \ h)" -proof +lemmas compose_comps [comp] = compose_def compose_comp -end \ No newline at end of file +end diff --git a/Proj.thy b/Proj.thy index d5ae6fa..76f9f11 100644 --- a/Proj.thy +++ b/Proj.thy @@ -60,4 +60,4 @@ lemmas Proj_types [intro] = fst_type snd_type lemmas Proj_comps [comp] = fst_comp snd_comp -end \ No newline at end of file +end diff --git a/Sum.thy b/Sum.thy index 145c303..8522af1 100644 --- a/Sum.thy +++ b/Sum.thy @@ -77,4 +77,4 @@ and lemmas Empty_rules [intro] = Empty_form Empty_elim -end \ No newline at end of file +end diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index ef6673c..cd5c4e1 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -19,9 +19,7 @@ text " This is also done in \CTT.thy\; there the work is easier as the equality type is extensional, and also the methods are set up a little more nicely. " -text " - First we show that the property we want is well-defined. -" +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 @@ -40,11 +38,11 @@ apply (rule Nat_rules | assumption)+ done text " - The above proof finds a candidate, namely \\<^bold>\n. ind\<^sub>\ (\a b. a) n n\. + The above proof finds a candidate, namely \\<^bold>\n. ind\<^sub>\ (\a b. a) 0 n\. We prove this has the required type and properties. " -definition pred :: Term where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) n n" +definition pred :: Term where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) 0 n" lemma pred_type: "pred: \ \ \" unfolding pred_def by simple @@ -52,7 +50,7 @@ lemma pred_props: "\n. refl(n)>: ((pred`0) =\<^sub>\ 0" unfolding pred_def proof compute - show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple + show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by simple show "ind\<^sub>\ (\a b. a) 0 0 \ 0" proof (rule Nat_comps) show "\: U(O)" .. @@ -62,10 +60,10 @@ proof (simple lems: pred_type) 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" + show "\n. n: \ \ refl(n): ((\<^bold>\n. ind\<^sub>\ (\a b. a) 0 n)`succ(n)) =\<^sub>\ n" proof compute - 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" + show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by simple + show "\n. n: \ \ refl(n): ind\<^sub>\ (\a b. a) 0 (succ n) =\<^sub>\ n" proof compute show "\: U(O)" .. qed simple -- cgit v1.2.3