MRG home page· Research · Publications·Projects·Software ·People

Horrible Monsters

Here we talk about some nasty monsters in IsaPlanner and how we plan to hunt them down.

Interactive monster ate my wave-rule

Rippling behaves differently when called from synthesis and interactivly! We first run synthesis to get a bunch of theorems about @, map and rev:

print_depth 30; use "synthesis/synth_prf_tools.ML"; use "synthesis/constInfo.ML"; use "synthesis/synthesise.ML"; use_thy "dbg/SynthL2"; val thy = theory "SynthL2";

(* Make the initial constant-information*)

val (cs, thy2) = ConstInfo.mk_const_infos_ac thy;

(* Run synthesis, get a new theory with a bunch of new wave-rules: *)

val ((cs2,thy3),(conjs,thrms)) = Synthesis.synth_w_stats 10 2 thy2 cs;

At this point, note that we could not prove the conjecture "rev(rev a @ b) = rev b @ a".

Now try and run the proof interactively, using the latest variant of the theory:

val rippling = RippleLemCalc.induct_ripple_lemcalc; val myrst = PPInterface.ipp thry (rippling "g") ("g", "rev(rev a @ b) = rev b @ a");

Ok, this doesn't work either. The last wave-rule to be considered is the associativity of @ (which we have synthesised), then we get a weak fertilisation and fail to prove the calculated lemma.

Now, run synthesis again, using the constant info and theory that came from the previous run:

val ((cs3,thy4),(conjs,thrms)) = Synthesis.synth_w_stats 10 2 thy3 cs2;

Behold! The above theorem CAN be proved, by using another synthesised theorem as a wave-rule: "rev x @ y = rev y @ rev x". But why isn't this available when we try to run it interactively??? I've checked and the rule is in the wave-rule database, but it's for some reason not considered applicable from the reasoning state resulting from the interactive proof attempt.

Did a monster eat my wave-rule?

Other things to do

HorribleMonsters (last edited 2008-12-04 18:28:44 by haggis)