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
Here is one I just ran into. It was easy to abstract from the rest of the
theory so I am posting it.
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"
(* try0 (* Says: 'Try this: by fastforce' *) *)
by fastforce (* Fails to prove lemma -- unification bound exceeded, etc. *)
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
The above example can be made to work as follows:
using [[unify_trace_bound = 60]]
Sledgehammer is internally very careful to provide a sensible value to
such options, see "silence_methods" here:
That setup is not active for the generated proof snippet, though.
This archive was generated by a fusion of
Pipermail (Mailman edition) and