Re: [isabelle] Understanding backtracking in by vs qed



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.