Skip to content

Commit

Permalink
More on quantfier heuristics (I did not add all changes to the first …
Browse files Browse the repository at this point in the history 
…commit)
  • Loading branch information
@thtuerk
thtuerk committed Jul 31, 2012
1 parent 6c1fcb8 commit d7a852e
Show file tree
Hide file tree
Showing 6 changed files with 918 additions and 774 deletions.
6 changes: 5 additions & 1 deletion src/quantHeuristics/quantHeuristicsArgsLib.sig
View file
Expand Up @@ -4,7 +4,11 @@ sig
(* stateful ones, copied from quantHeuristicsLib *)
val stateful_qp : quantHeuristicsLib.quant_param;
val pure_stateful_qp : quantHeuristicsLib.quant_param;
val TypeBase_qp : quantHeuristicsLib.quant_param
val TypeBase_qp : quantHeuristicsLib.quant_param;

val clear_stateful_qp : unit -> unit;
val stateful_qp___add_combine_arguments :
quantHeuristicsLib.quant_param list -> unit;


(* ones for specific types *)
Expand Down
43 changes: 35 additions & 8 deletions src/quantHeuristics/quantHeuristicsLib-examples.txt
View file
Expand Up @@ -7,7 +7,7 @@ loadPath :=


open HolKernel Parse boolLib Drule ConseqConv computeLib
open quantHeuristicsLib
open quantHeuristicsLib;
open quantHeuristicsArgsLib;

