aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--hott/Equivalence.thy20
-rw-r--r--hott/Identity.thy2
-rw-r--r--spartan/core/Spartan.thy30
-rw-r--r--spartan/core/context_tactical.ML4
-rw-r--r--spartan/core/eqsubst.ML2
-rw-r--r--spartan/core/rewrite.ML2
-rw-r--r--spartan/core/tactics.ML20
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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-03 03:11:21 +0000