From f4f468878fc0459a806b02cdf8921af6fcac2759 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 15 Aug 2018 11:47:30 +0200 Subject: Tweak proof methods, some type rules; add HoTT Book examples --- EqualProps.thy | 58 ++++++++++++++++++++++++++-------------------------- HoTT_Methods.thy | 14 ++++++------- Prod.thy | 2 +- Proj.thy | 12 +++++------ ex/HoTT Book/Ch1.thy | 37 +++++++++++++++++++++++++++++++++ ex/Methods.thy | 4 ++-- ex/Synthesis.thy | 10 ++++----- 7 files changed, 87 insertions(+), 50 deletions(-) create mode 100644 ex/HoTT Book/Ch1.thy diff --git a/EqualProps.thy b/EqualProps.thy index 2da7e2f..9b43345 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -26,7 +26,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 lem: assms) +by (rule Equal_elim[where ?x=x and ?y=y]) (simple lems: assms) \ \The type doesn't depend on \p\ so we don't need to specify \?p\ in the \where\ clause above.\ text " @@ -39,7 +39,7 @@ lemma inv_comp: unfolding inv_def proof show "\x. x: A \ refl x: x =\<^sub>A x" .. -qed (simple lem: assms) +qed (simple lems: assms) section \Transitivity / Path composition\ @@ -75,18 +75,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 lem: assms asm) - qed (simple lem: assms) + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms asm) + qed (simple lems: assms) qed (rule assms) - qed (simple lem: assms 1 2 3) - qed (simple lem: assms 1 2) + qed (simple lems: assms 1 2 3) + qed (simple 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 "reqcompose`x`y`p`z`q: x =\<^sub>A z" - by (simple lem: assms reqcompose_type) + by (simple lems: assms reqcompose_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. @@ -112,11 +112,11 @@ proof (subst comp) 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) + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms asm) + qed (simple lems: assms) qed (rule assms) - qed (simple lem: assms 1 2 3) - qed (simple lem: assms 1 2) + qed (simple lems: assms 1 2 3) + qed (simple 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)" @@ -134,11 +134,11 @@ proof (subst comp) 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) + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 3 4) + qed (simple lems: assms 3 4) qed fact - qed (simple lem: assms 1 2) - qed (simple lem: assms 1) } + qed (simple lems: assms 1 2) + qed (simple 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 (subst comp) @@ -152,10 +152,10 @@ proof (subst comp) 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) + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 2 3) + qed (simple lems: assms 2) qed fact - qed (simple lem: assms 1) } + qed (simple lems: assms 1) } show "(ind\<^sub>=(\_. \<^bold>\z q. ind\<^sub>= refl q)(refl(a)))`a`refl(a) \ refl(a)" proof (subst comp) @@ -166,8 +166,8 @@ proof (subst comp) 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) + by (rule Equal_elim[where ?x=u and ?y=z]) (simple lems: assms 1 2) + qed (simple lems: assms 1) qed fact } show "(\<^bold>\z q. ind\<^sub>= refl q)`a`refl(a) \ refl(a)" @@ -176,21 +176,21 @@ proof (subst comp) 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) } + by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: assms 1) + qed (simple lems: 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) + by (rule Equal_elim[where ?x=a and ?y=a]) (simple lems: 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 (simple lems: assms) + qed (simple lems: assms) qed fact - qed (simple lem: assms) - qed (simple lem: assms) + qed (simple lems: assms) + qed (simple lems: assms) qed fact qed fact @@ -210,11 +210,11 @@ lemma eqcompose_type: shows "p \ q: x =\<^sub>A z" proof (subst eqcompose_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 reqcompose_type) +qed (simple lems: assms reqcompose_type) lemma eqcompose_comp: assumes "A : U(i)" and "a : A" shows "refl(a) \ refl(a) \ refl(a)" -by (subst eqcompose_def) (simple lem: assms reqcompose_comp) +by (subst eqcompose_def) (simple lems: assms reqcompose_comp) lemmas EqualProps_rules [intro] = inv_type eqcompose_type diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy index e2eb4f1..d7f0821 100644 --- a/HoTT_Methods.thy +++ b/HoTT_Methods.thy @@ -23,7 +23,7 @@ text " Can also perform typechecking, and search for elements of a type. " -method simple uses lem = (assumption | rule lem | standard)+ +method simple uses lems = (assumption | rule lems | standard)+ subsection \Wellformedness checker\ @@ -33,21 +33,21 @@ text " The named theorem \wellform\ is declared in HoTT_Base.thy. " -method wellformed' uses jmt declares wellform = +method wellformed' uses jdmt declares wellform = match wellform in rl: "PROP ?P" \ \( - catch \rule rl[OF jmt]\ \fail\ | - catch \wellformed' jmt: rl[OF jmt]\ \fail\ + catch \rule rl[OF jdmt]\ \fail\ | + catch \wellformed' jdmt: rl[OF jdmt]\ \fail\ )\ -method wellformed uses lem = - match lem in lem: "?X : ?Y" \ \wellformed' jmt: lem\ +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 lem = (simple lem: lem | wellformed lem: lem)+ +method derive uses lems = (simple lems: lems | wellformed lems: lems)+ subsection \Substitution and simplification\ diff --git a/Prod.thy b/Prod.thy index 496bf3e..59c6cc3 100644 --- a/Prod.thy +++ b/Prod.thy @@ -43,7 +43,7 @@ and and Prod_elim: "\f: \x:A. B(x); a: A\ \ f`a: B(a)" and - Prod_comp: "\a: A; \x. x: A \ b(x): B(x)\ \ (\<^bold>\x. b(x))`a \ b(a)" + Prod_comp: "\\x. x: A \ b(x): B(x); a: A\ \ (\<^bold>\x. b(x))`a \ b(a)" and Prod_uniq: "f : \x:A. B(x) \ \<^bold>\x. (f`x) \ f" diff --git a/Proj.thy b/Proj.thy index 5c05eb2..d5ae6fa 100644 --- a/Proj.thy +++ b/Proj.thy @@ -20,7 +20,7 @@ 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 by (derive lem: assms) +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" @@ -33,14 +33,14 @@ 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)" by (derive lem: assms fst_type) + show "\p. p: \x:A. B(x) \ B(fst p): U(i)" by (derive lems: 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)" by (wellformed lem: assms(1)) - show "\x. x: A \ B(x): U(i)" by (wellformed lem: assms(1)) + show "A: U(i)" by (wellformed lems: assms(1)) + show "\x. x: A \ B(x): U(i)" by (wellformed lems: assms(1)) qed fact+ qed fact @@ -51,13 +51,13 @@ proof show "\x y. y: B(x) \ y: B(x)" . show "a: A" by fact show "b: B(a)" by fact -qed (simple lem: assms) +qed (simple lems: assms) text "Rule declarations:" lemmas Proj_types [intro] = fst_type snd_type -lemmas Proj_comps [intro] = fst_comp snd_comp +lemmas Proj_comps [comp] = fst_comp snd_comp end \ No newline at end of file diff --git a/ex/HoTT Book/Ch1.thy b/ex/HoTT Book/Ch1.thy new file mode 100644 index 0000000..84a5cf4 --- /dev/null +++ b/ex/HoTT Book/Ch1.thy @@ -0,0 +1,37 @@ +theory Ch1 + imports "../../HoTT" +begin + +chapter \HoTT Book, Chapter 1\ + +section \1.6 Dependent pair types (\-types)\ + +text "Prove that the only inhabitants of the \-type are those given by the pair constructor." + +schematic_goal + assumes "(\x:A. B(x)): U(i)" and "p: \x:A. B(x)" + shows "?a: p =[\x:A. B(x)] " + +text "Proof by induction on \p: \x:A. B(x)\:" + +proof (rule Sum_elim[where ?p=p]) + text "We just need to prove the base case; the rest will be taken care of automatically." + + fix x y assume asm: "x: A" "y: B(x)" show + "refl(): =[\x:A. B(x)] , snd >" + proof (subst (0 1) comp) + text " + The computation rules for \fst\ and \snd\ require that \x\ and \y\ have appropriate types. + The automatic proof methods have trouble picking the appropriate types, so we state them explicitly, + " + show "x: A" and "y: B(x)" by (fact asm)+ + + text "...twice, once each for the substitutions of \fst\ and \snd\." + show "x: A" and "y: B(x)" by (fact asm)+ + + qed (derive lems: assms asm) + +qed (derive lems: assms) + + +end \ No newline at end of file diff --git a/ex/Methods.thy b/ex/Methods.thy index b0c5f92..699d620 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -13,7 +13,7 @@ begin 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 lem: assms) +by (simple lems: assms) lemma @@ -29,7 +29,7 @@ proof - "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) + by (derive lems: assms) qed diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index 60655e5..48d762c 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -33,10 +33,10 @@ text " " schematic_goal "?p`0 \ 0" and "\n. n: \ \ (?p`(succ n)) \ n" -apply (subst comp, rule Nat_rules) -prefer 3 apply (subst comp, rule Nat_rules) +apply (subst comp) +prefer 4 apply (subst comp) prefer 3 apply (rule Nat_rules) -prefer 8 apply (rule Nat_rules | assumption)+ +apply (rule Nat_rules | assumption)+ done text " @@ -49,7 +49,7 @@ definition pred :: Term where "pred \ \<^bold>\n. ind\<^sub>\ \ \" unfolding pred_def by simple lemma pred_props: "\n. refl(n)>: ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -proof (simple lem: pred_type) +proof (simple lems: pred_type) have *: "pred`0 \ 0" unfolding pred_def proof (subst comp) show "\n. n: \ \ ind\<^sub>\ (\a b. a) n n: \" by simple @@ -75,7 +75,7 @@ qed theorem "\n. refl(n)>>: \pred:\\\ . ((pred`0) =\<^sub>\ 0) \ (\n:\. (pred`(succ n)) =\<^sub>\ n)" -by (simple lem: pred_welltyped pred_type pred_props) +by (simple lems: pred_welltyped pred_type pred_props) end \ No newline at end of file -- cgit v1.2.3