(FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* goals; resolving with conditional typing judgments (e.g. type family assumptions) is part of check_infer_step

3 files changed, 18 insertions, 18 deletions

diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy
index d85e6de..7d1f2b1 100644
--- a/hott/Equivalence.thy
+++ b/hott/Equivalence.thy
@@ -162,8 +162,7 @@ Corollary (def) commute_homotopy':
           rewrite at "_ = \<hole>" id_comp[symmetric])
 
     have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]"
-      by (rule left_whisker) (fact, rule
-        ap_id[where ?A=A and ?x="f x" and ?y=x, simplified id_comp, symmetric])
+      by (rule left_whisker, transport eq: ap_id) (reduce+, refl)
     also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x"
       by (rule commute_homotopy)
     finally have *: "{}" by this
@@ -433,28 +432,28 @@ Lemma (def) equiv_if_equal:
       \<^enum> vars A B
         apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
         using [[solve_side_conds=1]]
-        apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+        apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact)
         apply (rule transport, rule Ui_in_USi)
         apply (rule lift_universe_codomain, rule Ui_in_USi)
         apply (typechk, rule Ui_in_USi)
-        done
+        by facts
       \<^enum> vars A
         using [[solve_side_conds=1]]
         apply (subst transport_comp)
           \<circ> by (rule Ui_in_USi)
           \<circ> by reduce (rule in_USi_if_in_Ui)
-          \<circ> by reduce (rule id_is_biinv)
+          \<circ> by reduce (rule id_is_biinv, fact)
         done
       done
 
     \<^item> \<comment> \<open>Similar proof as in the first subgoal above\<close>
       apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric])
       using [[solve_side_conds=1]]
-      apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric])
+      apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric], fact)
       apply (rule transport, rule Ui_in_USi)
       apply (rule lift_universe_codomain, rule Ui_in_USi)
       apply (typechk, rule Ui_in_USi)
-      done
+      by facts
   done
 
 (*Uncomment this to see all implicits from here on.
diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index 446af15..45fd119 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -82,8 +82,8 @@ fun internalize_fact_tac t =
         Drule.infer_instantiate' ctxt [NONE, NONE, SOME B, SOME a] @{thm PiE}
     in
       HEADGOAL (resolve_tac ctxt [resolvent])
-      (*known_tac infers the correct type T inferred by unification*)
-      THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.known_ctac [])
+      (*Infer the correct type T*)
+      THEN SOMEGOAL (NO_CONTEXT_TACTIC ctxt o Types.check_infer [])
     end)
 
 fun elim_core_tac tms types ctxt =
diff --git a/spartan/core/typechecking.ML b/spartan/core/typechecking.ML
index b7a7f9b..ca89c8c 100644
--- a/spartan/core/typechecking.ML
+++ b/spartan/core/typechecking.ML
@@ -50,18 +50,15 @@ fun known_ctac facts = CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
       if Lib.no_vars concl orelse
         (Lib.is_typing concl andalso Lib.no_vars (Lib.term_of_typing concl))
       then
-        let val ths = map (Simplifier.norm_hhf ctxt)
-          (facts @ map fst (Facts.props (Proof_Context.facts_of ctxt)))
-          (*FIXME: Shouldn't pull nameless facts directly from context*)
-        in
-          (debug_tac ctxt "resolve" THEN resolve_tac ctxt ths i ORELSE
-          debug_tac ctxt "assume" THEN assume_tac ctxt i) st
+        let val ths = map (Simplifier.norm_hhf ctxt) facts
+        in st |>
+          (assume_tac ctxt ORELSE' resolve_tac ctxt ths THEN_ALL_NEW K no_tac) i
         end
       else Seq.empty
     end)
 
 (*Simple bidirectional typing tactic, with some nondeterminism from backtracking
-  search over arbitrary `typechk` rules. The current implementation does not
+  search over arbitrary `type` rules. The current implementation does not
   perform any normalization.*)
 fun check_infer_step facts i (ctxt, st) =
   let
@@ -69,8 +66,12 @@ fun check_infer_step facts i (ctxt, st) =
       if Lib.rigid_typing_concl goal
       then
         let val net = Tactic.build_net (
-          map (Simplifier.norm_hhf ctxt) facts
-          (*MAYBE FIXME: Remove `typechk` from this list, and instead perform
+          map (Simplifier.norm_hhf ctxt)
+            (*FIXME: Shouldn't pull nameless facts directly from context. Note
+              that we *do* need to be able to resolve with conditional
+              statements expressing type family judgments*)
+            (facts @ map fst (Facts.props (Proof_Context.facts_of ctxt)))
+          (*MAYBE FIXME: Remove `type` from this list, and instead perform
             definitional unfolding to (w?)hnf.*)
           @(Named_Theorems.get ctxt \<^named_theorems>\<open>type\<close>)
           @(Named_Theorems.get ctxt \<^named_theorems>\<open>form\<close>)