From 9ffa5ed2a972db4ae6274a7852de37945a32ab0e Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 3 Jul 2018 17:06:58 +0200 Subject: Rewrote methods: wellformed now two lines, uses named theorems. New, more powerful derive method. Used these to rewrite proofs. --- EqualProps.thy | 48 +++++++------------ HoTT_Base.thy | 9 ++-- HoTT_Methods.thy | 143 +++++++++++++++++++++++++++++++++---------------------- Prod.thy | 3 +- Proj.thy | 33 +++---------- Sum.thy | 2 +- 6 files changed, 117 insertions(+), 121 deletions(-) diff --git a/EqualProps.thy b/EqualProps.thy index b691133..10d3b17 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -18,6 +18,7 @@ section \Symmetry / Path inverse\ definition inv :: "[Term, Term, Term] \ Term" ("(1inv[_,/ _,/ _])") where "inv[A,x,y] \ \<^bold>\p:x =\<^sub>A y. indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) x y p" + lemma inv_type: assumes "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x" @@ -64,45 +65,32 @@ section \Transitivity / Path composition\ text "``Raw'' composition function, of type \\x,y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)\." definition rcompose :: "Term \ Term" ("(1rcompose[_])") - where "rcompose[A] \ \<^bold>\x:A. \<^bold>\y:A. \<^bold>\p:x =\<^sub>A y. indEqual[A] + where "rcompose[A] \ \<^bold>\x:A. \<^bold>\y:A. \<^bold>\p:(x =\<^sub>A y). indEqual[A] (\x y _. \z:A. y =\<^sub>A z \ x =\<^sub>A z) - (\x. \<^bold>\z:A. \<^bold>\p:x =\<^sub>A z. indEqual[A](\x z _. x =\<^sub>A z) (\x. refl(x)) x z p) + (\x. \<^bold>\z:A. \<^bold>\p:(x =\<^sub>A z). indEqual[A](\x z _. x =\<^sub>A z) (\x. refl(x)) x z p) x y p" text "``Natural'' composition function abbreviation, effectively equivalent to a function of type \\x,y,z:A. x =\<^sub>A y \ y =\<^sub>A z \ x =\<^sub>A z\." abbreviation compose :: "[Term, Term, Term, Term] \ Term" ("(1compose[_,/ _,/ _,/ _])") - where "compose[A,x,y,z] \ \<^bold>\p:x =\<^sub>A y. \<^bold>\q:y =\<^sub>A z. rcompose[A]`x`y`p`z`q" + where "compose[A,x,y,z] \ \<^bold>\p:(x =\<^sub>A y). \<^bold>\q:(y =\<^sub>A z). rcompose[A]`x`y`p`z`q" + + +lemma compose_type: + assumes "p : x =\<^sub>A y" and "q : y =\<^sub>A z" + shows "compose[A,x,y,z]`p`q : x =\<^sub>A z" + +sorry lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" -proof (unfold rcompose_def) - have "compose[A,a,a,a]`refl(a) \ \<^bold>\q:a =\<^sub>A a. rcompose[A]`a`a`refl(a)`a`q" - proof standard+ (*TODO: Set up the Simplifier to handle this proof at some point.*) - fix p q assume "p : a =\<^sub>A a" and "q : a =\<^sub>A a" - then show "rcompose[A]`a`a`p`a`q : a =\<^sub>A a" - proof (unfold rcompose_def) - have "(\<^bold>\x:A. \<^bold>\y:A. \<^bold>\p:x =\<^sub>A y. (indEqual[A] - (\x y _. \z:A. y =[A] z \ x =[A] z) - (\x. \<^bold>\z:A. \<^bold>\q:x =\<^sub>A z. (indEqual[A] (\x z _. x =\<^sub>A z) refl x z q)) - x y p))`a`a`p`a`q \ ..." (*Okay really need to set up the Simplifier...*) -oops - -text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \using\ clause in the proof. -This would likely involve something like: - 1. Recognizing that there is a function application that can be simplified. - 2. Noting that the obstruction to applying \Prod_comp\ is the requirement that \refl(a) : a =\<^sub>A a\. - 3. Obtaining such a condition, using the known fact \a : A\ and the introduction rule \Equal_intro\." - -lemmas Equal_simps [simp] = inv_comp compose_comp - -section \Pretty printing\ - -abbreviation inv_pretty :: "[Term, Term, Term, Term] \ Term" ("(1_\<^sup>-\<^sup>1[_, _, _])" 500) - where "p\<^sup>-\<^sup>1[A,x,y] \ inv[A,x,y]`p" - -abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \ Term" ("(1_ \[_, _, _, _]/ _)") - where "p \[A,x,y,z] q \ compose[A,x,y,z]`p`q" \ No newline at end of file +sorry \ \Long and tedious proof if the Simplifier is not set up.\ + + +lemmas Equal_simps [intro] = inv_comp compose_comp + + +end \ No newline at end of file diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 561dbe6..e5c0776 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -11,13 +11,14 @@ begin section \Setup\ -text "Set up type checking routines, proof methods etc." +text "Declare rules expressing necessary wellformedness conditions for type and inhabitation judgments." +named_theorems wellform section \Metalogical definitions\ text "A single meta-type \Term\ suffices to implement the object-logic types and terms. -We do not implement universes, and simply use \a : U\ as a convenient shorthand to mean ''\a\ is a type''." +We do not implement universes, and simply use \a : U\ as a convenient shorthand to mean ``\a\ is a type''." typedecl Term @@ -35,7 +36,7 @@ consts text "The following fact is used to make explicit the assumption of well-formed contexts." axiomatization where - inhabited_implies_type [intro, elim]: "\a A. a : A \ A : U" + inhabited_implies_type [intro, elim, wellform]: "\a A. a : A \ A : U" section \Type families\ @@ -47,7 +48,7 @@ type_synonym Typefam = "Term \ Term" abbreviation (input) is_type_family :: "[Typefam, Term] \ prop" ("(3_:/ _ \ U)") where "P: A \ U \ (\x. x : A \ P x : U)" -text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML code, and is for the moment not really crucial." +\ \There is an obvious generalization to multivariate type families, but implementing such an abbreviation would probably involve writing ML code, and is for the moment not really crucial.\ end \ No newline at end of file diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index 7886c1a..bce5123 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -3,7 +3,7 @@ Date: Jun 2018 Method setup for the HoTT library. -Relies on Eisbach, which for the moment lives in HOL/Eisbach. +Relies heavily on Eisbach. *) theory HoTT_Methods @@ -16,71 +16,100 @@ theory HoTT_Methods Sum begin +section \Method setup\ -text "This method finds a proof of any valid typing judgment derivable from a given wellformed judgment." +text "Prove type judgments \A : U\ and inhabitation judgments \a : A\ using rules declared [intro] and [elim], as well as additional provided lemmas." + +method simple uses lems = (assumption|standard|rule lems)+ + + +text "Find a proof of any valid typing judgment derivable from a given wellformed judgment." method wellformed uses jdgmt = ( - match jdgmt in - "?a : ?A" \ \ - rule HoTT_Base.inhabited_implies_type[OF jdgmt] | - wellformed jdgmt: HoTT_Base.inhabited_implies_type[OF jdgmt] - \ \ - "A : U" for A \ \ - match (A) in - "\x:?A. ?B x" \ \ - print_term "\", - (rule Prod.Prod_form_cond1[OF jdgmt] | - rule Prod.Prod_form_cond2[OF jdgmt] | - catch \wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\ \fail\) - \ \ - "\x:?A. ?B x" \ \ - rule Sum.Sum_form_cond1[OF jdgmt] | - rule Sum.Sum_form_cond2[OF jdgmt] | - catch \wellformed jdgmt: Sum.Sum_form_cond1[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: Sum.Sum_form_cond2[OF jdgmt]\ \fail\ - \ \ - "?a =[?A] ?b" \ \ - rule Equal.Equal_form_cond1[OF jdgmt] | - rule Equal.Equal_form_cond2[OF jdgmt] | - rule Equal.Equal_form_cond3[OF jdgmt] | - catch \wellformed jdgmt: Equal.Equal_form_cond1[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: Equal.Equal_form_cond2[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: Equal.Equal_form_cond3[OF jdgmt]\ \fail\ - \ - \ \ - "PROP ?P \ PROP Q" for Q \ \ - catch \rule Prod.Prod_form_cond1[OF jdgmt]\ \fail\ | - catch \rule Prod.Prod_form_cond2[OF jdgmt]\ \fail\ | - catch \rule Sum.Sum_form_cond1[OF jdgmt]\ \fail\ | - catch \rule Sum.Sum_form_cond2[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: Prod.Prod_form_cond1[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: Prod.Prod_form_cond2[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: Sum.Sum_form_cond1[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: Sum.Sum_form_cond2[OF jdgmt]\ \fail\ - \ + match wellform in rl: "PROP ?P" \ \( + catch \rule rl[OF jdgmt]\ \fail\ | + catch \wellformed jdgmt: rl[OF jdgmt]\ \fail\ + )\ ) -notepad \ \Examples using \wellformed\\ -begin -assume 0: "f : \x:A. B x" - have "\x:A. B x : U" by (wellformed jdgmt: 0) - have "A : U" by (wellformed jdgmt: 0) - have "B: A \ U" by (wellformed jdgmt: 0) +text "Combine \simple\ and \wellformed\ to search for derivations." + +method derive uses lems = ( + catch \unfold lems\ \fail\ | + catch \simple lems: lems\ \fail\ | + match lems in lem: "?X : ?Y" \ \wellformed jdgmt: lem\ + )+ + + +section \Examples\ + +lemma + assumes "A : U" "B: A \ U" "\x. x : A \ C x: B x \ U" + shows "\x:A. \y:B x. \z:C x y. \w:A. x =\<^sub>A w : U" +by (simple lems: assms) + +lemma + assumes "f : \x:A. \y: B x. \z: C x y. D x y z" + shows + "A : U" and + "B: A \ U" and + "\x. x : A \ C x: B x \ U" and + "\x y. \x : A; y : B x\ \ D x y: C x y \ U" +proof - + show "A : U" by (wellformed jdgmt: assms) + show "B: A \ U" by (wellformed jdgmt: assms) + show "\x. x : A \ C x: B x \ U" by (wellformed jdgmt: assms) + show "\x y. \x : A; y : B x\ \ D x y: C x y \ U" by (wellformed jdgmt: assms) +qed + + +section \Experimental methods\ + +text "Playing around with ML, following CTT/CTT.thy by Larry Paulson." + +lemmas forms = Prod_form Sum_form Equal_form +lemmas intros = Prod_intro Sum_intro Equal_intro +lemmas elims = Prod_elim Sum_elim Equal_elim +lemmas elements = intros elims + +ML \ +(* Try solving \a : A\ by assumption provided \a\ is rigid *) +fun test_assume_tac ctxt = let + fun is_rigid (Const(@{const_name is_of_type},_) $ a $ _) = not(is_Var (head_of a)) + | is_rigid (Const(@{const_name is_a_type},_) $ a $ _ $ _) = not(is_Var (head_of a)) + | is_rigid _ = false + in + SUBGOAL (fn (prem, i) => + if is_rigid (Logic.strip_assums_concl prem) + then assume_tac ctxt i else no_tac) + end + +fun ASSUME ctxt tf i = test_assume_tac ctxt i ORELSE tf i + +(* Solve all subgoals \A : U\ using formation rules. *) +val form_net = Tactic.build_net @{thms forms}; +fun form_tac ctxt = + REPEAT_FIRST (ASSUME ctxt (filt_resolve_from_net_tac ctxt 1 form_net)); -assume 1: "f : \x:A. \y: B x. C x y" - have "A : U" by (wellformed jdgmt: 1) - have "B: A \ U" by (wellformed jdgmt: 1) - have "\x. x : A \ C x: B x \ U" by (wellformed jdgmt: 1) +(* Try to prove inhabitation judgments \a : A\ (\a\ flexible, \A\ rigid) by introduction rules. *) +fun intro_tac ctxt thms = + let val tac = + filt_resolve_from_net_tac ctxt 1 + (Tactic.build_net (thms @ @{thms forms} @ @{thms intros})) + in REPEAT_FIRST (ASSUME ctxt tac) end -assume 2: "g : \x:A. \y: B x. \z: C x y. D x y z" - have a: "A : U" by (wellformed jdgmt: 2) - have b: "B: A \ U" by (wellformed jdgmt: 2) - have c: "\x. x : A \ C x : B x \ U" by (wellformed jdgmt: 2) - have d: "\x y. \x : A; y : B x\ \ D x y : C x y \ U" by (wellformed jdgmt: 2) +(*Type checking: solve \a : A\ (\a\ rigid, \A\ flexible) by formation, introduction and elimination rules. *) +fun typecheck_tac ctxt thms = + let val tac = + filt_resolve_from_net_tac ctxt 3 + (Tactic.build_net (thms @ @{thms forms} @ @{thms elements})) + in REPEAT_FIRST (ASSUME ctxt tac) end +\ -end +method_setup form = \Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))\ +method_setup intro = \Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intro_tac ctxt ths))\ +method_setup typecheck = \Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typecheck_tac ctxt ths))\ end \ No newline at end of file diff --git a/Prod.thy b/Prod.thy index 162b2e6..18582a8 100644 --- a/Prod.thy +++ b/Prod.thy @@ -59,8 +59,7 @@ This is what the additional formation rules \Prod_form_cond1\ and \ text "The type rules should be able to be used as introduction and elimination rules by the standard reasoner:" lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq -lemmas Prod_form_conds [elim] = Prod_form_cond1 Prod_form_cond2 -lemmas Prod_simps [simp] = Prod_comp Prod_uniq +lemmas Prod_form_conds [elim, wellform] = Prod_form_cond1 Prod_form_cond2 text "Nondependent functions are a special case." diff --git a/Proj.thy b/Proj.thy index c4703d7..fe80c4c 100644 --- a/Proj.thy +++ b/Proj.thy @@ -49,16 +49,7 @@ text "Typing judgments and computation rules for the dependent and non-dependent lemma fst_dep_type: assumes "p : \x:A. B x" shows "fst[A,B]`p : A" - -proof - show "fst[A,B]: (\x:A. B x) \ A" - proof (unfold fst_dep_def, standard) - show "\p. p : \x:A. B x \ indSum[A,B] (\_. A) (\x y. x) p : A" - proof - show "A : U" by (wellformed jdgmt: assms) - qed - qed (wellformed jdgmt: assms) -qed (rule assms) + by (derive lems: fst_dep_def assms) lemma fst_dep_comp: @@ -67,18 +58,10 @@ lemma fst_dep_comp: proof - have "fst[A,B]`(a,b) \ indSum[A,B] (\_. A) (\x y. x) (a,b)" - proof (unfold fst_dep_def, standard) - show "(a,b) : \x:A. B x" using assms .. - show "\p. p : \x:A. B x \ indSum[A,B] (\_. A) (\x y. x) p : A" - proof - show "A : U" by (wellformed jdgmt: assms(2)) - qed - qed + by (derive lems: fst_dep_def assms) also have "indSum[A,B] (\_. A) (\x y. x) (a,b) \ a" - proof - show "A : U" by (wellformed jdgmt: assms(2)) - qed (assumption, (rule assms)+) + by (derive lems: assms) finally show "fst[A,B]`(a,b) \ a" . qed @@ -89,12 +72,8 @@ text "In proving results about the second dependent projection function we often lemma lemma1: assumes "p : \x:A. B x" shows "B (fst[A,B]`p) : U" + by (derive lems: assms fst_dep_def) -proof - - have *: "B: A \ U" by (wellformed jdgmt: assms) - have "fst[A,B]`p : A" using assms by (rule fst_dep_type) - then show "B (fst[A,B]`p) : U" by (rule *) -qed lemma lemma2: assumes "B: A \ U" and "x : A" and "y : B x" @@ -110,7 +89,7 @@ lemma snd_dep_type: assumes "p : \x:A. B x" shows "snd[A,B]`p : B (fst[A,B]`p)" -proof +proof (derive lems: assms snd_dep_def) show "snd[A, B] : \p:(\x:A. B x). B (fst[A,B]`p)" proof (unfold snd_dep_def, standard) show "\p. p : \x:A. B x \ indSum[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p : B (fst[A,B]`p)" @@ -216,7 +195,7 @@ lemma snd_nondep_comp: proof - have "snd[A,B]`(a,b) \ indSum[A, \_. B] (\_. B) (\x y. y) (a,b)" proof (unfold snd_nondep_def, standard) - show "(a,b) : A \ B" using assms .. + show "(a,b) : A \ B" by (simple conds: assms) show "\p. p : A \ B \ indSum[A, \_. B] (\_. B) (\x y. y) p : B" proof show "B : U" by (wellformed jdgmt: assms(2)) diff --git a/Sum.thy b/Sum.thy index 8f40b74..7e688a2 100644 --- a/Sum.thy +++ b/Sum.thy @@ -51,7 +51,7 @@ and \ \ indSum[A,B] C f (a,b) \ f a b" lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp -lemmas Sum_form_conds [elim] = Sum_form_cond1 Sum_form_cond2 +lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2 \ \Nondependent pair\ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) -- cgit v1.2.3