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

2 files changed, 7 insertions, 15 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