Crush improvements: add wp split rules, automatic eta-expansion, more branch control

Various improvements to crush proof automation:
1. Definitions added to `simp [prems,concls] add:` now work for definitions of the
form `some_def \equiv \lambda x. `: these are now automatically eta-expanded
2. Add a `wp split:` parameter to `crush`. This accepts the same arguments as
`split:`, but only applies them when the top-level expression in a WP statement
get stuck on the split.
3. Guard the crush branches `crush_branch_base_simps_early_unfold` and
`crush_branch_base_detect_aentails_contradiction` with a configuration option. This
is helpful when debugging/speeding up long-running crush calls.
4. Change SSA normalization from top-down to bottom-up. This avoids having to define
new SSA rules for additional datatypes.
5. No longer drop premises marked `ASSUMPTION` in the MePo filter
6. Add a configuration option `crush_stop_at_full_blown_clarsimp` to make crush stop
whenever it would otherwise apply a full-blown clarsimp. This makes it easier to
figure out why such last-resort full-blown clarsimps happen.

Signed-off-by: Ike Mulder <ikemul@amazon.com>

Author: hanno-becker

Crush/Examples.thy

@@ -646,6 +646,19 @@ lemma
   irrelevant premises:\<close>
   apply (tactic \<open>MePo_Prem.drop_irrelevant_prems_tac @{context} 2 1\<close>)
   oops
+
+\<comment>\<open>The MePo filter never drops premises wrapped as \<^verbatim>\<open>ASSUMPTION\<close>:\<close>
+lemma 
+  assumes \<open>x < 42\<close>
+      and \<open>ASSUMPTION (g (g (f t0)) = s0)\<close>
+      and \<open>g (f t1) = s1\<close>
+      and \<open>x + y < 10*z\<close>
+    shows \<open>10*z < 20\<close>
+  using assms apply -
+  \<comment>\<open>Keeps \<^verbatim>\<open>(g (g (f t0)) = s0)\<close> which would otherwise have been thrown out.\<close>
+  apply (tactic \<open>MePo_Prem.ignore_irrelevant_prems_tac @{context} 2 1\<close>)
+  oops
+
 end
 
 subsubsection\<open>Conversions\<close>

Crush/Separation_Logic_Tactics.thy

