From 8833cdf99d3128466d85eb88aeb8e340e07e937c Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 18 Aug 2018 23:27:25 +0200 Subject: Reorganize methods --- Coprod.thy | 2 +- Equal.thy | 2 +- EqualProps.thy | 66 +++++++++++++++++++++++++++---------------------------- HoTT.thy | 8 +++---- HoTT_Methods.thy | 42 +++++++++++++++++++---------------- Nat.thy | 2 +- Prod.thy | 4 ++-- ProdProps.thy | 12 +++++----- Proj.thy | 8 +++---- Sum.thy | 2 +- ex/Methods.thy | 12 +++++----- ex/Synthesis.thy | 20 ++++++++--------- tests/Subgoal.thy | 12 +++++----- 13 files changed, 98 insertions(+), 94 deletions(-) diff --git a/Coprod.thy b/Coprod.thy index f62bb06..4607d1d 100644 --- a/Coprod.thy +++ b/Coprod.thy @@ -59,7 +59,7 @@ lemmas Coprod_intro = Coprod_intro_inl Coprod_intro_inr 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_comp Coprod_elim +lemmas Coprod_routine [intro] = Coprod_form Coprod_intro Coprod_elim end diff --git a/Equal.thy b/Equal.thy index 722a9b9..772072a 100644 --- a/Equal.thy +++ b/Equal.thy @@ -60,7 +60,7 @@ text "Rule attribute declarations:" lemmas Equal_comp [comp] lemmas Equal_wellform [wellform] = Equal_wellform1 Equal_wellform2 Equal_wellform3 -lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_comp Equal_elim +lemmas Equal_routine [intro] = Equal_form Equal_intro Equal_elim end diff --git a/EqualProps.thy b/EqualProps.thy index 8b83c5b..a1d4c45 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -24,7 +24,7 @@ text " lemma inv_type: assumes "A : U(i)" and "x : A" and "y : A" and "p: x =\<^sub>A y" shows "p\: y =\<^sub>A x" unfolding inv_def -by (rule Equal_elim[where ?x=x and ?y=y]) (simple lems: assms) +by (rule Equal_elim[where ?x=x and ?y=y]) (routine lems: assms) \ \The type doesn't depend on \p\ so we don't need to specify \?p\ in the \where\ clause above.\ text " @@ -35,9 +35,9 @@ text " lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\ \ refl(a)" unfolding inv_def -proof +proof compute show "\x. x: A \ refl x: x =\<^sub>A x" .. -qed (simple lems: assms) +qed (routine lems: assms) section \Transitivity / Path composition\ @@ -72,18 +72,18 @@ proof 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]) (simple lems: assms asm) - qed (simple lems: assms) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) + qed (routine lems: assms) qed (rule assms) - qed (simple lems: assms 1 2 3) - qed (simple lems: assms 1 2) + 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 (simple lems: assms rpathcomp_type) + by (routine 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. @@ -109,11 +109,11 @@ proof compute proof fix u z assume asm: "u: A" "z: A" show "\q. q: u =\<^sub>A z \ ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms asm) - qed (simple lems: assms) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms asm) + qed (routine lems: assms) qed (rule assms) - qed (simple lems: assms 1 2 3) - qed (simple lems: assms 1 2) + qed (routine lems: assms 1 2 3) + qed (routine lems: assms 1 2) qed (rule assms) } show "(\<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p)`a`refl(a)`a`refl(a) \ refl(a)" @@ -131,11 +131,11 @@ proof compute show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" proof show "\q. q: u =\<^sub>A z \ ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 3 4) - qed (simple lems: assms 3 4) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 3 4) + qed (routine lems: assms 3 4) qed fact - qed (simple lems: assms 1 2) - qed (simple lems: assms 1) } + qed (routine lems: assms 1 2) + qed (routine lems: assms 1) } show "(\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \ refl(a)" proof compute @@ -149,10 +149,10 @@ proof compute show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" proof show "\q. q: u =\<^sub>A z \ ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 2 3) - qed (simple lems: assms 2 3) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 2 3) + qed (routine lems: assms 2 3) qed fact - qed (simple lems: assms 1) } + qed (routine lems: assms 1) } show "(ind\<^sub>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \ refl(a)" proof compute @@ -163,8 +163,8 @@ proof compute show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" proof show "\q. q: u =\<^sub>A z \ ind\<^sub>= refl q: u =\<^sub>A z" - by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 1 2) - qed (simple lems: assms 1 2) + by (rule Equal_elim[where ?x=u and ?y=z]) (routine lems: assms 1 2) + qed (routine lems: assms 1 2) qed fact } show "(\<^bold>\z q. ind\<^sub>= refl q)`a`refl(a) \ refl(a)" @@ -173,21 +173,21 @@ proof compute show "\<^bold>\q. ind\<^sub>= refl q: a =\<^sub>A a \ a =\<^sub>A a" proof show "\q. q: a =\<^sub>A a \ ind\<^sub>= refl q: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: assms 1) - qed (simple lems: assms 1) } + by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms 1) + qed (routine lems: assms 1) } show "(\<^bold>\q. ind\<^sub>= refl q)`refl(a) \ refl(a)" proof compute show "\p. p: a =\<^sub>A a \ ind\<^sub>= refl p: a =\<^sub>A a" - by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: assms) + by (rule Equal_elim[where ?x=a and ?y=a]) (routine lems: assms) show "ind\<^sub>= refl (refl(a)) \ refl(a)" - proof + proof compute show "\x. x: A \ refl(x): x =\<^sub>A x" .. - qed (simple lems: assms) - qed (simple lems: assms) + qed (routine lems: assms) + qed (routine lems: assms) qed fact - qed (simple lems: assms) - qed (simple lems: assms) + qed (routine lems: assms) + qed (routine lems: assms) qed fact qed fact @@ -207,15 +207,15 @@ lemma pathcomp_type: shows "p \ 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 (simple lems: assms rpathcomp_type) +qed (routine lems: assms rpathcomp_type) lemma pathcomp_comp: assumes "A : U(i)" and "a : A" shows "refl(a) \ refl(a) \ refl(a)" -by (subst pathcomp_def) (simple lems: assms rpathcomp_comp) +by (subst pathcomp_def) (routine lems: assms rpathcomp_comp) -lemmas EqualProps_rules [intro] = inv_type pathcomp_type -lemmas EqualProps_comps [comp] = inv_comp pathcomp_comp +lemmas EqualProps_type [intro] = inv_type pathcomp_type +lemmas EqualProps_comp [comp] = inv_comp pathcomp_comp end diff --git a/HoTT.thy b/HoTT.thy index 789eed2..60e0e71 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -25,13 +25,13 @@ Proj begin -lemmas form_rules = +lemmas forms = Nat_form Prod_form Sum_form Coprod_form Equal_form Unit_form Empty_form -lemmas intro_rules = +lemmas intros = Nat_intro Prod_intro Sum_intro Equal_intro Coprod_intro Unit_intro -lemmas elim_rules = +lemmas elims = Nat_elim Prod_elim Sum_elim Equal_elim Coprod_elim Unit_elim Empty_elim -lemmas routine_rules = +lemmas routines = Nat_routine Prod_routine Sum_routine Equal_routine Coprod_routine Unit_routine Empty_routine end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 4d2174b..32e412b 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -12,23 +12,19 @@ theory HoTT_Methods begin -section \Method definitions\ - -subsection \Simple type rule proof search\ +section \Deriving typing judgments\ text " - Prove type judgments \A : U\ and inhabitation judgments \a : A\ using the type rules declared [intro] in the respective theory files, as well as additional provided lemmas. - - Can also perform typechecking, and search for elements of a type. + \routine\ proves routine type judgments \a : A\ using the rules declared [intro] in the respective theory files, as well as additional provided lemmas. " -method simple uses lems = (assumption | rule lems | standard)+ - - -subsection \Wellformedness checker\ +method routine uses lems = (assumption | rule lems | standard)+ text " - \wellformed\ finds a proof of any valid typing judgment derivable from the judgments passed as \lem\. + \wellformed'\ finds a proof of any valid typing judgment derivable from the judgment passed as \jdmt\. + If no judgment is passed, it will try to resolve with the theorems declared \wellform\. + \wellform\ is like \wellformed'\ but takes multiple judgments. + The named theorem \wellform\ is declared in HoTT_Base.thy. " @@ -42,14 +38,7 @@ method wellformed uses lems = match lems in lem: "?X : ?Y" \ \wellformed' jdmt: lem\ -subsection \Derivation search\ - -text " Combine \simple\ and \wellformed\ to search for derivations of judgments." - -method derive uses lems = (simple lems: lems | wellformed lems: lems)+ - - -subsection \Substitution and simplification\ +section \Substitution and simplification\ text "Import the \subst\ method, used for substituting definitional equalities." @@ -64,4 +53,19 @@ text "Perform basic single-step computations:" method compute uses lems = (subst lems comp | rule lems comp) +section \Derivation search\ + +text " Combine \routine\, \wellformed\, and \compute\ to search for derivations of judgments." + +method derive uses lems = (routine lems: lems | compute lems: lems | wellformed lems: lems)+ + + +section \Induction\ + +text " + Placeholder section for the automation of induction, i.e. using the elimination rules. + At the moment one must directly apply them with \rule X_elim\. +" + + end diff --git a/Nat.thy b/Nat.thy index b48804a..45c3a2e 100644 --- a/Nat.thy +++ b/Nat.thy @@ -48,7 +48,7 @@ text "Rule attribute declarations:" 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_comp Nat_elim +lemmas Nat_routine [intro] = Nat_form Nat_intro Nat_elim end diff --git a/Prod.thy b/Prod.thy index 323bef4..9dbb01e 100644 --- a/Prod.thy +++ b/Prod.thy @@ -70,7 +70,7 @@ text "Rule attribute declarations---set up various methods to use the type rules lemmas Prod_comp [comp] = Prod_appl Prod_uniq lemmas Prod_wellform [wellform] = Prod_wellform1 Prod_wellform2 -lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_comp Prod_elim +lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim section \Function composition\ @@ -97,7 +97,7 @@ and Unit_comp: "\C: \ \ U(i); c: C(\)\ \ ind\<^sub>\(c)(\) \ c" lemmas Unit_comp [comp] -lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_comp Unit_elim +lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim end diff --git a/ProdProps.thy b/ProdProps.thy index 3e51102..1af6ad3 100644 --- a/ProdProps.thy +++ b/ProdProps.thy @@ -29,10 +29,10 @@ proof (subst (0 1 2 3) compose_def) 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) + show "\x. x: A \ g`(f`x): C" by (routine lems: assms) qed - show "\x. x: B \ h`(g`x): D(g`x)" by (simple lems: assms) - qed (simple lems: assms) + show "\x. x: B \ h`(g`x): D(g`x)" by (routine lems: assms) + qed (routine lems: assms) qed fact qed @@ -44,9 +44,9 @@ proof (subst compose_def, subst Prod_eq) show "\a. a: A \ (\<^bold>\x. c(x))`((\<^bold>\x. b(x))`a) \ (\<^bold>\x. c (b x))`a" proof compute show "\a. a: A \ c((\<^bold>\x. b(x))`a) \ (\<^bold>\x. c(b(x)))`a" - by compute (simple lems: assms, compute?)+ - qed (simple lems: assms) -qed (simple lems: assms) + by (derive lems: assms) + qed (routine lems: assms) +qed (derive lems: assms) end diff --git a/Proj.thy b/Proj.thy index dffc127..a1c4c8f 100644 --- a/Proj.thy +++ b/Proj.thy @@ -24,9 +24,9 @@ unfolding fst_def by (derive lems: assms) lemma fst_comp: assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "fst() \ a" unfolding fst_def -proof +proof compute show "a: A" and "b: B(a)" by fact+ -qed (simple lems: assms)+ +qed (routine lems: assms)+ lemma snd_type: assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "snd(p): B(fst p)" @@ -46,11 +46,11 @@ qed fact lemma snd_comp: assumes "A: U(i)" and "B: A \ U(i)" and "a: A" and "b: B(a)" shows "snd() \ b" unfolding snd_def -proof +proof compute show "\x y. y: B(x) \ y: B(x)" . show "a: A" by fact show "b: B(a)" by fact -qed (simple lems: assms) +qed (routine lems: assms) text "Rule attribute declarations:" diff --git a/Sum.thy b/Sum.thy index dce5834..f97bef1 100644 --- a/Sum.thy +++ b/Sum.thy @@ -63,7 +63,7 @@ text "Rule attribute declarations:" lemmas Sum_comp [comp] lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2 -lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_comp Sum_elim +lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim section \Empty type\ diff --git a/ex/Methods.thy b/ex/Methods.thy index 415fbc3..c78af14 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -14,7 +14,7 @@ text "Wellformedness results, metatheorems written into the object theory using lemma assumes "A : U(i)" "B: A \ U(i)" "\x. x : A \ C x: B x \ U(i)" shows "\x:A. \y:B x. \z:C x y. \w:A. x =\<^sub>A w : U(i)" -by (simple lems: assms) +by (routine lems: assms) lemma @@ -38,7 +38,7 @@ text "Typechecking and constructing inhabitants:" \ \Correctly determines the type of the pair\ schematic_goal "\A: U(i); B: U(i); a : A; b : B\ \ : ?A" -by simple +by routine \ \Finds pair (too easy).\ schematic_goal "\A: U(i); B: U(i); a : A; b : B\ \ ?x : A \ B" @@ -56,19 +56,19 @@ lemma assumes "A: U(i)" "a: A" shows "(\<^bold>\x. )`a \ " proof compute - show "\x. x: A \ : A \ \" by simple -qed (simple lems: assms) + show "\x. x: A \ : A \ \" by routine +qed (routine lems: assms) lemma assumes "A: U(i)" "B: A \ U(i)" "a: A" "b: B(a)" shows "(\<^bold>\x y. )`a`b \ " proof compute - show "\x. x: A \ \<^bold>\y. : \y:B(x). \x:A. B(x)" by (simple lems: assms) + show "\x. x: A \ \<^bold>\y. : \y:B(x). \x:A. B(x)" by (routine lems: assms) show "(\<^bold>\b. )`b \ " proof compute - show "\b. b: B(a) \ : \x:A. B(x)" by (simple lems: assms) + show "\b. b: B(a) \ : \x:A. B(x)" by (routine lems: assms) qed fact qed fact diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index cff9374..a5e77ec 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -21,7 +21,7 @@ text " 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 +by routine text " Now we look for an inhabitant of this type. @@ -33,7 +33,7 @@ schematic_goal "?p`0 \ 0" and "\n. n: \ \ (?p`( apply compute prefer 4 apply compute prefer 3 apply compute -apply (rule Nat_routine Nat_elim | assumption)+ +apply (rule Nat_routine Nat_elim | compute | assumption)+ done text " @@ -43,36 +43,36 @@ text " definition pred :: Term where "pred \ \<^bold>\n. ind\<^sub>\ (\a b. a) 0 n" -lemma pred_type: "pred: \ \ \" unfolding pred_def by simple +lemma pred_type: "pred: \ \ \" unfolding pred_def by routine lemma pred_props: "\n. refl(n)>: ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -proof (simple lems: pred_type) +proof (routine lems: pred_type) have *: "pred`0 \ 0" unfolding pred_def proof compute - show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by simple + show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by routine show "ind\<^sub>\ (\a b. a) 0 0 \ 0" proof compute show "\: U(O)" .. - qed simple + qed routine qed rule - then show "refl(0): (pred`0) =\<^sub>\ 0" by (subst *) simple + then show "refl(0): (pred`0) =\<^sub>\ 0" by (subst *) routine 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) 0 n)`succ(n)) =\<^sub>\ n" proof compute - show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by simple + show "\n. n: \ \ ind\<^sub>\ (\a b. a) 0 n: \" by routine show "\n. n: \ \ refl(n): ind\<^sub>\ (\a b. a) 0 (succ n) =\<^sub>\ n" proof compute show "\: U(O)" .. - qed simple + qed routine qed rule qed rule qed theorem "\n. refl(n)>>: \pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -by (simple lems: pred_welltyped pred_type pred_props) +by (routine lems: pred_welltyped pred_type pred_props) end diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy index 9690013..82d7e5d 100644 --- a/tests/Subgoal.thy +++ b/tests/Subgoal.thy @@ -25,11 +25,11 @@ apply standard apply (rule Prod_intro) subgoal premises 4 for u z q apply (rule Equal_elim[where ?x=u and ?y=z]) - apply (simple lems: assms 4) + apply (routine lems: assms 4) done - apply (simple lems: assms 1 2 3) + apply (routine lems: assms 1 2 3) done - apply (simple lems: assms 1 2) + apply (routine lems: assms 1 2) done apply fact done @@ -52,9 +52,9 @@ text " Try (and fail) to synthesize the constant for path composition, following the proof of \rpathcomp_type\ below. " -apply (rule Prod_intro) - apply (rule Prod_intro) - apply (rule Prod_intro) +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 -- cgit v1.2.3