(*
Expand All @@ -18,16 +18,14 @@ quietdec := false;
(*Simple find an equation and instatiate it,
same as UNWIND_CONV*)

val t = ``?x. (x=7) /\ P x /\ Q``;
val t = ``?x. Q /\ (x=7) /\ P x``;
val t = ``!x. ((x=7) /\ Q) ==> P x``;

(* Result: P 7 /\ Q *)
val thm = SIMP_CONV std_ss [] t
(* Result: Q /\ P 7 *)
val thm = SIMP_CONV std_ss [] t;
val thm = QUANT_INSTANTIATE_CONV [] t;




(*Quantifiers are resorted to be able to find easy instantations*)
val t = ``?y x z. (x=y+z) /\ X x y z``;
val t = ``!y x z. ~(x=y+z) \/ X x y z``;
Expand All @@ -36,19 +34,28 @@ val thm = SIMP_CONV std_ss [] t
val thm = QUANT_INSTANTIATE_CONV [] t


QUANT_INSTANTIATE_CONV [] ``?x. (!z. Q z /\ (x=7)) /\ P x``
QUANT_INSTANTIATE_CONV [std_qp] ``!x. IS_SOME x ==> P x``



(*However, the new library can handle more difficult nestings than
the existing UNWIND conversions*)

val t = ``?x. (!z. (x=7) /\ Q z) /\ P x /\ Q t``
val t = ``?x. ((x=7) \/ (7 = x)) /\ P x``;
(* Result: P 7 *)

val t = ``?x. !y. (x=7) /\ P x y``;
(* Result: !y. P 7 y *)

val t = ``?x. (!z. Q z /\ (x=7)) /\ P x``
(* Result: (!z. Q z) /\ P 7 /\ Q t *)

val t = ``!x z. ?g. (((x=7) /\ Q g)) ==> P x``
(* Result: (?g. Q g) ==> P 7 *)

val thm = QUANT_INSTANTIATE_CONV [] t
val thm = SIMP_CONV std_ss [] t


(*
Expand Down Expand Up @@ -89,6 +96,10 @@ val thm = QUANT_INSTANTIATE_CONV [] t


(*The new library also uses matching to figure out instantions*)
val t = ``?x. (f(8 + 2) = f(x + 2)) /\ P(10)``;
val t = ``?x. (f(8 + 2) = f(x + 2)) /\ P(f (x + 2))``;
val t = ``?x. (f(8 + 2) = f(x + 2)) /\ P(f (2 + x))``; (*fails *)

val t = ``?x. P \/ (f(8 + 2) = f(x + 2)) \/ Z``;
val t = ``?x. P /\ (f(8 + 2) = f(x + 2)) /\
g (f (x+2)) /\ Z``;
Expand All @@ -97,6 +108,7 @@ val t = ``?x. P /\ (f 2 = f x) /\ Q /\ Q2(f x) /\ Z /\
(f x = f 2)``;

val thm = QUANT_INSTANTIATE_CONV [] t
val thm = SIMP_CONV [] t



Expand Down Expand Up @@ -620,8 +632,14 @@ val thm = QUANT_INSTANTIATE_CONV [pair_qp [split_pair___ALL___pred]] t


(*Some things about option types*)
val t = ``!x. IS_SOME x``
val thm = QUANT_INSTANTIATE_CONV [std_qp] t

val t = ``!x. IS_NONE x``
val thm = QUANT_INSTANTIATE_CONV [std_qp] t

val t = ``!x. IS_SOME x ==> P x``;
val thm = QUANT_INSTANTIATE_CONV [option_qp] t
val thm = QUANT_INSTANTIATE_CONV [std_qp] t

val t = ``!x. IS_NONE x \/ P x``
val thm = QUANT_INSTANTIATE_CONV [option_qp] t
Expand All @@ -639,6 +657,7 @@ val thm = QUANT_INSTANTIATE_CONV [std_qp] t
val t = ``!l. (~(l = []) ==> (LENGTH l > 0))``;
val thm = QUANT_INSTANTIATE_CONV [stateful_qp] t
val thm = QUANT_INSTANTIATE_CONV [list_qp] t
val thm = QUANT_INSTANTIATE_CONV [std_qp] t

val t = ``!l. (l = h::h2) \/ X``
val thm = QUANT_INSTANTIATE_CONV [stateful_qp] t
Expand Down Expand Up @@ -686,13 +705,21 @@ e (SRW_TAC [QUANT_INST_ss [record_default_qp]] [])

(*Tactics using the assumption*)

set_goal ([], ``!x. IS_SOME x ==> P x``);

set_goal ([], ``!x y. IS_SOME x /\ IS_SOME y ==> (x = y)``);

e (
REPEAT STRIP_TAC THEN
ASM_QUANT_INSTANTIATE_TAC [std_qp]
)

(* in contrast, the simplifier does not work, since it does not instantiate free variables *)
e (
REPEAT STRIP_TAC THEN
FULL_SIMP_TAC (std_ss++(QUANT_INST_ss [std_qp])) []
)



(*A combination of quantHeuristics with consequence Conversions
Expand Down
40 changes: 18 additions & 22 deletions src/quantHeuristics/quantHeuristicsLib.sig
View file
Expand Up @@ -123,16 +123,18 @@ sig
exception QUANT_INSTANTIATE_HEURISTIC___no_guess_exp;

(*Some types*)
type quant_heuristic = term -> term -> guess_collection;
type quant_heuristic_base = term -> term -> guess_collection;
type quant_heuristic = quant_heuristic_base -> quant_heuristic_base;

type quant_param =
{distinct_thms : thm list,
cases_thms : thm list,
rewrite_thms : thm list,
inference_thms : thm list,
convs : conv list,
filter : (term -> term -> bool) list,
heuristics : (quant_heuristic -> quant_heuristic) list,
top_heuristics : (quant_heuristic -> quant_heuristic) list,
heuristics : quant_heuristic list,
top_heuristics : quant_heuristic list,
final_rewrite_thms : thm list};
type quant_heuristic_cache;

Expand All @@ -142,22 +144,19 @@ sig


(*Heuristics that might be useful to write own ones*)
val QUANT_INSTANTIATE_HEURISTIC___REWRITE :
quant_heuristic -> term -> thm -> guess_collection
val QUANT_INSTANTIATE_HEURISTIC___CONV :
conv -> quant_heuristic -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct : thm list -> quant_heuristic -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___EQUATION_cases : thm -> quant_heuristic -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___one_case : thm -> quant_heuristic -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___cases : thm -> quant_heuristic -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___CONV : conv -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___EQUATION_distinct : thm list -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___EQUATION_two_cases: thm -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___one_case : thm -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___cases : thm -> quant_heuristic;



val QUANT_INSTANTIATE_HEURISTIC___max_rec_depth : int ref

val QUANT_INSTANTIATE_HEURISTIC___COMBINE :
((term -> term -> bool) list) -> ((quant_heuristic -> quant_heuristic) list) ->
((quant_heuristic -> quant_heuristic) list) -> quant_heuristic_cache ref option -> quant_heuristic;
((term -> term -> bool) list) -> quant_heuristic list ->
quant_heuristic list -> quant_heuristic_cache ref option -> quant_heuristic_base;


val COMBINE_HEURISTIC_FUNS : (unit -> guess_collection) list -> guess_collection;
Expand Down Expand Up @@ -194,6 +193,9 @@ sig
val QUANT_INST_TAC : (string * Parse.term Lib.frag list * Parse.term Parse.frag list list) list
-> tactic;

(*combination with simplifier*)
val QUANT_INST_ss : quant_param list -> simpLib.ssfrag;
val FAST_QUANT_INST_ss : quant_param list -> simpLib.ssfrag;



Expand All @@ -204,7 +206,7 @@ sig
val stateful_qp___add_combine_arguments :
quant_param list -> unit;

val QUANT_INSTANTIATE_HEURISTIC___STATEFUL : quant_heuristic -> quant_heuristic;
val QUANT_INSTANTIATE_HEURISTIC___STATEFUL : quant_heuristic;

val empty_qp : quant_param;
val stateful_qp : quant_param;
Expand All @@ -226,16 +228,10 @@ sig
val cases_qp : thm list -> quant_param
val inference_qp : thm list -> quant_param
val convs_qp : conv list -> quant_param
val heuristics_qp : (quant_heuristic -> quant_heuristic) list ->
quant_param
val top_heuristics_qp: (quant_heuristic -> quant_heuristic) list ->
quant_param
val heuristics_qp : quant_heuristic list -> quant_param
val top_heuristics_qp: quant_heuristic list -> quant_param
val filter_qp : (term -> term -> bool) list -> quant_param


(*combination with simplifier*)
val QUANT_INST_ss : quant_param list -> simpLib.ssfrag;

(* Traces *)
(* "QUANT_INSTANTIATE_HEURISTIC" can be used to get debug information on
how guesses are obtained *)
Expand Down

0 comments on commit d7a852e

Please sign in to comment.