From 8f4ff41d24dd8fa6844312456d47cad4be6cb239 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 9 Aug 2020 18:34:58 +0200 Subject: (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 --- hott/Equivalence.thy | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) (limited to 'hott/Equivalence.thy') 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 "_ = \" id_comp[symmetric]) have "H (f x) \ H x = H (f x) \ (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) \ (id A)[H x] = f[H x] \ 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 \ B" id_comp[symmetric]) using [[solve_side_conds=1]] - apply (rewrite at B in "_ \ B" id_comp[symmetric]) + apply (rewrite at B in "_ \ 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) \ by (rule Ui_in_USi) \ by reduce (rule in_USi_if_in_Ui) - \ by reduce (rule id_is_biinv) + \ by reduce (rule id_is_biinv, fact) done done \<^item> \ \Similar proof as in the first subgoal above\ apply (rewrite at A in "A \ B" id_comp[symmetric]) using [[solve_side_conds=1]] - apply (rewrite at B in "_ \ B" id_comp[symmetric]) + apply (rewrite at B in "_ \ 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. -- cgit v1.2.3