Stream: Beginner Questions

Topic: difference between `proof` and `proof -`

Naso (Jul 15 2023 at 03:24):

What is the difference between these when starting a proof?
e.g.

lemma test : "∃ x . x = 0"
proof

has

proof (state)
goal (1 subgoal):
 1. ?x = 0

whereas

lemma test : "∃ x . x = 0"
proof -

has state

proof (state)
goal (1 subgoal):
 1. ∃x. x = 0

a pointer to where this is documented in the manual will be mch appreciated as i could not find it myself

Adem Rimpapa (Jul 15 2023 at 14:11):

The relevant sections in isar-ref.pdf are 6.4.2 and 6.4.3 (pages 146-152). Basically, proof - just starts the proof but does not perform any actual proof steps, whereas proof starts a "default proof", i.e. it will perform one standard reduction step based on the form of the statement to be shown. For example, if the statement is a conjunction, it will split the statement into two subgoals, if the statement is a negation, it will start a proof which assumes the argument of the negation and tries to derive False, etc.

Wolfgang Jeltsch (Jul 15 2023 at 20:55):

The rather precise, technical explanation is that proof is the same as proof standard and thus applies the standard proof method, which does something “reasonable” based on the goal, while proof - applies, well, the proof method -, which almost does nothing: it actually does something, namely adding chained facts to the goal as extra premises (occasionally handy if you write custom proof methods with Eisbach and otherwise often not harmful).

Wolfgang Jeltsch (Jul 15 2023 at 21:02):

Regarding your example with the existential quantifier, note that when just using proof you get a goal with a schematic variable. For a long time I was confused by these but then discovered how useful these are: you can just show the statement for a concrete term to replace this variable, and Isabelle will automatically instantiate the variable for you. As a contrived example, look at this (untested) one:

lemma test:
  shows "∃n :: nat. n = 0"
proof
  show "(1 - 1 :: nat) = 0"
    by simp
qed

Here you implicitly say what your example n is by just mentioning it in the statement after show.

If you happen to have several subgoals that share schematic variables, instantiating the variable for one of them automatically instantiates them for the others. Again a somewhat contrived (and untested) example:

lemma
  shows "∃n :: nat. n = 0 ∧ n < 1"
proof standard+
  show "(1 - 1 :: nat) = 0"
    by simp
qed simp

After you have proved the first subgoal with show, the second subgoal is not ?n < 1 anymore but 1 - 1 < 1, which the simp after qed can (hopefully) prove.

Naso (Jul 17 2023 at 02:51):

Why does the second version test2 below not work?

lemma test1 : "∃x. x = x" (is "∃x. ?P x")
proof -
  have "∃x. ?P x"
    by simp
  then obtain "x" where "?P x"
    by simp
  show "∃ x. ?P x"
    by simp
qed

lemma test2 : "∃x. x = x" (is "∃x. ?P x")
proof
  have "∃x. ?P x"
    by simp
  then obtain "x" where "?P x"
    by simp
  show "?P x" (* error *)

the proof state is

this:
  x = x

goal (1 subgoal):
 1. ?x = ?x
Result contains obtained parameters: x
Local statement fails to refine any pending goal

Edit: ok I think I found the answer here: https://groups.google.com/g/fa.isabelle/c/ZdSGteleBnk

It seems that one cannot use obtain when using the proof method for existential proofs (i.e. without the -), if I understood correctly. I'll leave my question ehre in case anyone wants to add anything :)

Alexandra Graß (Jul 18 2023 at 14:56):

Very interesting, thanks for sharing! I was wondering about this peculiarity for quite some while, but never bothered to investigate.

Last updated: Apr 28 2024 at 08:19 UTC