Stream: General

Topic: Transforming a proof state from "state" mode to "prove" mode

Chengsong Tan (Jun 05 2024 at 01:28):

Suppose I have the following snippet:

theory Scratch
  imports "HOL-ex.Sketch_and_Explore"  Main
begin

lemma
  fixes x :: nat
  assumes "foo x ∧ bar x ∧ baz x ∧ qux x"
  shows "(foo (f x) ∨ x + 1 > x) ∧ (bar (f x) ∨ x + 1 > x) ∧ (baz (f x) ∨ x + 1 > x) ∧ (qux (f x) ∨ x + 1 > x)"
proof -
  have "foo x"

    using assms by argo
  have "bar x"

    using assms by argo
  have "baz x"
    using assms by argo
  have "qux x"
    using assms by argo

  show ?thesis
  (* sketch (intro conjI) *)
    sketch(intro conjI)
  proof (intro conjI)

    show "foo (f x) ∨ x < x + 1"
    next
      by simp
  next
    show "bar (f x) ∨ x < x + 1"
      by simp
  next
    show "baz (f x) ∨ x < x + 1"
      by simp
  next
    show "qux (f x) ∨ x < x + 1"
      by simp
  qed
qed


end

And I have some way of obtaining the proof state (which we callstate0) in ML just after the line proof (intro conjI) in our lemma, how do we transform state0 to a new state state1, where state1 is identical to state0 except that now it is in "prove" mode instead? Is it possible to additionally make all the subgoals in the lemma (in our example there are 4) exposed in state1 (as opposed to having only.1 subgoal present if we mundanely use the "show ...(goal 1)" command afterwards)?

The background is that I'm trying to extend the sketch command from HOL-ex, so that it automatically also generates the one-liners created by sledgehammer wherever possible rather than sorry-ing all subgoal proofs.

thanks a lot,
Chengsong

Mathias Fleury (Jun 05 2024 at 04:15):

why are you using proof (intro conjI) instead of apply (intro conjI)?

Mathias Fleury (Jun 05 2024 at 04:16):

maybe followed by subgoal to focus on a single goal in order to sorry it?

Chengsong Tan (Jun 05 2024 at 10:43):

Mathias Fleury said:

maybe followed by subgoal to focus on a single goal in order to sorry it?

Good point, I currently only have the state in Isar proof mode available, as I was modifying the Sketch_and_Explore.thy file, in which the proof (intro conjI) seems to be what you get after parsing from the command keyword argument (even if what we pass to sketch is (intro conjI) only), and I don't have a way of intervening:

fun print_proof_text_from_state print (some_method_ref : ((Method.text * Position.range) * Token.T list) option) state =
  let
    val state' = state
      |> Proof.proof (Option.map fst some_method_ref)
      |> Seq.the_result ""
... (some code in between)
val super_sketch = print_proof_text_from_state_generate_oneliners print_super_sketch;

fun sketch_cmd some_method_text =
  Toplevel.keep_proof (K () o sketch some_method_text o Toplevel.proof_of)

val _ =
  Outer_Syntax.command \<^command_keyword>\<open>sketch\<close>
    "print sketch of Isar proof text after method application"
    (Scan.option (Scan.trace Method.parse) >> sketch_cmd);

If you try to call sledgehammer from state' you get Illegal application of ... in "state" mode.

So a more general question I should have asked in the first place: how to parse a string and update the proof state after that string's tactics/methods have been consumed? Would it be more difficult if it is not an Isar command?

Last updated: Dec 21 2024 at 12:33 UTC