Brand-spanking new version using Spartan infrastructure

1 files changed, 143 insertions, 0 deletions

diff --git a/spartan/lib/tactics.ML b/spartan/lib/tactics.ML
new file mode 100644
index 0000000..0e09533
--- /dev/null
+++ b/spartan/lib/tactics.ML
@@ -0,0 +1,143 @@
+(*  Title:      tactics.ML
+    Author:     Joshua Chen
+
+General tactics for dependent type theory.
+*)
+
+structure Tactics:
+sig
+
+val assumptions_tac: Proof.context -> int -> tactic
+val known_tac: Proof.context -> int -> tactic
+val typechk_tac: Proof.context -> int -> tactic
+val auto_typechk: bool Config.T
+val SIDE_CONDS: (int -> tactic) -> Proof.context -> int -> tactic
+val rule_tac: thm list -> Proof.context -> int -> tactic
+val dest_tac: int option -> thm list -> Proof.context -> int -> tactic
+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
+
+(*An assumption tactic that only solves typing goals with rigid terms and
+  judgmental equalities without schematic variables*)
+fun assumptions_tac ctxt = SUBGOAL (fn (goal, i) =>
+  let
+    val concl = Logic.strip_assums_concl goal
+  in
+    if
+      Lib.is_typing concl andalso Lib.is_rigid (Lib.term_of_typing concl)
+      orelse not ((exists_subterm is_Var) concl)
+    then assume_tac ctxt i
+    else no_tac
+  end)
+
+(*Solves typing goals with rigid term by resolving with context facts and
+  simplifier premises, or arbitrary goals by *non-unifying* assumption*)
+fun known_tac ctxt = SUBGOAL (fn (goal, i) =>
+  let
+    val concl = Logic.strip_assums_concl goal
+  in
+    ((if Lib.is_typing concl andalso Lib.is_rigid (Lib.term_of_typing concl)
+      then
+        let val ths = map fst (Facts.props (Proof_Context.facts_of ctxt))
+        in resolve_tac ctxt (ths @ Simplifier.prems_of ctxt) end
+      else K no_tac)
+    ORELSE' assumptions_tac ctxt) i
+  end)
+
+(*Typechecking: try to solve goals of the form "a: A" where a is rigid*)
+fun typechk_tac ctxt =
+  let
+    val tac = SUBGOAL (fn (goal, i) =>
+      if Lib.rigid_typing_concl goal
+      then
+        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))
+        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)
+  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)
+
+(*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
+
+local
+fun mk_rules _ ths [] = ths
+  | mk_rules n ths ths' =
+      let val ths'' = foldr1 (op @)
+        (map (fn th => [rotate_prems n (th RS @{thm PiE})] handle THM _ => []) ths')
+      in
+        mk_rules n (ths @ ths') ths''
+      end
+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
+
+(*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
+
+end
+
+(*Applies some introduction rule*)
+fun intro_tac ctxt = SUBGOAL (fn (_, i) => SIDE_CONDS
+  (resolve_tac ctxt (Named_Theorems.get ctxt \<^named_theorems>\<open>intros\<close>)) ctxt i)
+
+fun intros_tac ctxt = SUBGOAL (fn (_, i) =>
+  (CHANGED o REPEAT o CHANGED o intro_tac ctxt) 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)
+  | 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
+          in
+            case opt_rl of
+              NONE => Drule.dummy_thm
+            | SOME rl => Drule.infer_instantiate' ctxt
+                [SOME (Thm.cterm_of ctxt tm)] rl
+          end
+
+        val template = Lib.typing_of_term tm
+
+        val facts = Proof_Context.facts_of ctxt
+        val candidate_typings = Facts.could_unify facts template
+        val candidate_rules =
+          map (elim_rule o Thm.prop_of o #1) candidate_typings
+
+        val prems = Logic.strip_assums_hyp goal
+        val candidate_typings' =
+          filter (fn prem => Term.could_unify (template, prem)) prems
+        val candidate_rules' = map elim_rule candidate_typings'
+      in
+        (resolve_tac ctxt candidate_rules
+        ORELSE' eresolve_tac ctxt candidate_rules') i
+      end)
+
+end
+
+open Tactics