From 7823d59b2d9436f1bf0042fff62ee2bcc4c29ec0 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 3 Jul 2018 18:57:57 +0200 Subject: Refactor HoTT_Methods.thy, proved more stuff with new methods. --- Equal.thy | 2 +- EqualProps.thy | 50 +++++++++++++------------- HoTT.thy | 17 ++++++--- HoTT_Base.thy | 4 ++- HoTT_Methods.thy | 92 ++++++++---------------------------------------- Proj.thy | 104 ++++++++++++++++--------------------------------------- Sum.thy | 8 ++--- ex/Methods.thy | 41 ++++++++++++++++++++++ scratch.thy | 20 ++--------- 9 files changed, 133 insertions(+), 205 deletions(-) create mode 100644 ex/Methods.thy diff --git a/Equal.thy b/Equal.thy index f0ced68..51a69ae 100644 --- a/Equal.thy +++ b/Equal.thy @@ -53,7 +53,7 @@ and \ \ indEqual[A] C f a a refl(a) \ f a" lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -lemmas Equal_form_conds [elim] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 +lemmas Equal_form_conds [elim, wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 end \ No newline at end of file diff --git a/EqualProps.thy b/EqualProps.thy index 10d3b17..8960a90 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -22,18 +22,7 @@ definition inv :: "[Term, Term, Term] \ Term" ("(1inv[_,/ _,/ _])") lemma inv_type: assumes "p : x =\<^sub>A y" shows "inv[A,x,y]`p : y =\<^sub>A x" - -proof - show "inv[A,x,y] : (x =\<^sub>A y) \ (y =\<^sub>A x)" - proof (unfold inv_def, standard) - fix p assume asm: "p : x =\<^sub>A y" - show "indEqual[A] (\x y _. y =[A] x) refl x y p : y =\<^sub>A x" - proof standard+ - show "x : A" by (wellformed jdgmt: asm) - show "y : A" by (wellformed jdgmt: asm) - qed (assumption | rule | rule asm)+ - qed (wellformed jdgmt: assms) -qed (rule assms) + by (derive lems: assms unfolds: inv_def) lemma inv_comp: @@ -42,19 +31,10 @@ lemma inv_comp: proof - have "inv[A,a,a]`refl(a) \ indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a)" - proof (unfold inv_def, standard) - show "refl(a) : a =\<^sub>A a" using assms .. - - fix p assume asm: "p : a =\<^sub>A a" - show "indEqual[A] (\x y _. y =\<^sub>A x) refl a a p : a =\<^sub>A a" - proof standard+ - show "a : A" by (wellformed jdgmt: asm) - then show "a : A" . \ \The elimination rule requires that both arguments to \indEqual\ be shown to have the correct type.\ - qed (assumption | rule | rule asm)+ - qed + by (derive lems: assms unfolds: inv_def) also have "indEqual[A] (\x y _. y =\<^sub>A x) (\x. refl(x)) a a refl(a) \ refl(a)" - by (standard | assumption | rule assms)+ + by (simple lems: assms) finally show "inv[A,a,a]`refl(a) \ refl(a)" . qed @@ -79,14 +59,34 @@ abbreviation compose :: "[Term, Term, Term, Term] \ Term" ("(1compo 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 + by (derive lems: assms unfolds: rcompose_def) lemma compose_comp: assumes "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" +proof (unfold rcompose_def) + show "(\<^bold>\p:a =[A] a. + lambda (a =[A] a) + (op ` + ((\<^bold>\x:A. + \<^bold>\y:A. + lambda (x =[A] y) + (indEqual[A] + (\x y _. \z:A. y =[A] z \ x =[A] z) + (\x. \<^bold>\z:A. + lambda (x =[A] z) + (indEqual[A] (\x z _. x =[A] z) refl x z)) + x y)) ` + a ` + a ` + p ` + a))) ` + refl(a) ` + refl(a) \ + refl(a)" + sorry \ \Long and tedious proof if the Simplifier is not set up.\ diff --git a/HoTT.thy b/HoTT.thy index b500150..42796c1 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -7,10 +7,19 @@ Load all the component modules for the HoTT logic. theory HoTT imports - HoTT_Base - HoTT_Methods - Prod - Sum + +(* Basic theories *) +HoTT_Base +HoTT_Methods + +(* Types *) +Equal +Prod +Sum + +(* Additional properties *) +EqualProps +Proj begin end diff --git a/HoTT_Base.thy b/HoTT_Base.thy index e5c0776..eaebfb0 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -9,12 +9,14 @@ theory HoTT_Base imports Pure begin + section \Setup\ -text "Declare rules expressing necessary wellformedness conditions for type and inhabitation judgments." +text "Declare rules expressing necessary wellformedness conditions for type and inhabitation judgments, to be used by proof methods later (see HoTT_Methods.thy)." named_theorems wellform + section \Metalogical definitions\ text "A single meta-type \Term\ suffices to implement the object-logic types and terms. diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index bce5123..20f3ece 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -2,8 +2,7 @@ Author: Josh Chen Date: Jun 2018 -Method setup for the HoTT library. -Relies heavily on Eisbach. +Method setup for the HoTT library. Relies heavily on Eisbach. *) theory HoTT_Methods @@ -11,14 +10,14 @@ theory HoTT_Methods "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" HoTT_Base - Equal - Prod - Sum begin + section \Method setup\ -text "Prove type judgments \A : U\ and inhabitation judgments \a : A\ using rules declared [intro] and [elim], as well as additional provided lemmas." +text "Prove type judgments \A : U\ and inhabitation judgments \a : A\ using rules declared [intro] and [elim], as well as additional provided lemmas. + +Can also perform typechecking, and search for elements of a type." method simple uses lems = (assumption|standard|rule lems)+ @@ -33,83 +32,20 @@ method wellformed uses jdgmt = ( ) -text "Combine \simple\ and \wellformed\ to search for derivations." +text "Combine \simple\ and \wellformed\ to search for derivations. +\wellformed\ uses the facts passed as \lems\ to derive any required typing judgments. +Definitions passed as \unfolds\ are unfolded throughout. + +Roughly speaking \derive\ is more powerful than \simple\, but may fail to find a proof where \simple\ does if it reduces too eagerly." -method derive uses lems = ( - catch \unfold lems\ \fail\ | - catch \simple lems: lems\ \fail\ | +method derive uses lems unfolds = ( + unfold unfolds | + simple lems: lems | 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)); - -(* 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 - -(*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 -\ - -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))\ +text "Simplify function applications." end \ No newline at end of file diff --git a/Proj.thy b/Proj.thy index fe80c4c..7957669 100644 --- a/Proj.thy +++ b/Proj.thy @@ -49,7 +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" - by (derive lems: fst_dep_def assms) + by (derive lems: assms unfolds: fst_dep_def) lemma fst_dep_comp: @@ -58,7 +58,7 @@ lemma fst_dep_comp: proof - have "fst[A,B]`(a,b) \ indSum[A,B] (\_. A) (\x y. x) (a,b)" - by (derive lems: fst_dep_def assms) + by (derive lems: assms unfolds: fst_dep_def) also have "indSum[A,B] (\_. A) (\x y. x) (a,b) \ a" by (derive lems: assms) @@ -67,15 +67,9 @@ proof - qed -text "In proving results about the second dependent projection function we often use the following two lemmas." +text "In proving results about the second dependent projection function we often use the following lemma." -lemma lemma1: - assumes "p : \x:A. B x" - shows "B (fst[A,B]`p) : U" - by (derive lems: assms fst_dep_def) - - -lemma lemma2: +lemma lem: assumes "B: A \ U" and "x : A" and "y : B x" shows "y : B (fst[A,B]`(x,y))" @@ -89,18 +83,13 @@ lemma snd_dep_type: assumes "p : \x:A. B x" shows "snd[A,B]`p : B (fst[A,B]`p)" -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)" - proof (standard, elim lemma1) - fix p assume *: "p : \x:A. B x" - have **: "B: A \ U" by (wellformed jdgmt: *) - fix x y assume "x : A" and "y : B x" - with ** show "y : B (fst[A,B]`(x,y))" by (rule lemma2) - qed - qed (wellformed jdgmt: assms) -qed (rule assms) +proof (derive lems: assms unfolds: snd_dep_def) + show "fst[A, B] : (\x:A. B x) \ A" by (derive lems: assms unfolds: fst_dep_def) + + fix x y assume asm: "x : A" "y : B x" + have "B: A \ U" by (wellformed jdgmt: assms) + then show "y : B (fst[A, B]`(x,y))" using asm by (rule lem) +qed (assumption | rule assms)+ lemma snd_dep_comp: @@ -109,22 +98,20 @@ lemma snd_dep_comp: proof - have "snd[A,B]`(a,b) \ indSum[A, B] (\q. B (fst[A,B]`q)) (\x y. y) (a,b)" - proof (unfold snd_dep_def, standard) - show "(a,b) : \x:A. B x" using assms .. + proof (derive lems: assms unfolds: snd_dep_def) + show "fst[A, B] : (\x:A. B x) \ A" by (derive lems: assms unfolds: fst_dep_def) - fix p assume *: "p : \x:A. B x" - show "indSum[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p : B (fst[A,B]`p)" - proof (standard, elim lemma1) - fix x y assume "x : A" and "y : B x" - with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lemma2) - qed (rule *) - qed + fix x y assume asm: "x : A" "y : B x" + with assms(1) show "y : B (fst[A, B]`(x,y))" by (rule lem) + qed (assumption | derive lems: assms)+ also have "indSum[A, B] (\q. B (fst[A,B]`q)) (\x y. y) (a,b) \ b" - proof (standard, elim lemma1) + proof (simple lems: assms) + show "fst[A, B] : (\x:A. B x) \ A" by (derive lems: assms unfolds: fst_dep_def) + fix x y assume "x : A" and "y : B x" - with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lemma2) - qed (rule assms)+ + with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lem) + qed (assumption | rule assms)+ finally show "snd[A,B]`(a,b) \ b" . qed @@ -135,17 +122,7 @@ text "For non-dependent projection functions:" lemma fst_nondep_type: assumes "p : A \ B" shows "fst[A,B]`p : A" - -proof - show "fst[A,B] : A \ B \ A" - proof (unfold fst_nondep_def, standard) - fix q assume *: "q : A \ B" - show "indSum[A, \_. B] (\_. A) (\x y. x) q : A" - proof - show "A : U" by (wellformed jdgmt: assms) - qed (assumption, rule *) - qed (wellformed jdgmt: assms) -qed (rule assms) + by (derive lems: assms unfolds: fst_nondep_def) lemma fst_nondep_comp: @@ -154,18 +131,10 @@ lemma fst_nondep_comp: proof - have "fst[A,B]`(a,b) \ indSum[A, \_. B] (\_. A) (\x y. x) (a,b)" - proof (unfold fst_nondep_def, standard) - show "(a,b) : A \ B" using assms .. - show "\p. p : A \ B \ indSum[A, \_. B] (\_. A) (\x y. x) p : A" - proof - show "A : U" by (wellformed jdgmt: assms(1)) - qed - qed + by (derive lems: assms unfolds: fst_nondep_def) also have "indSum[A, \_. B] (\_. A) (\x y. x) (a,b) \ a" - proof - show "A : U" by (wellformed jdgmt: assms(1)) - qed (assumption, (rule assms)+) + by (derive lems: assms) finally show "fst[A,B]`(a,b) \ a" . qed @@ -177,15 +146,10 @@ lemma snd_nondep_type: proof show "snd[A,B] : A \ B \ B" - proof (unfold snd_nondep_def, standard) - fix q assume *: "q : A \ B" - show "indSum[A, \_. B] (\_. B) (\x y. y) q : B" - proof - have **: "\_. B: A \ U" by (wellformed jdgmt: assms) - have "fst[A,B]`p : A" using assms by (rule fst_nondep_type) - then show "B : U" by (rule **) - qed (assumption, rule *) - qed (wellformed jdgmt: assms) + proof (derive unfolds: snd_nondep_def) + fix q assume asm: "q : A \ B" + show "indSum[A, \_. B] (\_. B) (\x y. y) q : B" by (derive lems: asm) + qed (wellformed jdgmt: assms)+ qed (rule assms) @@ -194,18 +158,10 @@ lemma snd_nondep_comp: shows "snd[A,B]`(a,b) \ b" 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" 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)) - qed - qed + by (derive lems: assms unfolds: snd_nondep_def) also have "indSum[A, \_. B] (\_. B) (\x y. y) (a,b) \ b" - proof - show "B : U" by (wellformed jdgmt: assms(2)) - qed (assumption, (rule assms)+) + by (derive lems: assms) finally show "snd[A,B]`(a,b) \ b" . qed diff --git a/Sum.thy b/Sum.thy index 7e688a2..bf7b829 100644 --- a/Sum.thy +++ b/Sum.thy @@ -59,10 +59,10 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) lemma Pair_intro [intro]: "\A B a b. \a : A; b : B\ \ (a,b) : A \ B" -proof - fix b B assume "b : B" - then show "B : U" .. -qed + proof + fix b B assume "b : B" + then show "B : U" .. + qed end \ No newline at end of file diff --git a/ex/Methods.thy b/ex/Methods.thy new file mode 100644 index 0000000..d174dde --- /dev/null +++ b/ex/Methods.thy @@ -0,0 +1,41 @@ +(* Title: HoTT/ex/Methods.thy + Author: Josh Chen + Date: Jul 2018 + +HoTT method usage examples +*) + +theory Methods + imports "../HoTT" +begin + +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 + + +text "Typechecking:" + +\ \Correctly determines the type of the pair\ +schematic_goal "\a : A; b : B\ \ (a, b) : ?A" by simple + +\ \Finds element\ +schematic_goal "\a : A; b : B\ \ ?x : A \ B" by simple + +end \ No newline at end of file diff --git a/scratch.thy b/scratch.thy index 331b607..b90fd59 100644 --- a/scratch.thy +++ b/scratch.thy @@ -1,24 +1,8 @@ theory scratch - imports IFOL + imports HoTT begin -lemma disj_swap: "P \ Q \ Q \ P" -apply (erule disjE) (* Compare with the less useful \rule disjE\ *) - apply (rule disjI2) - apply assumption -apply (rule disjI1) -apply assumption -done - -lemma imp_uncurry: "P \ (Q \ R) \ P \ Q \ R" -apply (rule impI) -apply (erule conjE) -apply (drule mp) -apply assumption -apply (drule mp) -apply assumption -apply assumption -done +schematic_goal "\a : A; b : B\ \ ?x : A \ B" by simple end \ No newline at end of file -- cgit v1.2.3