Simon Cruanes
2020-05-12 13:7:19 (GMT)
https://twitter.com/andrejbauer/status/1259901971991052290 well well wellโฆ
Let me share a story about research in mathematics.
- Andrej Bauer (@andrejbauer)Jasmin Blanchette
2020-05-12 15:45:27 (GMT)
So what is he waiting to formalize that particular paper? ;)
Simon Cruanes
2020-05-12 15:55:8 (GMT)
he's waiting for sledgehammer 2.0 with Ehoh and Zipperposition-ho, that's what.
Jasmin Blanchette
2020-05-12 16:14:59 (GMT)
I'm actually waiting for SH right now. Oh, wait, it found a proof!
Jasmin Blanchette
2020-05-12 16:15:8 (GMT)
Sledgehammering...
Proof found...
"e": Try this: by (metis (no_types, hide_lams) Diff_subset grounding_of_clss_def inference_system.inferences_from_mono subset_eq) (191 ms)
"cvc4": Try this: by (metis (no_types, lifting) Diff_subset gd.inferences_from_mono grounding_of_clss_def subsetD) (275 ms)
"vampire": Try this: by (smt Diff_subset gd.inferences_from_mono subset_eq substitution_ops.grounding_of_clss_def) (175 ms)
Isar proof (failed):
proof -
fix x :: "'a Inference_System.inference"
assume a1: "gd.inferences_from Sts (โ (๐ข_F ` Liminf_llist (lmap Q_of_state Sts))) โ src.Ri Sts (โ (๐ข_F ` Liminf_llist (lmap Q_of_state Sts)))"
assume a2: "x โ gd.inferences_from Sts (grounding_of_clss (Liminf_llist (lmap Q_of_state Sts)) - src.Rf (grounding_of_clss (Liminf_llist (lmap Q_of_state Sts))))"
have "โX1 X0. (โx. (x::'a Inference_System.inference) โ X1 โง x โ X0) โถ sK1 X1 X0 โ X1 โง sK1 X1 X0 โ X0"
by auto (* failed *)
then obtain ii :: "'a Inference_System.inference set โ 'a Inference_System.inference set โ 'a Inference_System.inference" where
"โI Ia. (I โ Ia โจ ii Ia I โ Ia โง ii Ia I โ I) โง ((โi. i โ Ia โจ i โ I) โจ ยฌ I โ Ia)"
by auto
then have "x โ gd.inferences_from Sts (โ (๐ข_F ` Liminf_llist (lmap Q_of_state Sts)))"
using a2 by (metis (no_types) Diff_subset gd.inferences_from_mono substitution_ops.grounding_of_clss_def)
then have "x โ src.Ri Sts (โ (๐ข_F ` Liminf_llist (lmap Q_of_state Sts)))"
using a1 by blast
then show "x โ src.Ri Sts (grounding_of_clss (Liminf_llist (lmap Q_of_state Sts)))"
by (simp add: substitution_ops.grounding_of_clss_def)
qed
"z3": Timed out
Simon Cruanes
2020-05-12 20:22:11 (GMT)
is this a cry for help for better proof reconstruction? :sweat_smile:
Jasmin Blanchette
2020-05-13 6:48:34 (GMT)
He he :)
Jasmin Blanchette
2020-05-13 6:48:58 (GMT)
Actually, the smt calls work -- it's just the detailed Isar proof that fails.