Skip to content

Commit

Permalink
Abduction: Fix SeLFiE.
Browse files Browse the repository at this point in the history
  • Loading branch information
@yutakang
yutakang committed Aug 14, 2023
1 parent b500ac4 commit c17f045
Show file tree
Hide file tree
Showing 7 changed files with 82 additions and 31 deletions.
2 changes: 2 additions & 0 deletions Abduction/Abduction.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -115,5 +115,7 @@ val _ = theorem \<^command_keyword>\<open>prove\<close> "prove";

end;
\<close>
ML\<open>
\<close>
end
2 changes: 1 addition & 1 deletion Abduction/Abduction_Graph.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -359,7 +359,7 @@ fun print_lemma_and_proof_of_key (ctxt:Proof.context) (graph:abduction_graph) (k
(* print_proof_of_graph *)
fun print_proof_of_graph (pst:Proof.state) (graph:abduction_graph) =
let
val keys = PGraph.keys graph |> filter is_ornode |> rev : keys;
val keys = keys graph |> filter is_ornode |> rev : keys;
val key_prf_id_pairs = map (fn key => (key, proof_id_of graph key)) keys : (key * int option) list;
val key_prf_id_pairs_solved_only = filter (fn (_, id) => is_some id) key_prf_id_pairs : (key * int option) list;
val key_prf_id_pairs_wo_opt = map (apsnd the) key_prf_id_pairs_solved_only : (key * int) list;
Expand Down
7 changes: 5 additions & 2 deletions Abduction/All_Top_Down_Conjecturing.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
* Huawei Technologies Research & Development (UK) Limited.
*)
(*** structure All_Top_Down_Conjecturing ***)
structure All_Top_Down_Conjecturing: TOP_DOWN_CONJECTURING =
structure All_Top_Down_Conjecturing(*: TOP_DOWN_CONJECTURING*) =
struct

fun is_composite trm = Isabelle_Utils.is_Abs trm orelse Isabelle_Utils.is_App trm: bool;
Expand Down Expand Up @@ -62,8 +62,10 @@ fun template_conjectures (ctxt:Proof.context) (trm:term): (string * term) list =

structure S4TD = SeLFiE_For_Top_Down;
structure SS = Shared_State;
structure AG = Abduction_Graph;

fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.state) trm =
fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.state)
(agraph:AG.abduction_graph) (trm:term) =
let
val ctxt = Proof.context_of pst: Proof.context;
fun tracing' mssg = ()(*tracing mssg*);
Expand Down Expand Up @@ -91,6 +93,7 @@ fun top_down_conjectures (term2name: SS.synched_term2string_table) (pst:Proof.st
|> parallel_filter (fn (_, trm) => S4TD.run_assertion pst trm S4TD.does_not_have_trivial_equality)
|> parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.nested_eq)
|> parallel_filter_out (fn (_, trm) => S4TD.run_assertion pst trm S4TD.var_appears_many_times_but_always_in_the_same_subtrm)

|> map (fn (_, term) => (SS.get_lemma_name term2name ctxt term, term));
val _ = tracing' "[[[[[[[[[[[top_down_conjecture ends]]]]]]]]]]": unit;
in
Expand Down
57 changes: 56 additions & 1 deletion Abduction/Proof_By_Abduction.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ open Abduction_Graph;

structure SOOE = Seed_Of_Or2And_Edge;
structure SS = Shared_State;
structure AG = Abduction_Graph;
structure TDU = Top_Down_Util;

(** functions to expand ornode leaves **)

Expand Down Expand Up @@ -59,9 +61,62 @@ fun expand_ornode_if_original_goral_is_unproved
let
val _ = tracing' "We did NOT prove the or-node.";
(*top-down explicit conjecturing*)
val explicit_conjectures = All_Top_Down_Conjecturing.top_down_conjectures term2name pst lemma_term : (string * term) list;
val explicit_conjectures = All_Top_Down_Conjecturing.top_down_conjectures term2name pst graph lemma_term : (string * term) list;
val filtered_explicit = filter_out (SOOE.condition_to_filter_out_cnjctr lemma_term refutation pst graph false o snd) explicit_conjectures: (string * term) list;
val explicit_wo_counterexample = filter_out (Shared_State.is_refuted refutation pst o snd) filtered_explicit : (string * term) list;

