Isabelle/ML function turns state mode to proof mode · General

Stream: General

Topic: Isabelle/ML function turns state mode to proof mode

Chengsong Tan (Sep 20 2024 at 15:43):

Dear all,

Suppose I am in the middle of an Isar proof, and want to invoke some commands on the rest of the proof goals:

If I want to try some commands which works on the rest of the subgoals (e.g. sledgehammer/auto/...), then Isabelle errors with message "Illegal application of proof command in "state" mode".
Is there a convenient way to transform at this point to "proof" mode in Isabelle or Isabelle/ML? Or at least is there a way to extract the goals from this "state" mode in Isabelle/ML so that sledgehammer can work on them.
A MWE:

theory Scratch imports Main  begin
sledgehammer_params[max_proofs = 4, preplay_timeout = 1]

lemma
  fixes x :: nat
  assumes "foo x ∧ bar x ∧ baz x ∧ qux x"
  shows "(foo (f x) ∨ x * x + 1 > x) ∧ (bar (f x) ∨ x ^2 + 1 ≥ 2 * 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

proof (intro conjI , insert assms)
  show goal1: "foo (f x) ∨ x < x * x + 1"
    if "foo x ∧ bar x ∧ baz x ∧ qux x"
    using that apply (smt (verit) add_cancel_left_left add_le_same_cancel1 divisors_zero le_square less_add_same_cancel2 less_one linorder_neqE_nat mult.right_neutral nat_0_less_mult_iff nat_mult_less_cancel_disj not_add_less2 not_one_le_zero trans_less_add1 trans_less_add2) done
  show goal2: "bar (f x) ∨ 2 * x ≤ x⇧2 + 1"
    if "foo x ∧ bar x ∧ baz x ∧ qux x"
    using that sorry
  apply auto (*HERE: want to be able to work on the rest of the subgoals. e.g. apply auto on them*)
qed

end

Thanks a lot,
Chengsong

Chelsea Edmonds (Sep 20 2024 at 22:09):

In general, if you have a tactic that will discharge all remaining proof goals, you can put this in brackets right after the qed, e.g. for the last part of your proof if auto works on all remaining goals you should be able to do it like this:

  show ?thesis

proof (intro conjI , insert assms)
  show goal1: "foo (f x) ∨ x < x * x + 1"
    if "foo x ∧ bar x ∧ baz x ∧ qux x"
    using that apply (smt (verit) add_cancel_left_left add_le_same_cancel1 divisors_zero le_square less_add_same_cancel2 less_one linorder_neqE_nat mult.right_neutral nat_0_less_mult_iff nat_mult_less_cancel_disj not_add_less2 not_one_le_zero trans_less_add1 trans_less_add2) done
  show goal2: "bar (f x) ∨ 2 * x ≤ x⇧2 + 1"
    if "foo x ∧ bar x ∧ baz x ∧ qux x"
    using that sorry
qed (auto)

Other than this, if you need different tactics for the remaining goals you can't just switch back in the middle of an Isar proof - the best method is to at least state the goal in Isar form (show ...) then you can always apply a series of tactics to that individual goal in apply style rather than opening up another proof...qed block (though stylistically I don't think this is really encouraged).

Mathias Fleury (Sep 21 2024 at 05:17):

Remark that insert assms is useless in Isar mode

Chengsong Tan (Sep 23 2024 at 14:22):

Chelsea Edmonds said:

In general, if you have a tactic that will discharge all remaining proof goals, you can put this in brackets right after the qed, e.g. for the last part of your proof if auto works on all remaining goals you should be able to do it like this:
  show ?thesis

proof (intro conjI , insert assms)
  show goal1: "foo (f x) ∨ x < x * x + 1"
    if "foo x ∧ bar x ∧ baz x ∧ qux x"
    using that apply (smt (verit) add_cancel_left_left add_le_same_cancel1 divisors_zero le_square less_add_same_cancel2 less_one linorder_neqE_nat mult.right_neutral nat_0_less_mult_iff nat_mult_less_cancel_disj not_add_less2 not_one_le_zero trans_less_add1 trans_less_add2) done
  show goal2: "bar (f x) ∨ 2 * x ≤ x⇧2 + 1"
    if "foo x ∧ bar x ∧ baz x ∧ qux x"
    using that sorry
qed (auto)
Other than this, if you need different tactics for the remaining goals you can't just switch back in the middle of an Isar proof - the best method is to at least state the goal in Isar form (show ...) then you can always apply a series of tactics to that individual goal in apply style rather than opening up another proof...qed block (though stylistically I don't think this is really encouraged).

Thanks a lot for the reply, Chelsea! However my use case is that I have a large proof almost completed (hundreds of subgoals), and now want to use an automated command to treat the rest of the goals (tens of subgoals) , which is not tractable altogether for tools like s/h or auto, but can be dealt with individually. In that case I do want to get a "fresh" proof state so I can invoke that command. It would be nice to get a more programmable proof state data structure in Isabelle/ML so such conversions are possible.

Chengsong Tan (Sep 23 2024 at 14:23):

Mathias Fleury said:

Remark that insert assms is useless in Isar mode

In my project I found it quite the contrary--sometimes insert assms would increase the probability sledgehammer finds a proof.

Mathias Fleury (Sep 23 2024 at 14:26):

Chengsong Tan said:

Mathias Fleury said:

Remark that insert assms is useless in Isar mode

In my project I found it quite the contrary--sometimes insert assms would increase the probability sledgehammer finds a proof.

using assms is the normal way to achieve that in Isar, not inserting the assumption in every case.

Mathias Fleury (Sep 23 2024 at 14:29):

I am not sure whether I should mention the fact that apply_end exists

Chengsong Tan (Sep 23 2024 at 14:30):

Mathias Fleury said:

I am not sure whether I should mention the fact that apply_end exists

What does it do?

Mathias Fleury (Sep 23 2024 at 14:34):

https://isabelle.in.tum.de/library/Doc/Isar_Ref/Proof_Script.html

Chengsong Tan (Sep 23 2024 at 14:37):

Mathias Fleury said:

Chengsong Tan said:

Mathias Fleury said:

Remark that insert assms is useless in Isar mode

In my project I found it quite the contrary--sometimes insert assms would increase the probability sledgehammer finds a proof.

using assms is the normal way to achieve that in Isar, not inserting the assumption in every case.

It's actually automatically generated (by my tool super_sketch). So there I need a method to fit in to my command (something like super_sketch3 (intro conjI) (simp) (insert assms) (cases "x") (auto) for example), and therefore the slightly weird apply (insert...).

Last updated: Dec 21 2024 at 12:33 UTC