(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.

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: \<Prod>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 \<rightarrow> B" "pf: is_qinv f"
   shows "is_qinv (fst pf)"
-using [[debug_typechk]]
-  using [[solve_side_conds=2]]
+  using \<open>pf:_\<close>[unfolded is_qinv_def] \<comment> \<open>Should be unfolded by the typechecker\<close>
   apply (rule is_qinvI)
-  back \<comment> \<open>Typechecking/inference goes too far here. Problem would likely be
-    solved with definitional unfolding\<close>
   \<^item> by (fact \<open>f:_\<close>)
   \<^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 \<circ> f) \<circ> finv \<circ> ginv ~ id C"
         proof -
           have "(g \<circ> f) \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> 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 \<open>
-  The following could perhaps be easier with transport (but then I think we need
-  univalence?)...
-\<close>
-
 Lemma (def) equivalence_symmetric:
   assumes "A: U i" "B: U i"
   shows "A \<simeq> B \<rightarrow> B \<simeq> A"
@@ -408,8 +400,8 @@ Lemma
   by (eq p) (rule equivalence_refl)
 
 text \<open>
-  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.
 \<close>
 
 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 "<trans (id (U i)) p, ?isequiv>: A \<simeq> B"
   unfolding equivalence_def
-  apply intros defer
+  apply intro defer
     \<^item> apply (eq p)
       \<^enum> vars A B
         apply (rewrite at A in "A \<rightarrow> 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 \<open>Path induction\<close>
 
 method_setup eq =
   \<open>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 \<open>Type-checking/inference\<close>
 named_theorems form and intr and comp and type
 
 \<comment> \<open>Defines elimination automation and the `elim` attribute\<close>
-ML_file \<open>elimination.ML\<close>  
+ML_file \<open>elimination.ML\<close>
 
 lemmas
   [form] = PiF SigF and
@@ -225,36 +225,40 @@ named_theorems intro \<comment> \<open>Logical introduction rules\<close>
 
 lemmas [intro] = PiI[rotated] SigI
 
-ML_file \<open>cases.ML\<close> \<comment> \<open>case reasoning rules\<close>
+\<comment> \<open>Case reasoning rules\<close>
+ML_file \<open>cases.ML\<close>
+
 ML_file \<open>tactics.ML\<close>
 
 method_setup rule =
   \<open>Attrib.thms >> (fn ths => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (rule_ctac ths))))\<close>
+    CHEADGOAL o SIDE_CONDS 0 (rule_ctac ths))))\<close>
 
 method_setup dest =
-  \<open>Scan.lift (Scan.option (Args.parens Parse.int))
+  \<open>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))))\<close>
+      CHEADGOAL o SIDE_CONDS 0 (dest_ctac n_opt ths))))\<close>
 
 method_setup intro =
   \<open>Scan.succeed (K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (intro_ctac))))\<close>
+    CHEADGOAL o SIDE_CONDS 0 intro_ctac)))\<close>
 
 method_setup intros =
-  \<open>Scan.succeed (K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (CREPEAT o intro_ctac))))\<close>
+  \<open>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))))))\<close>
 
 method_setup elim =
   \<open>Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (elim_ctac tms))))\<close>
-
-method elims = elim+
+    CHEADGOAL o SIDE_CONDS 0 (elim_ctac tms))))\<close>
 
 method_setup cases =
   \<open>Args.term >> (fn tm => K (CONTEXT_METHOD (
-    CHEADGOAL o SIDE_CONDS (cases_ctac tm))))\<close>
+    CHEADGOAL o SIDE_CONDS 0 (cases_ctac tm))))\<close>
 
+method elims = elim+
 method facts = fact+
 
 
@@ -267,7 +271,7 @@ subsection \<open>Trivial proofs (modulo automatic discharge of side conditions)
 
 method_setup this =
   \<open>Scan.succeed (K (CONTEXT_METHOD (fn facts =>
-    CHEADGOAL (SIDE_CONDS
+    CHEADGOAL (SIDE_CONDS 0
       (CONTEXT_TACTIC' (fn ctxt => resolve_tac ctxt facts))
       facts))))\<close>
 
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>\<open>subst\<close>
         (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>\<open>rewrite\<close> (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>\<open>solve_side_conds\<close> (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>\<open>intro\<close>) 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>\<open>intro\<close>) i
+    else no_tac
+  end))
 
 
 (* Induction/elimination *)