From 710f314a9ccb84cdd9df9bc8bf52482b8d1f5a56 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 3 Aug 2020 13:34:53 +0200 Subject: (FEAT) SIDE_CONDS tactical has additional argument specifying how many initial subgoals to skip applying the side condition solver to. (FEAT) `intro`, `intros` methods for "logical introduction rules" (as opposed to typechecking `intr` attribute), only works on conclusions with rigid type. (FEAT) CREPEAT_N bounded repetition tactical, used in `intros n` method. --- hott/Equivalence.thy | 20 ++++++-------------- hott/Identity.thy | 2 +- spartan/core/Spartan.thy | 30 +++++++++++++++++------------- spartan/core/context_tactical.ML | 4 ++++ spartan/core/eqsubst.ML | 2 +- spartan/core/rewrite.ML | 2 +- spartan/core/tactics.ML | 20 ++++++++++++-------- 7 files changed, 42 insertions(+), 38 deletions(-) diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index b29a213..a4eea93 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -40,7 +40,7 @@ Lemma (def) homotopy_refl [refl]: "f: \x: A. B x" shows "f ~ f" unfolding homotopy_def - by intros + by intros fact Lemma (def) hsym: assumes @@ -205,11 +205,8 @@ Lemma is_qinv_components [type]: Lemma (def) qinv_is_qinv: assumes "A: U i" "B: U i" "f: A \ B" "pf: is_qinv f" shows "is_qinv (fst pf)" -using [[debug_typechk]] - using [[solve_side_conds=2]] + using \pf:_\[unfolded is_qinv_def] \ \Should be unfolded by the typechecker\ apply (rule is_qinvI) - back \ \Typechecking/inference goes too far here. Problem would likely be - solved with definitional unfolding\ \<^item> by (fact \f:_\) \<^item> by (rule sec_of_is_qinv) \<^item> by (rule ret_of_is_qinv) @@ -233,7 +230,7 @@ Lemma (def) funcomp_is_qinv: also have ".. ~ id A" by reduce fact finally show "{}" by this qed - + show "(g \ f) \ finv \ ginv ~ id C" proof - have "(g \ f) \ finv \ ginv ~ g \ (f \ finv) \ ginv" by reduce refl @@ -363,11 +360,6 @@ Lemma (def) equivalence_refl: show "is_biinv (id A)" by (rule is_biinv_if_is_qinv) (rule id_is_qinv) qed typechk -text \ - The following could perhaps be easier with transport (but then I think we need - univalence?)... -\ - Lemma (def) equivalence_symmetric: assumes "A: U i" "B: U i" shows "A \ B \ B \ A" @@ -408,8 +400,8 @@ Lemma by (eq p) (rule equivalence_refl) text \ - The following proof is wordy because (1) the typechecker doesn't rewrite, and - (2) we don't yet have universe automation. + The following proof is wordy because (1) the typechecker doesn't normalize, + and (2) we don't yet have universe level inference. \ Lemma (def) equiv_if_equal: @@ -417,7 +409,7 @@ Lemma (def) equiv_if_equal: "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B" shows ": A \ B" unfolding equivalence_def - apply intros defer + apply intro defer \<^item> apply (eq p) \<^enum> vars A B apply (rewrite at A in "A \ B" id_comp[symmetric]) diff --git a/hott/Identity.thy b/hott/Identity.thy index b9ebafb..b06604f 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -54,7 +54,7 @@ section \Path induction\ method_setup eq = \Args.term >> (fn tm => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS ( + CHEADGOAL o SIDE_CONDS 0 ( CONTEXT_SUBGOAL (fn (goal, i) => fn cst as (ctxt, st) => let val facts = Proof_Context.facts_of ctxt diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index 180354c..ea72208 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -192,7 +192,7 @@ subsection \Type-checking/inference\ named_theorems form and intr and comp and type \ \Defines elimination automation and the `elim` attribute\ -ML_file \elimination.ML\ +ML_file \elimination.ML\ lemmas [form] = PiF SigF and @@ -225,36 +225,40 @@ named_theorems intro \ \Logical introduction rules\ lemmas [intro] = PiI[rotated] SigI -ML_file \cases.ML\ \ \case reasoning rules\ +\ \Case reasoning rules\ +ML_file \cases.ML\ + ML_file \tactics.ML\ method_setup rule = \Attrib.thms >> (fn ths => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\ + CHEADGOAL o SIDE_CONDS 0 (rule_ctac ths))))\ method_setup dest = - \Scan.lift (Scan.option (Args.parens Parse.int)) + \Scan.lift (Scan.option (Args.parens Parse.nat)) -- Attrib.thms >> (fn (n_opt, ths) => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (dest_ctac n_opt ths))))\ + CHEADGOAL o SIDE_CONDS 0 (dest_ctac n_opt ths))))\ method_setup intro = \Scan.succeed (K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (intro_ctac))))\ + CHEADGOAL o SIDE_CONDS 0 intro_ctac)))\ method_setup intros = - \Scan.succeed (K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (CREPEAT o intro_ctac))))\ + \Scan.lift (Scan.option Parse.nat) >> (fn n_opt => + K (CONTEXT_METHOD (fn facts => + case n_opt of + SOME n => CREPEAT_N n (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)) + | NONE => CREPEAT (CCHANGED (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))))))\ method_setup elim = \Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (elim_ctac tms))))\ - -method elims = elim+ + CHEADGOAL o SIDE_CONDS 0 (elim_ctac tms))))\ method_setup cases = \Args.term >> (fn tm => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS (cases_ctac tm))))\ + CHEADGOAL o SIDE_CONDS 0 (cases_ctac tm))))\ +method elims = elim+ method facts = fact+ @@ -267,7 +271,7 @@ subsection \Trivial proofs (modulo automatic discharge of side conditions) method_setup this = \Scan.succeed (K (CONTEXT_METHOD (fn facts => - CHEADGOAL (SIDE_CONDS + CHEADGOAL (SIDE_CONDS 0 (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts)) facts))))\ diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML index b5a6c00..0aa6f20 100644 --- a/spartan/core/context_tactical.ML +++ b/spartan/core/context_tactical.ML @@ -28,6 +28,7 @@ val CAPPEND': context_tactic' * context_tactic' -> context_tactic' val CTRY: context_tactic -> context_tactic val CREPEAT: context_tactic -> context_tactic val CREPEAT1: context_tactic -> context_tactic +val CREPEAT_N: int -> context_tactic -> context_tactic val CFILTER: (context_state -> bool) -> context_tactic -> context_tactic val CCHANGED: context_tactic -> context_tactic val CTHEN_ALL_NEW: context_tactic' * context_tactic' -> context_tactic' @@ -91,6 +92,9 @@ fun CREPEAT ctac = fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac +fun CREPEAT_N 0 _ = all_ctac + | CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac + fun CFILTER pred ctac cst = ctac cst |> Seq.filter_results diff --git a/spartan/core/eqsubst.ML b/spartan/core/eqsubst.ML index e7ecf63..31d5126 100644 --- a/spartan/core/eqsubst.ML +++ b/spartan/core/eqsubst.ML @@ -433,7 +433,7 @@ val _ = "single-step substitution" #> Method.setup \<^binding>\subst\ (parser >> (fn ((asm, occs), inthms) => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS + CHEADGOAL o SIDE_CONDS 0 ((if asm then eqsubst_asm_ctac else eqsubst_ctac) occs inthms))))) "single-step substitution with automatic discharge of side conditions" ) diff --git a/spartan/core/rewrite.ML b/spartan/core/rewrite.ML index eba0e81..99c21b5 100644 --- a/spartan/core/rewrite.ML +++ b/spartan/core/rewrite.ML @@ -458,7 +458,7 @@ val _ = "single-step rewriting, allowing subterm selection via patterns" #> Method.setup \<^binding>\rewrite\ (subst_parser >> (fn (pattern, inthms, (to, pat_ctxt)) => K (CONTEXT_METHOD ( - CHEADGOAL o SIDE_CONDS + CHEADGOAL o SIDE_CONDS 0 (rewrite_export_ctac ((pattern, to), SOME pat_ctxt) inthms))))) "single-step rewriting with auto-typechecking" end diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML index 959050e..446af15 100644 --- a/spartan/core/tactics.ML +++ b/spartan/core/tactics.ML @@ -8,7 +8,7 @@ structure Tactics: sig val solve_side_conds: int Config.T -val SIDE_CONDS: context_tactic' -> thm list -> context_tactic' +val SIDE_CONDS: int -> context_tactic' -> thm list -> context_tactic' val rule_ctac: thm list -> context_tactic' val dest_ctac: int option -> thm list -> context_tactic' val intro_ctac: context_tactic' @@ -21,12 +21,12 @@ end = struct (* Side conditions *) val solve_side_conds = Attrib.setup_config_int \<^binding>\solve_side_conds\ (K 2) -fun SIDE_CONDS ctac facts i (cst as (ctxt, st)) = cst |> (ctac i CTHEN +fun SIDE_CONDS j ctac facts i (cst as (ctxt, st)) = cst |> (case Config.get ctxt solve_side_conds of - 1 => CALLGOALS (CTRY o Types.known_ctac facts) - | 2 => CREPEAT_IN_RANGE i (Thm.nprems_of st - i) + 1 => (ctac CTHEN_ALL_NEW (CTRY o Types.known_ctac facts)) i + | 2 => ctac i CTHEN CREPEAT_IN_RANGE (i + j) (Thm.nprems_of st - i) (CTRY o CREPEAT_ALL_NEW_FWD (Types.check_infer facts)) - | _ => all_ctac)) + | _ => ctac i) (* rule, dest, intro *) @@ -55,9 +55,13 @@ fun dest_ctac opt_n ths i (ctxt, st) = end -(*Applies some introduction rule*) -fun intro_ctac i (ctxt, st) = TACTIC_CONTEXT ctxt (resolve_tac ctxt - (Named_Theorems.get ctxt \<^named_theorems>\intro\) i st) +(*Applies an appropriate introduction rule*) +val intro_ctac = CONTEXT_TACTIC' (fn ctxt => SUBGOAL (fn (goal, i) => + let val concl = Logic.strip_assums_concl goal in + if Lib.is_typing concl andalso Lib.is_rigid (Lib.type_of_typing concl) + then resolve_tac ctxt (Named_Theorems.get ctxt \<^named_theorems>\intro\) i + else no_tac + end)) (* Induction/elimination *) -- cgit v1.2.3