diff options
Diffstat (limited to '')
| -rw-r--r-- | Equal.thy | 2 | ||||
| -rw-r--r-- | EqualProps.thy | 50 | ||||
| -rw-r--r-- | HoTT.thy | 17 | ||||
| -rw-r--r-- | HoTT_Base.thy | 4 | ||||
| -rw-r--r-- | HoTT_Methods.thy | 92 | ||||
| -rw-r--r-- | Proj.thy | 104 | ||||
| -rw-r--r-- | Sum.thy | 8 | ||||
| -rw-r--r-- | ex/Methods.thy | 41 | ||||
| -rw-r--r-- | scratch.thy | 20 |
9 files changed, 133 insertions, 205 deletions
@@ -53,7 +53,7 @@ and \<rbrakk> \<Longrightarrow> indEqual[A] C f a a refl(a) \<equiv> 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] \<Rightarrow> 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) \<rightarrow> (y =\<^sub>A x)" - proof (unfold inv_def, standard) - fix p assume asm: "p : x =\<^sub>A y" - show "indEqual[A] (\<lambda>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) \<equiv> indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>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] (\<lambda>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" . \<comment> \<open>The elimination rule requires that both arguments to \<open>indEqual\<close> be shown to have the correct type.\<close> - qed (assumption | rule | rule asm)+ - qed + by (derive lems: assms unfolds: inv_def) also have "indEqual[A] (\<lambda>x y _. y =\<^sub>A x) (\<lambda>x. refl(x)) a a refl(a) \<equiv> refl(a)" - by (standard | assumption | rule assms)+ + by (simple lems: assms) finally show "inv[A,a,a]`refl(a) \<equiv> refl(a)" . qed @@ -79,14 +59,34 @@ abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> 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) \<equiv> refl(a)" +proof (unfold rcompose_def) + show "(\<^bold>\<lambda>p:a =[A] a. + lambda (a =[A] a) + (op ` + ((\<^bold>\<lambda>x:A. + \<^bold>\<lambda>y:A. + lambda (x =[A] y) + (indEqual[A] + (\<lambda>x y _. \<Prod>z:A. y =[A] z \<rightarrow> x =[A] z) + (\<lambda>x. \<^bold>\<lambda>z:A. + lambda (x =[A] z) + (indEqual[A] (\<lambda>x z _. x =[A] z) refl x z)) + x y)) ` + a ` + a ` + p ` + a))) ` + refl(a) ` + refl(a) \<equiv> + refl(a)" + sorry \<comment> \<open>Long and tedious proof if the Simplifier is not set up.\<close> @@ -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 \<open>Setup\<close> -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 \<open>Metalogical definitions\<close> text "A single meta-type \<open>Term\<close> 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 \<open>Method setup\<close> -text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> using rules declared [intro] and [elim], as well as additional provided lemmas." +text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<open>a : A\<close> 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 \<open>simple\<close> and \<open>wellformed\<close> to search for derivations." +text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations. +\<open>wellformed\<close> uses the facts passed as \<open>lems\<close> to derive any required typing judgments. +Definitions passed as \<open>unfolds\<close> are unfolded throughout. + +Roughly speaking \<open>derive\<close> is more powerful than \<open>simple\<close>, but may fail to find a proof where \<open>simple\<close> does if it reduces too eagerly." -method derive uses lems = ( - catch \<open>unfold lems\<close> \<open>fail\<close> | - catch \<open>simple lems: lems\<close> \<open>fail\<close> | +method derive uses lems unfolds = ( + unfold unfolds | + simple lems: lems | match lems in lem: "?X : ?Y" \<Rightarrow> \<open>wellformed jdgmt: lem\<close> )+ -section \<open>Examples\<close> - -lemma - assumes "A : U" "B: A \<rightarrow> U" "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" - shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U" -by (simple lems: assms) - -lemma - assumes "f : \<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z" - shows - "A : U" and - "B: A \<rightarrow> U" and - "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" and - "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" -proof - - show "A : U" by (wellformed jdgmt: assms) - show "B: A \<rightarrow> U" by (wellformed jdgmt: assms) - show "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" by (wellformed jdgmt: assms) - show "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" by (wellformed jdgmt: assms) -qed - - -section \<open>Experimental methods\<close> - -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 \<open> -(* Try solving \<open>a : A\<close> by assumption provided \<open>a\<close> 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 \<open>A : U\<close> 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 \<open>a : A\<close> (\<open>a\<close> flexible, \<open>A\<close> 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 \<open>a : A\<close> (\<open>a\<close> rigid, \<open>A\<close> 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 -\<close> - -method_setup form = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (form_tac ctxt))\<close> -method_setup intro = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (intro_tac ctxt ths))\<close> -method_setup typecheck = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (typecheck_tac ctxt ths))\<close> +text "Simplify function applications." end
\ No newline at end of file @@ -49,7 +49,7 @@ text "Typing judgments and computation rules for the dependent and non-dependent lemma fst_dep_type: assumes "p : \<Sum>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) \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>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] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> 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 : \<Sum>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 \<rightarrow> 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 : \<Sum>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] : \<Prod>p:(\<Sum>x:A. B x). B (fst[A,B]`p)" - proof (unfold snd_dep_def, standard) - show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p : B (fst[A,B]`p)" - proof (standard, elim lemma1) - fix p assume *: "p : \<Sum>x:A. B x" - have **: "B: A \<rightarrow> 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] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def) + + fix x y assume asm: "x : A" "y : B x" + have "B: A \<rightarrow> 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) \<equiv> indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b)" - proof (unfold snd_dep_def, standard) - show "(a,b) : \<Sum>x:A. B x" using assms .. + proof (derive lems: assms unfolds: snd_dep_def) + show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def) - fix p assume *: "p : \<Sum>x:A. B x" - show "indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>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] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b) \<equiv> b" - proof (standard, elim lemma1) + proof (simple lems: assms) + show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> 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) \<equiv> b" . qed @@ -135,17 +122,7 @@ text "For non-dependent projection functions:" lemma fst_nondep_type: assumes "p : A \<times> B" shows "fst[A,B]`p : A" - -proof - show "fst[A,B] : A \<times> B \<rightarrow> A" - proof (unfold fst_nondep_def, standard) - fix q assume *: "q : A \<times> B" - show "indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>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) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" - proof (unfold fst_nondep_def, standard) - show "(a,b) : A \<times> B" using assms .. - show "\<And>p. p : A \<times> B \<Longrightarrow> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>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, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> 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) \<equiv> a" . qed @@ -177,15 +146,10 @@ lemma snd_nondep_type: proof show "snd[A,B] : A \<times> B \<rightarrow> B" - proof (unfold snd_nondep_def, standard) - fix q assume *: "q : A \<times> B" - show "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) q : B" - proof - have **: "\<lambda>_. B: A \<rightarrow> 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 \<times> B" + show "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>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) \<equiv> b" proof - have "snd[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b)" - proof (unfold snd_nondep_def, standard) - show "(a,b) : A \<times> B" by (simple conds: assms) - show "\<And>p. p : A \<times> B \<Longrightarrow> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>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, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b) \<equiv> 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) \<equiv> b" . qed @@ -59,10 +59,10 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) lemma Pair_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a,b) : A \<times> 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 \<rightarrow> U" "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" + shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U" +by (simple lems: assms) + + +lemma + assumes "f : \<Sum>x:A. \<Prod>y: B x. \<Sum>z: C x y. D x y z" + shows + "A : U" and + "B: A \<rightarrow> U" and + "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" and + "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" +proof - + show "A : U" by (wellformed jdgmt: assms) + show "B: A \<rightarrow> U" by (wellformed jdgmt: assms) + show "\<And>x. x : A \<Longrightarrow> C x: B x \<rightarrow> U" by (wellformed jdgmt: assms) + show "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> D x y: C x y \<rightarrow> U" by (wellformed jdgmt: assms) +qed + + +text "Typechecking:" + +\<comment> \<open>Correctly determines the type of the pair\<close> +schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (a, b) : ?A" by simple + +\<comment> \<open>Finds element\<close> +schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> 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 \<or> Q \<Longrightarrow> Q \<or> P" -apply (erule disjE) (* Compare with the less useful \<open>rule disjE\<close> *) - apply (rule disjI2) - apply assumption -apply (rule disjI1) -apply assumption -done - -lemma imp_uncurry: "P \<longrightarrow> (Q \<longrightarrow> R) \<Longrightarrow> P \<and> Q \<longrightarrow> R" -apply (rule impI) -apply (erule conjE) -apply (drule mp) -apply assumption -apply (drule mp) -apply assumption -apply assumption -done +schematic_goal "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> ?x : A \<times> B" by simple end
\ No newline at end of file |