From 306721649f0963ab225deb8d5670cfe196bb360d Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 21 Jul 2020 16:28:05 +0200 Subject: 1. Bugfix: implicits now properly name schematic variables. Fixes problems caused by variable name clashes. 2. reduce method now more principled: restricts to repeating on first subgoal. 3. An example declarative proof in Equivalence.thy. --- hott/Equivalence.thy | 24 ++++++++++++------------ hott/Identity.thy | 17 ++++++++++------- spartan/core/Spartan.thy | 18 +++++++++++------- spartan/core/implicits.ML | 21 ++++++++++++--------- 4 files changed, 45 insertions(+), 35 deletions(-) diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 88adc8b..d976677 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -338,18 +338,18 @@ Lemma (derive) equivalence_symmetric: Lemma (derive) equivalence_transitive: assumes "A: U i" "B: U i" "C: U i" shows "A \ B \ B \ C \ A \ C" - (* proof intros - fix AB BC assume "AB: A \ B" "BC: B \ C" - let "?f: {}" = "(fst AB) :: o" *) - apply intros - unfolding equivalence_def - focus vars p q apply (elim p, elim q) - focus vars f biinv\<^sub>f g biinv\<^sub>g apply intro - \ apply (rule funcompI) defer by assumption+ known - \ by (rule funcomp_biinv) - done - done - done + proof intros + fix AB BC assume *: "AB: A \ B" "BC: B \ C" + then have + "fst AB: A \ B" and 1: "snd AB: biinv (fst AB)" + "fst BC: B \ C" and 2: "snd BC: biinv (fst BC)" + unfolding equivalence_def by typechk+ + then have "fst BC \ fst AB: A \ C" by typechk + moreover have "biinv (fst BC \ fst AB)" + using * unfolding equivalence_def by (rules funcomp_biinv 1 2) + ultimately show "A \ C" + unfolding equivalence_def by intro facts + qed text \ Equal types are equivalent. We give two proofs: the first by induction, and diff --git a/hott/Identity.thy b/hott/Identity.thy index 1cb3946..29ce26a 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -49,6 +49,9 @@ lemmas section \Path induction\ +\ \With `p: x = y` in the context the invokation `eq p` is essentially + `elim p x y`, with some extra bits before and after.\ + method_setup eq = \Args.term >> (fn tm => K (CONTEXT_METHOD ( CHEADGOAL o SIDE_CONDS ( @@ -155,12 +158,12 @@ translations Lemma lu_refl [comp]: assumes "A: U i" "x: A" shows "lu (refl x) \ refl (refl x)" - unfolding refl_pathcomp_def by reduce+ + unfolding refl_pathcomp_def by reduce Lemma ru_refl [comp]: assumes "A: U i" "x: A" shows "ru (refl x) \ refl (refl x)" - unfolding pathcomp_refl_def by reduce+ + unfolding pathcomp_refl_def by reduce Lemma (derive) inv_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" @@ -374,7 +377,7 @@ Lemma transport_const_comp [comp]: "x: A" "b: B" "A: U i" "B: U i" shows "trans_const B (refl x) b\ refl b" - unfolding transport_const_def by reduce+ + unfolding transport_const_def by reduce Lemma (derive) pathlift: assumes @@ -398,7 +401,7 @@ Lemma pathlift_comp [comp]: "\x. x: A \ P x: U i" "A: U i" shows "lift P (refl x) u \ refl " - unfolding pathlift_def by reduce+ + unfolding pathlift_def by reduce Lemma (derive) pathlift_fst: assumes @@ -438,7 +441,7 @@ Lemma dependent_map_comp [comp]: "A: U i" "\x. x: A \ P x: U i" shows "apd f (refl x) \ refl (f x)" - unfolding apd_def by reduce+ + unfolding apd_def by reduce Lemma (derive) apd_ap: assumes @@ -495,13 +498,13 @@ Lemma whisker_refl [comp]: assumes "A: U i" "a: A" "b: A" shows "\p: a = b; q: a = b; \: p =\<^bsub>a = b\<^esub> q\ \ \ \\<^sub>r\<^bsub>a\<^esub> (refl b) \ ru p \ \ \ (ru q)\" - unfolding right_whisker_def by reduce+ + unfolding right_whisker_def by reduce Lemma refl_whisker [comp]: assumes "A: U i" "a: A" "b: A" shows "\p: a = b; q: a = b; \: p = q\ \ (refl a) \\<^sub>l\<^bsub>b\<^esub> \ \ (lu p) \ \ \ (lu q)\" - unfolding left_whisker_def by reduce+ + unfolding left_whisker_def by reduce method left_whisker = (rule left_whisker) method right_whisker = (rule right_whisker) diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index a4ad300..fa6148f 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -52,7 +52,7 @@ paragraph \ typedecl o -judgment has_type :: \o \ o \ prop\ ("(2_:/ _)" 999) +consts has_type :: \o \ o \ prop\ ("(2_:/ _)" 999) text \Type annotations for type-checking and inference.\ @@ -232,6 +232,10 @@ method_setup rule = \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\ +method_setup rules = + \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( + CREPEAT o CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\ + method_setup dest = \Scan.lift (Scan.option (Args.parens Parse.int)) -- Attrib.thms >> (fn (n_opt, ths) => K (CONTEXT_METHOD ( @@ -255,6 +259,8 @@ method_setup cases = \Args.term >> (fn tm => K (CONTEXT_METHOD ( CHEADGOAL o SIDE_CONDS (cases_ctac tm))))\ +method facts = fact+ + subsection \Reflexivity\ @@ -310,7 +316,8 @@ setup \map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "" (fn ctxt' => NO_CONTEXT_TACTIC ctxt' o Types.check_infer (Simplifier.prems_of ctxt'))))\ -method reduce uses add = changed \((simp add: comp add | sub comp); typechk?)+\ +method reduce uses add = + changed \repeat_new \(simp add: comp add | sub comp); typechk?\\ subsection \Implicits\ @@ -327,10 +334,7 @@ ML_file \implicits.ML\ attribute_setup implicit = \Scan.succeed Implicits.implicit_defs_attr\ -ML \ -val _ = Context.>> - (Syntax_Phases.term_check 1 "" (fn ctxt => map (Implicits.make_holes ctxt))) -\ +ML \val _ = Context.>> (Syntax_Phases.term_check 1 "" Implicits.make_holes)\ text \Automatically insert inhabitation judgments where needed:\ @@ -488,7 +492,7 @@ lemma snd_type [typechk]: lemma snd_comp [comp]: assumes "a: A" "b: B a" "A: U i" "\x. x: A \ B x: U i" shows "snd A B \ b" - unfolding snd_def by reduce+ + unfolding snd_def by reduce subsection \Notation\ diff --git a/spartan/core/implicits.ML b/spartan/core/implicits.ML index 4d73c8d..ab64b0f 100644 --- a/spartan/core/implicits.ML +++ b/spartan/core/implicits.ML @@ -3,7 +3,7 @@ sig val implicit_defs: Proof.context -> (term * term) Symtab.table val implicit_defs_attr: attribute -val make_holes: Proof.context -> term -> term +val make_holes: Proof.context -> term list -> term list end = struct @@ -25,16 +25,15 @@ val implicit_defs_attr = Thm.declaration_attribute (fn th => Defs.map (Symtab.update (Term.term_name head, (head, def'))) end) -fun make_holes ctxt = +fun make_holes_single ctxt tm name_ctxt = let fun iarg_to_hole (Const (\<^const_name>\iarg\, T)) = Const (\<^const_name>\hole\, T) | iarg_to_hole t = t fun expand head args = - let - fun betapplys (head', args') = - Term.betapplys (map_aterms iarg_to_hole head', args') + let fun betapplys (head', args') = + Term.betapplys (map_aterms iarg_to_hole head', args') in case head of Abs (x, T, t) => @@ -66,13 +65,17 @@ fun make_holes ctxt = in subst t (take n vs) Ts $ subst u (drop n vs) Ts end | subst t _ _ = t - val vars = map (fn n => Var ((n, 0), dummyT)) - (Name.invent (Variable.names_of ctxt) "*" (count t)) + val names = Name.invent name_ctxt "*" (count t) + val vars = map (fn n => Var ((n, 0), dummyT)) names in - subst t vars [] + (subst t vars [], fold Name.declare names name_ctxt) end in - Lib.traverse_term expand #> holes_to_vars + holes_to_vars (Lib.traverse_term expand tm) end +fun make_holes ctxt tms = #1 + (fold_map (make_holes_single ctxt) tms (Variable.names_of ctxt)) + + end -- cgit v1.2.3