new work on elimination tactic

5 files changed, 113 insertions, 42 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
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 \<circ> (id B)" id_right[symmetric])
           apply (rewrite to "(id A) \<circ> h" id_left[symmetric])
-          by (rule homotopy_transitive) (assumption, typechk)
+          by (rule homotopy_transitive) (assumption+, typechk)
 
         then have "f \<circ> g ~ f \<circ> 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 \<open>../lib/elimination.ML\<close> \<comment> \<open>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 \<open>
+val ctxt = @{context};
+val typing = @{term "t: \<Sum>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
+\<close>
+
 ML_file \<open>../lib/tactics.ML\<close>
 
 method_setup assumptions =
@@ -180,25 +195,30 @@ method_setup intro =
 method_setup intros =
   \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\<close>
 
-method_setup elim =
+method_setup elim' =
   \<open>Scan.option Args.term >> (fn tm => fn ctxt =>
     SIMPLE_METHOD' (SIDE_CONDS (elims_tac tm ctxt) ctxt))\<close>
 
+method_setup elim =
+  \<open>Scan.repeat Args.term >> (fn tms => fn ctxt =>
+    SIMPLE_METHOD' (SIDE_CONDS (elim_tac' tms ctxt) ctxt))\<close>
+
 method elims = elim+
 
 (*This could possibly use additional simplification hints via a simp: modifier*)
 method_setup typechk =
-  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (
-    CHANGED (ALLGOALS (TRY o typechk_tac ctxt))))\<close>
+  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (
+    SIDE_CONDS (typechk_tac ctxt) ctxt))
+    (* CHANGED (ALLGOALS (TRY o typechk_tac ctxt)))) *)\<close>
 
 method_setup rule =
   \<open>Attrib.thms >> (fn ths => fn ctxt =>
-    SIMPLE_METHOD (HEADGOAL (rule_tac ths ctxt)))\<close>
+    SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (rule_tac ths ctxt) ctxt)))\<close>
 
 method_setup dest =
   \<open>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)))\<close>
+        SIMPLE_METHOD (HEADGOAL (SIDE_CONDS (dest_tac opt_n ths ctxt) ctxt)))\<close>
 
 subsection \<open>Rewriting\<close>