aboutsummaryrefslogtreecommitdiff
path: root/spartan/lib
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/lib')
-rw-r--r--spartan/lib/elimination.ML38
-rw-r--r--spartan/lib/tactics.ML81
2 files changed, 85 insertions, 34 deletions
diff --git a/spartan/lib/elimination.ML b/spartan/lib/elimination.ML
index bd23c94..617f83e 100644
--- a/spartan/lib/elimination.ML
+++ b/spartan/lib/elimination.ML
@@ -1,38 +1,46 @@
(* Title: elimination.ML
Author: Joshua Chen
-Type elimination automation.
+Type elimination setup.
*)
-structure Elim = struct
+structure Elim: sig
+
+val rules: Proof.context -> (thm * indexname list) list
+val lookup_rule: Proof.context -> Termtab.key -> (thm * indexname list) option
+val register_rule: term list -> thm -> Context.generic -> Context.generic
+
+end = struct
(** Context data **)
+
(* Elimination rule data *)
+
+(*Stores elimination rules together with a list of the indexnames of the
+ variables each rule eliminates. Keyed by head of the type being eliminated.*)
structure Rules = Generic_Data (
- type T = thm Termtab.table
+ type T = (thm * indexname list) Termtab.table
val empty = Termtab.empty
val extend = I
- val merge = Termtab.merge Thm.eq_thm_prop
+ val merge = Termtab.merge (eq_fst Thm.eq_thm_prop)
)
-fun register_rule rl =
+fun rules ctxt = map (op #2) (Termtab.dest (Rules.get (Context.Proof ctxt)))
+fun lookup_rule ctxt = Termtab.lookup (Rules.get (Context.Proof ctxt))
+fun register_rule tms rl =
let val hd = Term.head_of (Lib.type_of_typing (Thm.major_prem_of rl))
- in Rules.map (Termtab.update (hd, rl)) end
+ in Rules.map (Termtab.update (hd, (rl, map (#1 o dest_Var) tms))) end
-fun get_rule ctxt = Termtab.lookup (Rules.get (Context.Proof ctxt))
-fun rules ctxt = map (op #2) (Termtab.dest (Rules.get (Context.Proof ctxt)))
-
-(* Set up [elims] attribute *)
+(* [elims] attribute *)
val _ = Theory.setup (
Attrib.setup \<^binding>\<open>elims\<close>
- (Scan.lift (Scan.succeed (Thm.declaration_attribute register_rule))) ""
+ (Scan.repeat Args.term_pattern >>
+ (Thm.declaration_attribute o register_rule))
+ ""
#> Global_Theory.add_thms_dynamic (\<^binding>\<open>elims\<close>,
- fn context => (rules (Context.proof_of context)))
+ fn context => (map #1 (rules (Context.proof_of context))))
)
-(** General elimination-induction tactic **)
-
-
end
diff --git a/spartan/lib/tactics.ML b/spartan/lib/tactics.ML
index c72947a..024abc1 100644
--- a/spartan/lib/tactics.ML
+++ b/spartan/lib/tactics.ML
@@ -4,7 +4,7 @@
General tactics for dependent type theory.
*)
-structure Tactics:
+structure Tactics(* :
sig
val assumptions_tac: Proof.context -> int -> tactic
@@ -18,7 +18,7 @@ val intro_tac: Proof.context -> int -> tactic
val intros_tac: Proof.context -> int -> tactic
val elims_tac: term option -> Proof.context -> int -> tactic
-end = struct
+end *) = struct
(*An assumption tactic that only solves typing goals with rigid terms and
judgmental equalities without schematic variables*)
@@ -56,25 +56,22 @@ fun typechk_tac ctxt =
let val net = Tactic.build_net
((Named_Theorems.get ctxt \<^named_theorems>\<open>typechk\<close>)
@(Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>)
- @(Elim.rules ctxt))
+ @(map #1 (Elim.rules ctxt)))
in (resolve_from_net_tac ctxt net) i end
else no_tac)
in
- CHANGED o REPEAT o REPEAT_ALL_NEW (known_tac ctxt ORELSE' tac)
+ REPEAT_ALL_NEW (known_tac ctxt ORELSE' tac)
end
(*Many methods try to automatically discharge side conditions by typechecking.
Switch this flag off to discharge by non-unifying assumption instead.*)
val auto_typechk = Attrib.setup_config_bool \<^binding>\<open>auto_typechk\<close> (K true)
+fun side_cond_tac ctxt = CHANGED o REPEAT o
+ (if Config.get ctxt auto_typechk then typechk_tac ctxt else known_tac ctxt)
+
(*Combinator runs tactic and tries to discharge all new typing side conditions*)
-fun SIDE_CONDS tac ctxt =
- let
- val side_cond_tac =
- if Config.get ctxt auto_typechk then typechk_tac ctxt else known_tac ctxt
- in
- tac THEN_ALL_NEW (TRY o side_cond_tac)
- end
+fun SIDE_CONDS tac ctxt = tac THEN_ALL_NEW (TRY o side_cond_tac ctxt)
local
fun mk_rules _ ths [] = ths
@@ -87,13 +84,11 @@ fun mk_rules _ ths [] = ths
in
(*Resolves with given rules, discharging as many side conditions as possible*)
-fun rule_tac ths ctxt =
- SIDE_CONDS (resolve_tac ctxt (mk_rules 0 [] ths)) ctxt
+fun rule_tac ths ctxt = resolve_tac ctxt (mk_rules 0 [] ths)
(*Attempts destruct-resolution with the n-th premise of the given rules*)
-fun dest_tac opt_n ths ctxt = SIDE_CONDS (dresolve_tac ctxt
- (mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths))
- ctxt
+fun dest_tac opt_n ths ctxt = dresolve_tac ctxt
+ (mk_rules (case opt_n of NONE => 0 | SOME 0 => 0 | SOME n => n-1) [] ths)
end
@@ -107,17 +102,17 @@ fun intros_tac ctxt = SUBGOAL (fn (_, i) =>
(*Basic elimination tactic, only uses existing type judgments from the context
(performs no type synthesis)*)
fun elims_tac opt_tm ctxt = case opt_tm of
- NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (Elim.rules ctxt) i)
+ NONE => SUBGOAL (fn (_, i) => eresolve_tac ctxt (map #1 (Elim.rules ctxt)) i)
| SOME tm => SUBGOAL (fn (goal, i) =>
let
fun elim_rule typing =
let
val hd = head_of (Lib.type_of_typing typing)
- val opt_rl = Elim.get_rule ctxt hd
+ val opt_rl = Elim.lookup_rule ctxt hd
in
case opt_rl of
NONE => Drule.dummy_thm
- | SOME rl => Drule.infer_instantiate' ctxt
+ | SOME (rl, _) => Drule.infer_instantiate' ctxt
[SOME (Thm.cterm_of ctxt tm)] rl
end
@@ -137,6 +132,54 @@ fun elims_tac opt_tm ctxt = case opt_tm of
ORELSE' eresolve_tac ctxt candidate_rules') i
end)
+(* Revamped general induction/elimination *)
+
+(*Pushes a context/goal premise typing t:T into a \<Prod>-type*)
+fun internalize_fact_tac t =
+ Subgoal.FOCUS_PARAMS (fn {context = ctxt, concl = raw_concl, ...} =>
+ let
+ val concl = Logic.strip_assums_concl (Thm.term_of raw_concl)
+ val C = Lib.type_of_typing concl
+ val B = Thm.cterm_of ctxt (Lib.lambda_var t C)
+ val a = Thm.cterm_of ctxt t
+ (*The resolvent is PiE[where ?B=B and ?a=a]*)
+ val resolvent =
+ 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 (known_tac ctxt)
+ end)
+
+fun elim_tac' tms ctxt = case tms of
+ [] => SUBGOAL (fn (_, i) => eresolve_tac ctxt (map #1 (Elim.rules ctxt)) i)
+ | major::_ => SUBGOAL (fn (goal, i) =>
+ let
+ val template = Lib.typing_of_term major
+ val facts = Proof_Context.facts_of ctxt
+ val prems = Logic.strip_assums_hyp goal
+ val types =
+ map (Thm.prop_of o #1) (Facts.could_unify facts template)
+ @ filter (fn prem => Term.could_unify (template, prem)) prems
+ |> map Lib.type_of_typing
+ in case types of
+ [] => no_tac
+ | _ =>
+ let
+ val rule_insts = map ((Elim.lookup_rule ctxt) o Term.head_of) types
+ val rules = flat (map
+ (fn rule_inst => case rule_inst of
+ NONE => []
+ | SOME (rl, idxnames) => [Drule.infer_instantiate ctxt
+ (idxnames ~~ map (Thm.cterm_of ctxt) tms) rl])
+ rule_insts)
+ in
+ resolve_tac ctxt rules i
+ THEN RANGE (replicate (length tms) (typechk_tac ctxt)) 1
+ end handle Option => no_tac
+ end)
+
+
end
open Tactics
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 06:28:53 +0000