(*TODO: I should apply simplification using proved lemmas here not in top_down_conjectures.*)
(*
val agraph = Synchronized.value synched_agraph;
val ctxt = Proof.context_of pst
fun is_already_in_graph (simplified:term) =
let
val orkey = (Abduction_Graph.Or_N, [simplified]): AG.key;
val already_exists = try (Abduction_Graph.PGraph.get_node agraph) orkey |> is_some;
val is_True = simplified = @{term True};
val _ = if already_exists then tracing ("already_exists: " ^ Isabelle_Utils.trm_to_string ctxt simplified) else ();
in
already_exists orelse is_True
end: bool;
val keys = AG.keys agraph: AG.keys;
val orkeys = filter AG.is_ornode keys: AG.keys;
val completely_proved_orkeys = filter (AG.is_proved_completely agraph) orkeys: AG.keys;
val completely_proved_terms:terms = map AG.orkey_to_term completely_proved_orkeys: terms;
val completely_proved_lemmas:thms = map (TDU.term_to_thm ctxt) completely_proved_terms: thms;
fun mk_simplifier (added:thm) (tobe_simplified:thm) = (added, Basic_Simplifier.asm_full_simplify (Simplifier.add_simp added ctxt) tobe_simplified): (thm * thm);
val simplifiers = map (mk_simplifier) completely_proved_lemmas: (thm -> (thm *thm)) list;
fun simplify_cnjctr_using_proved_lemma (cnjctr:term) =
let
val _ = tracing "Conjecture is:"
val _ = tracing (Isabelle_Utils.trm_to_string ctxt cnjctr);
val cnjctr_as_thm = TDU.term_to_thm ctxt cnjctr;
val thm_pairs = Utils.map_arg cnjctr_as_thm simplifiers: (thm * thm) list;(*(used_proved_lemma * simplified_result) list*)
val term_pairs = map (apply2 Thm.full_prop_of) thm_pairs: (term * term) list;
val _ = tracing ("The length of term_pairs is: " ^ Int.toString (length term_pairs))
val _ = tracing "They are:"
val _ = map (fn (_, trm) => tracing (Isabelle_Utils.trm_to_string ctxt trm)) term_pairs
(*We only care if we can simplify the conjecture using already proved lemmas.*)
val filtered = filter_out (fn (_, simplified:term) => cnjctr = simplified) term_pairs: (term * term) list;
val _ = tracing ("The length of filtered is: " ^ Int.toString (length filtered))
val used_lemmas = map fst filtered: terms;
val distinct_pairs = distinct (op =) filtered: (term * term) list;
in
distinct_pairs (*already completely proved lemmas that are used to reduce the conjecture to an or-term in the abduction graph.*)
end;
fun replace_cnjctr_if_we_can_simplify_it_to_term_in_graph (string:string, cnjctr:term) =
let
val used_and_existing_lemma_pairs = simplify_cnjctr_using_proved_lemma cnjctr;
val used_and_existing_lemmas = map Utils.pair_to_list used_and_existing_lemma_pairs |> flat |> distinct (op =): terms;
val result_terms = if null used_and_existing_lemmas then [cnjctr] else used_and_existing_lemmas;
val _ = if null used_and_existing_lemmas then () else tracing "NOT NULL";
val w_string = map (pair string) result_terms: (string * term) list;
in
w_string: (string * term) list
end;
val explicit_wo_counterexample = explicit_wo_counterexample |> Par_List.map replace_cnjctr_if_we_can_simplify_it_to_term_in_graph |> flat |> distinct (op =)
*)
val seed_from_explicit = SOOE.conjectures_to_seed_of_or2and_edge term2name pst explicit_wo_counterexample : seed_of_or2and_edge;
val _ = SOOE.decremental_abduction pst or_key seed_from_explicit term2name synched_agraph : unit;
(*tactic application as conjecturing. A little expensive*)
Expand Down
23 changes: 2 additions & 21 deletions Abduction/Seed_Of_Or2And_Edge.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,18 +80,12 @@ fun apply_PSL_to_get_seeds_of_or2and_edges (synched_term2string:SS.synched_term2
val _ = map (tracing' o (Isabelle_Utils.trm_to_string ctxt)) standardized_props: unit list;

fun check_print_read ctxt term = term
|> (fn x => (tracing' ("checking " ^ Isabelle_Utils.trm_to_string ctxt term); x))
|> Isabelle_Utils.trm_to_string ctxt
|> (fn x => (tracing' "STEP 1"; x))
|> Syntax.read_term ctxt
|> (fn x => (tracing' "STEP 2"; x))
|> Isabelle_Utils.strip_atyp
|> (fn x => (tracing' "STEP 3"; x))
|> Syntax.check_term ctxt
|> (fn x => (tracing' "STEP 4"; x))
|> Top_Down_Util.standardize_vnames;


fun check_print_read_terms ctxt terms = map (check_print_read ctxt) terms: terms;
fun pass_check_print_read_terms ctxt terms = try (check_print_read_terms ctxt) terms |> is_some;
val mk_lemma_name = SS.get_lemma_name synched_term2string: Proof.context -> term -> string;
Expand Down Expand Up @@ -180,10 +174,6 @@ fun conjectures_to_seed_of_or2and_edge (term2name:SS.synched_term2string_table)
val cnjctrs = map snd cnjctrs_w_name : terms;
val cnjctrs_as_props = map mk_prop cnjctrs : terms;
val checked_cnjctrs = List.mapPartial check_prop cnjctrs_as_props : terms;
(*
val _ = tracing "++ 2: conjectures_to_seed_of_or2and_edge ++"
val _ = checked_cnjctrs |> map (tracing o Isabelle_Utils.trm_to_string (Proof.context_of pst));
*)
val ctxt = Proof.context_of pst : Proof.context;
val name_cnjctr_pairs = map (fn cnjctr => (SS.get_lemma_name term2name ctxt cnjctr, cnjctr)) checked_cnjctrs: (string * term) list;
val result = conjecture_to_seed_of_or2and_edge name_cnjctr_pairs : seed_of_or2and_edge;
Expand Down Expand Up @@ -219,22 +209,13 @@ fun add_or2and_edge_and_connect_it_to_parental_ornode
then tracing' ("--------- because they are the result of applying this induction: " ^ space_implode " " (Or2And_Edge.how_to_get_andnodes_from_ornode_of proof))
else tracing' "--------- because they are the result of explicit conjecturing";

fun cnjctr_to_thm (ctxt:Proof.context) (cnjctr:term) =
let
val prop = if Top_Down_Util.is_prop cnjctr then cnjctr else HOLogic.mk_Trueprop cnjctr;
val fvar_names = Isabelle_Utils.get_free_var_names_in_trm prop |> distinct (op =): strings;
val thm = Goal.prove ctxt fvar_names [] cnjctr (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)): thm;
in
thm
end;

fun register_proved_thm_in_lthy (name:string) (thm:thm) (lthy:local_theory): local_theory =
Local_Theory.note ((Binding.name name, []), [thm]) lthy |> snd: local_theory;

fun assm_cnjctr_in_pst (name:string, cnjctr:term) (pst:Proof.state) =
let
val ctxt = Proof.context_of pst : Proof.context;
val cnjctr_as_thm = cnjctr_to_thm ctxt cnjctr : thm;
val ctxt = Proof.context_of pst : Proof.context;
val cnjctr_as_thm = Top_Down_Util.term_to_thm ctxt cnjctr : thm;
val pst_w_cnjctr_opt = try (Proof.map_context (register_proved_thm_in_lthy name cnjctr_as_thm)) pst: Proof.state option;
val pst_w_cnjctr = case pst_w_cnjctr_opt of SOME no_dup_pst => no_dup_pst | _ => pst
in
Expand Down
12 changes: 11 additions & 1 deletion Abduction/Top_Down_Util.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ val get_lemma_names_from_sh_output : theory -> string -> strings;
val is_thm_name_registered : Proof.context -> string -> bool;
val mk_new_lemma_name : Proof.context -> bool(*is_final_goal*) -> string;
val term_compare : term * term -> order;
val term_to_thm : Proof.context -> term -> thm;

end;

Expand Down Expand Up @@ -217,6 +218,15 @@ fun mk_new_lemma_name (ctxt:Proof.context) (is_final_goal:bool): string =
fun term_compare (trm1, trm2) =
Term_Ord.term_ord (standardize_vnames trm1, standardize_vnames trm2);

fun term_to_thm (ctxt:Proof.context) (cnjctr:term) =
let
val prop = if is_prop cnjctr then cnjctr else HOLogic.mk_Trueprop cnjctr;
val fvar_names = Isabelle_Utils.get_free_var_names_in_trm prop |> distinct (op =): strings;
val thm = Goal.prove ctxt fvar_names [] cnjctr (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)): thm;
in
thm
end;

end;


Expand All @@ -243,7 +253,7 @@ fun non_prop_trm_to_dummy_eq (ctxt:Proof.context) (lhs:term) =
fun simp_non_prop_term (ctxt:Proof.context) (trm:term) =
let
val dummy_thm = non_prop_trm_to_dummy_eq ctxt trm: thm option;
val simplifier = Basic_Simplifier.simplify ctxt
val simplifier = Basic_Simplifier.asm_full_simplify ctxt
val simped_dummy_thm = Option.mapPartial (try (Isabelle_Utils.timeout_apply (Time.fromSeconds 1) simplifier)) dummy_thm: thm option;
val simped_fst_goal = Option.map Thm.concl_of simped_dummy_thm: term option;
val simped_fst_pair = Option.mapPartial (try (HOLogic.dest_eq o HOLogic.dest_Trueprop)) simped_fst_goal: (term * term) option;
Expand Down
10 changes: 5 additions & 5 deletions SeLFiE/Assertion_Generalization.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,7 +256,7 @@ Imply (
All ("recursive_on_nth_param", QOuter_Number,
Imply (
Ands [
Node_Takes_Less_Than_N_Arguments (Variable "func_occ", Variable "recursive_on_nth_param"),
Node_Takes_More_Than_N_Arguments (Variable "func_occ", Variable "recursive_on_nth_param"),
In_Some_Definitions (
Variable "func",
is_defined_recursively_on_nth,
Expand All @@ -266,7 +266,7 @@ Imply (
All ("used_to_update_mth_arg", QOuter_Number,
Imply (
Ands [
Node_Takes_Less_Than_N_Arguments (Variable "func_occ", Variable "used_to_update_mth_arg"),
Node_Takes_More_Than_N_Arguments (Variable "func_occ", Variable "used_to_update_mth_arg"),
Not (Are_Same_Number (Variable "recursive_on_nth_param", Variable "used_to_update_mth_arg")),
In_Some_Definitions (
Variable "func",
Expand Down Expand Up @@ -342,12 +342,12 @@ Imply (
Ands [
Some ("func_is_recurse_on_nth", QOuter_Number,
Ands [
Node_Takes_Less_Than_N_Arguments (Variable "func_trm_occ", Variable "func_is_recurse_on_nth"), (*Does this actually harm us?*)
Node_Takes_More_Than_N_Arguments (Variable "func_trm_occ", Variable "func_is_recurse_on_nth"), (*Does this actually harm us?*)
Is_Nth_Argument_Or_Below_Nth_Argument_Of (Variable "ind_occ", Variable "func_is_recurse_on_nth", Variable "func_trm_occ"),(*Does this actually harm us?*)
Some_Of ("arb_trm_occ", Variable "arb_trm",
Some ("mth_arg_of_func_occ_has_arb", QOuter_Number,
Ands [
Node_Takes_Less_Than_N_Arguments (Variable "func_trm_occ", Variable "mth_arg_of_func_occ_has_arb"),
Node_Takes_More_Than_N_Arguments (Variable "func_trm_occ", Variable "mth_arg_of_func_occ_has_arb"),
Some_Of ("func_trm_occ2", Variable "func_trm", (*we do not always talk about the same occurrence of the function. See addO_exp\<omega>_inj in Goodstein_Lambda.thy where we have to deal with two different occurrences of add0.*)
Ands [
Is_Nth_Argument_Or_Below_Nth_Argument_Of (Variable "arb_trm_occ", Variable "mth_arg_of_func_occ_has_arb", Variable "func_trm_occ2"),
Expand Down Expand Up @@ -488,7 +488,7 @@ Ors [
Ands [
All ("used_to_update_mth_arg", QOuter_Number,
Ands [
Node_Takes_Less_Than_N_Arguments (Variable "func_occ", Variable "used_to_update_mth_arg"),
Node_Takes_More_Than_N_Arguments (Variable "func_occ", Variable "used_to_update_mth_arg"),
In_Some_Definitions (
Variable "func",
mth_arg_of_func_occ_has_different_print_straw,
Expand Down

0 comments on commit c17f045

Please sign in to comment.