Skip to content

Commit

Permalink
Abduction: first version of the simp-strategy working.
Browse files Browse the repository at this point in the history 
Checked.

TODOs:
- the absence of equality check against the parental or-node should not break
  this tool, but it does so for some reasons.
- we have to make it sure that this really simplifies the conjecture.
- Should we check for simplification using proved lemmas after registering
  the results of decremental conjecturing?
- Or else maybe we should apply simplification *before* applying decremental
  conjecturing. This sounds a little risky, but probably results in better
  performance for most cases.
  • Loading branch information
@yutakang
yutakang committed Aug 20, 2023
1 parent 070bddd commit d2554b1
Show file tree
Hide file tree
Showing 5 changed files with 240 additions and 71 deletions.
62 changes: 62 additions & 0 deletions Abduction/Abduction.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,4 +132,66 @@ val _ = theorem \<^command_keyword>\<open>prove\<close> "prove";
end;
\<close>

ML\<open>
structure df = Syntax
type tsdf = thm
val thm = Top_Down_Util.term_to_thm @{context} (Syntax.read_term @{context} "x = x");
\<close>
find_theorems name: "List"
ML\<open>
structure TDU = Top_Down_Util;
structure SS = Shared_State;
structure SOOE = Seed_Of_Or2And_Edge;
val timeout = Isabelle_Utils.timeout_apply (Time.fromSeconds 1);
val d = Basic_Simplifier.asm_full_simplify @{context} thm;
val s = simp_non_prop_term @{context} @{term "True = True"};
fun simp_explicit_conjecture (synched_term2string:SS.synched_term2string_table) (ctxt:Proof.context)
(simp as (_:string, simp_term:term)) (cnjctr as (_:string, cnjctr_term:term)): SOOE.conjectures =
let
val simp_thm = TDU.term_to_thm ctxt simp_term: thm;
val ctxt_w_simp = Simplifier.add_simp simp_thm ctxt: Proof.context;
val simplifier = Basic_Simplifier.asm_full_simplify ctxt_w_simp: thm -> thm;
val simplifier_w_timeout = try (Isabelle_Utils.timeout_apply (Time.fromSeconds 1) simplifier): thm -> thm option;
val cnjctr_thm = TDU.term_to_thm ctxt simp_term: thm;
val simp_result = simplifier_w_timeout cnjctr_thm: thm option;
in
if is_none simp_result
then [cnjctr]
else
let
val simp_result_term = the simp_result |> Thm.full_prop_of: term;
val simp_result_name = SS.get_lemma_name synched_term2string ctxt simp_result_term: string;
in
if simp_result_term = cnjctr_term
then [simp, (simp_result_name, simp_result_term)]
else [cnjctr]
end
end;
fun simp_explicit_conjectures (synched_term2string:SS.synched_term2string_table) (ctxt:Proof.context)
(cnjctrs:SOOE.conjectures) (simp:SOOE.conjecture): SOOE.conjectures =
map (simp_explicit_conjecture synched_term2string ctxt simp) cnjctrs |> flat;
val sdf = Thm.prop_of @{thm List.distinct_adj_Nil};
\<close>
ML\<open>
val saf = @{thm List.distinct_adj_ConsD} |> Thm.full_prop_of |> Isabelle_Utils.trm_to_string @{context} |> tracing;
\<close>
thm List.distinct_adj_Nil

lemma "False \<Longrightarrow> True"
apply(tactic \<open>fn thm => (
thm |> Thm.full_prop_of |> Isabelle_Utils.trm_to_string @{context} |> tracing;
thm |> Thm.prop_of |> Isabelle_Utils.trm_to_string @{context} |> tracing;
thm |> Thm.concl_of |> Isabelle_Utils.trm_to_string @{context} |> tracing;
Seq.single thm)\<close>)
oops

end
5 changes: 3 additions & 2 deletions Abduction/All_Top_Down_Conjecturing.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ structure SS = Shared_State;
structure AG = Abduction_Graph;
structure TBC = Template_Based_Conjecturing;

