From 3ad2f03f7dbc922e2c711241146db091d193003d Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sun, 24 May 2020 20:44:33 +0200 Subject: new work on elimination tactic --- hott/Nat.thy | 2 +- spartan/lib/elimination.ML | 38 +++++++++++-------- spartan/lib/tactics.ML | 81 ++++++++++++++++++++++++++++++---------- spartan/theories/Equivalence.thy | 2 +- spartan/theories/Identity.thy | 2 +- spartan/theories/Spartan.thy | 32 +++++++++++++--- 6 files changed, 114 insertions(+), 43 deletions(-) diff --git a/hott/Nat.thy b/hott/Nat.thy index 3d938cd..bd58fbc 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -39,7 +39,7 @@ where lemmas [intros] = NatF Nat_zero Nat_suc and - [elims] = NatE and + [elims "?n"] = NatE and [comps] = Nat_comp_zero Nat_comp_suc text \Non-dependent recursion\ 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>\elims\ - (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>\elims\, - 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>\typechk\) @(Named_Theorems.get ctxt \<^named_theorems>\intros\) - @(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>\auto_typechk\ (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 \-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 diff --git a/spartan/theories/Equivalence.thy b/spartan/theories/Equivalence.thy index 97cd18d..73f1e0d 100644 --- a/spartan/theories/Equivalence.thy +++ b/spartan/theories/Equivalence.thy @@ -276,7 +276,7 @@ Lemma (derive) biinv_imp_qinv: ultimately have "g ~ h" apply (rewrite to "g \ (id B)" id_right[symmetric]) apply (rewrite to "(id A) \ h" id_left[symmetric]) - by (rule homotopy_transitive) (assumption, typechk) + by (rule homotopy_transitive) (assumption+, typechk) then have "f \ g ~ f \ h" by (rule homotopy_funcomp_right) diff --git a/spartan/theories/Identity.thy b/spartan/theories/Identity.thy index 4a4cc40..3f16f4c 100644 --- a/spartan/theories/Identity.thy +++ b/spartan/theories/Identity.thy @@ -40,7 +40,7 @@ axiomatization where lemmas [intros] = IdF IdI and - [elims] = IdE and + [elims "?p" (*"?x" "?y"*)] = IdE and [comps] = Id_comp diff --git a/spartan/theories/Spartan.thy b/spartan/theories/Spartan.thy index 5274ea2..ab2606e 100644 --- a/spartan/theories/Spartan.thy +++ b/spartan/theories/Spartan.thy @@ -160,10 +160,25 @@ ML_file \../lib/elimination.ML\ \ \declares the [eli named_theorems intros and comps lemmas [intros] = PiF PiI SigF SigI and - [elims] = PiE SigE and + [elims "?f"] = PiE and + [elims "?p"] = SigE and [comps] = beta Sig_comp and [cong] = Pi_cong lam_cong Sig_cong +ML \ +val ctxt = @{context}; +val typing = @{term "t: \x: A. B x"}; +val insts = []; +let + val (eterm, typing) = Lib.dest_typing typing + val (rl, tms) = the (Elim.lookup_rule ctxt (Term.head_of typing)) +in + Drule.infer_instantiate @{context} + (tms ~~ map (Thm.cterm_of ctxt) (eterm::insts)) + rl +end +\ + ML_file \../lib/tactics.ML\ method_setup assumptions = @@ -180,25 +195,30 @@ method_setup intro = method_setup intros = \Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\ -method_setup elim = +method_setup elim' = \Scan.option Args.term >> (fn tm => fn ctxt => SIMPLE_METHOD' (SIDE_CONDS (elims_tac tm ctxt) ctxt))\ +method_setup elim = + \Scan.repeat Args.term >> (fn tms => fn ctxt => + SIMPLE_METHOD' (SIDE_CONDS (elim_tac' tms ctxt) ctxt))\ + method elims = elim+ (*This could possibly use additional simplification hints via a simp: modifier*) method_setup typechk = - \Scan.succeed (fn ctxt => SIMPLE_METHOD ( - CHANGED (ALLGOALS (TRY o typechk_tac ctxt))))\ + \Scan.succeed (fn ctxt => SIMPLE_METHOD' ( + SIDE_CONDS (typechk_tac ctxt) ctxt)) + (* CHANGED (ALLGOALS (TRY o typechk_tac ctxt)))) *)\ method_setup rule = \Attrib.thms >> (fn ths => fn ctxt => - SIMPLE_METHOD (HEADGOAL (rule_tac ths ctxt)))\ + SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (rule_tac ths ctxt) ctxt)))\ method_setup dest = \Scan.lift (Scan.option (Args.parens Parse.int)) -- Attrib.thms >> (fn (opt_n, ths) => fn ctxt => - SIMPLE_METHOD (HEADGOAL (dest_tac opt_n ths ctxt)))\ + SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (dest_tac opt_n ths ctxt) ctxt)))\ subsection \Rewriting\ -- cgit v1.2.3