From 0036345412d5c145b63693ed672b175018fa3791 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 22 Feb 2019 19:43:53 +0100 Subject: Proof of pathcomp associativity done. Some comments --- Eq.thy | 229 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ HoTT_Methods.thy | 41 +++++----- HoTT_Typing.thy | 2 +- 3 files changed, 249 insertions(+), 23 deletions(-) create mode 100644 Eq.thy diff --git a/Eq.thy b/Eq.thy new file mode 100644 index 0000000..e93dd8a --- /dev/null +++ b/Eq.thy @@ -0,0 +1,229 @@ +(******** +Isabelle/HoTT: Equality +Feb 2019 + +********) + +theory Eq +imports Prod HoTT_Methods + +begin + + +section \Type definitions\ + +axiomatization + Eq :: "[t, t, t] \ t" and + refl :: "t \ t" and + indEq :: "[[t, t, t] \ t, t \ t, t, t, t] \ t" + +syntax + "_Eq" :: "[t, t, t] \ t" ("(3_ =[_]/ _)" [101, 0, 101] 100) +translations + "a =[A] b" \ "(CONST Eq) A a b" + +axiomatization where + Eq_form: "\A: U i; a: A; b: A\ \ a =[A] b: U i" and + + Eq_intro: "a: A \ (refl a): a =[A] a" and + + Eq_elim: "\ + p: a =[A] b; + a: A; + b: A; + \x. x: A \ f x: C x x (refl x); + \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f a b p: C a b p" and + + Eq_comp: "\ + a: A; + \x. x: A \ f x: C x x (refl x); + \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f a a (refl a) \ f a" + +lemmas Eq_form [form] +lemmas Eq_routine [intro] = Eq_form Eq_intro Eq_elim +lemmas Eq_comp [comp] + + +section \Path induction\ + +text \We set up rudimentary automation of path induction:\ + +method path_ind for a b p :: t = + (rule Eq_elim[where ?a=a and ?b=b and ?p=p]; (assumption | fact)?) + +method path_ind' for C :: "[t, t, t] \ t" = + (rule Eq_elim[where ?C=C]; (assumption | fact)?) + + +section \Properties of equality\ + +subsection \Symmetry (path inverse)\ + +definition inv :: "[t, t, t, t] \ t" +where "inv A x y p \ indEq (\x y. ^(y =[A] x)) (\x. refl x) x y p" + +syntax "_inv" :: "t \ t" ("~_" [1000]) + +text \Pretty-printing switch for path inverse:\ + +ML \val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\ + +print_translation \ +let fun inv_tr' ctxt [A, x, y, p] = + if Config.get ctxt pretty_inv + then Syntax.const @{syntax_const "_inv"} $ p + else @{const inv} $ A $ x $ y $ p +in + [(@{const_syntax inv}, inv_tr')] +end +\ + +lemma inv_type: "\A: U i; x: A; y: A; p: x =[A] y\ \ inv A x y p: y =[A] x" +unfolding inv_def by derive + +lemma inv_comp: "\A: U i; a: A\ \ inv A a a (refl a) \ refl a" +unfolding inv_def by derive + +declare + inv_type [intro] + inv_comp [comp] + +subsection \Transitivity (path composition)\ + +schematic_goal transitivity: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?p: \z: A. y =[A]z \ x =[A] z" +proof (path_ind x y p, quantify_all) + fix x z show "\p. p: x =[A] z \ p: x =[A] z" . +qed (routine add: assms) + +definition pathcomp :: "[t, t, t, t, t, t] \ t" +where + "pathcomp A x y z p q \ + (indEq (\x y _. \z: A. y =[A] z \ x =[A] z) (\x. \y: A. id (x =[A] y)) x y p)`z`q" + +syntax "_pathcomp" :: "[t, t] \ t" (infixl "*" 110) + +text \Pretty-printing switch for path composition:\ + +ML \val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\ + +print_translation \ +let fun pathcomp_tr' ctxt [A, x, y, z, p, q] = + if Config.get ctxt pretty_pathcomp + then Syntax.const @{syntax_const "_pathcomp"} $ p $ q + else @{const pathcomp} $ A $ x $ y $ z $ p $ q +in + [(@{const_syntax pathcomp}, pathcomp_tr')] +end +\ + +lemma pathcomp_type: + assumes "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z" + shows "pathcomp A x y z p q: x =[A] z" +unfolding pathcomp_def by (routine add: transitivity assms) + +lemma pathcomp_cmp: + assumes "A: U i" and "a: A" + shows "pathcomp A a a a (refl a) (refl a) \ refl a" +unfolding pathcomp_def by (derive lems: assms) + +lemmas pathcomp_type [intro] +lemmas pathcomp_comp [comp] = pathcomp_cmp + + +section \Higher groupoid structure of types\ + +schematic_goal pathcomp_idr: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: pathcomp A x y y p (refl y) =[x =[A] y] p" +proof (path_ind x y p) + show "\x. x: A \ refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +schematic_goal pathcomp_idl: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: pathcomp A x x y (refl x) p =[x =[A] y] p" +proof (path_ind x y p) + show "\x. x: A \ refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +schematic_goal pathcomp_invr: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)" +proof (path_ind x y p) + show + "\x. x: A \ refl(refl x): + pathcomp A x x x (refl x) (inv A x x (refl x)) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +schematic_goal pathcomp_invl: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)" +proof (path_ind x y p) + show + "\x. x: A \ refl(refl x): + pathcomp A x x x (inv A x x (refl x)) (refl x) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +schematic_goal inv_involutive: + assumes "A: U i" "x: A" "y: A" "p: x =[A] y" + shows "?a: inv A y x (inv A x y p) =[x =[A] y] p" +proof (path_ind x y p) + show "\x. x: A \ refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)" + by (derive lems: assms) +qed (routine add: assms) + +text \ +We use the proof of associativity of path composition to demonstrate the process of deriving proof terms. +The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the form of the proof term in the first place. +However, using proof scripts the derivation becomes quite easy; we simply give the correct form of the statements to induct over, and prove the simple subgoals returned by the prover. +\ + +declare[[pretty_pathcomp=false]] + +schematic_goal pathcomp_assoc: + assumes "A: U i" + shows + "?a: \x: A. \y: A. \p: x =[A] y. \z: A. \q: y =[A] z. \w: A. \r: z =[A] w. + pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w] + pathcomp A x z w (pathcomp A x y z p q) r" + apply (quantify 3) + apply (path_ind' + "\x y p. \(z: A). \(q: y =[A] z). \(w: A). \(r: z =[A] w). + Eq.pathcomp A x y w p (Eq.pathcomp A y z w q r) =[x =[A] w] + Eq.pathcomp A x z w (Eq.pathcomp A x y z p q) r") + apply (quantify 2) + apply (path_ind' + "\xa z q. \(w: A). \(r: z =[A] w). + Eq.pathcomp A xa xa w (refl xa) (Eq.pathcomp A xa z w q r) =[xa =[A] w] + Eq.pathcomp A xa z w (Eq.pathcomp A xa xa z (refl xa) q) r") + apply (quantify 2) + apply (path_ind' + "\xb w r. Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w] + Eq.pathcomp A xb xb w (Eq.pathcomp A xb xb xb (refl xb) (refl xb)) r") + + text \\ + + apply (derive; (rule assms|assumption)?) + apply (compute, rule assms, assumption)+ + apply (elim Eq_intro, rule Eq_intro, assumption) + apply (compute, rule assms, assumption)+ + apply (elim Eq_intro) + apply (compute, rule assms, assumption)+ + apply (rule Eq_intro, elim Eq_intro) + apply (compute, rule assms, assumption)+ + apply (rule Eq_intro, elim Eq_intro) + apply (derive lems: assms) +done + +(* Possible todo: + implement a custom version of schematic_goal/theorem that exports the derived proof term. +*) + + +end diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index d93680a..099a73e 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -12,25 +12,6 @@ imports HoTT_Base "HOL-Eisbach.Eisbach" "HOL-Eisbach.Eisbach_Tools" begin -section \More method combinators\ - -ML \ -(* Use as "repeat n tac" *) -fun repeat tac = - let - fun cparser_of parser (ctxt, toks) = parser toks ||> (fn toks => (ctxt, toks)) - in - cparser_of Args.text >> - (fn n => fn ctxt => fn facts => - SIMPLE_METHOD ( - REPEAT_DETERM_N - (the (Int.fromString n)) - (tac ctxt)) - facts) - end -\ - - section \Substitution and simplification\ ML_file "~~/src/Tools/misc_legacy.ML" @@ -52,11 +33,9 @@ section \Handling universes\ text \ Methods @{theory_text provelt}, @{theory_text hierarchy}, and @{theory_text cumulativity} prove propositions of the form - \<^item> \n < (Suc (... (Suc n) ...))\, \<^item> \U i: U (Suc (... (Suc i) ...))\, and \<^item> @{prop "A: U i \ A: U j"}, where @{prop "i \ j"}, - respectively. \ @@ -72,7 +51,7 @@ method cumulativity declares form = ( section \Deriving typing judgments\ -method routine uses add = (assumption | rule add | rule)+ +method routine uses add = (rule add | assumption | rule)+ text \ The method @{method routine} proves typing judgments @{prop "a: A"} using the rules declared @{attribute intro} in the respective theory files, as well as any additional lemmas provided with the modifier @{theory_text add}. @@ -88,4 +67,22 @@ It also handles universes using @{method hierarchy} and @{method cumulativity}. method derive uses lems = (routine add: lems | compute comp: lems | cumulativity form: lems | hierarchy)+ + +section \Additional method combinators\ + +text \ +The ML expression @{ML_text "repeat tac"} below yields a @{ML_type "(Proof.context -> Proof.method) context_parser"}, which may be passed to @{command method_setup} to set up a method that scans for an integer n and executes the tactic returned by @{ML_text tac} n times. +See the setup of method @{text quantify} in @{file Prod.thy} for an example. +\ + +ML \ +fun repeat (tac: Proof.context -> tactic) = + let + fun cparser_of parser (ctxt, toks) = parser toks ||> (fn toks => (ctxt, toks)) + in + cparser_of Args.text >> (fn n => fn ctxt => fn facts => + SIMPLE_METHOD (REPEAT_DETERM_N (the (Int.fromString n))(tac ctxt)) facts) + end +\ + end diff --git a/HoTT_Typing.thy b/HoTT_Typing.thy index 6433139..ec7456e 100644 --- a/HoTT_Typing.thy +++ b/HoTT_Typing.thy @@ -27,7 +27,7 @@ section \Terms and typing\ typedecl t \ \Type of object-logic terms (which includes the types)\ -judgment has_type :: "[t, t] \ prop" ("(3_:/ _)") +judgment has_type :: "[t, t] \ prop" ("(3_ :/ _)") section \Typing functionality\ -- cgit v1.2.3