fun template_based_conjecture_for_simplification (ctxt:Proof.context) (trm): (string * term) list =
fun template_based_conjecture_for_simplification term2name (ctxt:Proof.context) (trm): (string * term) list =
let
val (_, relevant_binary_funcs, relevant_unary_funcs) = TBC_Utils.get_relevant_constants ctxt trm;
fun ctxt_n_const_to_all_conjecture_term context tm =
Expand All @@ -74,7 +74,8 @@ fun template_based_conjecture_for_simplification (ctxt:Proof.context) (trm): (st
@ TBC.ctxt_n_const_to_zero_element ctxt tm
@ TBC.ctxt_n_consts_to_projection ctxt tm
@ TBC.ctxt_n_consts_to_square ctxt tm)
|> map (apfst Template_Based_Conjecturing.property_as_string);
|> map (apfst Template_Based_Conjecturing.property_as_string)
|> map (fn (_, term) => (SS.get_lemma_name term2name ctxt term, term));;
val result = map (ctxt_n_const_to_all_conjecture_term ctxt) (relevant_unary_funcs @ relevant_binary_funcs) |> flat
: (string * term) list;
in
Expand Down
41 changes: 26 additions & 15 deletions Abduction/Proof_By_Abduction.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,19 +46,28 @@ fun prove_standard_simp_rules
val ctxt = Proof.context_of pst: Proof.context;
val graph = Synchronized.value synched_agraph : abduction_graph;
val condition_to_filter_out = SOOE.condition_to_filter_out_conjecture lemma_term refutation pst graph false o snd: string * term -> bool;
val explicit_conjectures = ATDC.template_based_conjecture_for_simplification ctxt lemma_term : (string * term) list;
val explicit_conjectures = ATDC.template_based_conjecture_for_simplification term2name ctxt lemma_term : (string * term) list;
val filtered_explicit = parallel_filter_out condition_to_filter_out explicit_conjectures : (string * term) list;
val refute = Shared_State.is_refuted refutation pst o snd : (string * term) -> bool;
val explicit_wo_counterexample = parallel_filter_out refute filtered_explicit : (string * term) list;

val _ = tracing "explicit_wo_counterexample are:"
val _ = map (tracing o Isabelle_Utils.trm_to_string (Proof.context_of pst) o snd) explicit_wo_counterexample: unit list;

fun prove_save_in_graph (lem_name:string, lem_term:term) =
let
(*expensive*)
val _ = tracing lem_name;
val maybe_prf = prove_term_completely pst lem_term: strings option;
val _ = if is_some maybe_prf then (tracing o Isabelle_Utils.trm_to_string ctxt) lem_term else ()
in
if is_none maybe_prf then () else SS.add_proved_simp proved_ors (lem_name, lem_term)
if is_none maybe_prf then (tracing ("DID NOT PROVE: " ^ Isabelle_Utils.trm_to_string ctxt lem_term))
else SS.add_proved_simp proved_ors (lem_name, lem_term)
(*Synchronized.change proved_ors (fn alist => (lem_name, lem_term)::alist)*)
end;

val _ = Par_List.map prove_save_in_graph explicit_wo_counterexample: unit list;

