Theory Zip_Examples
section ‹Examples and Brief Technical Overview for Zip›
theory Zip_Examples
imports
Zip_Try0
HOL.List
begin
paragraph ‹Summary›
text ‹The @{method zip} method is a customisable general-purpose white-box prover based on the
Zippy framework. This theory begins with examples demonstrating some key features and concludes
with a brief technical overview for users interested in customising the method.
On a high-level, @{method zip} performs a proof tree search with customisable
expansion actions and search strategies. By default, it uses an ‹A⇧*› search and integrates the
classical reasoner, simplifier, the blast and metis prover, and supports resolution with higher-order
and proof-producing unification \cite{ML_Unification-AFP}, conditional substitutions, case splitting
and induction, among other things.
In most cases, @{method zip} can be used as a drop-in replacement for Isabelle's classical methods
like @{method auto}, @{method fastforce}, @{method force}, @{method fast}, etc.,
as demonstrated in @{dir Benchmarks}. Note, however, that @{method zip} can be slower than those
methods due to a more general search procedure.
Like @{method auto}, @{method zip} supports non-terminal calls and interactive proof exploration.
@{method zip} comes with @{command try0} integration in @{file "../Zip_Try0.thy"}.
Import that theory as a first file to obtain the integration.
If you want to omit the integration, import @{file "../Zip_Metis.thy"} instead.›
subsection ‹Examples›
text ‹Note: some examples in this files are adapted from @{theory HOL.List}. Some original proofs
from @{theory HOL.List} are left in comments and tagged with "ORIG" for comparison.›
experiment
begin
text ‹You can use it like @{method auto}:›
lemma "sorted_wrt (>) l ⟷ sorted (rev l) ∧ distinct l"
by (induction l) (zip iff: antisym_conv1 simp: sorted_wrt_append)
lemma "sorted_wrt (>) l ⟷ sorted (rev l) ∧ distinct l"
by (induction l) (zip iff: antisym_conv1 simp: sorted_wrt_append)
text ‹You can use it for proof exploration (i.e. the method returns incomplete attempts):›
lemma
assumes [intro]: "P ⟹ Q"
and [simp]: "A = B"
shows "A ⟶ Q"
apply zip
back
back
oops
text ‹Note that the method returned the goal @{prop "B ⟹ Q"} but not @{prop "B ⟹ P"}.
The reason is that, by default, the method only returns those incomplete attempts that only use
"promising" expansions on its search path, as further elaborated in the technical overview.
The simplifier, for instance, is marked as a "promising" expansion action.
For the classical reasoner, expansions with unsafe (introduction) rules are not marked as promising
while safe rules are.
One can instruct the method to return all attempts by changing its default strategy from
@{ML Zip.AStar.promising'} to @{ML Zip.AStar.all'}:›
lemma
assumes [intro]: "P ⟹ Q"
and [simp]: "A = B"
shows "A ⟶ Q"
apply (zip run exec: Zip.AStar.all')
oops
text ‹Alternatively, the introduction rule can be marked as safe:›
lemma
assumes [intro!]: "P ⟹ Q"
and [simp]: "A = B"
shows "A ⟶ Q"
apply zip
oops
text ‹Many explorations are possibly infinite or too large for an exhaustive search. In such cases,
one may limit the number of expansion steps. Below, we fuel the method with 20 steps:›
lemma
assumes [intro]: "P ∧ P ⟹ P"
shows "P"
apply (zip 20 run exec: Zip.AStar.all')
oops
text ‹One can also limit the maximum search depth, e.g. to depth 2:›
lemma
assumes [intro]: "P ∧ P ⟹ P"
shows "P"
apply (zip run exec: "Zip.AStar.all 2")
oops
text ‹You can perform case splits:›
lemma "tl xs ≠ [] ⟷ xs ≠ [] ∧ ¬(∃x. xs = [x])"
by (zip cases xs)
fun foo :: "nat ⇒ nat" where
"foo 0 = 0"
| "foo (Suc 0) = 1"
| "foo (Suc (Suc n)) = 1"
lemma "foo n + foo m < 4"
by (zip cases n rule: foo.cases and m rule: foo.cases)
text ‹You may also use patterns of the shape (pattern - anti-patterns). All terms occurring in the
goal that (1) satisfy the pattern and (2) do not satisfy any of the anti-patterns are then taken as
instantiation candidates:›
lemma "foo n + foo m < 4"
by (zip cases (pat) ("_ :: nat" - "_ _") rule: foo.cases)
text ‹Note that for a function ‹f› with multiple arguments, the function package creates a cases
rule ‹f.cases› where ‹f›'s arguments are tupled and equated to a single variable. Example:›
fun bar :: "nat ⇒ bool ⇒ nat" where
"bar 0 _ = 0"
| "bar (Suc 0) True = 1"
| "bar (Suc 0) False = 0"
| "bar (Suc (Suc n)) b = 1"
thm bar.cases
text ‹As a result ‹cases "n :: nat" "b :: bool" rule: bar.cases› will raise an error:
The cases rule requires a @{typ "nat × bool"} pair for instantiation. The right invocation is
‹cases "(n, b)" rule: bar.cases›.
Moreover, the invocation ‹cases (pat) "(?n :: nat, ?b :: nat)" rule: bar.cases› will not find any
matches in a goal term @{term "bar n b < 2"} since no @{typ "nat × bool"} pair occurs in the goal.
The solution is to transform the cases rule to the desired form with @{attribute deprod_cases}:
›
thm bar.cases[deprod_cases]
lemma "bar n b < 2"
by (zip cases (pat) "_ :: nat" "_ :: bool" rule: bar.cases[deprod_cases])
text ‹You may even use predicates on term zippers (see @{ML_structure Term_Zipper}):›
lemma "foo n + foo m < 4"
by (zip cases (pred) "fst #> member (op =) [@{term n}, @{term m}]" rule: foo.cases)
text ‹You can use induction:›
lemma "foo n + foo m < 4"
by (zip induct rule: foo.induct)
text ‹Again, you may also use patterns and predicates:›
lemma "foo n + foo m < 4"
by (zip induct (pat) ("_ :: nat" - "_ _") rule: foo.induct)
text ‹Here are some more complex combinations (the original code from the standard library is marked
with ORIG in the following). Note that configurations for different actions are separated by
∗‹where›.›
lemma list_induct2:
"length xs = length ys ⟹ P [] [] ⟹
(⋀x xs y ys. length xs = length ys ⟹ P xs ys ⟹ P (x#xs) (y#ys))
⟹ P xs ys"
by (zip induct xs arbitrary: ys where cases (pat) ("_ :: _ list" - "[]" "_ _"))
lemma list_induct2':
"⟦ P [] [];
⋀x xs. P (x#xs) [];
⋀y ys. P [] (y#ys);
⋀x xs y ys. P xs ys ⟹ P (x#xs) (y#ys) ⟧
⟹ P xs ys"
by (zip induct xs arbitrary: ys where cases (pat) ("_ :: _ list" - "[]" "_ _"))
text ‹Data passed as method modifiers can also be stored in the context more generally:›
fun gauss :: "nat ⇒ nat" where
"gauss 0 = 0"
| "gauss (Suc n) = n + 1 + gauss n"
context notes gauss.induct[zip_induct (pat) ("_ :: nat" - "_ _")]
begin
lemma "gauss n = (n * (n + 1)) div 2" by zip
lemma "gauss n < gauss (Suc n)" by zip
lemma "gauss n > 0 ⟷ n > 0" by zip
end
text ‹In some cases, it is necessary (or advisable for performance reasons) to change the search
strategy from the default ‹A⇧*› (@{ML_structure Zip.AStar}) search to breadth-first
(@{ML_structure Zip.Breadth_First}), depth-first (@{ML_structure Zip.Depth_First}),
or best-first (@{ML_structure Zip.Best_First}) search. You can either try them individually or use
@{ML_structure Zip.Try} to search for the fastest one in parallel. Note that @{ML_structure Zip.Try}
is only meant for exploration. It should be replaced by the discovered, most efficient strategy in
the final proof document!›
lemma list_induct3:
"length xs = length ys ⟹ length ys = length zs ⟹ P [] [] [] ⟹
(⋀x xs y ys z zs. length xs = length ys ⟹ length ys = length zs ⟹ P xs ys zs ⟹ P (x#xs) (y#ys) (z#zs))
⟹ P xs ys zs"
by (induct xs arbitrary: ys zs)
(zip cases (pat) ("_ :: _ list" - "[]") where run exec: Zip.Breadth_First.all')
text ‹@{method zip} is also registered to @{command try0} for each search strategy:›
lemma "map f xs = map g ys ⟷ length xs = length ys ∧ (∀i<length ys. f (xs!i) = g (ys!i))"
by (zip simp: list_eq_iff_nth_eq)
text ‹One can use conditional substitution rules:›
lemma filter_insort:
"sorted (map f xs) ⟹ P x ⟹ filter P (insort_key f x xs) = insort_key f x (filter P xs)"
by (induct xs)
(zip subst insort_is_Cons where run exec: Zip.Best_First.all')
lemma rev_eq_append_conv: "rev xs = ys @ zs ⟷ xs = rev zs @ rev ys"
by (zip subst rev_rev_ident[symmetric])
lemma dropWhile_neq_rev: "⟦distinct xs; x ∈ set xs⟧ ⟹
dropWhile (λy. y ≠ x) (rev xs) = x # rev (takeWhile (λy. y ≠ x) xs)"
by (zip induct xs where subst dropWhile_append2)
text ‹Zip integrates the @{method blast} prover. In cases where @{method blast} loops or takes too
long, users may specify a limit on its search depth or disable it completely:›
lemma "(∀X. X ⊆ X) ⟹ 1 + 1 = 2"
by (zip blast depth: 0)
text ‹Zip also integrates the @{method metis} provers. Since @{method metis} easily loops, it is
only activated if
(1) users explicitly provide it some options and/or rules and
(2) @{method zip} is not expected to make any promising progress on the given goal node without
using @{method metis} (cf. the setup in @{theory Zippy.Zip_Metis}).
Users may pass several options/runs to metis using the separator ‹and›.
A typical workflow with @{method zip} looks as follows:
▸ Check if @{method zip} is successful.
▸ If it is unsuccessful but terminates:
▸ Check if there is a relevant lemma missing based on the returned goals.
It might also be helpful to check non-promising attempts by switching from
@{ML Zip.AStar.promising'} to @{ML Zip.AStar.all'} (or analogously for another search strategy).
▸ Call @{command sledgehammer} on the remaining goals and either add the metis calls to
@{method zip} directly or check if there are some helpful lemmas in the @{method metis} call
that you could add another way (e.g. as a simp or classical rule) such that the @{method metis}
call becomes unnecessary.
Hint: you may also want to use @{attribute metis_instantiate} for this step.
▸ If it is unsuccessful and does not terminate:
▸ Check if @{method zip} is successful with a different strategy
(e.g. by using @{ML_structure Zip.Try} or trying the strategies manually) and/or depth limit.
▸ If none of the above is successful:
▸ Limit @{method zip}'s search steps to a number such that the set of returned subgoals looks
reasonable to you.
▸ Check which of the returned subgoals were not solvable by sequentially applying ‹zip[1]› to
each subgoal. For each subgoal that is not solved: continue with step 2 of this workflow.
›
lemma : "List.extract P (x # xs) = (if P x then Some ([], x, xs)
else (case List.extract P xs of None ⇒ None | Some (ys, y, zs) ⇒ Some (x#ys, y, zs)))"
apply (zip simp add: extract_def comp_def split: list.splits
where metis dropWhile_eq_Nil_conv list.distinct(1))
done
lemma longest_common_prefix:
"∃ps xs' ys'. xs = ps @ xs' ∧ ys = ps @ ys' ∧ (xs' = [] ∨ ys' = [] ∨ hd xs' ≠ hd ys')"
apply (induct xs ys rule: list_induct2')
apply (zip metis append_eq_Cons_conv list.sel(1) self_append_conv)
done
lemma not_distinct_decomp: "¬ distinct ws ⟹ ∃xs ys zs y. ws = xs@[y]@ys@[y]@zs"
proof (induct n ≡ "length ws" arbitrary:ws)
case (Suc n ws)
then show ?case using length_Suc_conv [of ws n]
apply (zip metis append_Cons and split_list append_eq_append_conv2)
done
qed simp
lemma lexord_cons_cons:
"(a # x, b # y) ∈ lexord r ⟷ (a = b ∧ (x,y)∈ lexord r) ∨ (a,b)∈ r" (is "?lhs = ?rhs")
by (zip metis hd_append list.sel(1,3) tl_append2 and Cons_eq_append_conv)
text ‹One can pass (elim-/dest-/forward-)rules that should be resolved by Isabelle's standard
higher-order unifier, matcher, or a customisable proof-producing unifier (see @{session ML_Unification}).
In contrast to the rules passed to the classical reasoner, each such rule can be annotated with
individual data, e.g. priority, cost, and proof-producing unifier to be used.
Resolving rules with a proof-producing unifier is particularly useful in situations where equations do
not hold up to ‹αβη›-equality but some stronger, provable equality (see the examples theories in
@{session ML_Unification} for more details). By default, the proof-producing unifier
@{ML Standard_Mixed_Comb_Unification.first_higherp_comb_unify} is used, which uses the simplifier
and unification hints (cf. @{theory ML_Unification.ML_Unification_Hints}), among other things.›
lemma
assumes "Q"
and [simp]: "Q = P"
shows "P"
by (zip urule assms)
text ‹Passing rules to ‹urule› is particularly useful when dealing with definitions. In such
cases, theorems for the abbreviated concept can re-used for the new definition (without making the
definition opaque in general, as is the case with @{command abbreviation}):›
definition "my_refl P ≡ reflp_on {x. P x}"
lemma my_refl_uhint [uhint]:
assumes "{x. P x} ≡ S"
shows "my_refl P ≡ reflp_on S"
using assms unfolding my_refl_def by simp
lemma "my_refl P Q ⟹ P x ⟹ ∃x. Q x x"
by (zip urule (d) reflp_onD)
lemma
assumes "⋀Q. P (reflp_on {x. Q x ∧ True})"
shows "True ∧ P (my_refl Q)"
by (zip urule assms)
text ‹For very fine-grained control, one can even specify individual functions to initialise the
proof trees linked to the rule's side conditions. By default, each such tree is again solved by all
expansion actions registered to @{method zip}. Below, we override that behaviour and let the
rule's second premise be solved by reflexivity instead. You may check the technical overview
section for more details about below code.›
lemma
assumes "P ⟹ U = U ⟹ Q"
shows "A ⟶ Q"
apply (zip rule assms updates: [2: ‹fn i =>
let open Zippy; open ZLPC Base_Data MU; open SC A
val id = @{binding "refl"}
val a_meta = AMeta.metadata (id, Lazy.value "proof by reflexivity")
fun mk_aa_meta _ _ = AAMeta.metadata {cost = Cost.VERY_LOW, progress = AAMeta.P.Promising}
fun ztac _ = Ctxt.with_ctxt (fn ctxt => arr (resolve_tac ctxt @{thms refl}
|> Tac_AAM.lift_tac mk_aa_meta |> Tac_AAM.Tac.zSOME_GOAL_FOCUS))
in
Tac.cons_action_cluster Util.exn (ACMeta.no_descr id) [(GFocus.single i, {
empty_action = Library.K Zippy.PAction.disable_action,
meta = a_meta,
result_action = Result_Action.action (Library.K (C.id ()))
Result_Action.copy_update_data_empty_changed,
presultsq = Zip.PResults.enum_scale_presultsq_default Cost.LOW,
tac = ztac})]
>>> (the #> Up3.morph)
end›])
back
oops
text ‹Zippy and zip both use the @{ML_structure Logger} from @{theory ML_Unification.ML_Logger}.
You can use it to trace its search. Check the logger's examples theory in @{session ML_Unification}
for a demonstration how to filter and modify the logger's output.›
lemma
assumes [intro]: "P ⟹ Q"
and [simp]: "A = B"
shows "A ⟶ Q"
supply [[ML_map_context ‹Logger.set_log_levels Zippy.Logging.logger Logger.DEBUG›]]
apply zip
oops
subsection ‹Technical Overview›
text ‹
The method @{method zip} is based on the Zippy framework. For a preprint about the latter see
\<^cite>‹zippy›. On a high-level, the method has three phases:
▸ Initialise the proof tree for a given goal.
▸ Repeatedly expand and modify nodes of the proof tree.
▸ Extract discovered theorems from the proof tree.
The particularities of the expansion (e.g. order of expansion, expansion rules, search bounds)
are largely customisable. Some configuration possibilities are demonstrated above.
During initialisation, the proof tree is (typically) augmented with action clusters. Each action
cluster stores a set of prioritised actions (short: ∗‹pactions›; cf. @{ML_functor Zippy_PAction_Mixin_Base}).
A paction consists of a priority and a function modifying the proof tree, called an ∗‹action›.
The paction's priority can be used to select action candidates during search.
By default, the tree is initialised with the set of initialisation functions registered in
@{ML_structure Zip.Run.Init_Goal_Cluster}. The current registrations can be seen as follows:
›
ML_val‹Zip.Run.Init_Goal_Cluster.Data.get_table (Context.the_generic_context ())›
text ‹A registration requires an identifier and an initialisation function modifying the proof
tree in the desired way. Below, we register and delete an initialisation that adds an action cluster
with a single paction, capable of closing goals by reflexivity:›
declare [[zip_init_gc ‹
let open Zippy; open ZLPC Base_Data MU; open A Mo
val id = @{binding refl}
val ac_meta = Mixin_Base3.Meta.Meta.metadata (id, Lazy.value "reflexivity action cluster")
val a_meta = Mixin_Base4.Meta.Meta.metadata (id, Lazy.value "proof by reflexivity")
fun mk_aa_meta _ _ = AAMeta.metadata {cost = Cost.VERY_LOW,
progress = AAMeta.P.Promising}
fun ztac _ = Ctxt.with_ctxt (fn ctxt => arr (resolve_tac ctxt @{thms refl}
|> Tac_AAM.lift_tac mk_aa_meta |> Tac_AAM.Tac.zSOME_GOAL_FOCUS))
val data = {
empty_action = Library.K Zippy.PAction.disable_action,
meta = a_meta,
result_action = Result_Action.action (Library.K (C.id ()))
Result_Action.copy_update_data_empty_changed,
presultsq = Zip.PResults.enum_scale_presultsq_default Cost.LOW,
tac = ztac}
fun init _ focus z = Tac.cons_action_cluster Util.exn (ACMeta.no_descr id) [(focus, data)] z
>>= AC.opt (K z) Up3.morph
in (id, init) end›]]
declare [[zip_init_gc del: "@{binding refl}"]]
text ‹Since the kind of pactions tried by zip is extensible, the parser of @{method zip} is also
extensible. Each parser has to apply its desired changes to the context and return a unit:
›
declare [[zip_parse add: ‹(@{binding refl},
apfst (Config.put_generic Unify.search_bound 5)
#> tap (fn _ => writeln "I got parsed!") #> Scan.succeed ())›]]
lemma "x = x"
by (zip refl)
declare [[zip_parse del: ‹@{binding refl}›]]
text ‹The initialised proof tree can then be expanded. By default, an ‹A⇧*› search is performed,
taking into consideration the pactions' user supplied priorities and the sum of costs of the path
leading to a paction. Other available search strategies are depth-first and breadth-first search
with ‹A⇧*›-cost tiebreakers, and best-first search on the pactions' priorities. Other search
strategies may at will.
For more details, check the sources of the setup in @{theory Zippy.Zip_Pure} and
@{theory Zippy.Zip_HOL}.›
end
end