Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Understanding backtracking in by vs qed

Email Gateway (Aug 22 2022 at 19:23):

From: Joshua Chen <joshua.chen@uibk.ac.at>
Dear Isabelle list,

I have a proof that works:

have <statement> using <facts>
proof (move, infer_ty) qed (auto simp: ty)

and one that doesn't:

have <statement> using <facts>
by (move, infer_ty) (auto simp: ty)

The manual says that "by" abbreviates "proof ... qed" but with
additional backtracking, what is it about this that could cause "by" to
fail and "qed" to succeed?

I'm unsure if it would be relevant, but infer_ty is a method that only
changes the proof context (by adding some theorems to context data)
without changing the goal.

Best,
Josh

Email Gateway (Aug 22 2022 at 19:23):

From: Makarius <makarius@sketis.net>
On 22/03/2019 17:53, Joshua Chen wrote:

I have a proof that works:

have <statement> using <facts>
   proof (move, infer_ty) qed (auto simp: ty)

and one that doesn't:

have <statement> using <facts>
   by (move, infer_ty) (auto simp: ty)

The manual says that "by" abbreviates "proof ... qed" but with
additional backtracking, what is it about this that could cause "by" to
fail and "qed" to succeed?

The 'by' step can enumerate all possibilities for the initial proof
method (move, infer_ty) and then try the auto step and then finish
(which is implicit). The proof-qed sequence only uses the first
possibility of 'proof' and 'qed' needs to finish that without further
backtracking.

You can try to put a few 'back' commands between 'proof' and 'qed'
above, to see if relevant alternative states emerge in between.

I'm unsure if it would be relevant, but infer_ty is a method that only
changes the proof context (by adding some theorems to context data)
without changing the goal.

Other things might go wrong here, as this sounds somewhat non-standard.

Makarius

Email Gateway (Aug 22 2022 at 19:23):

From: Joshua Chen <joshua.chen@uibk.ac.at>

The 'by' step can enumerate all possibilities for the initial proof
method (move, infer_ty) and then try the auto step and then finish
(which is implicit). The proof-qed sequence only uses the first
possibility of 'proof' and 'qed' needs to finish that without further
backtracking.

Right, so this is what I don't yet fully understand, if 'by' enumerates
all possibilities, what is preventing it from finding the same proof as
'proof...qed'? Does the latter somehow force the methods to try harder,
while they would give up earlier with backtracking?

Other things might go wrong here, as this sounds somewhat non-standard.
Just as an aside, the same situation has happened in Isabelle/HoTT too,
there only Eisbach methods are used so there shouldn't be the same
complications.

Best,
Josh

On 3/23/19 11:38 AM, Makarius wrote:

On 22/03/2019 17:53, Joshua Chen wrote:

I have a proof that works:

have <statement> using <facts>
   proof (move, infer_ty) qed (auto simp: ty)

and one that doesn't:

have <statement> using <facts>
   by (move, infer_ty) (auto simp: ty)

The manual says that "by" abbreviates "proof ... qed" but with
additional backtracking, what is it about this that could cause "by" to
fail and "qed" to succeed?
The 'by' step can enumerate all possibilities for the initial proof
method (move, infer_ty) and then try the auto step and then finish
(which is implicit). The proof-qed sequence only uses the first
possibility of 'proof' and 'qed' needs to finish that without further
backtracking.

You can try to put a few 'back' commands between 'proof' and 'qed'
above, to see if relevant alternative states emerge in between.

I'm unsure if it would be relevant, but infer_ty is a method that only
changes the proof context (by adding some theorems to context data)
without changing the goal.
Other things might go wrong here, as this sounds somewhat non-standard.

Makarius

Email Gateway (Aug 22 2022 at 19:23):

From: Makarius <makarius@sketis.net>
I would say there is something odd with the context update of the proof
method. (In my explanation above, I was actually talking about typical
situations where 'by' works but 'proof' ... 'qed' fails.)

If you can isolate a well-defined example, it is easier to look what
really happens.

Makarius

Last updated: Apr 25 2024 at 20:15 UTC