in
()
end;
Expand Down Expand Up @@ -87,20 +96,20 @@ fun expand_ornode_if_original_goral_is_unproved
else (*if we cannot prove the ornode completely, expand it using Extend_Leaf and conjecturing*)
let
(*top-down explicit conjecturing*)
val explicit_conjectures = All_Top_Down_Conjecturing.top_down_conjectures term2name pst lemma_term : (string * term) list;
val condition_to_filter_out = SOOE.condition_to_filter_out_conjecture lemma_term refutation pst graph false o snd : string * term -> bool;
val filtered_explicit = parallel_filter_out condition_to_filter_out explicit_conjectures: (string * term) list: (string * term) list;
val explicit_wo_counterexample = parallel_filter_out (Shared_State.is_refuted refutation pst o snd) filtered_explicit : (string * term) list;
val seed_from_explicit = SOOE.conjectures_to_seed_of_or2and_edge term2name pst explicit_wo_counterexample : seed_of_or2and_edge;
val explicit_cnjnctrs = #new_goals seed_from_explicit : SOOE.conjectures;
val _ = SOOE.decremental_abduction pst or_key explicit_cnjnctrs term2name synched_agraph proved_ors: unit;
val explicit_conjectures = All_Top_Down_Conjecturing.top_down_conjectures term2name pst lemma_term : (string * term) list;
val condition_to_filter_out = SOOE.condition_to_filter_out_conjecture lemma_term refutation pst graph false o snd : string * term -> bool;
val filtered_explicit = parallel_filter_out condition_to_filter_out explicit_conjectures: (string * term) list: (string * term) list;
val explicit_wo_counterexample = parallel_filter_out (Shared_State.is_refuted refutation pst o snd) filtered_explicit : (string * term) list;
val seed_from_explicit = SOOE.conjectures_to_seed_of_or2and_edge term2name pst explicit_wo_counterexample : seed_of_or2and_edge;
val explicit_cnjnctrs = #new_goals seed_from_explicit : SOOE.conjectures;
val _ = SOOE.abduction_for_explicit_conjectures pst or_key explicit_cnjnctrs (term2name, synched_agraph) proved_ors: unit;
(*tactic application as conjecturing. A little expensive*)
val pst_to_prove = mk_pst_to_prove_from_term pst lemma_term : state;
val seeds_from_tactics = SOOE.apply_PSL_to_get_seeds_of_or2and_edges term2name pst_to_prove : seeds_of_or2and_edge;
val graph_extended_by_conjecture = Synchronized.value synched_agraph : abduction_graph;
val filtered_seeds_from_tactics = SOOE.filter_out_bad_seeds_from_tactic lemma_term refutation pst graph_extended_by_conjecture seeds_from_tactics
|> filter_out (SOOE.seed_has_counterexample refutation pst) : seeds_of_or2and_edge;
val _ = SOOE.implicit_conjecturing pst or_key filtered_seeds_from_tactics synched_agraph : unit;
val pst_to_prove = mk_pst_to_prove_from_term pst lemma_term : state;
val seeds_from_tactics = SOOE.apply_PSL_to_get_seeds_of_or2and_edges term2name pst_to_prove : seeds_of_or2and_edge;
val graph_extended_by_conjecture = Synchronized.value synched_agraph : abduction_graph;
val filtered_seeds_from_tactics = SOOE.filter_out_bad_seeds_from_tactic lemma_term refutation pst graph_extended_by_conjecture seeds_from_tactics
|> filter_out (SOOE.seed_has_counterexample refutation pst) : seeds_of_or2and_edge;
val _ = SOOE.abduction_for_tactic_based_conjectures pst or_key filtered_seeds_from_tactics synched_agraph: unit;
in
(*seeds_to_updated_graph is very expensive*)
SS.final_goal_proved_completely synched_agraph
Expand Down Expand Up @@ -216,6 +225,8 @@ fun proof_by_abduction (pst:Proof.state) (start:Timing.start) (term:term) =
val synched_proved_simps = SS.mk_synched_proved_simps ();
val quadruple = (pst, synched_agraph, synched_refutation_table, synched_lemma_name_table, synched_proved_simps);
val _ = prove_standard_simp_rules quadruple standardized_term: unit;
val _ = tracing "--- the number of elems in the association list is: "
val _ = Synchronized.value synched_proved_simps |> length |> Int.toString |> tracing;
val solved = loop 0 max_depth start quadruple;
val final_graph = Synchronized.value synched_agraph: Abduction_Graph.abduction_graph;
val lemma_name2term = abduction_graph_to_string2term_table final_graph: string2term_table;
Expand Down
Loading

0 comments on commit d2554b1

Please sign in to comment.