aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-05-26 16:50:13 +0200
committerJosh Chen2020-05-26 16:50:13 +0200
commit028f43a0737128024742234f3ee95b24986d6403 (patch)
tree566ea92495d93db334fda605af1e8e598cf4bc41
parent8ba8357a0b4640a3be817fd0645d026b568bc552 (diff)
1. New congruence declarations for calculational reasoning. 2. Remove old elimination tactic.
Diffstat (limited to '')
-rw-r--r--spartan/core/Spartan.thy12
-rw-r--r--spartan/core/congruence.ML90
-rw-r--r--spartan/core/tactics.ML41
3 files changed, 87 insertions, 56 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 50002a6..1d93885 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -8,8 +8,9 @@ imports
keywords
"Theorem" "Lemma" "Corollary" "Proposition" :: thy_goal_stmt and
"focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and
- "derive" "prems" "vars":: quasi_command and
- "print_coercions" :: thy_decl
+ "congruence" "print_coercions" :: thy_decl and
+ "rhs" "derive" "prems" "vars" :: quasi_command
+
begin
@@ -154,7 +155,8 @@ ML_file \<open>focus.ML\<close>
section \<open>Congruence automation\<close>
-(*Potential to be retired*)
+consts "rhs" :: \<open>'a\<close> ("..")
+
ML_file \<open>congruence.ML\<close>
@@ -186,10 +188,6 @@ method_setup intro =
method_setup intros =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (intros_tac ctxt)))\<close>
-method_setup old_elim =
- \<open>Scan.option Args.term >> (fn tm => fn ctxt =>
- SIMPLE_METHOD' (SIDE_CONDS (old_elims_tac tm ctxt) ctxt))\<close>
-
method_setup elim =
\<open>Scan.repeat Args.term >> (fn tms => fn ctxt =>
CONTEXT_METHOD (K (elim_context_tac tms ctxt 1)))\<close>
diff --git a/spartan/core/congruence.ML b/spartan/core/congruence.ML
index bb7348c..d9f4ffa 100644
--- a/spartan/core/congruence.ML
+++ b/spartan/core/congruence.ML
@@ -1,16 +1,82 @@
-signature Sym_Attr_Data =
-sig
- val name: string
- val symmetry_rule: thm
-end
+structure Congruence = struct
+
+(* Congruence context data *)
-functor Sym_Attr (D: Sym_Attr_Data) =
-struct
- local
- val distinct_prems = the_single o Seq.list_of o Tactic.distinct_subgoals_tac
+structure RHS = Generic_Data (
+ type T = (term * indexname) Termtab.table
+ val empty = Termtab.empty
+ val extend = I
+ val merge = Termtab.merge (Term.aconv o apply2 #1)
+)
+
+fun register_rhs t var =
+ let
+ val key = Term.head_of t
+ val idxname = #1 (dest_Var var)
in
- val attr = Thm.rule_attribute []
- (K (fn th => distinct_prems (th RS D.symmetry_rule) handle THM _ => th))
- val setup = Attrib.setup (Binding.name D.name) (Scan.succeed attr) ""
+ RHS.map (Termtab.update (key, (t, idxname)))
end
+
+fun lookup_congruence ctxt t =
+ Termtab.lookup (RHS.get (Context.Proof ctxt)) (Term.head_of t)
+
+
+(* Congruence declarations *)
+
+local val Frees_to_Vars =
+ map_aterms (fn tm =>
+ case tm of
+ Free (name, T) => Var (("*!"^name, 0), T) (*Hacky naming!*)
+ | _ => tm)
+in
+
+(*Declare the "right-hand side" of types that are congruences.
+ Does not handle bound variables, so no dependent RHS in declarations!*)
+val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>congruence\<close>
+ "declare right hand side of congruence"
+ (Parse.term -- (\<^keyword>\<open>rhs\<close> |-- Parse.term) >>
+ (fn (t_str, rhs_str) => fn lthy =>
+ let
+ val (t, rhs) = apply2 (Frees_to_Vars o Syntax.read_term lthy)
+ (t_str, rhs_str)
+ in lthy |>
+ Local_Theory.background_theory (
+ Context.theory_map (register_rhs t rhs))
+ end))
+
+end
+
+
+(* Calculational reasoning: ".." setup *)
+
+fun last_rhs ctxt = map_aterms (fn t =>
+ case t of
+ Const (\<^const_name>\<open>rhs\<close>, _) =>
+ let
+ val this_name = Name_Space.full_name (Proof_Context.naming_of ctxt)
+ (Binding.name Auto_Bind.thisN)
+ val this = #thms (the (Proof_Context.lookup_fact ctxt this_name))
+ handle Option => []
+ val rhs =
+ (case map Thm.prop_of this of
+ [prop] =>
+ (let
+ val typ = Lib.type_of_typing (Logic.strip_assums_concl prop)
+ val (cong_pttrn, varname) = the (lookup_congruence ctxt typ)
+ val unif_res = Pattern.unify (Context.Proof ctxt)
+ (cong_pttrn, typ) Envir.init
+ val rhs = #2 (the
+ (Vartab.lookup (Envir.term_env unif_res) varname))
+ in
+ rhs
+ end handle Option =>
+ error (".. can't match right-hand side of congruence"))
+ | _ => Term.dummy)
+ in rhs end
+ | _ => t)
+
+val _ = Context.>>
+ (Syntax_Phases.term_check 5 "" (fn ctxt => map (last_rhs ctxt)))
+
+
end
diff --git a/spartan/core/tactics.ML b/spartan/core/tactics.ML
index f23bfee..0e7db43 100644
--- a/spartan/core/tactics.ML
+++ b/spartan/core/tactics.ML
@@ -4,7 +4,7 @@
General tactics for dependent type theory.
*)
-structure Tactics(* :
+structure Tactics:
sig
val assumptions_tac: Proof.context -> int -> tactic
@@ -16,9 +16,9 @@ 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 old_elims_tac: term option -> Proof.context -> int -> tactic
+val elim_context_tac: term list -> Proof.context -> int -> context_tactic
-end *) = struct
+end = struct
(*An assumption tactic that only solves typing goals with rigid terms and
judgmental equalities without schematic variables*)
@@ -99,40 +99,7 @@ fun intro_tac ctxt = SUBGOAL (fn (_, i) => SIDE_CONDS
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 old_elims_tac opt_tm ctxt = case opt_tm of
- 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.lookup_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)
-
-(* Revamped general induction/elimination *)
+(* Induction/elimination *)
(*Pushes a context/goal premise typing t:T into a \<Prod>-type*)
fun internalize_fact_tac t =