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.