# Re: [isabelle] Sledgehammer 2015 oddity

On Sat, 30 May 2015, Eugene W. Stark wrote:

On 05/28/2015 03:56 AM, Jasmin Blanchette wrote:

`Appeal to the list: Please let me know if you run into other examples
``where either Sledgehammer finds a proof that doesnât work and it claims
``it does or vice versa. The issues are normally easy to track down and
``address if you can provide me with an example that reproduces the
``problem.
`

Here is one I just ran into. It was easy to abstract from the rest of the
theory so I am posting it.

theory Barf
imports Main
begin
definition graph :: "'a set â 'a set â ('a â 'a) â 'a â 'a â bool"
(*
* With the more general type "'a set â ' b set â ('a â 'b) â 'a â 'b â bool"
* the proof by fastforce succeeds below.
*)
where "graph A B f a b = (a â A â b â B â f a = b)"
lemma "a â A â b â B â c â C â f a = b â g b = c â graph A C (g o f) a c"
using graph_def
(* try0 (* Says: 'Try this: by fastforce' *) *)
by fastforce (* Fails to prove lemma -- unification bound exceeded, etc. *)
end

`The above actually works, but fastforce is stalled and waiting for
``confirmation to spill out more "potentially useful tracing messages" at
``the very bottom.
`

`This is a light form of denial-of-service attack on the front-end. A
``heavy form would be a bombing of the IDE process with tons of pointless
``messages.
`
The above example can be made to work as follows:
using [[unify_trace_bound = 60]]
by fastforce

`Sledgehammer is internally very careful to provide a sensible value to
``such options, see "silence_methods" here:
``http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2015/src/HOL/Tools/try0.ML#l104
`
That setup is not active for the generated proof snippet, though.
Makarius

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*