From f83534561085c224ab30343b945ee74d1ce547f4 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 14 Aug 2018 15:08:37 +0200 Subject: Equality inverse and composition done. Cleaned up methods and method example theory. --- EqualProps.thy | 192 +++++++++++++++++++++++++++++++++++++++++++------------ HoTT_Methods.thy | 67 ++++++++----------- Nat.thy | 2 +- Proj.thy | 32 ++++------ ex/Methods.thy | 43 +++++++------ 5 files changed, 215 insertions(+), 121 deletions(-) diff --git a/EqualProps.thy b/EqualProps.thy index d645fb6..3d99456 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -1,6 +1,6 @@ (* Title: HoTT/EqualProps.thy Author: Josh Chen - Date: Jun 2018 + Date: Aug 2018 Properties of equality. *) @@ -18,22 +18,28 @@ section \Symmetry / Path inverse\ axiomatization inv :: "Term \ Term" ("_\" [1000] 1000) where inv_def: "inv \ \p. ind\<^sub>= (\x. refl(x)) p" +text " + In the proof below we begin by using path induction on \p\ with the application of \rule Equal_elim\, telling Isabelle the specific substitutions to use. + The proof is finished with a standard application of the relevant type rules. +" 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 -proof (rule Equal_elim[where ?x=x and ?y=y]) \ \Path induction\ - show "\x y. \x: A; y: A\ \ y =\<^sub>A x: U(i)" using assms(1) .. - show "\x. x: A \ refl x: x =\<^sub>A x" .. -qed (fact assms)+ +by (rule Equal_elim[where ?x=x and ?y=y]) (simple lem: assms) + \ \The type doesn't depend on \p\ so we don't need to specify \?p\ in the \where\ clause above.\ +text " + The next proof requires explicitly telling Isabelle what to substitute on the RHS of the typing judgment after the initial application of the type rules. + (If viewing this inside Isabelle, place the cursor after the \proof\ statement and observe the second subgoal.) +" -lemma inv_comp: assumes "A : U(i)" and "a : A" shows "(refl a)\ \ refl(a)" +lemma inv_comp: + assumes "A : U(i)" and "a : A" shows "(refl a)\ \ refl(a)" unfolding inv_def proof show "\x. x: A \ refl x: x =\<^sub>A x" .. - show "\x. x: A \ x =\<^sub>A x: U(i)" using assms(1) .. -qed (fact assms) +qed (simple lem: assms) section \Transitivity / Path composition\ @@ -45,67 +51,173 @@ text " axiomatization rcompose :: Term where rcompose_def: "rcompose \ \<^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 rcompose_type: assumes "A: U(i)" shows "rcompose: \x:A. \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" unfolding rcompose_def proof - show "\x. x: A \ - \<^bold>\y p. ind\<^sub>= (\_. \<^bold>\z p. ind\<^sub>= refl p) p: \y:A. x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" + 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)" proof - show "\x y. \x: A ; y: A\ \ - \<^bold>\p. ind\<^sub>= (\_. \<^bold>\z p. ind\<^sub>= refl p) p: x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" + fix y assume 2: "y: A" + show "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" proof - { fix x y p assume asm: "x: A" "y: A" "p: x =\<^sub>A y" - show "ind\<^sub>= (\_. \<^bold>\z p. ind\<^sub>= refl p) p: \z:A. y =[A] z \ x =[A] z" + fix p assume 3: "p: x =\<^sub>A y" + show "ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \z:A. y =\<^sub>A z \ x =\<^sub>A z" proof (rule Equal_elim[where ?x=x and ?y=y]) - show "\x y. \x: A; y: A\ \ \z:A. y =\<^sub>A z \ x =\<^sub>A z: U(i)" + show "\u. u: A \ \<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A z \ u =\<^sub>A z" proof - show "\x y z. \x: A; y: A; z: A\ \ y =\<^sub>A z \ x =\<^sub>A z: U(i)" - by (rule Prod_form Equal_form assms | assumption)+ - qed (rule assms) - - show "\x. x: A \ \<^bold>\z p. ind\<^sub>= refl p: \z:A. x =\<^sub>A z \ x =\<^sub>A z" - proof - show "\x z. \x: A; z: A\ \ \<^bold>\p. ind\<^sub>= refl p: x =\<^sub>A z \ x =\<^sub>A z" + show "\u z. \u: A; z: A\ \ \<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" proof - { fix x z p assume asm: "x: A" "z: A" "p: x =\<^sub>A z" - show "ind\<^sub>= refl p: x =[A] z" - proof (rule Equal_elim[where ?x=x and ?y=z]) - show "\x y. \x: A; y: A\ \ x =\<^sub>A y: U(i)" by standard (rule assms) - show "\x. x: A \ refl x: x =\<^sub>A x" .. - qed (fact asm)+ } - show "\x z. \x: A; z: A\ \ x =\<^sub>A z: U(i)" by standard (rule assms) - qed + 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 lem: assms asm) + qed (simple lem: assms) qed (rule assms) - qed (rule asm)+ } - show "\x y. \x: A; y: A\ \ x =\<^sub>A y: U(i)" by standard (rule assms) - qed + qed (simple lem: assms 1 2 3) + qed (simple lem: assms 1 2) qed (rule assms) -qed (fact 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 "rcompose`x`y`p`z`q: x =\<^sub>A z" - by standard+ (rule rcompose_type assms)+ + by (simple lem: assms rcompose_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 rcompose_comp: + assumes "A: U(i)" and "a: A" + shows "rcompose`a`a`refl(a)`a`refl(a) \ refl(a)" +unfolding rcompose_def +proof (subst comp) + { 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)" + proof + fix y assume 2: "y: A" + show "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: x =\<^sub>A y \ (\z:A. y =\<^sub>A z \ x =\<^sub>A z)" + proof + fix p assume 3: "p: x =\<^sub>A y" + show "ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \z:A. y =\<^sub>A z \ x =\<^sub>A z" + proof (rule Equal_elim[where ?x=x and ?y=y]) + show "\u. u: A \ \<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A z \ u =\<^sub>A z" + proof + show "\u z. \u: A; z: A\ \ \<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A z \ u =\<^sub>A z" + 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 lem: assms asm) + qed (simple lem: assms) + qed (rule assms) + qed (simple lem: assms 1 2 3) + qed (simple lem: 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)" + proof (subst comp) + { fix y assume 1: "y: A" + show "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: a =\<^sub>A y \ (\z:A. y =\<^sub>A z \ a =\<^sub>A z)" + proof + fix p assume 2: "p: a =\<^sub>A y" + show "ind\<^sub>= (\_. \<^bold>\z q. ind\<^sub>= refl q) p: \z:A. y =\<^sub>A z \ a =\<^sub>A z" + proof (rule Equal_elim[where ?x=a and ?y=y]) + fix u assume 3: "u: A" + show "\<^bold>\z q. ind\<^sub>= refl q: \z:A. u =[A] z \ u =[A] z" + proof + fix z assume 4: "z: A" + 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 lem: assms 3 4) + qed (simple lem: assms 3 4) + qed fact + qed (simple lem: assms 1 2) + qed (simple lem: assms 1) } + + show "(\<^bold>\p. ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p)`refl(a)`a`refl(a) \ refl(a)" + proof (subst comp) + { fix p assume 1: "p: a =\<^sub>A a" + show "ind\<^sub>= (\_. \<^bold>\z. \<^bold>\q. ind\<^sub>= refl q) p: \z:A. a =\<^sub>A a \ a =\<^sub>A z" + proof (rule Equal_elim[where ?x=a and ?y=a]) + fix u assume 2: "u: A" + show "\<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A u\ u =\<^sub>A z" + proof + fix z assume 3: "z: A" + show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A u \ u =\<^sub>A z" + proof + show "\q. q: u =\<^sub>A u \ ind\<^sub>= refl q: u =\<^sub>A z" + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 2 3) + qed (simple lem: assms 2) + qed fact + qed (simple lem: assms 1) } + + show "(ind\<^sub>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \ refl(a)" + proof (subst comp) + { fix u assume 1: "u: A" + show "\<^bold>\z q. ind\<^sub>= refl q: \z:A. u =\<^sub>A u\ u =\<^sub>A z" + proof + fix z assume 2: "z: A" + show "\<^bold>\q. ind\<^sub>= refl q: u =\<^sub>A u \ u =\<^sub>A z" + proof + show "\q. q: u =\<^sub>A u \ ind\<^sub>= refl q: u =\<^sub>A z" + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lem: assms 1 2) + qed (simple lem: assms 1) + qed fact } + + show "(\<^bold>\z q. ind\<^sub>= refl q)`a`refl(a) \ refl(a)" + proof (subst comp) + { fix a assume 1: "a: A" + 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 lem: assms 1) + qed (simple lem: assms 1) } + + show "(\<^bold>\q. ind\<^sub>= refl q)`refl(a) \ refl(a)" + proof (subst comp) + 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 lem: assms) + show "ind\<^sub>= refl (refl(a)) \ refl(a)" + proof + show "\x. x: A \ refl(x): x =\<^sub>A x" .. + qed (simple lem: assms) + qed (simple lem: assms) + qed fact + qed (simple lem: assms) + qed (simple lem: assms) + qed fact +qed fact + + +text "The raw object lambda term is cumbersome to use, so we define a simpler constant instead." axiomatization compose :: "[Term, Term] \ Term" (infixl "\" 60) where - compose_comp: "\ + compose_def: "\ A: U(i); x: A; y: A; z: A; p: x =\<^sub>A y; q: y =\<^sub>A z \ \ p \ q \ rcompose`x`y`p`z`q" +lemma compose_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 compose_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 lem: assms rcompose_type) + lemma compose_comp: - assumes "A : U(i)" and "a : A" shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" - unfolding rcompose_def - by (simplify lems: assms) + assumes "A : U(i)" and "a : A" shows "refl(a) \ refl(a) \ refl(a)" +by (subst compose_def) (simple lem: assms rcompose_comp) -lemmas EqualProps_rules [intro] = inv_type inv_comp compose_type compose_comp +lemmas EqualProps_rules [intro] = inv_type compose_type lemmas EqualProps_comps [comp] = inv_comp compose_comp diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index f80b99b..e2eb4f1 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -13,69 +13,52 @@ theory HoTT_Methods begin -section \Setup\ - -text "Import the \subst\ method, used by \simplify\." - -ML_file "~~/src/Tools/misc_legacy.ML" -ML_file "~~/src/Tools/IsaPlanner/isand.ML" -ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" -ML_file "~~/src/Tools/IsaPlanner/zipper.ML" -ML_file "~~/src/Tools/eqsubst.ML" - - section \Method definitions\ subsection \Simple type rule proof search\ -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." +text " + Prove type judgments \A : U\ and inhabitation judgments \a : A\ using the type rules declared [intro] and [elim] (in the respective theory files), as well as additional provided lemmas. + + Can also perform typechecking, and search for elements of a type. +" -method simple uses lems = (assumption | rule lems | standard)+ +method simple uses lem = (assumption | rule lem | standard)+ subsection \Wellformedness checker\ -text "Find a proof of any valid typing judgment derivable from a given wellformed judgment. -The named theorem \wellform\ is declared in HoTT_Base.thy." +text " + \wellformed\ finds a proof of any valid typing judgment derivable from the judgments passed as \lem\. + The named theorem \wellform\ is declared in HoTT_Base.thy. +" -method wellformed uses jdgmt declares wellform = +method wellformed' uses jmt declares wellform = match wellform in rl: "PROP ?P" \ \( - catch \rule rl[OF jdgmt]\ \fail\ | - catch \wellformed jdgmt: rl[OF jdgmt]\ \fail\ + catch \rule rl[OF jmt]\ \fail\ | + catch \wellformed' jmt: rl[OF jmt]\ \fail\ )\ +method wellformed uses lem = + match lem in lem: "?X : ?Y" \ \wellformed' jmt: lem\ -subsection \Derivation search\ - -text "Combine \simple\, \wellformed\ and the universe hierarchy rules to search for derivations of judgments. -\wellformed\ uses the facts passed as \lems\ to derive any required typing judgments. -Definitions passed as \unfolds\ are unfolded throughout." - -method derive uses lems unfolds = ( - unfold unfolds | - simple lems: lems | - match lems in lem: "?X : ?Y" \ \wellformed jdgmt: lem\ | - rule U_hierarchy (*| - (rule U_cumulative, simple lems: lems) | - (rule U_cumulative, match lems in lem: "?X : ?Y" \ \wellformed jdgmt: lem\)*) - )+ +subsection \Derivation search\ -subsection \Simplification\ +text " Combine \simple\ and \wellformed\ to search for derivations of judgments." -text "The methods \rsimplify\ and \simplify\ search for lambda applications to simplify and are suitable for solving definitional equalities, as well as harder proofs where \derive\ fails. +method derive uses lem = (simple lem: lem | wellformed lem: lem)+ -It is however not true that these methods are strictly stronger; if they fail to find a suitable substitution they will fail where \derive\ may succeed. -\simplify\ is allowed to use the Pure Simplifier and is hence unsuitable for simplifying lambda expressions using only the type rules. -In this case use \rsimplify\ instead." +subsection \Substitution and simplification\ -method rsimplify uses lems = (subst (0) comp, derive lems: lems)+ - \ \\subst\ performs an equational rewrite according to some computation rule declared as [comp], after which \derive\ attempts to solve any new assumptions that arise.\ +text "Import the \subst\ method, used for substituting definitional equalities." -method simplify uses lems = (simp add: lems | rsimplify lems: lems)+ +ML_file "~~/src/Tools/misc_legacy.ML" +ML_file "~~/src/Tools/IsaPlanner/isand.ML" +ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML" +ML_file "~~/src/Tools/IsaPlanner/zipper.ML" +ML_file "~~/src/Tools/eqsubst.ML" end \ No newline at end of file diff --git a/Nat.thy b/Nat.thy index eed9226..388df0f 100644 --- a/Nat.thy +++ b/Nat.thy @@ -42,8 +42,8 @@ and n: \ \ \ ind\<^sub>\(f)(a)(succ n) \ f(n)(ind\<^sub>\ f a n)" -lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2 lemmas Nat_intro = Nat_intro1 Nat_intro2 +lemmas Nat_rules [intro] = Nat_form Nat_intro Nat_elim Nat_comp1 Nat_comp2 lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2 diff --git a/Proj.thy b/Proj.thy index e90cd95..aa7e8ec 100644 --- a/Proj.thy +++ b/Proj.thy @@ -21,17 +21,14 @@ text "Typing judgments and computation rules for the dependent and non-dependent lemma fst_type: assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "fst(p): A" -unfolding fst_def -proof - show "A: U(i)" using assms(1) by (rule Sum_wellform) -qed (fact assms | assumption)+ +unfolding fst_def by (derive lem: 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 - show "\x. x: A \ x: A" . + show "a: A" and "b: B(a)" by fact+ qed (rule assms)+ @@ -39,20 +36,16 @@ lemma snd_type: assumes "\x:A. B(x): U(i)" and "p: \x:A. B(x)" shows "snd(p): B(fst p)" unfolding snd_def proof - show "\p. p: \x:A. B(x) \ B(fst p): U(i)" - proof - - have "\p. p: \x:A. B(x) \ fst(p): A" using assms(1) by (rule fst_type) - with assms(1) show "\p. p: \x:A. B(x) \ B(fst p): U(i)" by (rule Sum_wellform) - qed - + show "\p. p: \x:A. B(x) \ B(fst p): U(i)" by (derive lem: assms fst_type) + fix x y assume asm: "x: A" "y: B(x)" show "y: B(fst )" proof (subst fst_comp) - show "A: U(i)" using assms(1) by (rule Sum_wellform) - show "\x. x: A \ B(x): U(i)" using assms(1) by (rule Sum_wellform) - qed (rule asm)+ -qed (fact assms) + show "A: U(i)" by (wellformed lem: assms(1)) + show "\x. x: A \ B(x): U(i)" by (wellformed lem: assms(1)) + qed fact+ +qed fact lemma snd_comp: @@ -60,13 +53,12 @@ lemma snd_comp: unfolding snd_def proof show "\x y. y: B(x) \ y: B(x)" . - show "a: A" by (fact assms) - show "b: B(a)" by (fact assms) - show *: "B(a): U(i)" using assms(3) by (rule assms(2)) - show "B(a): U(i)" by (fact *) -qed + show "a: A" by fact + show "b: B(a)" by fact +qed (simple lem: assms) +lemmas Proj_types [intro] = fst_type snd_type lemmas Proj_comps [intro] = fst_comp snd_comp diff --git a/ex/Methods.thy b/ex/Methods.thy index d174dde..b0c5f92 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -1,6 +1,6 @@ (* Title: HoTT/ex/Methods.thy Author: Josh Chen - Date: Jul 2018 + Date: Aug 2018 HoTT method usage examples *) @@ -9,33 +9,40 @@ 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) + 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 lem: assms) lemma - assumes "f : \x:A. \y: B x. \z: C x y. D x y z" + assumes "\x:A. \y: B x. \z: C x y. D x y z: U(i)" 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" + "A : U(i)" and + "B: A \ U(i)" and + "\x. x : A \ C x: B x \ U(i)" and + "\x y. \x : A; y : B x\ \ D x y: C x y \ U(i)" 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) + show + "A : U(i)" and + "B: A \ U(i)" and + "\x. x : A \ C x: B x \ U(i)" and + "\x y. \x : A; y : B x\ \ D x y: C x y \ U(i)" + by (derive lem: assms) qed -text "Typechecking:" +text "Typechecking and constructing inhabitants:" \ \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 +schematic_goal "\A: U(i); B: U(i); a : A; b : B\ \ : ?A" +by simple + +\ \Finds pair (too easy).\ +schematic_goal "\A: U(i); B: U(i); a : A; b : B\ \ ?x : A \ B" +apply (rule Sum_intro) +apply assumption+ +done end \ No newline at end of file -- cgit v1.2.3