@@ -29,6 +29,7 @@ ML\<open>
    val _ =  Theory.setup (Named_Theorems.declare @{binding "crush_concls_simps"}      "" #> snd |> Named_Target.theory_map)
    val _ =  Theory.setup (Named_Theorems.declare @{binding "crush_aentails_rules"}    "" #> snd |> Named_Target.theory_map)
    val _ =  Theory.setup (Named_Theorems.declare @{binding "crush_aentails_drules"}   "" #> snd |> Named_Target.theory_map)
+   val _ =  Theory.setup (Named_Theorems.declare @{binding "crush_wp_split_simps"}    "" #> snd |> Named_Target.theory_map)
    val _ =  Theory.setup (Named_Theorems.declare @{binding "crush_aentails_crules"}   "" #> snd |> Named_Target.theory_map)
    val _ =  Theory.setup (Named_Theorems.declare @{binding "crush_asepconj_simp"}     "" #> snd |> Named_Target.theory_map)
    val _ =  Theory.setup (Named_Theorems.declare @{binding "crush_specs_eager"}       "" #> snd |> Named_Target.theory_map)

Crush/base.ML

@@ -65,6 +65,10 @@ sig
  val force_meta_eq : thm -> thm
  val force_meta_eqs : thm list -> thm list
 
+ \<comment>\<open>Eta expand definitional theorem so there's no toplevel \<^verbatim>\<open>\<lambda>x. _\<close> on the RHS\<close>
+ val eta_expand: thm -> thm 
+ val eta_expands: thm list -> thm list  
+
  val intro_tac : thm list -> Proof.context -> int -> tactic
  val elim_tac : thm list -> Proof.context -> int -> tactic
 
@@ -424,6 +428,20 @@ struct
   fun force_meta_eq (t : thm): thm = t RS eq_reflection handle THM _ => t
   val force_meta_eqs : thm list -> thm list = List.map force_meta_eq
 
+  fun eta_expand thm =
+    let
+      val num_abs = thm 
+        |> Thm.prop_of 
+        |> Logic.dest_equals 
+        |> snd 
+        |> Term.strip_abs 
+        |> fst 
+        |> length      
+    in
+      funpow num_abs (fn t => t RS @{thm meta_fun_cong}) thm
+    end
+  val eta_expands : thm list -> thm list = List.map eta_expand
+
   fun filter_to_conv (f : cterm -> bool) : conv = fn t =>
      if f t then Conv.all_conv t else Conv.no_conv t
 
@@ -533,6 +551,9 @@ local
   val _ = Theory.setup (Attrib.setup @{binding "meta_all_intro"}
                        (Thm.rule_attribute [] (K Thm.forall_intr_vars) |> Scan.succeed) "")
 
+  val _ = Theory.setup (Attrib.setup @{binding "unabs_def"}
+                       (Thm.rule_attribute [] (K Crush_Base.eta_expand) |> Scan.succeed) "")
+
   fun all_intro ctxt thm = 
      let val ctxt = Context.proof_of ctxt
          val thm' = Thm.forall_intr_vars thm

Crush/config.ML

@@ -57,11 +57,16 @@ sig
 
   val enable_branch_safe : bool Config.T
   val enable_branch_clarsimp : bool Config.T
+  val enable_branch_clarsimp_warn_at_success : bool Config.T
+  val enable_branch_clarsimp_stop_at_success : bool Config.T
   val enable_branch_filtered_clarsimp : bool Config.T
   val enable_branch_reduced_clarsimp : bool Config.T
   val enable_schematics : bool Config.T
   val enable_branch_split : bool Config.T
 
+  val enable_base_simps_detect_aentails_contradiction : bool Config.T
+  val enable_base_simps_early_unfold : bool Config.T
+
   val enable_urust_split_branch : bool Config.T
   val enable_urust_determine_branch : bool Config.T
 
@@ -118,6 +123,8 @@ struct
 
   val enable_branch_safe = Attrib.setup_config_bool @{binding "use_safe"} (K true)
   val enable_branch_clarsimp = Attrib.setup_config_bool @{binding "crush_use_clarsimp"} (K true)
+  val enable_branch_clarsimp_stop_at_success = Attrib.setup_config_bool @{binding "crush_stop_at_full_blown_clarsimp"} (K false)
+  val enable_branch_clarsimp_warn_at_success = Attrib.setup_config_bool @{binding "crush_warn_at_full_blown_clarsimp"} (K true)
   (* TODO: Consider enabling this by default *)
   val enable_branch_filtered_clarsimp = Attrib.setup_config_bool @{binding "crush_use_filtered_clarsimp"} (K false)
   (* TODO: Consider enabling this by default *)
@@ -143,6 +150,9 @@ struct
 
   val fail_on_bad_schematic = Attrib.setup_config_bool @{binding "crush_fail_on_bad_schematic"} (K true)
 
+  val enable_base_simps_early_unfold = Attrib.setup_config_bool @{binding "crush_enable_early_unfold"} (K true)
+  val enable_base_simps_detect_aentails_contradiction = Attrib.setup_config_bool @{binding "crush_enable_contradiction_detection"} (K true)
+
   val relevance_filter_max_facts = Attrib.setup_config_int @{binding "crush_relevance_filter_max_facts"} (K 20)
 
   val simp_general_implies_prems = Attrib.setup_config_bool @{binding "crush_simp_general_implies_prems"} (K false)

Crush/crush.ML

@@ -150,6 +150,13 @@ struct
 
   val get_urust_contract_simpset = Context.Proof #> URustContractSimps.get
 
+  val crush_register_wp_split_attrib = Thm.declaration_attribute (fn t => fn ctxt =>
+    let val t' = Separation_Logic_Tactics.specialize_split_rule_to_wp_single
+                   (Context.proof_of ctxt) t
+    in ctxt |> Named_Theorems.add_thm @{named_theorems "crush_wp_split_simps"} t'
+    end
+  )  
+
   val simp_focus_basic_tac : Proof.context -> int -> tactic = fn ctxt =>
     let val focus_intros =
       Named_Theorems.get ctxt @{named_theorems focus_intros} @
@@ -173,17 +180,23 @@ struct
 
   val crush_branch_base_simps_early_unfold : Proof.context -> int -> tactic = fn ctxt =>
     let val early_simps = Named_Theorems.get ctxt @{named_theorems crush_early_simps}
-      val congs = Named_Theorems.get ctxt @{named_theorems "crush_cong"}
+      val congs = Named_Theorems.get ctxt @{named_theorems "crush_cong"}      
     in
-      safe_unfold_tac' ctxt congs early_simps
+      if Config.get ctxt Crush_Config.enable_base_simps_early_unfold then
+        safe_unfold_tac' ctxt congs early_simps
+      else
+        K no_tac
     end
 
   val crush_branch_base_detect_aentails_contradiction: Proof.context -> int -> tactic = fn ctxt =>
-    IF' Separation_Logic_Tactics.is_entailment (
-      let val congs = Named_Theorems.get ctxt @{named_theorems "crush_cong"} in
-      CHANGED_PROP o (safe_simp_no_asm_only_tac' ctxt congs @{thms asepconj_bot_zero asepconj_bot_zero2})
-      THEN' TRY o resolve_tac ctxt @{thms bot_aentails_all} end
-    )
+    if Config.get ctxt Crush_Config.enable_base_simps_detect_aentails_contradiction then
+      IF' Separation_Logic_Tactics.is_entailment (
+        let val congs = Named_Theorems.get ctxt @{named_theorems "crush_cong"} in
+        CHANGED_PROP o (safe_simp_no_asm_only_tac' ctxt congs @{thms asepconj_bot_zero asepconj_bot_zero2})
+        THEN' TRY o resolve_tac ctxt @{thms bot_aentails_all} end
+      )
+    else
+      K no_tac
 
   val crush_branch_base_simps_tac : Proof.context -> int -> tactic = fn ctxt =>
     let val crush_intros = Named_Theorems.get ctxt @{named_theorems crush_intros}
@@ -219,9 +232,12 @@ struct
 
   val crush_branch_wp_case_split_tac_core : Proof.context -> int -> tactic = fn ctxt =>
     if not (Config.get ctxt Crush_Config.enable_urust_split_branch) then K no_tac else
-    let val wp_intros = Named_Theorems.get ctxt @{named_theorems micro_rust_wp_case_splits}
+    let val wp_split_intros = Named_Theorems.get ctxt @{named_theorems micro_rust_wp_case_splits}
+      val wp_split_simps = Named_Theorems.get ctxt @{named_theorems crush_wp_split_simps}
+        |> force_meta_eqs
     in
-      intro_tac wp_intros ctxt
+      intro_tac wp_split_intros ctxt ORELSE' 
+      CONVERSION (Conv.params_conv ~1 (fn _ => (Conv.concl_conv ~1 (prop_conv (Conv.rewrs_conv wp_split_simps)))) ctxt)
     end
 
   val crush_branch_wp_case_split_tac : Proof.context -> int -> tactic = fn ctxt =>
@@ -392,9 +408,33 @@ struct
     end
 
   val crush_branch_clarsimp_fallback_tac = fn ctxt =>
-   if Config.get ctxt Crush_Config.enable_branch_clarsimp then
-     CHANGED_PROP o clarsimp_tac ctxt
-   else K no_tac
+   let fun log_before_after old_goal new_goal_opt =
+      (let val old_txt = 
+             [Pretty.str "Needed to apply full-blown clarsimp to progress the following pure goal:", Pretty.brk 1,
+              Syntax.pretty_term ctxt old_goal, Pretty.fbrk] in
+       if Config.get ctxt Crush_Config.enable_branch_clarsimp_stop_at_success then
+         ((old_txt @ [Pretty.fbrk, Pretty.str "Aborting as requested by `crush_stop_at_full_blown_clarsimp` option"]
+          |> Pretty.block |> Pretty.string_of |> Output.warning);
+          raise SMART "Stopping after successful clarsimp -- consider debugging why MePo-filtered clarsimp didn't work!")
+       else if old_goal |> Separation_Logic_Tactics.is_entailment |> not
+         andalso Config.get ctxt Crush_Config.enable_branch_clarsimp_warn_at_success then 
+         let 
+           val new_txt = case new_goal_opt of 
+              NONE => [Pretty.str "Goal was solved"]
+            | SOME new_goal => [Pretty.str "New goal: ", Pretty.fbrk,
+                                Syntax.pretty_term ctxt new_goal]
+         in
+           old_txt @ new_txt @ 
+            [Pretty.fbrk, Pretty.str "Consider debugging why MePo-filtered clarsimp is not successful here.", Pretty.fbrk,
+             Pretty.str "If you want to stop `crush` at this point, set `crush_stop_at_full_blown_clarsimp=true` and `crush_do_big_steps=false`"]
+           |> Pretty.block |> Pretty.string_of |> Output.warning
+         end
+      else () end)
+   in
+     if Config.get ctxt Crush_Config.enable_branch_clarsimp then
+       DEBUG_BEFORE_AFTER' log_before_after (CHANGED_PROP o clarsimp_tac ctxt)
+     else K no_tac
+   end
 
   val crush_branch_misc_tac : Proof.context -> int -> tactic = fn ctxt =>
              intro_tac @{thms mset_sub_drop_nth word_unat_lt} ctxt
@@ -731,6 +771,7 @@ struct
      make_del_parser "intro"     @{named_theorems crush_intros} \<^here>,
      make_add_parser "specs"     @{named_theorems crush_specs} \<^here>,
      make_del_parser "specs"     @{named_theorems crush_specs} \<^here>,
+     make_attrib_parser (Args.$$$ "wp" -- Args.$$$ "split") \<^here> (K crush_register_wp_split_attrib),
      make_attrib_parser (Args.$$$ "contracts" -- Args.add) \<^here> (K (crush_register_contract_attrib false)),
      make_attrib_parser (Args.$$$ "contracts" -- Args.del) \<^here> (K (crush_register_contract_attrib true)),
      make_add_parser "cong"     @{named_theorems crush_cong} \<^here>,

Crush/mepo_prem.ML

@@ -33,6 +33,8 @@ sig
  (* reverse the action of ignore_tac_idxs_xxx *)
  val unignore_tac : Proof.context -> int -> tactic
 
+ val matching_prems : Proof.context -> thm -> (term -> bool) -> int -> int list
+
  val relevant_prems_core : Proof.context -> int ->
     relevance_fudge option -> term -> (int * term) list -> (int * term) list
 
@@ -57,6 +59,22 @@ end;
 structure MePo_Prem: MEPO_PREM =
 struct
 
+  fun enumerate ls =
+    let
+      fun aux _ acc [] = List.rev acc
+        | aux base acc (x :: xs) = aux (base + 1) ((base, x) :: acc) xs
+    in
+      aux 0 [] ls
+    end
+
+  fun matching_prems (_: Proof.context) (thm: thm) (prem_filter: term -> bool) i =
+    let
+      val subgoal = Thm.cprem_of thm i |> Thm.term_of
+      val prems = Logic.strip_imp_prems subgoal
+    in
+      prems |> enumerate |> filter (snd #> prem_filter) |> map fst
+    end
+
   val ignore_tac0 : Proof.context -> int -> tactic = fn ctxt =>
     DETERM o (eresolve_tac ctxt [@{thm IGNORE_imp_ignoreE}])
 
@@ -189,11 +207,20 @@ fun add_pconst_to_table (s, p) = Symtab.map_default (s, [p]) (insert ptype_eq p)
    more or less as if they were built-in but add their axiomatization at the end. *)
 val set_consts = [\<^const_name>\<open>Collect\<close>, \<^const_name>\<open>Set.member\<close>]
 
+val ignore_consts = [\<^const_name>\<open>ASSUMPTION\<close>]
+
+fun mepo_keep_premise_filter t = (case t of 
+   \<^Const_>\<open>Trueprop for t1\<close> => mepo_keep_premise_filter t1
+ | \<^Const_>\<open>ASSUMPTION for _\<close> => true
+ | _ => false)
+
 fun add_pconsts_in_term thy =
   let
     fun do_const const (x as (s, _)) ts =
       if member (op =) set_consts s then
         fold (do_term false) ts
+      else if member (op =) ignore_consts s then
+        I
       else
         (not (is_irrelevant_const s) ? add_pconst_to_table (rich_pconst thy const x))
         #> fold (do_term false) ts
@@ -255,6 +282,7 @@ fun pconsts_in_fact thy t =
     []
 
 fun pair_consts_fact' thy term_of_fact fact =
+  if mepo_keep_premise_filter (fact |> term_of_fact) then NONE else
   (case fact |> term_of_fact |> pconsts_in_fact thy of
     [] => NONE
   | consts => SOME ((fact, consts), NONE))
@@ -517,14 +545,6 @@ fun relevance_filter_generic ctxt thres0 decay max_facts (term_of_fact: 'a -> te
        relevance_filter' ctxt thres0 decay max_facts fudge facts concl_t)
   end
 
-  fun enumerate ls =
-    let
-      fun aux _ acc [] = List.rev acc
-        | aux base acc (x :: xs) = aux (base + 1) ((base, x) :: acc) xs
-    in
-      aux 0 [] ls
-    end
-
   fun subst_abs_constify v b = subst_bound (v |> apfst wrap_bound_name |> Const, b);
 
   fun dest_abs_constify t =
@@ -582,11 +602,15 @@ fun relevance_filter_generic ctxt thres0 decay max_facts (term_of_fact: 'a -> te
       aux a b [] exclude
     end
 
+  fun sorted_union (a : int list) (b : int list) : int list = a @ b |> sort int_ord
+
   fun irrelevant_prems_in_goal ctxt max_facts fudge i thm =
     let
       val (nprems, relevant_prems_idxs) = relevant_prems_in_goal ctxt max_facts fudge i thm
+      val force_relevant_idxs = matching_prems ctxt thm mepo_keep_premise_filter i
+      val all_relevant_prems = sorted_union relevant_prems_idxs force_relevant_idxs
     in
-      (nprems, upto_without 0 (nprems - 1) relevant_prems_idxs)
+      (nprems, upto_without 0 (nprems - 1) all_relevant_prems)
     end
     handle THM _ => (0, [])