Re: [isabelle] Understanding backtracking in by vs qed



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.