Re: [isabelle] Understanding backtracking in by vs qed



On 23/03/2019 11:43, Joshua Chen wrote:
>> 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.

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





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